Merge pull request #7172 from ethereum/smt_fix_return_tuple

[SMTChecker] CHC create function returned expressions

Changelog.md

@@ -22,6 +22,7 @@ Bugfixes:
  * SMTChecker: Fix internal error when inlining functions that contain tuple expressions.
  * SMTChecker: Fix pointer knowledge erasing in loops.
  * SMTChecker: Fix internal error when using compound bitwise assignment operators inside branches.
+ * SMTChecker: Fix internal error when inlining a function that returns a tuple containing an unsupported type inside a branch.
  * View/Pure Checker: Properly detect state variable access through base class.
  * Yul analyzer: Check availability of data objects already in analysis phase.
  * Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program.

libsolidity/formal/BMC.cpp

@@ -426,21 +426,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 			initFunction(*funDef);
 		funDef->accept(*this);
 
-		auto const& returnParams = funDef->returnParameters();
+		createReturnedExpressions(_funCall);
-		if (returnParams.size() > 1)
-		{
-			vector<shared_ptr<smt::SymbolicVariable>> components;
-			for (auto param: returnParams)
-			{
-				solAssert(m_context.variable(*param), "");
-				components.push_back(m_context.variable(*param));
-			}
-			auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
-			solAssert(symbTuple, "");
-			symbTuple->setComponents(move(components));
-		}
-		else if (returnParams.size() == 1)
-			defineExpr(_funCall, currentValue(*returnParams.front()));
 	}
 }
 

libsolidity/formal/CHC.cpp

@@ -123,6 +123,8 @@ void CHC::endVisit(FunctionCall const& _funCall)
 	}
 
 	SMTEncoder::endVisit(_funCall);
+
+	createReturnedExpressions(_funCall);
 }
 
 void CHC::visitAssert(FunctionCall const&)

libsolidity/formal/SMTEncoder.cpp

@@ -643,13 +643,15 @@ void SMTEncoder::endVisit(Return const& _return)
 		auto returnParams = m_callStack.back().first->returnParameters();
 		if (returnParams.size() > 1)
 		{
-			auto tuple = dynamic_cast<TupleExpression const*>(_return.expression());
+			auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*_return.expression()));
-			solAssert(tuple, "");
+			solAssert(symbTuple, "");
-			auto const& components = tuple->components();
+			auto const& components = symbTuple->components();
 			solAssert(components.size() == returnParams.size(), "");
 			for (unsigned i = 0; i < returnParams.size(); ++i)
-				if (components.at(i))
+			{
-					m_context.addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i)));
+				solAssert(components.at(i), "");
+				m_context.addAssertion(components.at(i)->currentValue() == m_context.newValue(*returnParams.at(i)));
+			}
 		}
 		else if (returnParams.size() == 1)
 			m_context.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
@@ -1411,3 +1413,32 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall cons
 
 	return funDef;
 }
+
+void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
+{
+	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
+	if (!funDef)
+		return;
+
+	auto const& returnParams = funDef->returnParameters();
+	for (auto param: returnParams)
+		createVariable(*param);
+
+	if (returnParams.size() > 1)
+	{
+		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
+		solAssert(symbTuple, "");
+		if (symbTuple->components().empty())
+		{
+			vector<shared_ptr<smt::SymbolicVariable>> components;
+			for (auto param: returnParams)
+			{
+				solAssert(m_context.knownVariable(*param), "");
+				components.push_back(m_context.variable(*param));
+			}
+			symbTuple->setComponents(move(components));
+		}
+	}
+	else if (returnParams.size() == 1)
+		defineExpr(_funCall, currentValue(*returnParams.front()));
+}

libsolidity/formal/SMTEncoder.h

@@ -208,6 +208,10 @@ protected:
 	/// @returns the VariableDeclaration referenced by an Identifier or nullptr.
 	VariableDeclaration const* identifierToVariable(Expression const& _expr);
 
+	/// Creates symbolic expressions for the returned values
+	/// and set them as the components of the symbolic tuple.
+	void createReturnedExpressions(FunctionCall const& _funCall);
+
 	/// @returns a note to be added to warnings.
 	std::string extraComment();
 

test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S { uint x; }
+
+	function g() internal pure returns (uint, S memory) {
+		return (2, S(3));
+	}
+	function f(uint a) public pure {
+		uint x;
+		S memory y;
+		if (a > 100)
+			(x, y) = g();
+	}
+}
+// ----
+// Warning: (112-120): Assertion checker does not yet support the type of this variable.
+// Warning: (137-141): Assertion checker does not yet implement type struct C.S memory
+// Warning: (137-141): Assertion checker does not yet implement this expression.
+// Warning: (193-203): Assertion checker does not yet support the type of this variable.
+// Warning: (137-141): Assertion checker does not yet implement type struct C.S memory
+// Warning: (137-141): Assertion checker does not yet implement this expression.
+// Warning: (227-228): Assertion checker does not yet implement type struct C.S memory