From 6f9b69ebc345202235e4986193d2c317fc9241da Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 25 Mar 2019 13:58:22 +0100 Subject: [PATCH 1/3] Refactor function that retrieves FunctionDefinition from FunctionCall --- libsolidity/formal/SMTChecker.cpp | 60 ++++++++++++++++++------------- libsolidity/formal/SMTChecker.h | 4 +++ 2 files changed, 39 insertions(+), 25 deletions(-) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 7cdaa49f3..4e25c44fe 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -616,20 +616,8 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall) void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) { - FunctionDefinition const* _funDef = nullptr; - Expression const* _calledExpr = &_funCall.expression(); - - if (TupleExpression const* _fun = dynamic_cast(&_funCall.expression())) - { - solAssert(_fun->components().size() == 1, ""); - _calledExpr = _fun->components().at(0).get(); - } - - if (Identifier const* _fun = dynamic_cast(_calledExpr)) - _funDef = dynamic_cast(_fun->annotation().referencedDeclaration); - else if (MemberAccess const* _fun = dynamic_cast(_calledExpr)) - _funDef = dynamic_cast(_fun->annotation().referencedDeclaration); - else + FunctionDefinition const* _funDef = inlinedFunctionCallToDefinition(_funCall); + if (!_funDef) { m_errorReporter.warning( _funCall.location(), @@ -637,7 +625,6 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) ); return; } - solAssert(_funDef, ""); if (visitedFunction(_funDef)) m_errorReporter.warning( @@ -645,14 +632,15 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) "Assertion checker does not support recursive function calls.", SecondarySourceLocation().append("Starting from function:", _funDef->location()) ); - else if (_funDef && _funDef->isImplemented()) + else { vector funArgs; - auto const& funType = dynamic_cast(_calledExpr->annotation().type.get()); + Expression const* calledExpr = &_funCall.expression(); + auto const& funType = dynamic_cast(calledExpr->annotation().type.get()); solAssert(funType, ""); if (funType->bound()) { - auto const& boundFunction = dynamic_cast(_calledExpr); + auto const& boundFunction = dynamic_cast(calledExpr); solAssert(boundFunction, ""); funArgs.push_back(expr(boundFunction->expression())); } @@ -672,13 +660,6 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) defineExpr(_funCall, currentValue(*returnParams[0])); } } - else - { - m_errorReporter.warning( - _funCall.location(), - "Assertion checker does not support calls to functions without implementation." - ); - } } void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall) @@ -1673,3 +1654,32 @@ void SMTChecker::resetVariableIndices(VariableIndices const& _indices) for (auto const& var: _indices) m_variables.at(var.first)->index() = var.second; } + +FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCall const& _funCall) +{ + if (_funCall.annotation().kind != FunctionCallKind::FunctionCall) + return nullptr; + + FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + if (funType.kind() != FunctionType::Kind::Internal) + return nullptr; + + FunctionDefinition const* funDef = nullptr; + Expression const* calledExpr = &_funCall.expression(); + + if (TupleExpression const* fun = dynamic_cast(&_funCall.expression())) + { + solAssert(fun->components().size() == 1, ""); + calledExpr = fun->components().front().get(); + } + + if (Identifier const* fun = dynamic_cast(calledExpr)) + funDef = dynamic_cast(fun->annotation().referencedDeclaration); + else if (MemberAccess const* fun = dynamic_cast(calledExpr)) + funDef = dynamic_cast(fun->annotation().referencedDeclaration); + + if (funDef && funDef->isImplemented()) + return funDef; + + return nullptr; +} diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 66f4397e8..4df80ec8f 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -55,6 +55,10 @@ public: /// the constructor. std::vector unhandledQueries() { return m_interface->unhandledQueries(); } + /// @return the FunctionDefinition of a called function if possible and should inline, + /// otherwise nullptr. + static FunctionDefinition const* inlinedFunctionCallToDefinition(FunctionCall const& _funCall); + private: // TODO: Check that we do not have concurrent reads and writes to a variable, // because the order of expression evaluation is undefined From 1d63b97857361f1bed09c054b0b18d1294d3aa40 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 25 Mar 2019 15:01:07 +0100 Subject: [PATCH 2/3] Take inlined function calls into account when collecting touched variables --- Changelog.md | 1 + libsolidity/formal/VariableUsage.cpp | 23 +++++++++++++++++------ 2 files changed, 18 insertions(+), 6 deletions(-) diff --git a/Changelog.md b/Changelog.md index d1e221080..ca9af19cd 100644 --- a/Changelog.md +++ b/Changelog.md @@ -7,6 +7,7 @@ Compiler Features: Bugfixes: + * SMTChecker: SSA control-flow did not take into account state variables that were modified inside inlined functions that were called inside branches. diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index 9282a5606..cf8bf73bc 100644 --- a/libsolidity/formal/VariableUsage.cpp +++ b/libsolidity/formal/VariableUsage.cpp @@ -17,6 +17,8 @@ #include +#include + #include using namespace std; @@ -27,17 +29,19 @@ VariableUsage::VariableUsage(ASTNode const& _node) { auto nodeFun = [&](ASTNode const& n) -> bool { - if (Identifier const* identifier = dynamic_cast(&n)) + if (auto identifier = dynamic_cast(&n)) { Declaration const* declaration = identifier->annotation().referencedDeclaration; solAssert(declaration, ""); if (VariableDeclaration const* varDecl = dynamic_cast(declaration)) - if ( - identifier->annotation().lValueRequested && - varDecl->annotation().type->isValueType() - ) + if (identifier->annotation().lValueRequested) m_touchedVariable[&n] = varDecl; } + else if (auto funCall = dynamic_cast(&n)) + { + if (FunctionDefinition const* funDef = SMTChecker::inlinedFunctionCallToDefinition(*funCall)) + m_children[&n].push_back(funDef); + } return true; }; auto edgeFun = [&](ASTNode const& _parent, ASTNode const& _child) @@ -56,6 +60,7 @@ vector VariableUsage::touchedVariables(ASTNode const return {}; set touched; + set visitedFunctions; vector toVisit; toVisit.push_back(&_node); @@ -63,10 +68,16 @@ vector VariableUsage::touchedVariables(ASTNode const { ASTNode const* n = toVisit.back(); toVisit.pop_back(); + + if (auto funDef = dynamic_cast(n)) + visitedFunctions.insert(funDef); + if (m_children.count(n)) { solAssert(!m_touchedVariable.count(n), ""); - toVisit += m_children.at(n); + for (auto const& child: m_children.at(n)) + if (!visitedFunctions.count(child)) + toVisit.push_back(child); } else { From 2764d2f5257a8aee06e2c5bf7568bdd96c13f58a Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 25 Mar 2019 16:15:19 +0100 Subject: [PATCH 3/3] Tests that used to give false negatives --- ...unction_inside_branch_modify_state_var.sol | 19 +++++++++++++ ...ction_inside_branch_modify_state_var_2.sol | 18 ++++++++++++ ...ction_inside_branch_modify_state_var_3.sol | 28 +++++++++++++++++++ 3 files changed, 65 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_2.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol diff --git a/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol b/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol new file mode 100644 index 000000000..9ea612aa3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + function f() internal { + require(x < 10000); + x = x + 1; + } + function g(bool b) public { + x = 0; + if (b) + f(); + // Should fail for `b == true`. + assert(x == 0); + } +} +// ---- +// Warning: (209-223): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_2.sol b/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_2.sol new file mode 100644 index 000000000..63e4c6d06 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_2.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + function f() internal { + require(x < 10000); + x = x + 1; + } + function g(bool b) public { + x = 0; + if (b) + f(); + else + f(); + assert(x == 1); + } +} diff --git a/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol b/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol new file mode 100644 index 000000000..e5f312e93 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + function f() internal { + require(x < 10000); + x = x + 1; + } + function g(bool b) public { + x = 0; + if (b) + f(); + // Should fail for `b == true`. + assert(x == 0); + } + function h(bool b) public { + x = 0; + if (!b) + f(); + // Should fail for `b == false`. + assert(x == 0); + } + +} +// ---- +// Warning: (209-223): Assertion violation happens here +// Warning: (321-335): Assertion violation happens here