Merge pull request #6668 from ethereum/smt_fix_short_circuit

Fix short circuit with assignments

Author: chriseth

libsolidity/formal/SMTChecker.cpp

@@ -1230,17 +1230,16 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
 	{
 		// @TODO check that both of them are not constant
 		_op.leftExpression().accept(*this);
-		auto touchedVars = touchedVariables(_op.leftExpression());
 		if (_op.getOperator() == Token::And)
 		{
 			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression()));
-			mergeVariables(touchedVars, !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
+			mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
 		}
 		else
 		{
 			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression()));
-			mergeVariables(touchedVars, expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
+			mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
 		}
 	}

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_touched.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	bool b;
+	function f() public {
+		if ((b = false) && (b == true)) {}
+		if ((b == false) && (b = true)) {}
+		if ((b = false) && (b = true)) {}
+		if ((b == false) && (b == true)) {}
+		if ((b = true) && b) {}
+	}
+}
+// ----
+// Warning: (84-110): Condition is always false.
+// Warning: (121-147): Condition is always true.
+// Warning: (158-183): Condition is always false.
+// Warning: (194-221): Condition is always false.
+// Warning: (232-247): Condition is always true.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_touched_function.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	bool b;
+	function g(bool _b) internal returns (bool) {
+		b = _b;
+		return b;
+	}
+	function f() public {
+		if (g(false) && (b == true)) {}
+		if ((b == false) && g(true)) {}
+		if (g(false) && g(true)) {}
+		if (g(false) && (b == true)) {}
+		if (g(true) && b) {}
+	}
+}
+// ----
+// Warning: (156-179): Condition is always false.
+// Warning: (190-213): Condition is always true.
+// Warning: (224-243): Condition is always false.
+// Warning: (254-277): Condition is always false.
+// Warning: (288-300): Condition is always true.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_touched.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	bool b;
+	function f() public {
+		if ((b = true) || (b == false)) {}
+		if ((b == true) || (b = false)) {}
+		if ((b = true) || (b = false)) {}
+		if ((b == true) || (b == false)) {}
+		if ((b = false) || b) {}
+	}
+}
+// ----
+// Warning: (84-110): Condition is always true.
+// Warning: (121-147): Condition is always true.
+// Warning: (158-183): Condition is always true.
+// Warning: (194-221): Condition is always true.
+// Warning: (232-248): Condition is always false.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_touched_function.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	bool b;
+	function g(bool _b) internal returns (bool) {
+		b = _b;
+		return b;
+	}
+	function f() public {
+		if (g(true) || (b == false)) {}
+		if ((b == true) || g(false)) {}
+		if (g(true) || g(false)) {}
+		if (g(true) || (b == false)) {}
+		if (g(false) || b) {}
+	}
+}
+// ----
+// Warning: (156-179): Condition is always true.
+// Warning: (190-213): Condition is always true.
+// Warning: (224-243): Condition is always true.
+// Warning: (254-277): Condition is always true.
+// Warning: (288-301): Condition is always false.