[SMTChecker] Loops are unrolled once

libsolidity/formal/SMTChecker.cpp

@@ -136,13 +136,24 @@ bool SMTChecker::visit(IfStatement const& _node)
 	return false;
 }
 
+// Here we consider the execution of two branches:
+// Branch 1 assumes the loop condition to be true and executes the loop once,
+// after resetting touched variables.
+// Branch 2 assumes the loop condition to be false and skips the loop after
+// visiting the condition (it might contain side-effects, they need to be considered)
+// and does not erase knowledge.
+// If the loop is a do-while, condition side-effects are lost since the body,
+// executed once before the condition, might reassign variables.
+// Variables touched by the loop are merged with Branch 2.
 bool SMTChecker::visit(WhileStatement const& _node)
 {
+	auto indicesBeforeLoop = copyVariableIndices();
 	auto touchedVariables = m_variableUsage->touchedVariables(_node);
 	resetVariables(touchedVariables);
+	decltype(indicesBeforeLoop) indicesAfterLoop;
 	if (_node.isDoWhile())
 	{
-		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())
@@ -154,19 +165,31 @@ bool SMTChecker::visit(WhileStatement const& _node)
 		if (isRootFunction())
 			checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
 
-		visitBranch(_node.body(), expr(_node.condition()));
+		indicesAfterLoop = visitBranch(_node.body(), expr(_node.condition()));
 	}
-	m_loopExecutionHappened = true;
-	resetVariables(touchedVariables);
 
+	// We reset the execution to before the loop
+	// and visit the condition in case it's not a do-while.
+	// A do-while's body might have non-precise information
+	// in its first run about variables that are touched.
+	resetVariableIndices(indicesBeforeLoop);
+	if (!_node.isDoWhile())
+		_node.condition().accept(*this);
+
+	mergeVariables(touchedVariables, expr(_node.condition()), indicesAfterLoop, copyVariableIndices());
+
+	m_loopExecutionHappened = true;
 	return false;
 }
 
+// Here we consider the execution of two branches similar to WhileStatement.
 bool SMTChecker::visit(ForStatement const& _node)
 {
 	if (_node.initializationExpression())
 		_node.initializationExpression()->accept(*this);
 
+	auto indicesBeforeLoop = copyVariableIndices();
+
 	// Do not reset the init expression part.
 	auto touchedVariables =
 		m_variableUsage->touchedVariables(_node.body());
@@ -193,13 +216,19 @@ bool SMTChecker::visit(ForStatement const& _node)
 	_node.body().accept(*this);
 	if (_node.loopExpression())
 		_node.loopExpression()->accept(*this);
-
 	m_interface->pop();
 
+	auto indicesAfterLoop = copyVariableIndices();
+	// We reset the execution to before the loop
+	// and visit the condition.
+	resetVariableIndices(indicesBeforeLoop);
+	if (_node.condition())
+		_node.condition()->accept(*this);
+
+	auto forCondition = _node.condition() ? expr(*_node.condition()) : smt::Expression(true);
+	mergeVariables(touchedVariables, forCondition, indicesAfterLoop, copyVariableIndices());
+
 	m_loopExecutionHappened = true;
-
-	resetVariables(touchedVariables);
-
 	return false;
 }
 
