[SMTChecker] Variables are merged after branches (ite variables)

libsolidity/formal/SMTChecker.cpp

@@ -91,15 +91,16 @@ bool SMTChecker::visit(IfStatement const& _node)
 
 	checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
 
-	visitBranch(_node.trueStatement(), expr(_node.condition()));
+	auto countersEndFalse = m_currentSequenceCounter;
+	auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
 	vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
 	if (_node.falseStatement())
 	{
-		visitBranch(*_node.falseStatement(), !expr(_node.condition()));
+		countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
 		touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
 	}
 
-	resetVariables(touchedVariables);
+	mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse);
 
 	return false;
 }
@@ -506,12 +507,12 @@ void SMTChecker::assignment(Declaration const& _variable, smt::Expression const&
 	m_interface->addAssertion(newValue(_variable) == _value);
 }
 
-void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
 {
-	visitBranch(_statement, &_condition);
+	return visitBranch(_statement, &_condition);
 }
 
-void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
+SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
 {
 	VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
 
@@ -522,7 +523,8 @@ void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const*
 		popPathCondition();
 
 	m_conditionalExecutionHappened = true;
-	m_currentSequenceCounter = sequenceCountersStart;
+	std::swap(sequenceCountersStart, m_currentSequenceCounter);
+	return sequenceCountersStart;
 }
 
 void SMTChecker::checkCondition(
@@ -702,6 +704,22 @@ void SMTChecker::resetVariables(vector<Declaration const*> _variables)
 	}
 }
 
+void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse)
+{
+	set<Declaration const*> uniqueVars(_variables.begin(), _variables.end());
+	for (auto const* decl: uniqueVars)
+	{
+		int trueCounter = _countersEndTrue.at(decl);
+		int falseCounter = _countersEndFalse.at(decl);
+		solAssert(trueCounter != falseCounter, "");
+		m_interface->addAssertion(newValue(*decl) == smt::Expression::ite(
+			_condition,
+			valueAtSequence(*decl, trueCounter),
+			valueAtSequence(*decl, falseCounter))
+		);
+	}
+}
+
 bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 {
 	if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))

libsolidity/formal/SMTChecker.h

@@ -75,10 +75,14 @@ private:
 	void assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location);
 	void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
 
-	// Visits the branch given by the statement, pushes and pops the SMT checker.
+	/// Maps a variable to an SSA index.
-	// @param _condition if present, asserts that this condition is true within the branch.
+	using VariableSequenceCounters = std::map<Declaration const*, int>;
-	void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+
-	void visitBranch(Statement const& _statement, smt::Expression _condition);
+	/// Visits the branch given by the statement, pushes and pops the current path conditions.
+	/// @param _condition if present, asserts that this condition is true within the branch.
+	/// @returns the variable sequence counter after visiting the branch.
+	VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+	VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression _condition);
 
 	/// Check that a condition can be satisfied.
 	void checkCondition(
@@ -106,6 +110,10 @@ private:
 
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void resetVariables(std::vector<Declaration const*> _variables);
+	/// Given two different branches and the touched variables,
+	/// merge the touched variables into after-branch ite variables
+	/// using the branch condition as guard.
+	void mergeVariables(std::vector<Declaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse);
 	/// Tries to create an uninitialized variable and returns true on success.
 	/// This fails if the type is not supported.
 	bool createVariable(VariableDeclaration const& _varDecl);
@@ -134,8 +142,6 @@ private:
 	static smt::Expression minValue(IntegerType const& _t);
 	static smt::Expression maxValue(IntegerType const& _t);
 
-	using VariableSequenceCounters = std::map<Declaration const*, int>;
-
 	/// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
 	smt::Expression expr(Expression const& _e);
 	/// Creates the expression (value can be arbitrary)

test/libsolidity/SMTChecker.cpp

@@ -168,9 +168,9 @@ BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars)
 	CHECK_SUCCESS_NO_WARNINGS(text);
 }
 
-BOOST_AUTO_TEST_CASE(branches_clear_variables)
+BOOST_AUTO_TEST_CASE(branches_merge_variables)
 {
-	// Only clears accessed variables
+	// Branch does not touch variable a
 	string text = R"(
 		contract C {
 			function f(uint x) public pure {
@@ -182,7 +182,7 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables)
 		}
 	)";
 	CHECK_SUCCESS_NO_WARNINGS(text);
-	// It is just a plain clear and will not combine branches.
+	// Positive branch touches variable a, but assertion should still hold.
 	text = R"(
 	contract C {
 			function f(uint x) public pure {
@@ -194,8 +194,8 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables)
 			}
 		}
 	)";
-	CHECK_WARNING(text, "Assertion violation happens here");
+	CHECK_SUCCESS_NO_WARNINGS(text);
-	// Clear also works on the else branch
+	// Negative branch touches variable a, but assertion should still hold.
 	text = R"(
 		contract C {
 			function f(uint x) public pure {
@@ -208,8 +208,8 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables)
 			}
 		}
 	)";
-	CHECK_WARNING(text, "Assertion violation happens here");
+	CHECK_SUCCESS_NO_WARNINGS(text);
-	// Variable is not cleared, if it is only read.
+	// Variable is not merged, if it is only read.
 	text = R"(
 		contract C {
 			function f(uint x) public pure {
@@ -224,6 +224,36 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables)
 		}
 	)";
 	CHECK_SUCCESS_NO_WARNINGS(text);
+	// Variable is reset in both branches
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 2;
+				if (x > 10) {
+					a = 3;
+				} else {
+					a = 3;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	// Variable is reset in both branches
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 2;
+				if (x > 10) {
+					a = 3;
+				} else {
+					a = 4;
+				}
+				assert(a >= 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
 }
 
 BOOST_AUTO_TEST_CASE(branches_assert_condition)
@@ -262,7 +292,7 @@ BOOST_AUTO_TEST_CASE(branches_assert_condition)
 	CHECK_SUCCESS_NO_WARNINGS(text);
 }
 
-BOOST_AUTO_TEST_CASE(ways_to_clear_variables)
+BOOST_AUTO_TEST_CASE(ways_to_merge_variables)
 {
 	string text = R"(
 		contract C {
@@ -275,6 +305,7 @@ BOOST_AUTO_TEST_CASE(ways_to_clear_variables)
 			}
 		}
 	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
 	text = R"(
 		contract C {
 			function f(uint x) public pure {