[SMTChecker] Small refactoring of defining SMT expressions for structs/tuples

libsolidity/formal/SMTEncoder.cpp

@@ -457,33 +457,23 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 
 		addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c); }));
 	}
-	else if (_tuple.components().size() == 1)
-		defineExpr(_tuple, expr(*_tuple.components().front()));
 	else
 	{
-		solAssert(_tuple.annotation().type->category() == Type::Category::Tuple, "");
+		auto values = applyMap(_tuple.components(), [this](auto const& component) -> optional<smtutil::Expression> {
-		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
+			if (component)
-		solAssert(symbTuple, "");
-		auto const& symbComponents = symbTuple->components();
-		auto const* tuple = dynamic_cast<TupleExpression const*>(innermostTuple(_tuple));
-		solAssert(tuple, "");
-		auto const& tupleComponents = tuple->components();
-		solAssert(symbComponents.size() == tupleComponents.size(), "");
-		for (unsigned i = 0; i < symbComponents.size(); ++i)
 			{
-			auto tComponent = tupleComponents.at(i);
+				if (auto varDecl = identifierToVariable(*component))
-			if (tComponent)
+					return currentValue(*varDecl);
-			{
-				if (auto varDecl = identifierToVariable(*tComponent))
-					m_context.addAssertion(symbTuple->component(i) == currentValue(*varDecl));
 				else
 				{
-					if (!m_context.knownExpression(*tComponent))
+					if (!m_context.knownExpression(*component))
-						createExpr(*tComponent);
+						createExpr(*component);
-					m_context.addAssertion(symbTuple->component(i) == expr(*tComponent));
+					return expr(*component);
-				}
 				}
 			}
+			return {};
+		});
+		defineExpr(_tuple, values);
 	}
 }
 
@@ -1064,19 +1054,8 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
 				m_context.addAssertion(structVar.currentValue() == currentExpr);
 				auto returnedMembers = structGetterReturnedMembers(dynamic_cast<StructType const&>(*structVar.type()));
 				solAssert(!returnedMembers.empty(), "");
-				auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) { return structVar.member(memberName); });
+				auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) -> optional<smtutil::Expression> { return structVar.member(memberName); });
-				if (returnedValues.size() == 1)
+				defineExpr(_funCall, returnedValues);
-					defineExpr(_funCall, returnedValues.front());
-				else
-				{
-					auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
-					solAssert(symbTuple, "");
-					symbTuple->increaseIndex(); // Increasing the index explicitly since we cannot use defineExpr in this case.
-					auto const& symbComponents = symbTuple->components();
-					solAssert(symbComponents.size() == returnedValues.size(), "");
-					for (unsigned i = 0; i < symbComponents.size(); ++i)
-						m_context.addAssertion(symbTuple->component(i) == returnedValues.at(i));
-				}
 				return;
 			}
 			default:
@@ -2476,7 +2455,23 @@ void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value)
 			currentPathConditions(),
 			smt::symbolicUnknownConstraints(expr(_e), type)
 		));
+}
 
+void SMTEncoder::defineExpr(Expression const& _e, vector<optional<smtutil::Expression>> const& _values)
+{
+	if (_values.size() == 1 && _values.front())
+	{
+		defineExpr(_e, *_values.front());
+		return;
+	}
+	auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_e));
+	solAssert(symbTuple, "");
+	symbTuple->increaseIndex();
+	auto const& symbComponents = symbTuple->components();
+	solAssert(symbComponents.size() == _values.size(), "");
+	for (unsigned i = 0; i < symbComponents.size(); ++i)
+		if (_values[i])
+			m_context.addAssertion(symbTuple->component(i) == *_values[i]);
 }
 
 void SMTEncoder::popPathCondition()
@@ -3007,23 +3002,11 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, Contrac
 	auto const& returnParams = funDef->returnParameters();
 	for (auto param: returnParams)
 		createVariable(*param);
-
+	auto returnValues = applyMap(returnParams, [this](auto const& param) -> optional<smtutil::Expression> {
-	if (returnParams.size() > 1)
+		solAssert(param && m_context.knownVariable(*param), "");
-	{
+		return currentValue(*param);
-		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
+	});
-		solAssert(symbTuple, "");
+	defineExpr(_funCall, returnValues);
-		auto const& symbComponents = symbTuple->components();
-		solAssert(symbComponents.size() == returnParams.size(), "");
-		for (unsigned i = 0; i < symbComponents.size(); ++i)
-		{
-			auto param = returnParams.at(i);
-			solAssert(param, "");
-			solAssert(m_context.knownVariable(*param), "");
-			m_context.addAssertion(symbTuple->component(i) == currentValue(*param));
-		}
-	}
-	else if (returnParams.size() == 1)
-		defineExpr(_funCall, currentValue(*returnParams.front()));
 }
 
 vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract)

libsolidity/formal/SMTEncoder.h

@@ -311,6 +311,8 @@ protected:
 	void createExpr(Expression const& _e);
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smtutil::Expression _value);
+	/// Creates the tuple expression and sets its value.
+	void defineExpr(Expression const& _e, std::vector<std::optional<smtutil::Expression>> const& _values);
 	/// Overwrites the current path condition
 	void setPathCondition(smtutil::Expression const& _e);
 	/// Adds a new path condition

test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol

@@ -10,5 +10,7 @@ contract C {
 		assert(h == k);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)\n    C.fi(data, 39) -- internal call
+// Warning 6328: (229-243): CHC: Assertion violation happens here.