@@ -820,6 +849,7 @@ void SMTChecker::checkCondition(
 		loopComment =
 			"\nNote that some information is erased after the execution of loops.\n"
 			"You can re-introduce information using require().";
+
 	switch (result)
 	{
 	case smt::CheckResult::SATISFIABLE:
@@ -838,19 +868,19 @@ void SMTChecker::checkCondition(
 
 			for (auto const& eval: sortedModel)
 				modelMessage << "  " << eval.first << " = " << eval.second << "\n";
-			m_errorReporter.warning(_location, message.str() + loopComment, SecondarySourceLocation().append(modelMessage.str(), SourceLocation()));
+			m_errorReporter.warning(_location, message.str(), SecondarySourceLocation().append(modelMessage.str(), SourceLocation()).append(loopComment, SourceLocation()));
 		}
 		else
 		{
 			message << ".";
-			m_errorReporter.warning(_location, message.str() + loopComment);
+			m_errorReporter.warning(_location, message.str(), SecondarySourceLocation().append(loopComment, SourceLocation()));
 		}
 		break;
 	}
 	case smt::CheckResult::UNSATISFIABLE:
 		break;
 	case smt::CheckResult::UNKNOWN:
-		m_errorReporter.warning(_location, _description + " might happen here." + loopComment);
+		m_errorReporter.warning(_location, _description + " might happen here.", SecondarySourceLocation().append(loopComment, SourceLocation()));
 		break;
 	case smt::CheckResult::CONFLICTING:
 		m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");

test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		do {
+			// Overflows due to resetting x.
+			x = x + 1;
+		} while (x < 10);
+		assert(x < 14);
+	}
+}
+// ----
+// Warning: (150-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (146-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (179-193): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		do {
+			// Overflows due to resetting x.
+			x = x + 1;
+		} while (x < 1000);
+		// The assertion is true but we can't infer so
+		// because x is touched in the loop.
+		assert(x > 0);
+	}
+}
+// ----
+// Warning: (150-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (146-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (269-282): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_1_fail.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		for(uint i = 0; i < 10; ++i) {
+			// Overflows due to resetting x.
+			x = x + 1;
+		}
+		assert(x < 14);
+	}
+}
+// ----
+// Warning: (176-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (172-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (189-203): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		for(uint i = 0; i < 10; ++i) {
+			// Overflows due to resetting x.
+			x = x + 1;
+		}
+		// The assertion is true but x is touched and reset.
+		assert(x > 0);
+	}
+}
+// ----
+// Warning: (176-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (172-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (244-257): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_5.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (167-181): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_6.sol

@@ -5,8 +5,9 @@ contract C {
         for (y = 2; x < 10; ) {
             y = 3;
         }
-        assert(y == 2);
+        // False positive due to resetting y.
+        assert(y < 4);
     }
 }
 // ----
-// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (213-226): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C {
+    function f(uint x) public pure {
+        require(x == 2);
+        for (; x == 2;) {}
+        assert(x == 2);
+    }
+}
+// ----
+// Warning: (122-128): For loop condition is always true.

test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+    function f(uint x) public pure {
+        require(x == 2);
+        uint y;
+        for (; x == 2;) {
+            y = 7;
+        }
+        assert(x == 2);
+    }
+}
+// ----
+// Warning: (138-144): For loop condition is always true.

test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+contract C {
+    function f(uint x) public pure {
+        require(x == 2);
+        uint y;
+        // The loop condition is always true,
+        // but since x is touched in the body
+        // we can't infer that.
+        for (; x == 2;) {
+            x = 2;
+        }
+        // False positive due to resetting x.
+        assert(x == 2);
+    }
+}
+// ----
+// Warning: (115-121): Unused local variable.
+// Warning: (356-370): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C {
+    function f(uint x) public pure {
+        require(x == 2);
+        for (; x > 2;) {}
+        assert(x == 2);
+    }
+}
+// ----
+// Warning: (122-127): For loop condition is always false.

test/libsolidity/smtCheckerTests/loops/while_1.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 100);
+		while (x < 10) {
+			if (b)
+				x = x + 1;
+			else
+				x = 0;
+		}
+		assert(x > 0);
+	}
+}
+// ----
+// Warning: (177-190): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_fail.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		while (x < 10) {
+			x = x + 1;
+		}
+		assert(x < 14);
+	}
+}
+// ----
+// Warning: (139-153): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_2_fail.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x) public pure {
+		x = 2;
+		while (x > 1) {
+			if (x > 10)
+				x = 2;
+			else
+				x = 10;
+		}
+		assert(x == 2);
+	}
+}
+// ----
+// Warning: (158-172): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol

@@ -4,10 +4,10 @@ contract C {
     function f(uint x) public pure {
         x = 2;
         while (x > 1) {
-            x = 2;
+            x = 1;
         }
         assert(x == 2);
     }
 }
 // ----
-// Warning: (194-208): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (194-208): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol

@@ -8,4 +8,4 @@ contract C {
     }
 }
 // ----
-// Warning: (187-201): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (187-201): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol

@@ -8,4 +8,4 @@ contract C {
     }
 }
 // ----
-// Warning: (199-213): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (199-213): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning: (216-230): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (216-230): Assertion violation happens here