[SMTChecker] Refactoring expression to tuple assignment

libsolidity/formal/BMC.cpp

@@ -351,11 +351,8 @@ bool BMC::visit(TryStatement const& _tryStatement)
 	solAssert(externalCall && externalCall->annotation().tryCall, "");
 
 	externalCall->accept(*this);
-	auto callExpr = expr(*externalCall);
 	if (_tryStatement.successClause()->parameters())
-		tryCatchAssignment(
+		expressionToTupleAssignment(_tryStatement.successClause()->parameters()->parameters(), *externalCall);
-			_tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall)
-		);
 
 	smtutil::Expression clauseId = m_context.newVariable("clause_choice_" + to_string(m_context.newUniqueId()), smtutil::SortProvider::uintSort);
 	auto const& clauses = _tryStatement.clauses();

libsolidity/formal/CHC.cpp

@@ -567,9 +567,8 @@ bool CHC::visit(TryStatement const& _tryStatement)
 	// Only now visit the actual call to record its effects and connect to the success clause.
 	endVisit(*externalCall);
 	if (_tryStatement.successClause()->parameters())
-		tryCatchAssignment(
+		expressionToTupleAssignment(_tryStatement.successClause()->parameters()->parameters(), *externalCall);
-			_tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall)
+
-		);
 	connectBlocks(m_currentBlock, predicate(*clauseBlocks[0]));
 
 	for (size_t i = 0; i < clauses.size(); ++i)

libsolidity/formal/SMTEncoder.cpp

@@ -323,37 +323,9 @@ void SMTEncoder::popInlineFrame(CallableDeclaration const&)
 }
 
 void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
-{
-	if (_varDecl.declarations().size() != 1)
 {
 	if (auto init = _varDecl.initialValue())
-		{
+		expressionToTupleAssignment(_varDecl.declarations(), *init);
-			auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*init));
-			solAssert(symbTuple, "");
-			auto const& symbComponents = symbTuple->components();
-
-			auto tupleType = dynamic_cast<TupleType const*>(init->annotation().type);
-			solAssert(tupleType, "");
-			solAssert(tupleType->components().size() == symbTuple->components().size(), "");
-			auto const& components = tupleType->components();
-
-			auto const& declarations = _varDecl.declarations();
-			solAssert(symbComponents.size() == declarations.size(), "");
-			for (unsigned i = 0; i < declarations.size(); ++i)
-				if (
-					components.at(i) &&
-					declarations.at(i) &&
-					m_context.knownVariable(*declarations.at(i))
-				)
-					assignment(*declarations.at(i), symbTuple->component(i, components.at(i), declarations.at(i)->type()));
-		}
-	}
-	else
-	{
-		solAssert(m_context.knownVariable(*_varDecl.declarations().front()), "");
-		if (_varDecl.initialValue())
-			assignment(*_varDecl.declarations().front(), *_varDecl.initialValue());
-	}
 }
 
 bool SMTEncoder::visit(Assignment const& _assignment)
@@ -2107,24 +2079,35 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
 	return values.first;
 }
 
-void SMTEncoder::tryCatchAssignment(vector<shared_ptr<VariableDeclaration>> const& _variables, smt::SymbolicVariable const& _rhs)
+void SMTEncoder::expressionToTupleAssignment(vector<shared_ptr<VariableDeclaration>> const& _variables, Expression const& _rhs)
 {
+	auto symbolicVar = m_context.expression(_rhs);
 	if (_variables.size() > 1)
 	{
-		auto const* symbTuple = dynamic_cast<smt::SymbolicTupleVariable const*>(&_rhs);
+		auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(symbolicVar);
 		solAssert(symbTuple, "");
 		auto const& symbComponents = symbTuple->components();
 		solAssert(symbComponents.size() == _variables.size(), "");
+		auto tupleType = dynamic_cast<TupleType const*>(_rhs.annotation().type);
+		solAssert(tupleType, "");
+		auto const& typeComponents = tupleType->components();
+		solAssert(typeComponents.size() == symbComponents.size(), "");
 		for (unsigned i = 0; i < symbComponents.size(); ++i)
 		{
 			auto param = _variables.at(i);
-			solAssert(param, "");
+			if (param)
+			{
 				solAssert(m_context.knownVariable(*param), "");
-			assignment(*param, symbTuple->component(i));
+				assignment(*param, symbTuple->component(i, typeComponents[i], param->type()));
+			}
 		}
 	}
 	else if (_variables.size() == 1)
-		assignment(*_variables.front(), _rhs.currentValue());
+	{
+		auto const& var = *_variables.front();
+		solAssert(m_context.knownVariable(var), "");
+		assignment(var, _rhs);
+	}
 }
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value)

libsolidity/formal/SMTEncoder.h

@@ -238,8 +238,8 @@ protected:
 	void tupleAssignment(Expression const& _left, Expression const& _right);
 	/// Computes the right hand side of a compound assignment.
 	smtutil::Expression compoundAssignment(Assignment const& _assignment);
-	/// Handles assignment of the result of external call in try statement to the parameters of success clause
+	/// Handles assignment of an expression to a tuple of variables.
-	void tryCatchAssignment(std::vector<std::shared_ptr<VariableDeclaration>> const& _variables, smt::SymbolicVariable const& rhs);
+	void expressionToTupleAssignment(std::vector<std::shared_ptr<VariableDeclaration>> const& _variables, Expression const& _rhs);
 
 	/// Maps a variable to an SSA index.
 	using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;

test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol

@@ -24,10 +24,8 @@ contract C {
     }
 }
 // ----
-// Warning 6031: (261-267): Internal error: Expression undefined for SMT solver.
 // Warning 7650: (284-296): Assertion checker does not yet support this expression.
 // Warning 6328: (470-495): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.check()\n  C.f() -- internal call\n  C.g() -- internal call
 // Warning 6328: (540-565): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.check()\n  C.f() -- internal call\n  C.g() -- internal call\n  C.i() -- internal call\n  C.i() -- internal call
-// Warning 6031: (261-267): Internal error: Expression undefined for SMT solver.
 // Warning 7650: (284-296): Assertion checker does not yet support this expression.
 // Warning 7650: (284-296): Assertion checker does not yet support this expression.