From 79d8a4e13a4d8262493d537cefa77331fa98f001 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 1 Apr 2019 11:10:28 +0200 Subject: [PATCH] [SMTChecker] Refactor VariableUsage --- libsolidity/formal/SMTChecker.cpp | 48 ++++---- libsolidity/formal/SMTChecker.h | 11 +- libsolidity/formal/VariableUsage.cpp | 107 ++++++++---------- libsolidity/formal/VariableUsage.h | 30 ++--- .../functions/function_inline_chain.sol | 41 +++++++ .../modifier_assignment_outside_branch.sol | 19 ++++ .../modifiers/modifier_inside_branch.sol | 13 +++ .../modifier_inside_branch_assignment.sol | 23 ++++ ...difier_inside_branch_assignment_branch.sol | 27 +++++ ...nside_branch_assignment_multi_branches.sol | 35 ++++++ 10 files changed, 249 insertions(+), 105 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/functions/function_inline_chain.sol create mode 100644 test/libsolidity/smtCheckerTests/modifiers/modifier_assignment_outside_branch.sol create mode 100644 test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch.sol create mode 100644 test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol create mode 100644 test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_branch.sol create mode 100644 test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 7d2a8c8bb..fc2382d01 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -18,7 +18,6 @@ #include #include -#include #include #include @@ -51,7 +50,6 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map const& _ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr const& _scanner) { - m_variableUsage = make_shared(_source); m_scanner = _scanner; if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) _source.accept(*this); @@ -202,17 +200,17 @@ bool SMTChecker::visit(IfStatement const& _node) checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE."); auto indicesEndTrue = visitBranch(&_node.trueStatement(), expr(_node.condition())); - vector touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement()); + auto touchedVars = touchedVariables(_node.trueStatement()); decltype(indicesEndTrue) indicesEndFalse; if (_node.falseStatement()) { indicesEndFalse = visitBranch(_node.falseStatement(), !expr(_node.condition())); - touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement()); + touchedVars += touchedVariables(*_node.falseStatement()); } else indicesEndFalse = copyVariableIndices(); - mergeVariables(touchedVariables, expr(_node.condition()), indicesEndTrue, indicesEndFalse); + mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse); return false; } @@ -229,8 +227,8 @@ bool SMTChecker::visit(IfStatement const& _node) bool SMTChecker::visit(WhileStatement const& _node) { auto indicesBeforeLoop = copyVariableIndices(); - auto touchedVariables = m_variableUsage->touchedVariables(_node); - resetVariables(touchedVariables); + auto touchedVars = touchedVariables(_node); + resetVariables(touchedVars); decltype(indicesBeforeLoop) indicesAfterLoop; if (_node.isDoWhile()) { @@ -257,7 +255,7 @@ bool SMTChecker::visit(WhileStatement const& _node) if (!_node.isDoWhile()) _node.condition().accept(*this); - mergeVariables(touchedVariables, expr(_node.condition()), indicesAfterLoop, copyVariableIndices()); + mergeVariables(touchedVars, expr(_node.condition()), indicesAfterLoop, copyVariableIndices()); m_loopExecutionHappened = true; return false; @@ -272,17 +270,13 @@ bool SMTChecker::visit(ForStatement const& _node) auto indicesBeforeLoop = copyVariableIndices(); // Do not reset the init expression part. - auto touchedVariables = - m_variableUsage->touchedVariables(_node.body()); + auto touchedVars = touchedVariables(_node.body()); if (_node.condition()) - touchedVariables += m_variableUsage->touchedVariables(*_node.condition()); + touchedVars += touchedVariables(*_node.condition()); if (_node.loopExpression()) - touchedVariables += m_variableUsage->touchedVariables(*_node.loopExpression()); - // Remove duplicates - std::sort(touchedVariables.begin(), touchedVariables.end()); - touchedVariables.erase(std::unique(touchedVariables.begin(), touchedVariables.end()), touchedVariables.end()); + touchedVars += touchedVariables(*_node.loopExpression()); - resetVariables(touchedVariables); + resetVariables(touchedVars); if (_node.condition()) { @@ -307,7 +301,7 @@ bool SMTChecker::visit(ForStatement const& _node) _node.condition()->accept(*this); auto forCondition = _node.condition() ? expr(*_node.condition()) : smt::Expression(true); - mergeVariables(touchedVariables, forCondition, indicesAfterLoop, copyVariableIndices()); + mergeVariables(touchedVars, forCondition, indicesAfterLoop, copyVariableIndices()); m_loopExecutionHappened = true; return false; @@ -1153,17 +1147,17 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op) { // @TODO check that both of them are not constant _op.leftExpression().accept(*this); - auto touchedVariables = m_variableUsage->touchedVariables(_op.leftExpression()); + auto touchedVars = touchedVariables(_op.leftExpression()); if (_op.getOperator() == Token::And) { auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())); - mergeVariables(touchedVariables, !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); + mergeVariables(touchedVars, !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression())); } else { auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())); - mergeVariables(touchedVariables, expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); + mergeVariables(touchedVars, expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression())); } } @@ -1498,7 +1492,7 @@ void SMTChecker::resetStorageReferences() resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); }); } -void SMTChecker::resetVariables(vector _variables) +void SMTChecker::resetVariables(set const& _variables) { for (auto const* decl: _variables) resetVariable(*decl); @@ -1520,12 +1514,6 @@ TypePointer SMTChecker::typeWithoutPointer(TypePointer const& _type) return _type; } -void SMTChecker::mergeVariables(vector const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) -{ - set uniqueVars(_variables.begin(), _variables.end()); - mergeVariables(uniqueVars, _condition, _indicesEndTrue, _indicesEndFalse); -} - void SMTChecker::mergeVariables(set const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) { for (auto const* decl: _variables) @@ -1755,3 +1743,9 @@ FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCa return nullptr; } + +set SMTChecker::touchedVariables(ASTNode const& _node) +{ + solAssert(!m_functionPath.empty(), ""); + return m_variableUsage.touchedVariables(_node, m_functionPath); +} diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index e47bd851c..b6967c2e6 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -20,6 +20,7 @@ #include #include +#include #include #include @@ -41,8 +42,6 @@ namespace dev namespace solidity { -class VariableUsage; - class SMTChecker: private ASTConstVisitor { public: @@ -200,7 +199,7 @@ private: void resetVariable(VariableDeclaration const& _variable); void resetStateVariables(); void resetStorageReferences(); - void resetVariables(std::vector _variables); + void resetVariables(std::set const& _variables); void resetVariables(std::function const& _filter); /// @returns the type without storage pointer information if it has it. TypePointer typeWithoutPointer(TypePointer const& _type); @@ -208,7 +207,6 @@ private: /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables /// using the branch condition as guard. - void mergeVariables(std::vector const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse); void mergeVariables(std::set const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse); /// Tries to create an uninitialized variable and returns true on success. /// This fails if the type is not supported. @@ -271,8 +269,11 @@ private: /// Resets the variable indices. void resetVariableIndices(VariableIndices const& _indices); + /// @returns variables that are touched in _node's subtree. + std::set touchedVariables(ASTNode const& _node); + std::shared_ptr m_interface; - std::shared_ptr m_variableUsage; + VariableUsage m_variableUsage; bool m_loopExecutionHappened = false; bool m_arrayAssignmentHappened = false; // True if the "No SMT solver available" warning was already created. diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index cf8bf73bc..9f0575072 100644 --- a/libsolidity/formal/VariableUsage.cpp +++ b/libsolidity/formal/VariableUsage.cpp @@ -19,72 +19,61 @@ #include -#include +#include using namespace std; using namespace dev; using namespace dev::solidity; -VariableUsage::VariableUsage(ASTNode const& _node) +void VariableUsage::endVisit(Identifier const& _identifier) { - auto nodeFun = [&](ASTNode const& n) -> bool - { - 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) - 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) - { - if (m_touchedVariable.count(&_child) || m_children.count(&_child)) - m_children[&_parent].push_back(&_child); - }; - - ASTReduce reducer(nodeFun, edgeFun); - _node.accept(reducer); + Declaration const* declaration = _identifier.annotation().referencedDeclaration; + solAssert(declaration, ""); + if (VariableDeclaration const* varDecl = dynamic_cast(declaration)) + if (_identifier.annotation().lValueRequested) + m_touchedVariables.insert(varDecl); } -vector VariableUsage::touchedVariables(ASTNode const& _node) const +void VariableUsage::endVisit(FunctionCall const& _funCall) { - if (!m_children.count(&_node) && !m_touchedVariable.count(&_node)) - return {}; - - set touched; - set visitedFunctions; - vector toVisit; - toVisit.push_back(&_node); - - while (!toVisit.empty()) - { - 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), ""); - for (auto const& child: m_children.at(n)) - if (!visitedFunctions.count(child)) - toVisit.push_back(child); - } - else - { - solAssert(m_touchedVariable.count(n), ""); - touched.insert(m_touchedVariable.at(n)); - } - } - - return {touched.begin(), touched.end()}; + if (auto const& funDef = SMTChecker::inlinedFunctionCallToDefinition(_funCall)) + if (find(m_functionPath.begin(), m_functionPath.end(), funDef) == m_functionPath.end()) + funDef->accept(*this); +} + +bool VariableUsage::visit(FunctionDefinition const& _function) +{ + m_functionPath.push_back(&_function); + return true; +} + +void VariableUsage::endVisit(FunctionDefinition const&) +{ + solAssert(!m_functionPath.empty(), ""); + m_functionPath.pop_back(); +} + +void VariableUsage::endVisit(ModifierInvocation const& _modifierInv) +{ + auto const& modifierDef = dynamic_cast(_modifierInv.name()->annotation().referencedDeclaration); + if (modifierDef) + modifierDef->accept(*this); +} + +void VariableUsage::endVisit(PlaceholderStatement const&) +{ + solAssert(!m_functionPath.empty(), ""); + FunctionDefinition const* function = m_functionPath.back(); + solAssert(function, ""); + if (function->isImplemented()) + function->body().accept(*this); +} + +set VariableUsage::touchedVariables(ASTNode const& _node, vector const& _outerCallstack) +{ + m_touchedVariables.clear(); + m_functionPath.clear(); + m_functionPath += _outerCallstack; + _node.accept(*this); + return m_touchedVariables; } diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h index dda13de25..c824eae62 100644 --- a/libsolidity/formal/VariableUsage.h +++ b/libsolidity/formal/VariableUsage.h @@ -17,33 +17,35 @@ #pragma once -#include -#include +#include + #include +#include namespace dev { namespace solidity { -class ASTNode; -class VariableDeclaration; - /** - * This class collects information about which local variables of value type - * are modified in which parts of the AST. + * This class computes information about which variables are modified in a certain subtree. */ -class VariableUsage +class VariableUsage: private ASTConstVisitor { public: - explicit VariableUsage(ASTNode const& _node); - - std::vector touchedVariables(ASTNode const& _node) const; + /// @param _outerCallstack the current callstack in the callers context. + std::set touchedVariables(ASTNode const& _node, std::vector const& _outerCallstack); private: - // Variable touched by a specific AST node. - std::map m_touchedVariable; - std::map> m_children; + void endVisit(Identifier const& _node) override; + void endVisit(FunctionCall const& _node) override; + bool visit(FunctionDefinition const& _node) override; + void endVisit(FunctionDefinition const& _node) override; + void endVisit(ModifierInvocation const& _node) override; + void endVisit(PlaceholderStatement const& _node) override; + + std::set m_touchedVariables; + std::vector m_functionPath; }; } diff --git a/test/libsolidity/smtCheckerTests/functions/function_inline_chain.sol b/test/libsolidity/smtCheckerTests/functions/function_inline_chain.sol new file mode 100644 index 000000000..2647e0771 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/function_inline_chain.sol @@ -0,0 +1,41 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + uint y; + uint z; + + function f() public { + if (x == 1) + x = 2; + else + x = 1; + g(); + assert(y == 1); + } + + function g() public { + y = 1; + h(); + assert(z == 1); + } + + function h() public { + z = 1; + x = 1; + f(); + // This fails for the following calls to the contract: + // h() + // g() h() + // It does not fail for f() g() h() because in that case + // h() will not inline f() since it already is in the callstack. + assert(x == 1); + } +} +// ---- +// Warning: (271-274): Assertion checker does not support recursive function calls. +// Warning: (140-143): Assertion checker does not support recursive function calls. +// Warning: (483-497): Assertion violation happens here +// Warning: (201-204): Assertion checker does not support recursive function calls. +// Warning: (483-497): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_assignment_outside_branch.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_assignment_outside_branch.sol new file mode 100644 index 000000000..b3c9ab0d6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_assignment_outside_branch.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + address owner; + + modifier onlyOwner { + if (msg.sender == owner) _; + } + + function f() public onlyOwner { + } + + function g(uint y) public { + y = 1; + if (y > x) f(); + } +} diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch.sol new file mode 100644 index 000000000..45202db3c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + address owner; + modifier onlyOwner { + if (msg.sender == owner) _; + } + function g() public onlyOwner { + } + function f(uint x) public { + if (x > 0) g(); + } +} diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol new file mode 100644 index 000000000..089cfffe3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; + +contract C { + uint x; + address owner; + + modifier onlyOwner { + if (msg.sender == owner) _; + } + + function f() public onlyOwner { + x = 0; + } + function g(uint y) public { + x = 1; + if (y > 0) + f(); + // Fails for {y = >0, msg.sender == owner, x = 0}. + assert(x > 0); + } +} +// ---- +// Warning: (287-300): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_branch.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_branch.sol new file mode 100644 index 000000000..eb56bfdd5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_branch.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; + +contract C { + uint x; + address owner; + + modifier onlyOwner { + if (msg.sender == owner) { + require(x > 0); + _; + } + } + + function f() public onlyOwner { + // Condition is always true due to `require(x > 0)` in the modifier. + if (x > 0) + x -= 1; + } + function g(uint y) public { + x = 2; + if (y > 0) + f(); + assert(x > 0); + } +} +// ---- +// Warning: (266-271): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol new file mode 100644 index 000000000..387047bb7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol @@ -0,0 +1,35 @@ +pragma experimental SMTChecker; + +contract C { + uint x; + address owner; + + modifier onlyOwner { + if (msg.sender == owner) { + require(x > 0); + _; + } + } + + function f() public onlyOwner { + x -= 1; + h(); + } + function h() public onlyOwner { + require(x < 10000); + x += 2; + } + function g(uint y) public { + require(y > 0 && y < 10000); + require(msg.sender == owner); + x = y; + if (y > 1) { + f(); + assert(x == y + 1); + } + // Fails for {y = 0, x = 0}. + assert(x == 0); + } +} +// ---- +// Warning: (461-475): Assertion violation happens here