Merge pull request #6382 from ethereum/smt_fix_short_circuit

[SMTChecker] Implement Boolean short-circuiting correctly

Changelog.md

@@ -8,6 +8,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Implement Boolean short-circuiting.
  * 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

@@ -200,12 +200,12 @@ bool SMTChecker::visit(IfStatement const& _node)
 	if (isRootFunction())
 		checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
 
-	auto indicesEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
+	auto indicesEndTrue = visitBranch(&_node.trueStatement(), expr(_node.condition()));
 	vector<VariableDeclaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
 	decltype(indicesEndTrue) indicesEndFalse;
 	if (_node.falseStatement())
 	{
-		indicesEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
+		indicesEndFalse = visitBranch(_node.falseStatement(), !expr(_node.condition()));
 		touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
 	}
 	else
@@ -233,7 +233,7 @@ bool SMTChecker::visit(WhileStatement const& _node)
 	decltype(indicesBeforeLoop) indicesAfterLoop;
 	if (_node.isDoWhile())
 	{
-		indicesAfterLoop = visitBranch(_node.body());
+		indicesAfterLoop = visitBranch(&_node.body());
 		// TODO the assertions generated in the body should still be active in the condition
 		_node.condition().accept(*this);
 		if (isRootFunction())
@@ -245,7 +245,7 @@ bool SMTChecker::visit(WhileStatement const& _node)
 		if (isRootFunction())
 			checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
 
-		indicesAfterLoop = visitBranch(_node.body(), expr(_node.condition()));
+		indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition()));
 	}
 
 	// We reset the execution to before the loop
@@ -502,20 +502,27 @@ bool SMTChecker::visit(UnaryOperation const& _op)
 
 bool SMTChecker::visit(BinaryOperation const& _op)
 {
-	return !shortcutRationalNumber(_op);
+	if (shortcutRationalNumber(_op))
+		return false;
+	if (TokenTraits::isBooleanOp(_op.getOperator()))
+	{
+		booleanOperation(_op);
+		return false;
+	}
+	return true;
 }
 
 void SMTChecker::endVisit(BinaryOperation const& _op)
 {
 	if (_op.annotation().type->category() == Type::Category::RationalNumber)
 		return;
+	if (TokenTraits::isBooleanOp(_op.getOperator()))
+		return;
 
 	if (TokenTraits::isArithmeticOp(_op.getOperator()))
 		arithmeticOperation(_op);
 	else if (TokenTraits::isCompareOp(_op.getOperator()))
 		compareOperation(_op);
-	else if (TokenTraits::isBooleanOp(_op.getOperator()))
-		booleanOperation(_op);
 	else
 		m_errorReporter.warning(
 			_op.location(),
@@ -1095,16 +1102,26 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
 	if (_op.annotation().commonType->category() == Type::Category::Bool)
 	{
 		// @TODO check that both of them are not constant
+		_op.leftExpression().accept(*this);
+		auto touchedVariables = m_variableUsage->touchedVariables(_op.leftExpression());
 		if (_op.getOperator() == Token::And)
+		{
+			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression()));
+			mergeVariables(touchedVariables, !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
+		}
 		else
+		{
+			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression()));
+			mergeVariables(touchedVariables, expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
+		}
 	}
 	else
 		m_errorReporter.warning(
 			_op.location(),
 			"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations"
-					);
+		);
 }
 
 smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _right, IntegerType const& _type)
@@ -1137,17 +1154,17 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio
 	m_interface->addAssertion(newValue(_variable) == _value);
 }
 
-SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+SMTChecker::VariableIndices SMTChecker::visitBranch(ASTNode const* _statement, smt::Expression _condition)
 {
 	return visitBranch(_statement, &_condition);
 }
 
-SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
+SMTChecker::VariableIndices SMTChecker::visitBranch(ASTNode const* _statement, smt::Expression const* _condition)
 {
 	auto indicesBeforeBranch = copyVariableIndices();
 	if (_condition)
 		pushPathCondition(*_condition);
-	_statement.accept(*this);
+	_statement->accept(*this);
 	if (_condition)
 		popPathCondition();
 	auto indicesAfterBranch = copyVariableIndices();
@@ -1456,7 +1473,12 @@ TypePointer SMTChecker::typeWithoutPointer(TypePointer const& _type)
 void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
 {
 	set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end());
-	for (auto const* decl: uniqueVars)
+	mergeVariables(uniqueVars, _condition, _indicesEndTrue, _indicesEndFalse);
+}
+
+void SMTChecker::mergeVariables(set<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
+{
+	for (auto const* decl: _variables)
 	{
 		solAssert(_indicesEndTrue.count(decl) && _indicesEndFalse.count(decl), "");
 		int trueIndex = _indicesEndTrue.at(decl);

libsolidity/formal/SMTChecker.h

@@ -132,8 +132,8 @@ private:
 	/// 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 indices after visiting the branch.
-	VariableIndices visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
-	VariableIndices visitBranch(Statement const& _statement, smt::Expression _condition);
+	VariableIndices visitBranch(ASTNode const* _statement, smt::Expression const* _condition = nullptr);
+	VariableIndices visitBranch(ASTNode const* _statement, smt::Expression _condition);
 
 	/// Check that a condition can be satisfied.
 	void checkCondition(
@@ -199,6 +199,7 @@ private:
 	/// merge the touched variables into after-branch ite variables
 	/// using the branch condition as guard.
 	void mergeVariables(std::vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
+	void mergeVariables(std::set<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
 	/// Tries to create an uninitialized variable and returns true on success.
 	/// This fails if the type is not supported.
 	bool createVariable(VariableDeclaration const& _varDecl);

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() == 0) && (f() == 0);
+		assert(x == 1);
+		assert(!b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() == 0) && (f() == 0);
+		assert(x == 1);
+		assert(b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (227-236): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g(bool a) public returns (bool) {
+		bool b;
+		if (a) {
+			x = 0;
+			b = (f() == 0) && (f() == 0);
+			assert(x == 1);
+			assert(!b);
+		} else {
+			x = 100;
+			b = (f() > 0) && (f() > 0);
+			assert(x == 102);
+			// Should fail.
+			assert(!b);
+		}
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (362-372): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() > 0) && (f() > 0);
+		assert(x == 2);
+		assert(b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() > 0) && (f() > 0);
+		assert(x == 2);
+		assert(!b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (225-235): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol

@@ -6,15 +6,13 @@ contract c {
 		x = x + 1;
 		return x;
 	}
-	function g() public {
+	function g() public returns (bool) {
 		x = 0;
-		assert((f() > 0) || (f() > 0));
-		// This assertion should NOT fail.
-		// It currently does because the SMTChecker does not
-		// handle short-circuiting properly and inlines f() twice.
+		bool b = (f() > 0) || (f() > 0);
 		assert(x == 1);
+		assert(b);
+		return b;
 	}
 }
 // ----
 // Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (344-358): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() > 0) || (f() > 0);
+		assert(x == 1);
+		assert(!b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (225-235): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g(bool a) public returns (bool) {
+		bool b;
+		if (a) {
+			x = 0;
+			b = (f() > 0) || (f() > 0);
+			assert(x == 1);
+			assert(b);
+		} else {
+			x = 100;
+			b = (f() == 0) || (f() > 0);
+			assert(x == 102);
+			// Should fail.
+			assert(!b);
+		}
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (360-370): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() > 1) || (f() > 1);
+		assert(x == 2);
+		assert(b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() > 1) || (f() > 1);
+		assert(x == 2);
+		assert(!b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (225-235): Assertion violation happens here