Merge pull request #6371 from ethereum/smt_variable_usage_function_calls

[SMTChecker] Merge SSA state vars properly

Changelog.md

@@ -8,6 +8,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.
 
 
 

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<TupleExpression const*>(&_funCall.expression()))
-	{
-		solAssert(_fun->components().size() == 1, "");
-		_calledExpr = _fun->components().at(0).get();
-	}
-
-	if (Identifier const* _fun = dynamic_cast<Identifier const*>(_calledExpr))
-		_funDef = dynamic_cast<FunctionDefinition const*>(_fun->annotation().referencedDeclaration);
-	else if (MemberAccess const* _fun = dynamic_cast<MemberAccess const*>(_calledExpr))
-		_funDef = dynamic_cast<FunctionDefinition const*>(_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<smt::Expression> funArgs;
-		auto const& funType = dynamic_cast<FunctionType const*>(_calledExpr->annotation().type.get());
+		Expression const* calledExpr = &_funCall.expression();
+		auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type.get());
 		solAssert(funType, "");
 		if (funType->bound())
 		{
-			auto const& boundFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
+			auto const& boundFunction = dynamic_cast<MemberAccess const*>(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<FunctionType const&>(*_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<TupleExpression const*>(&_funCall.expression()))
+	{
+		solAssert(fun->components().size() == 1, "");
+		calledExpr = fun->components().front().get();
+	}
+
+	if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
+		funDef = dynamic_cast<FunctionDefinition const*>(fun->annotation().referencedDeclaration);
+	else if (MemberAccess const* fun = dynamic_cast<MemberAccess const*>(calledExpr))
+		funDef = dynamic_cast<FunctionDefinition const*>(fun->annotation().referencedDeclaration);
+
+	if (funDef && funDef->isImplemented())
+		return funDef;
+
+	return nullptr;
+}

libsolidity/formal/SMTChecker.h

@@ -55,6 +55,10 @@ public:
 	/// the constructor.
 	std::vector<std::string> 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

libsolidity/formal/VariableUsage.cpp

@@ -17,6 +17,8 @@
 
 #include <libsolidity/formal/VariableUsage.h>
 
+#include <libsolidity/formal/SMTChecker.h>
+
 #include <libsolidity/ast/ASTVisitor.h>
 
 using namespace std;
@@ -27,17 +29,19 @@ VariableUsage::VariableUsage(ASTNode const& _node)
 {
 	auto nodeFun = [&](ASTNode const& n) -> bool
 	{
-		if (Identifier const* identifier = dynamic_cast<decltype(identifier)>(&n))
+		if (auto identifier = dynamic_cast<Identifier const*>(&n))
 		{
 			Declaration const* declaration = identifier->annotation().referencedDeclaration;
 			solAssert(declaration, "");
 			if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
-				if (
-					identifier->annotation().lValueRequested &&
-					varDecl->annotation().type->isValueType()
-				)
+				if (identifier->annotation().lValueRequested)
 					m_touchedVariable[&n] = varDecl;
 		}
+		else if (auto funCall = dynamic_cast<FunctionCall const*>(&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<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const
 		return {};
 
 	set<VariableDeclaration const*> touched;
+	set<ASTNode const*> visitedFunctions;
 	vector<ASTNode const*> toVisit;
 	toVisit.push_back(&_node);
 
@@ -63,10 +68,16 @@ vector<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const
 	{
 		ASTNode const* n = toVisit.back();
 		toVisit.pop_back();
+
+		if (auto funDef = dynamic_cast<FunctionDefinition const*>(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
 		{

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

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

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