diff --git a/Changelog.md b/Changelog.md index 44af0b689..49bc87bee 100644 --- a/Changelog.md +++ b/Changelog.md @@ -7,6 +7,7 @@ Compiler Features: * Function calls with named arguments now work with overloaded functions. * Inline Assembly: Issue error when using ``callvalue()`` inside nonpayable function (in the same way that ``msg.value`` already does). * SMTChecker: Show callstack together with model if applicable. + * SMTChecker: Support modifiers. * Yul Optimizer: Enable stack allocation optimization by default if yul optimizer is active (disable in yulDetails). diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 95622c380..5085a7991 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -93,14 +93,20 @@ void SMTChecker::endVisit(VariableDeclaration const& _varDecl) assignment(_varDecl, *_varDecl.value(), _varDecl.location()); } +bool SMTChecker::visit(ModifierDefinition const&) +{ + return false; +} + bool SMTChecker::visit(FunctionDefinition const& _function) { - if (!_function.modifiers().empty() || _function.isConstructor()) + if (_function.isConstructor()) m_errorReporter.warning( _function.location(), - "Assertion checker does not yet support constructors and functions with modifiers." + "Assertion checker does not yet support constructors." ); m_functionPath.push_back(&_function); + m_modifierDepthStack.push_back(-1); // Not visited by a function call if (isRootFunction()) { @@ -116,7 +122,54 @@ bool SMTChecker::visit(FunctionDefinition const& _function) m_loopExecutionHappened = false; m_arrayAssignmentHappened = false; } + _function.parameterList().accept(*this); + if (_function.returnParameterList()) + _function.returnParameterList()->accept(*this); + visitFunctionOrModifier(); + return false; +} +void SMTChecker::visitFunctionOrModifier() +{ + solAssert(!m_functionPath.empty(), ""); + solAssert(!m_modifierDepthStack.empty(), ""); + + ++m_modifierDepthStack.back(); + FunctionDefinition const& function = *m_functionPath.back(); + + if (m_modifierDepthStack.back() == int(function.modifiers().size())) + { + if (function.isImplemented()) + function.body().accept(*this); + } + else + { + solAssert(m_modifierDepthStack.back() < int(function.modifiers().size()), ""); + ASTPointer const& modifierInvocation = function.modifiers()[m_modifierDepthStack.back()]; + solAssert(modifierInvocation, ""); + modifierInvocation->accept(*this); + auto const& modifierDef = dynamic_cast( + *modifierInvocation->name()->annotation().referencedDeclaration + ); + vector modifierArgsExpr; + if (modifierInvocation->arguments()) + for (auto arg: *modifierInvocation->arguments()) + modifierArgsExpr.push_back(expr(*arg)); + initializeFunctionCallParameters(modifierDef, modifierArgsExpr); + pushCallStack(modifierInvocation.get()); + modifierDef.body().accept(*this); + popCallStack(); + } + + --m_modifierDepthStack.back(); +} + +bool SMTChecker::visit(PlaceholderStatement const&) +{ + solAssert(!m_functionPath.empty(), ""); + ASTNode const* lastCall = popCallStack(); + visitFunctionOrModifier(); + pushCallStack(lastCall); return true; } @@ -131,8 +184,11 @@ void SMTChecker::endVisit(FunctionDefinition const&) { checkUnderOverflow(); removeLocalVariables(); + solAssert(m_callStack.empty(), ""); } m_functionPath.pop_back(); + solAssert(m_modifierDepthStack.back() == -1, ""); + m_modifierDepthStack.pop_back(); } bool SMTChecker::visit(IfStatement const& _node) @@ -497,9 +553,9 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) visitGasLeft(_funCall); break; case FunctionType::Kind::Internal: - m_callStack.push_back(&_funCall); + pushCallStack(&_funCall); inlineFunctionCall(_funCall); - m_callStack.pop_back(); + popCallStack(); break; case FunctionType::Kind::External: resetStateVariables(); @@ -1261,7 +1317,7 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co // can't do anything. } else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE) - m_errorReporter.warning(_condition.location(), "Condition unreachable."); + m_errorReporter.warning(_condition.location(), "Condition unreachable.", currentCallStack()); else { string value; @@ -1276,7 +1332,11 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co solAssert(negatedResult == smt::CheckResult::SATISFIABLE, ""); value = "false"; } - m_errorReporter.warning(_condition.location(), boost::algorithm::replace_all_copy(_description, "$VALUE", value)); + m_errorReporter.warning( + _condition.location(), + boost::algorithm::replace_all_copy(_description, "$VALUE", value), + currentCallStack() + ); } } @@ -1316,7 +1376,7 @@ smt::CheckResult SMTChecker::checkSatisfiable() return checkSatisfiableAndGenerateModel({}).first; } -void SMTChecker::initializeFunctionCallParameters(FunctionDefinition const& _function, vector const& _callArgs) +void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _function, vector const& _callArgs) { auto const& funParams = _function.parameters(); solAssert(funParams.size() == _callArgs.size(), ""); @@ -1564,6 +1624,19 @@ SecondarySourceLocation SMTChecker::currentCallStack() return callStackLocation; } +ASTNode const* SMTChecker::popCallStack() +{ + solAssert(!m_callStack.empty(), ""); + ASTNode const* lastCalled = m_callStack.back(); + m_callStack.pop_back(); + return lastCalled; +} + +void SMTChecker::pushCallStack(ASTNode const* _node) +{ + m_callStack.push_back(_node); +} + void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e) { m_interface->addAssertion(currentPathConditions() && _e); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index a547e0133..33aeada2c 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -63,8 +63,10 @@ private: bool visit(ContractDefinition const& _node) override; void endVisit(ContractDefinition const& _node) override; void endVisit(VariableDeclaration const& _node) override; + bool visit(ModifierDefinition const& _node) override; bool visit(FunctionDefinition const& _node) override; void endVisit(FunctionDefinition const& _node) override; + bool visit(PlaceholderStatement const& _node) override; bool visit(IfStatement const& _node) override; bool visit(WhileStatement const& _node) override; bool visit(ForStatement const& _node) override; @@ -100,6 +102,10 @@ private: void abstractFunctionCall(FunctionCall const& _funCall); void visitFunctionIdentifier(Identifier const& _identifier); + /// Encodes a modifier or function body according to the modifier + /// visit depth. + void visitFunctionOrModifier(); + void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false); void defineGlobalFunction(std::string const& _name, Expression const& _expr); /// Handles the side effects of assignment @@ -174,7 +180,7 @@ private: smt::CheckResult checkSatisfiable(); void initializeLocalVariables(FunctionDefinition const& _function); - void initializeFunctionCallParameters(FunctionDefinition const& _function, std::vector const& _callArgs); + void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector const& _callArgs); void resetVariable(VariableDeclaration const& _variable); void resetStateVariables(); void resetStorageReferences(); @@ -231,6 +237,10 @@ private: smt::Expression currentPathConditions(); /// Returns the current callstack. Used for models. langutil::SecondarySourceLocation currentCallStack(); + /// Copies and pops the last called node. + ASTNode const* popCallStack(); + /// Adds @param _node to the callstack. + void pushCallStack(ASTNode const* _node); /// Conjoin the current path conditions with the given parameter and add to the solver void addPathConjoinedExpression(smt::Expression const& _e); /// Add to the solver: the given expression implied by the current path conditions @@ -280,6 +290,12 @@ private: bool visitedFunction(FunctionDefinition const* _funDef); std::vector m_overflowTargets; + + /// Depth of visit to modifiers. + /// When m_modifierDepth == #modifiers the function can be visited + /// when placeholder is visited. + /// Needs to be a stack because of function calls. + std::vector m_modifierDepthStack; }; } diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol new file mode 100644 index 000000000..d4b486767 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + + modifier m { + require(x > 0); + _; + // Fails because of overflow behavior. + // Overflow is not reported because this assertion prevents + // it from reaching the end of the function. + assert(x > 1); + } + + function f() m public { + assert(x > 0); + x = x + 1; + } +} +// ---- +// Warning: (245-258): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_control_flow.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_control_flow.sol new file mode 100644 index 000000000..7a8d9264d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_control_flow.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + + modifier m { + if (x == 0) + _; + } + + function f() m public view { + assert(x == 0); + assert(x > 1); + } +} +// ---- +// Warning: (144-157): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol new file mode 100644 index 000000000..8a508cd68 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + + modifier m { + require(x > 0); + require(x < 10000); + _; + } + + modifier n { + x = x + 1; + _; + assert(x > 2); + assert(x > 8); + } + + function f() m n public { + x = x + 1; + } +} +// ---- +// Warning: (170-183): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol new file mode 100644 index 000000000..903d4f91c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; + +contract C +{ + modifier m(uint a, uint b) { + require(g(a, b)); + _; + } + + modifier notZero(uint x) { + require(x > 0); + _; + } + + function g(uint a, uint b) notZero(a) internal pure returns (bool) { + return a > b; + } + + function f(uint x) m(x, 0) public pure { + assert(x > 0); + assert(x > 1); + } +} +// ---- +// Warning: (86-93): Condition is always true. +// Warning: (311-324): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions_recursive.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions_recursive.sol new file mode 100644 index 000000000..4346b2cc2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions_recursive.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C +{ + modifier m(uint a, uint b) { + require(g(a, b)); + _; + } + + function g(uint a, uint b) m(a, b) internal pure returns (bool) { + return a > b; + } + + function f(uint x) m(x, 0) public pure { + assert(x > 0); + assert(x > 1); + } +} +// ---- +// Warning: (86-93): Assertion checker does not support recursive function calls. +// Warning: (86-93): Internal error: Expression undefined for SMT solver. +// Warning: (86-93): Assertion checker does not support recursive function calls. +// Warning: (86-93): Internal error: Expression undefined for SMT solver. +// Warning: (253-266): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_parameters.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_parameters.sol new file mode 100644 index 000000000..ec6ce47de --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_parameters.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C +{ + modifier m(uint a, uint b) { + require(a > b); + _; + } + + function f(uint x) m(x, 0) public pure { + assert(x > 0); + assert(x > 1); + } +} +// ---- +// Warning: (164-177): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol new file mode 100644 index 000000000..60b35e59d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + + modifier m { + require(x > 0); + _; + } + + function f() m public { + assert(x > 0); + x = x + 1; + } +} +// ---- +// Warning: (145-150): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_parameter_copy.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_parameter_copy.sol new file mode 100644 index 000000000..b91d2ee51 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_parameter_copy.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C +{ + modifier m(uint x) { + x == 2; + _; + } + + function f(uint x) m(x) public pure { + assert(x == 2); + } +} +// ---- +// Warning: (128-142): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_parameters.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_parameters.sol new file mode 100644 index 000000000..90eab0afd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_parameters.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + uint s; + modifier m(uint a) { + // Condition is always true for m(2). + require(a > 0); + _; + } + + function f(uint x) m(x) m(2) m(s) public view { + assert(x > 0); + assert(s > 0); + } +} +// ---- +// Warning: (127-132): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_return.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_return.sol new file mode 100644 index 000000000..2681b896f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_return.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C +{ + modifier m(uint x) { + require(x == 2); + _; + return; + } + + modifier n(uint x) { + require(x == 3); + _; + } + + function f(uint x) m(x) n(x) public pure { + assert(x == 3); + } +} +// ---- +// Warning: (138-144): Condition is always false. diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol new file mode 100644 index 000000000..7c43a311d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C +{ + modifier m { + uint x = 2; + _; + } + + function f(uint x) m public pure { + assert(x == 2); + } +} +// ---- +// Warning: (121-135): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_simple.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_simple.sol new file mode 100644 index 000000000..47df69872 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_simple.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + + modifier m { + require(x > 0); + _; + } + + function f() m public view { + assert(x > 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations.sol new file mode 100644 index 000000000..f954cf7ca --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + + modifier m { + // Condition is always true for the second invocation. + require(x > 0); + require(x < 10000); + _; + assert(x > 1); + } + + function f() m m public { + x = x + 1; + } +} +// ---- +// Warning: (137-142): Condition is always true. +// Warning: (155-164): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol new file mode 100644 index 000000000..288506607 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + + modifier m { + require(x > 0); + require(x < 10000); + _; + assert(x > 1); + _; + assert(x > 2); + assert(x > 10); + } + + function f() m public { + x = x + 1; + } +} +// ---- +// Warning: (156-170): Assertion violation happens here