Merge pull request #6244 from ethereum/smt_modifiers

[SMTChecker] Support modifiers

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).
 
 

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<ModifierInvocation> const& modifierInvocation = function.modifiers()[m_modifierDepthStack.back()];
+		solAssert(modifierInvocation, "");
+		modifierInvocation->accept(*this);
+		auto const& modifierDef = dynamic_cast<ModifierDefinition const&>(
+			*modifierInvocation->name()->annotation().referencedDeclaration
+		);
+		vector<smt::Expression> 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<smt::Expression> const& _callArgs)
+void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smt::Expression> 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);

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<smt::Expression> const& _callArgs);
+	void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smt::Expression> 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<OverflowTarget> 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<int> m_modifierDepthStack;
 };
 
 }

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

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

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

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

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

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

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

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

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.

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.

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

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);
+	}
+}

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.

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