Merge pull request #14448 from pgebal/pgebal/fix_for_loop_iterations

SMTChecker fix: Do not unroll loop after it completes

Author: pgebal

Changelog.md

@@ -8,6 +8,7 @@ Compiler Features:
 
 Bugfixes:
  * NatSpec: Fix internal error when requesting userdoc or devdoc for a contract that emits an event defined in a foreign contract or interface.
+ * SMTChecker: Fix encoding error that causes loops to unroll after completion.
 
 
 ### 0.8.21 (2023-07-19)

libsolidity/formal/BMC.cpp

@@ -328,13 +328,13 @@ bool BMC::visit(WhileStatement const& _node)
 				indicesBefore,
 				copyVariableIndices()
 			);
-			loopCondition = expr(_node.condition());
+			loopCondition = loopCondition && expr(_node.condition());
 			broke = broke || brokeInCurrentIteration;
 			m_loopCheckpoints.pop();
 		}
 	}
 	else {
-		smtutil::Expression loopConditionOnPreviousIteration(true);
+		smtutil::Expression loopConditionOnPreviousIterations(true);
 		for (unsigned int i = 0; i < bmcLoopIterations; ++i)
 		{
 			m_loopCheckpoints.emplace();
@@ -361,13 +361,13 @@ bool BMC::visit(WhileStatement const& _node)
 			// breaks in current iterations are handled when traversing loop checkpoints
 			// handles case when the loop condition no longer holds but bmc loop iterations still unrolls the loop
 			mergeVariables(
-				broke || !loopConditionOnPreviousIteration,
+				broke || !loopConditionOnPreviousIterations,
 				indicesBefore,
 				copyVariableIndices()
 			);
 			m_loopCheckpoints.pop();
 			broke = broke || brokeInCurrentIteration;
-			loopConditionOnPreviousIteration = loopCondition;
+			loopConditionOnPreviousIterations = loopConditionOnPreviousIterations && loopCondition;
 		}
 	}
 	if (bmcLoopIterations > 0)
@@ -384,7 +384,7 @@ bool BMC::visit(ForStatement const& _node)
 
 	smtutil::Expression broke(false);
 	smtutil::Expression forCondition(true);
-	smtutil::Expression forConditionOnPreviousIteration(true);
+	smtutil::Expression forConditionOnPreviousIterations(true);
 	unsigned int bmcLoopIterations = m_settings.bmcLoopIterations.value_or(1);
 	for (unsigned int i = 0; i < bmcLoopIterations; ++i)
 	{
@@ -427,13 +427,13 @@ bool BMC::visit(ForStatement const& _node)
 		// breaks in current iterations are handled when traversing loop checkpoints
 		// handles case when the loop condition no longer holds but bmc loop iterations still unrolls the loop
 		mergeVariables(
-			broke || !forConditionOnPreviousIteration,
+			broke || !forConditionOnPreviousIterations,
 			indicesBefore,
 			copyVariableIndices()
 		);
 		m_loopCheckpoints.pop();
 		broke = broke || brokeInCurrentIteration;
-		forConditionOnPreviousIteration = forCondition;
+		forConditionOnPreviousIterations = forConditionOnPreviousIterations && forCondition;
 	}
 	if (bmcLoopIterations > 0)
 		m_context.addAssertion(not(forCondition) || broke);

test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_6.sol

@@ -0,0 +1,26 @@
+contract C
+{
+	uint x;
+	uint y;
+
+	function condition() private returns(bool) {
+		x = (x + 1) % 2;
+		return (x == 1);
+	}
+
+	function f() public {
+		require(x == 0);
+		require(y == 0);
+		do {
+			++y;
+		} while (condition());
+		assert(y == 2);
+	}
+}
+// ====
+// SMTEngine: bmc
+// SMTSolvers: z3
+// BMCLoopIterations: 5
+// ----
+// Warning 2661: (85-90): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_2.sol

@@ -9,12 +9,13 @@ contract C {
 		} while (x < 3 || y == 1);
         // BMC loop iteration setting is just enough to leave the loop
 		assert(x == 3); // should hold
-		assert(y == 1); // should hold
+		assert(y == 1); // should fail, when x == 3 loop is completed
 	}
 }
 // ====
 // SMTEngine: bmc
 // SMTSolvers: z3
 // BMCLoopIterations: 4
 // ----
-// Info 6002: BMC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Warning 4661: (244-258): BMC: Assertion violation happens here.
+// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_3.sol

@@ -9,7 +9,7 @@ contract C {
 		} while (x < 3 || y == 1);
         // BMC loop iteration setting is more than enough to leave the loop
 		assert(x == 3); // should hold
-		assert(y == 1); // should hold
+		assert(y == 0); // should hold
 	}
 }
 // ====

test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_4.sol

@@ -0,0 +1,20 @@
+contract C {
+	function f() public pure {
+		uint x = 0;
+		int y = 0;
+		do {
+            ++x;
+			if (x >= 3)
+				y = 1;
+		} while (x < 3 || y == 1);
+        // BMC loop iteration setting is more than enough to leave the loop
+		assert(x == 3); // should hold
+		assert(y == 1); // should hold
+	}
+}
+// ====
+// SMTEngine: bmc
+// SMTSolvers: z3
+// BMCLoopIterations: 5
+// ----
+// Info 6002: BMC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_9.sol

@@ -0,0 +1,26 @@
+contract C
+{
+	uint x;
+	uint y;
+
+	function condition() private returns(bool) {
+		x = (x + 1) % 2;
+		return (x == 1);
+	}
+
+	function f() public {
+		require(x == 0);
+		require(y == 0);
+		for (; condition();) {
+			++y;
+		}
+		assert(y == 1);
+	}
+}
+// ====
+// SMTEngine: bmc
+// SMTSolvers: z3
+// BMCLoopIterations: 5
+// ----
+// Warning 2661: (85-90): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_6.sol

@@ -0,0 +1,26 @@
+contract C
+{
+	uint x;
+	uint y;
+
+	function condition() private returns(bool) {
+		x = (x + 1) % 2;
+		return (x == 1);
+	}
+
+	function f() public {
+		require(x == 0);
+		require(y == 0);
+		while (condition()) {
+			++y;
+		}
+		assert(y == 1);
+	}
+}
+// ====
+// SMTEngine: bmc
+// SMTSolvers: z3
+// BMCLoopIterations: 5
+// ----
+// Warning 2661: (85-90): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.