From b46b827c30584968c6815b456b8c0c775c35ae48 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 18 Oct 2018 15:03:52 +0200 Subject: [SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash --- libsolidity/formal/SMTChecker.cpp | 100 +++++++++++++++++---- libsolidity/formal/SMTChecker.h | 16 ++-- libsolidity/formal/SymbolicAddressVariable.cpp | 11 ++- libsolidity/formal/SymbolicAddressVariable.h | 1 - libsolidity/formal/SymbolicBoolVariable.cpp | 6 +- libsolidity/formal/SymbolicBoolVariable.h | 2 +- libsolidity/formal/SymbolicIntVariable.cpp | 8 +- libsolidity/formal/SymbolicIntVariable.h | 2 +- libsolidity/formal/SymbolicTypes.cpp | 15 ++-- libsolidity/formal/SymbolicVariable.cpp | 4 +- libsolidity/formal/SymbolicVariable.h | 5 +- test/libsolidity/SMTChecker.cpp | 17 ---- .../smtCheckerTests/special/blockhash.sol | 14 +++ .../smtCheckerTests/special/gasleft.sol | 10 +++ test/libsolidity/smtCheckerTests/special/many.sol | 25 ++++++ .../smtCheckerTests/special/msg_data.sol | 14 +++ .../smtCheckerTests/special/msg_sender_1.sol | 10 +++ .../smtCheckerTests/special/msg_sender_2.sol | 14 +++ .../smtCheckerTests/special/msg_sender_fail_1.sol | 13 +++ .../smtCheckerTests/special/msg_sig.sol | 14 +++ 20 files changed, 233 insertions(+), 68 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/special/blockhash.sol create mode 100644 test/libsolidity/smtCheckerTests/special/gasleft.sol create mode 100644 test/libsolidity/smtCheckerTests/special/many.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_data.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_sender_1.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_sender_2.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_sig.sol diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index e5648eb3..db0cec7f 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -363,6 +363,10 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) visitAssert(_funCall); else if (funType.kind() == FunctionType::Kind::Require) visitRequire(_funCall); + else if (funType.kind() == FunctionType::Kind::GasLeft) + visitGasLeft(_funCall); + else if (funType.kind() == FunctionType::Kind::BlockHash) + visitBlockHash(_funCall); else if (funType.kind() == FunctionType::Kind::Internal) inlineFunctionCall(_funCall); else @@ -393,6 +397,22 @@ void SMTChecker::visitRequire(FunctionCall const& _funCall) addPathImpliedExpression(expr(*args[0])); } +void SMTChecker::visitGasLeft(FunctionCall const& _funCall) +{ + string gasLeft = "gasleft"; + // We increase the variable index since gasleft changes + // inside a tx. + defineSpecialVariable(gasLeft, _funCall, true); + m_specialVariables.at(gasLeft)->setUnknownValue(); +} + +void SMTChecker::visitBlockHash(FunctionCall const& _funCall) +{ + string blockHash = "blockhash"; + // TODO Define blockhash as an uninterpreted function + defineSpecialVariable(blockHash, _funCall); +} + void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) { FunctionDefinition const* _funDef = nullptr; @@ -460,7 +480,11 @@ void SMTChecker::endVisit(Identifier const& _identifier) } else if (FunctionType const* fun = dynamic_cast(_identifier.annotation().type.get())) { - if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require) + if (fun->kind() == FunctionType::Kind::Assert || + fun->kind() == FunctionType::Kind::Require || + fun->kind() == FunctionType::Kind::GasLeft || + fun->kind() == FunctionType::Kind::BlockHash + ) return; createExpr(_identifier); } @@ -468,6 +492,8 @@ void SMTChecker::endVisit(Identifier const& _identifier) { if (VariableDeclaration const* decl = dynamic_cast(_identifier.annotation().referencedDeclaration)) defineExpr(_identifier, currentValue(*decl)); + else if (_identifier.name() == "now") + defineSpecialVariable(_identifier.name(), _identifier); else // TODO: handle MagicVariableDeclaration here m_errorReporter.warning( @@ -496,7 +522,7 @@ void SMTChecker::endVisit(Literal const& _literal) void SMTChecker::endVisit(Return const& _return) { - if (hasExpr(*_return.expression())) + if (knownExpr(*_return.expression())) { auto returnParams = m_functionPath.back()->returnParameters(); if (returnParams.size() > 1) @@ -509,6 +535,45 @@ void SMTChecker::endVisit(Return const& _return) } } +bool SMTChecker::visit(MemberAccess const& _memberAccess) +{ + auto const& exprType = _memberAccess.expression().annotation().type; + solAssert(exprType, ""); + if (exprType->category() == Type::Category::Magic) + { + defineSpecialVariable(_memberAccess.memberName(), _memberAccess); + return false; + } + else + m_errorReporter.warning( + _memberAccess.location(), + "Assertion checker does not yet support this expression." + ); + + return true; +} + +void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _expr, bool _increaseIndex) +{ + if (!knownSpecialVariable(_name)) + { + auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); + m_specialVariables.emplace(_name, result.second); + result.second->setUnknownValue(); + if (result.first) + m_errorReporter.warning( + _expr.location(), + "Assertion checker does not yet support this special variable." + ); + } + else if (_increaseIndex) + m_specialVariables.at(_name)->increaseIndex(); + // The default behavior is not to increase the index since + // most of the special values stay the same throughout a tx. + defineExpr(_expr, m_specialVariables.at(_name)->currentValue()); +} + + void SMTChecker::arithmeticOperation(BinaryOperation const& _op) { switch (_op.getOperator()) @@ -681,11 +746,15 @@ void SMTChecker::checkCondition( expressionNames.push_back(_additionalValueName); } for (auto const& var: m_variables) - if (knownVariable(*var.first)) - { - expressionsToEvaluate.emplace_back(currentValue(*var.first)); - expressionNames.push_back(var.first->name()); - } + { + expressionsToEvaluate.emplace_back(currentValue(*var.first)); + expressionNames.push_back(var.first->name()); + } + for (auto const& var: m_specialVariables) + { + expressionsToEvaluate.emplace_back(var.second->currentValue()); + expressionNames.push_back(var.first); + } } smt::CheckResult result; vector values; @@ -910,7 +979,7 @@ void SMTChecker::mergeVariables(vector const& _varia bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { // This might be the case for multiple calls to the same function. - if (hasVariable(_varDecl)) + if (knownVariable(_varDecl)) return true; auto const& type = _varDecl.type(); solAssert(m_variables.count(&_varDecl) == 0, ""); @@ -927,11 +996,6 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) return true; } -string SMTChecker::uniqueSymbol(Expression const& _expr) -{ - return "expr_" + to_string(_expr.id()); -} - bool SMTChecker::knownVariable(VariableDeclaration const& _decl) { return m_variables.count(&_decl); @@ -969,7 +1033,7 @@ void SMTChecker::setUnknownValue(VariableDeclaration const& _decl) smt::Expression SMTChecker::expr(Expression const& _e) { - if (!hasExpr(_e)) + if (!knownExpr(_e)) { m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." ); createExpr(_e); @@ -977,20 +1041,20 @@ smt::Expression SMTChecker::expr(Expression const& _e) return m_expressions.at(&_e)->currentValue(); } -bool SMTChecker::hasExpr(Expression const& _e) const +bool SMTChecker::knownExpr(Expression const& _e) const { return m_expressions.count(&_e); } -bool SMTChecker::hasVariable(VariableDeclaration const& _var) const +bool SMTChecker::knownSpecialVariable(string const& _var) const { - return m_variables.count(&_var); + return m_specialVariables.count(_var); } void SMTChecker::createExpr(Expression const& _e) { solAssert(_e.annotation().type, ""); - if (hasExpr(_e)) + if (knownExpr(_e)) m_expressions.at(&_e)->increaseIndex(); else { diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index f66693d2..95e01708 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -66,6 +66,7 @@ private: virtual void endVisit(Identifier const& _node) override; virtual void endVisit(Literal const& _node) override; virtual void endVisit(Return const& _node) override; + virtual bool visit(MemberAccess const& _node) override; void arithmeticOperation(BinaryOperation const& _op); void compareOperation(BinaryOperation const& _op); @@ -73,10 +74,14 @@ private: void visitAssert(FunctionCall const&); void visitRequire(FunctionCall const&); + void visitGasLeft(FunctionCall const&); + void visitBlockHash(FunctionCall const&); /// Visits the FunctionDefinition of the called function /// if available and inlines the return value. void inlineFunctionCall(FunctionCall const&); + void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false); + /// Division expression in the given type. Requires special treatment because /// of rounding for signed division. smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type); @@ -129,8 +134,6 @@ private: /// This fails if the type is not supported. bool createVariable(VariableDeclaration const& _varDecl); - static std::string uniqueSymbol(Expression const& _expr); - /// @returns true if _delc is a variable that is known at the current point, i.e. /// has a valid index bool knownVariable(VariableDeclaration const& _decl); @@ -154,10 +157,13 @@ private: /// Creates the expression (value can be arbitrary) void createExpr(Expression const& _e); /// Checks if expression was created - bool hasExpr(Expression const& _e) const; + bool knownExpr(Expression const& _e) const; /// Creates the expression and sets its value. void defineExpr(Expression const& _e, smt::Expression _value); + /// Checks if special variable was seen. + bool knownSpecialVariable(std::string const& _var) const; + /// Adds a new path condition void pushPathCondition(smt::Expression const& _e); /// Remove the last path condition @@ -172,9 +178,6 @@ private: /// Removes local variables from the context. void removeLocalVariables(); - /// Checks if VariableDeclaration was seen. - bool hasVariable(VariableDeclaration const& _e) const; - /// Copy the SSA indices of m_variables. VariableIndices copyVariableIndices(); /// Resets the variable indices. @@ -187,6 +190,7 @@ private: /// repeated calls to the same function. std::unordered_map> m_expressions; std::unordered_map> m_variables; + std::unordered_map> m_specialVariables; std::vector m_pathConditions; ErrorReporter& m_errorReporter; diff --git a/libsolidity/formal/SymbolicAddressVariable.cpp b/libsolidity/formal/SymbolicAddressVariable.cpp index 68b95080..67a18540 100644 --- a/libsolidity/formal/SymbolicAddressVariable.cpp +++ b/libsolidity/formal/SymbolicAddressVariable.cpp @@ -24,18 +24,17 @@ using namespace dev; using namespace dev::solidity; SymbolicAddressVariable::SymbolicAddressVariable( - Type const& _type, string const& _uniqueName, smt::SolverInterface& _interface ): - SymbolicIntVariable(_type, _uniqueName, _interface) + SymbolicIntVariable(make_shared(160), _uniqueName, _interface) { - solAssert(isAddress(_type.category()), ""); } void SymbolicAddressVariable::setUnknownValue() { - IntegerType intType{160}; - m_interface.addAssertion(currentValue() >= minValue(intType)); - m_interface.addAssertion(currentValue() <= maxValue(intType)); + auto intType = dynamic_cast(m_type.get()); + solAssert(intType, ""); + m_interface.addAssertion(currentValue() >= minValue(*intType)); + m_interface.addAssertion(currentValue() <= maxValue(*intType)); } diff --git a/libsolidity/formal/SymbolicAddressVariable.h b/libsolidity/formal/SymbolicAddressVariable.h index 4a0f2361..3c9c379a 100644 --- a/libsolidity/formal/SymbolicAddressVariable.h +++ b/libsolidity/formal/SymbolicAddressVariable.h @@ -31,7 +31,6 @@ class SymbolicAddressVariable: public SymbolicIntVariable { public: SymbolicAddressVariable( - Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _interface ); diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index 9c41ca9d..4d753c5c 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -22,13 +22,13 @@ using namespace dev; using namespace dev::solidity; SymbolicBoolVariable::SymbolicBoolVariable( - Type const& _type, + TypePointer _type, string const& _uniqueName, smt::SolverInterface&_interface ): - SymbolicVariable(_type, _uniqueName, _interface) + SymbolicVariable(move(_type), _uniqueName, _interface) { - solAssert(_type.category() == Type::Category::Bool, ""); + solAssert(m_type->category() == Type::Category::Bool, ""); } smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h index 85e41b3b..438af2c6 100644 --- a/libsolidity/formal/SymbolicBoolVariable.h +++ b/libsolidity/formal/SymbolicBoolVariable.h @@ -31,7 +31,7 @@ class SymbolicBoolVariable: public SymbolicVariable { public: SymbolicBoolVariable( - Type const& _type, + TypePointer _type, std::string const& _uniqueName, smt::SolverInterface& _interface ); diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp index cf1a7486..a5939842 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -24,13 +24,13 @@ using namespace dev; using namespace dev::solidity; SymbolicIntVariable::SymbolicIntVariable( - Type const& _type, + TypePointer _type, string const& _uniqueName, smt::SolverInterface& _interface ): - SymbolicVariable(_type, _uniqueName, _interface) + SymbolicVariable(move(_type), _uniqueName, _interface) { - solAssert(isNumber(_type.category()), ""); + solAssert(isNumber(m_type->category()), ""); } smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const @@ -45,7 +45,7 @@ void SymbolicIntVariable::setZeroValue() void SymbolicIntVariable::setUnknownValue() { - auto intType = dynamic_cast(&m_type); + auto intType = dynamic_cast(m_type.get()); solAssert(intType, ""); m_interface.addAssertion(currentValue() >= minValue(*intType)); m_interface.addAssertion(currentValue() <= maxValue(*intType)); diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index 110ebb09..a9e51b1b 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -31,7 +31,7 @@ class SymbolicIntVariable: public SymbolicVariable { public: SymbolicIntVariable( - Type const& _type, + TypePointer _type, std::string const& _uniqueName, smt::SolverInterface& _interface ); diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index d47869db..7e5db7bd 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -43,27 +43,28 @@ pair> dev::solidity::newSymbolicVariable( { bool abstract = false; shared_ptr var; + TypePointer type = _type.shared_from_this(); if (!isSupportedType(_type)) { abstract = true; - var = make_shared(IntegerType{256}, _uniqueName, _solver); + var = make_shared(make_shared(256), _uniqueName, _solver); } else if (isBool(_type.category())) - var = make_shared(_type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _solver); else if (isFunction(_type.category())) - var = make_shared(IntegerType{256}, _uniqueName, _solver); + var = make_shared(make_shared(256), _uniqueName, _solver); else if (isInteger(_type.category())) - var = make_shared(_type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _solver); else if (isAddress(_type.category())) - var = make_shared(_type, _uniqueName, _solver); + var = make_shared(_uniqueName, _solver); else if (isRational(_type.category())) { auto rational = dynamic_cast(&_type); solAssert(rational, ""); if (rational->isFractional()) - var = make_shared(IntegerType{256}, _uniqueName, _solver); + var = make_shared(make_shared(256), _uniqueName, _solver); else - var = make_shared(_type, _uniqueName, _solver); + var = make_shared(type, _uniqueName, _solver); } else solAssert(false, ""); diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp index c042ec48..8259ffee 100644 --- a/libsolidity/formal/SymbolicVariable.cpp +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -24,11 +24,11 @@ using namespace dev; using namespace dev::solidity; SymbolicVariable::SymbolicVariable( - Type const& _type, + TypePointer _type, string const& _uniqueName, smt::SolverInterface& _interface ): - m_type(_type), + m_type(move(_type)), m_uniqueName(_uniqueName), m_interface(_interface), m_ssa(make_shared()) diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h index 417e1f92..9beaf0e0 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -39,10 +39,11 @@ class SymbolicVariable { public: SymbolicVariable( - Type const& _type, + TypePointer _type, std::string const& _uniqueName, smt::SolverInterface& _interface ); + virtual ~SymbolicVariable() = default; smt::Expression currentValue() const @@ -71,7 +72,7 @@ public: protected: std::string uniqueSymbol(int _index) const; - Type const& m_type; + TypePointer m_type = nullptr; std::string m_uniqueName; smt::SolverInterface& m_interface; std::shared_ptr m_ssa = nullptr; diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index c7e60256..195004cb 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -133,23 +133,6 @@ BOOST_AUTO_TEST_CASE(assignment_in_declaration) CHECK_SUCCESS_NO_WARNINGS(text); } -BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars) -{ - string text = R"( - contract C { - function g() public pure {} - function f() public view { - uint a = 3; - this.g(); - assert(a == 3); - g(); - assert(a == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call"); -} - BOOST_AUTO_TEST_CASE(branches_merge_variables) { // Branch does not touch variable a diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol new file mode 100644 index 00000000..d0f263eb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(blockhash(2) > 0); + } +} +// ---- +// Warning: (86-98): Assertion checker does not yet support this special variable. +// Warning: (86-98): Assertion checker does not yet implement this type. +// Warning: (86-102): Assertion checker does not yet implement the type bytes32 for comparisons +// Warning: (86-102): Internal error: Expression undefined for SMT solver. +// Warning: (79-103): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/gasleft.sol b/test/libsolidity/smtCheckerTests/special/gasleft.sol new file mode 100644 index 00000000..ec56d957 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/gasleft.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public view { + assert(gasleft() > 0); + } +} +// ---- +// Warning: (76-97): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/many.sol b/test/libsolidity/smtCheckerTests/special/many.sol new file mode 100644 index 00000000..40e5d987 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/many.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(msg.sender == block.coinbase); + assert(block.difficulty == block.gaslimit); + assert(block.number == block.timestamp); + assert(tx.gasprice == msg.value); + assert(tx.origin == msg.sender); + uint x = block.number; + assert(x + 2 > block.number); + assert(now > 10); + assert(gasleft() > 100); + } +} +// ---- +// Warning: (79-115): Assertion violation happens here +// Warning: (119-161): Assertion violation happens here +// Warning: (165-204): Assertion violation happens here +// Warning: (208-240): Assertion violation happens here +// Warning: (244-275): Assertion violation happens here +// Warning: (311-316): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (336-352): Assertion violation happens here +// Warning: (356-379): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol new file mode 100644 index 00000000..7e748f09 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_data.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(msg.data.length > 0); + } +} +// ---- +// Warning: (86-101): Assertion checker does not yet support this expression. +// Warning: (86-94): Assertion checker does not yet support this special variable. +// Warning: (86-94): Assertion checker does not yet implement this type. +// Warning: (86-101): Internal error: Expression undefined for SMT solver. +// Warning: (79-106): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol new file mode 100644 index 00000000..dd2366e2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public view { + address a = msg.sender; + address b = msg.sender; + assert(a == b); + } +} diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol new file mode 100644 index 00000000..ad45d076 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public view { + require(msg.sender != address(0)); + address a = msg.sender; + address b = msg.sender; + assert(a == b); + } +} +// ---- +// Warning: (98-108): Assertion checker does not yet implement this expression. +// Warning: (98-108): Internal error: Expression undefined for SMT solver. diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol new file mode 100644 index 00000000..9a4eefd5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(address c) public view { + address a = msg.sender; + address b = msg.sender; + assert(a == b); + assert(c == msg.sender); + } +} +// ---- +// Warning: (155-178): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol new file mode 100644 index 00000000..6f832179 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public payable { + assert(msg.sig == 0x00000000); + } +} +// ---- +// Warning: (86-93): Assertion checker does not yet support this special variable. +// Warning: (86-93): Assertion checker does not yet implement this type. +// Warning: (86-107): Assertion checker does not yet implement the type bytes4 for comparisons +// Warning: (86-107): Internal error: Expression undefined for SMT solver. +// Warning: (79-108): Assertion violation happens here -- cgit From e2cf5f6ed94c571c7478b9a313f8e4fceee2aec3 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 22 Oct 2018 18:19:11 +0200 Subject: Add gasleft constraint and use full member access name --- libsolidity/formal/SMTChecker.cpp | 27 +++++++++++++++++----- libsolidity/formal/SSAVariable.cpp | 2 +- libsolidity/formal/SSAVariable.h | 10 ++++---- libsolidity/formal/SymbolicVariable.cpp | 2 +- libsolidity/formal/SymbolicVariable.h | 6 ++--- .../smtCheckerTests/special/difficulty.sol | 10 ++++++++ .../smtCheckerTests/special/gasleft.sol | 4 ++++ 7 files changed, 45 insertions(+), 16 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/special/difficulty.sol diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index db0cec7f..03ec7fac 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -399,16 +399,21 @@ void SMTChecker::visitRequire(FunctionCall const& _funCall) void SMTChecker::visitGasLeft(FunctionCall const& _funCall) { - string gasLeft = "gasleft"; + string gasLeft = "gasleft()"; // We increase the variable index since gasleft changes // inside a tx. defineSpecialVariable(gasLeft, _funCall, true); - m_specialVariables.at(gasLeft)->setUnknownValue(); + auto const& symbolicVar = m_specialVariables.at(gasLeft); + unsigned index = symbolicVar->index(); + // We set the current value to unknown anyway to add type constraints. + symbolicVar->setUnknownValue(); + if (index > 0) + m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); } void SMTChecker::visitBlockHash(FunctionCall const& _funCall) { - string blockHash = "blockhash"; + string blockHash = "blockhash()"; // TODO Define blockhash as an uninterpreted function defineSpecialVariable(blockHash, _funCall); } @@ -480,11 +485,12 @@ void SMTChecker::endVisit(Identifier const& _identifier) } else if (FunctionType const* fun = dynamic_cast(_identifier.annotation().type.get())) { - if (fun->kind() == FunctionType::Kind::Assert || + if ( + fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require || fun->kind() == FunctionType::Kind::GasLeft || fun->kind() == FunctionType::Kind::BlockHash - ) + ) return; createExpr(_identifier); } @@ -541,7 +547,16 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess) solAssert(exprType, ""); if (exprType->category() == Type::Category::Magic) { - defineSpecialVariable(_memberAccess.memberName(), _memberAccess); + auto identifier = dynamic_cast(&_memberAccess.expression()); + string accessedName; + if (identifier) + accessedName = identifier->name(); + else + m_errorReporter.warning( + _memberAccess.location(), + "Assertion checker does not yet support this expression." + ); + defineSpecialVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess); return false; } else diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index dbc58664..36e15508 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -28,6 +28,6 @@ SSAVariable::SSAVariable() void SSAVariable::resetIndex() { m_currentIndex = 0; - m_nextFreeIndex.reset (new int); + m_nextFreeIndex.reset (new unsigned); *m_nextFreeIndex = 1; } diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index d357740d..46935472 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -34,19 +34,19 @@ public: void resetIndex(); /// This function returns the current index of this SSA variable. - int index() const { return m_currentIndex; } - int& index() { return m_currentIndex; } + unsigned index() const { return m_currentIndex; } + unsigned& index() { return m_currentIndex; } - int operator++() + unsigned operator++() { return m_currentIndex = (*m_nextFreeIndex)++; } private: - int m_currentIndex; + unsigned m_currentIndex; /// The next free index is a shared pointer because we want /// the copy and the copied to share it. - std::shared_ptr m_nextFreeIndex; + std::shared_ptr m_nextFreeIndex; }; } diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp index 8259ffee..530564d2 100644 --- a/libsolidity/formal/SymbolicVariable.cpp +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -35,7 +35,7 @@ SymbolicVariable::SymbolicVariable( { } -string SymbolicVariable::uniqueSymbol(int _index) const +string SymbolicVariable::uniqueSymbol(unsigned _index) const { return m_uniqueName + "_" + to_string(_index); } diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h index 9beaf0e0..e554139f 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -59,8 +59,8 @@ public: return currentValue(); } - int index() const { return m_ssa->index(); } - int& index() { return m_ssa->index(); } + unsigned index() const { return m_ssa->index(); } + unsigned& index() { return m_ssa->index(); } /// Sets the var to the default value of its type. /// Inherited types must implement. @@ -70,7 +70,7 @@ public: virtual void setUnknownValue() {} protected: - std::string uniqueSymbol(int _index) const; + std::string uniqueSymbol(unsigned _index) const; TypePointer m_type = nullptr; std::string m_uniqueName; diff --git a/test/libsolidity/smtCheckerTests/special/difficulty.sol b/test/libsolidity/smtCheckerTests/special/difficulty.sol new file mode 100644 index 00000000..4469d4e5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/difficulty.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint difficulty) public view { + assert(block.difficulty == difficulty); + } +} +// ---- +// Warning: (91-129): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/gasleft.sol b/test/libsolidity/smtCheckerTests/special/gasleft.sol index ec56d957..857230fe 100644 --- a/test/libsolidity/smtCheckerTests/special/gasleft.sol +++ b/test/libsolidity/smtCheckerTests/special/gasleft.sol @@ -4,7 +4,11 @@ contract C { function f() public view { assert(gasleft() > 0); + uint g = gasleft(); + assert(g < gasleft()); + assert(g >= gasleft()); } } // ---- // Warning: (76-97): Assertion violation happens here +// Warning: (123-144): Assertion violation happens here -- cgit