SMTChecker: Visit the condition in for and while loops after loop is unrolled

Changelog.md

@@ -10,6 +10,7 @@ Bugfixes:
  * AST: Fix wrong initial ID for Yul nodes in the AST.
  * 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.
+ * SMTChecker: Fix inconsistency on constant condition checks when ``while`` or ``for`` loops are unrolled before the condition check.
 
 
 ### 0.8.21 (2023-07-19)

libsolidity/formal/BMC.cpp

@@ -313,7 +313,7 @@ bool BMC::visit(WhileStatement const& _node)
 			auto indicesBefore = copyVariableIndices();
 			_node.body().accept(*this);
 
-			auto [continues, brokeInCurrentIteration] =	mergeVariablesFromLoopCheckpoints();
+			auto brokeInCurrentIteration = mergeVariablesFromLoopCheckpoints();
 
 			auto indicesBreak = copyVariableIndices();
 			_node.condition().accept(*this);
@@ -332,6 +332,8 @@ bool BMC::visit(WhileStatement const& _node)
 			broke = broke || brokeInCurrentIteration;
 			m_loopCheckpoints.pop();
 		}
+		if (bmcLoopIterations > 0)
+			m_context.addAssertion(!loopCondition || broke);
 	}
 	else {
 		smtutil::Expression loopConditionOnPreviousIterations(true);
@@ -348,7 +350,7 @@ bool BMC::visit(WhileStatement const& _node)
 			_node.body().accept(*this);
 			popPathCondition();
 
-			auto [continues, brokeInCurrentIteration] =	mergeVariablesFromLoopCheckpoints();
+			auto brokeInCurrentIteration =	mergeVariablesFromLoopCheckpoints();
 
 			// merges indices modified when accepting loop condition that no longer holds
 			mergeVariables(
@@ -369,9 +371,21 @@ bool BMC::visit(WhileStatement const& _node)
 			broke = broke || brokeInCurrentIteration;
 			loopConditionOnPreviousIterations = loopConditionOnPreviousIterations && loopCondition;
 		}
+		if (bmcLoopIterations > 0)
+		{
+			//after loop iterations are done, we check the loop condition last final time
+			auto indices = copyVariableIndices();
+			_node.condition().accept(*this);
+			loopCondition = expr(_node.condition());
+			// asseert that the loop is complete
+			m_context.addAssertion(!loopCondition || broke || !loopConditionOnPreviousIterations);
+			mergeVariables(
+				broke || !loopConditionOnPreviousIterations,
+				indices,
+				copyVariableIndices()
+			);
+		}
 	}
-	if (bmcLoopIterations > 0)
-		m_context.addAssertion(not(loopCondition) || broke);
 	m_loopExecutionHappened = true;
 	return false;
 }
@@ -401,7 +415,7 @@ bool BMC::visit(ForStatement const& _node)
 		pushPathCondition(forCondition);
 		_node.body().accept(*this);
 
-		auto [continues, brokeInCurrentIteration] =	mergeVariablesFromLoopCheckpoints();
+		auto brokeInCurrentIteration =	mergeVariablesFromLoopCheckpoints();
 
 		// accept loop expression if there was no break
 		if (_node.loopExpression())
@@ -436,12 +450,29 @@ bool BMC::visit(ForStatement const& _node)
 		forConditionOnPreviousIterations = forConditionOnPreviousIterations && forCondition;
 	}
 	if (bmcLoopIterations > 0)
-		m_context.addAssertion(not(forCondition) || broke);
+	{
+		//after loop iterations are done, we check the loop condition last final time
+		auto indices = copyVariableIndices();
+		if (_node.condition())
+		{
+			_node.condition()->accept(*this);
+			forCondition = expr(*_node.condition());
+		}
+		// asseert that the loop is complete
+		m_context.addAssertion(!forCondition || broke || !forConditionOnPreviousIterations);
+		mergeVariables(
+			broke || !forConditionOnPreviousIterations,
+			indices,
+			copyVariableIndices()
+		);
+	}
 	m_loopExecutionHappened = true;
 	return false;
 }
 
-std::tuple<smtutil::Expression, smtutil::Expression> BMC::mergeVariablesFromLoopCheckpoints()
+// merges variables based on loop control statements
+// returns expression indicating whether there was a break in current loop unroll iteration
+smtutil::Expression BMC::mergeVariablesFromLoopCheckpoints()
 {
 	smtutil::Expression continues(false);
 	smtutil::Expression brokeInCurrentIteration(false);
@@ -461,7 +492,7 @@ std::tuple<smtutil::Expression, smtutil::Expression> BMC::mergeVariablesFromLoop
 		else if (loopControl.kind == LoopControlKind::Continue)
 			continues = continues || loopControl.pathConditions;
 	}
-	return std::pair(continues, brokeInCurrentIteration);
+	return brokeInCurrentIteration;
 }
 
 bool BMC::visit(TryStatement const& _tryStatement)

libsolidity/formal/BMC.h

@@ -190,7 +190,7 @@ private:
 	smtutil::CheckResult checkSatisfiable();
 	//@}
 
-	std::tuple<smtutil::Expression, smtutil::Expression> mergeVariablesFromLoopCheckpoints();
+	smtutil::Expression mergeVariablesFromLoopCheckpoints();
 	bool isInsideLoop() const;
 
 	std::unique_ptr<smtutil::SolverInterface> m_interface;

test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_7.sol

@@ -0,0 +1,19 @@
+contract C
+{
+	uint256[] y;
+
+	function f() public view {
+		uint256 x = 0;
+		do {
+			++x;
+		} while (x < y.length);
+		require(x != 0);
+	}
+}
+// ====
+// SMTEngine: bmc
+// SMTSolvers: z3
+// BMCLoopIterations: 1
+// ----
+// Warning 6838: (124-130): BMC: Condition is always true.
+// Info 6002: BMC: 1 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_1.sol

@@ -7,7 +7,7 @@ contract C {
 				y = 1;
 			++x;
 		} while (x < 3 || y == 1);
-        // BMC loop iteration setting is not enough to leave the loop
+		// BMC loop iteration setting is not enough to leave the loop
 		assert(x == 0); // should hold - no assumptions on value if didn't complete loop
 		assert(y == 0); // should hold - no assumptions on value if didn't complete loop
 	}

test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_2.sol

@@ -7,9 +7,10 @@ contract C {
 				y = 1;
 			++x;
 		} while (x < 3 || y == 1);
-        // BMC loop iteration setting is just enough to leave the loop
-		assert(x == 3); // should hold
+		// BMC loop iteration setting is just enough to leave the loop
+		assert(x == 3);
 		assert(y == 1); // should fail, when x == 3 loop is completed
+		assert(y == 0);
 	}
 }
 // ====
@@ -17,5 +18,5 @@ contract C {
 // SMTSolvers: z3
 // BMCLoopIterations: 4
 // ----
-// 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.
+// Warning 4661: (223-237): BMC: Assertion violation happens here.
+// 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/do_while_bmc_iterations_semantics_3.sol

@@ -7,9 +7,10 @@ contract C {
 				y = 1;
 			++x;
 		} while (x < 3 || y == 1);
-        // BMC loop iteration setting is more than enough to leave the loop
-		assert(x == 3); // should hold
-		assert(y == 0); // should hold
+		// BMC loop iteration setting is more than enough to leave the loop
+		assert(x == 3);
+		assert(y == 1); // should fail
+		assert(y == 0);
 	}
 }
 // ====
@@ -17,4 +18,5 @@ contract C {
 // SMTSolvers: z3
 // BMCLoopIterations: 5
 // ----
+// Warning 4661: (228-242): BMC: Assertion violation happens here.
 // 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/do_while_bmc_iterations_semantics_4.sol

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

test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_10.sol

@@ -0,0 +1,19 @@
+contract C
+{
+	uint256[] y;
+
+	function f() public view {
+		uint256 x = 0;
+		for (uint i = 0; i < y.length; i++) {
+			x = 1;
+		}
+		// tests that constant condition warning is not reported
+		require(x != 0);
+	}
+}
+// ====
+// SMTEngine: bmc
+// SMTSolvers: z3
+// BMCLoopIterations: 1
+// ----
+// Info 6002: BMC: 1 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_semantics_1.sol

@@ -7,13 +7,13 @@ contract C {
 				y = 1;
 		}
         // BMC loop iteration setting is not enough to leave the loop
-		assert(x == 0); // should hold - no assumptions on value if didn't complete loop
-		assert(y == 0); // should hold - no assumptions on value if didn't complete loop
+		assert(x == 0); // should hold - no assumptions on value if didn't complete the loop
+		assert(y == 0); // should hold - no assumptions on value if didn't complete the loop
 	}
 }
 // ====
 // SMTEngine: bmc
 // SMTSolvers: z3
-// BMCLoopIterations: 3
+// BMCLoopIterations: 2
 // ----
 // 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_semantics_2.sol

@@ -6,14 +6,16 @@ contract C {
 			if (x >= 3)
 				y = 1;
 		}
-        // BMC loop iteration setting is just enough to leave the loop
-		assert(x == 3); // should hold - no assumptions on value if didn't complete loop
-		assert(y == 0); // should hold - no assumptions on value if didn't complete loop
+		// BMC loop iteration setting is just enough to leave the loop
+		assert(x == 3);
+		assert(y == 1); // should fail
+		assert(y == 0);
 	}
 }
 // ====
 // SMTEngine: bmc
 // SMTSolvers: z3
-// BMCLoopIterations: 4
+// BMCLoopIterations: 3
 // ----
+// Warning 4661: (216-230): BMC: Assertion violation happens here.
 // 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_semantics_3.sol

@@ -6,14 +6,16 @@ contract C {
 			if (x >= 3)
 				y = 1;
 		}
-        // BMC loop iteration setting is more than enough to leave the loop
-		assert(x == 3); // should hold - no assumptions on value if didn't complete loop
-		assert(y == 0); // should hold - no assumptions on value if didn't complete loop
+		// BMC loop iteration setting is more than enough to leave the loop
+		assert(x == 3);
+		assert(y == 1); // should fail
+		assert(y == 0);
 	}
 }
 // ====
 // SMTEngine: bmc
 // SMTSolvers: z3
-// BMCLoopIterations: 5
+// BMCLoopIterations: 4
 // ----
+// Warning 4661: (221-235): BMC: Assertion violation happens here.
 // 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/while_bmc_iterations_8.sol

@@ -0,0 +1,18 @@
+contract C
+{
+	uint256[] y;
+
+	function f() public view {
+ 		uint256 x = 0;
+		while (x < y.length) {
+			x = 1;
+		}
+		// tests that constant condition warning is not reported
+		require(x != 0);
+	}
+}
+// ====
+// SMTEngine: bmc
+// SMTSolvers: z3
+// BMCLoopIterations: 1
+// ----

test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_1.sol

@@ -7,14 +7,14 @@ contract C {
 				y = 1;
 			++x;
 		}
-        // BMC loop iteration setting is not enough to leave the loop
-		assert(x == 3);
-		assert(y == 1);
+		// BMC loop iteration setting is not enough to leave the loop
+		assert(x == 0); // should hold - no assumptions on value if didn't complete the loop
+		assert(y == 0); // should hold - no assumptions on value if didn't complete the loop
 	}
 }
 // ====
 // SMTEngine: bmc
 // SMTSolvers: z3
-// BMCLoopIterations: 3
+// BMCLoopIterations: 2
 // ----
 // 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/while_bmc_iterations_semantics_2.sol

@@ -7,15 +7,16 @@ contract C {
 				y = 1;
 			++x;
 		}
-        // BMC loop iteration setting is just enough to leave the loop
-		assert(x == 3); // should hold
+ 		// BMC loop iteration setting is just enough to leave the loop
+		assert(x == 3);
 		assert(y == 1); // should fail
+		assert(y == 0);
 	}
 }
 // ====
 // SMTEngine: bmc
 // SMTSolvers: z3
-// BMCLoopIterations: 4
+// BMCLoopIterations: 3
 // ----
-// Warning 4661: (240-254): 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.
+// Warning 4661: (220-234): BMC: Assertion violation happens here.
+// 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/while_bmc_iterations_semantics_3.sol

@@ -7,14 +7,16 @@ contract C {
 				y = 1;
 			++x;
 		}
-        // BMC loop iteration setting is more than enough to leave the loop
-		assert(x == 3); // should hold
-		assert(y == 0); // should hold
+		// BMC loop iteration setting is more than enough to leave the loop
+		assert(x == 3);
+		assert(y == 1); // should fail
+		assert(y == 0);
 	}
 }
 // ====
 // SMTEngine: bmc
 // SMTSolvers: z3
-// BMCLoopIterations: 5
+// BMCLoopIterations: 4
 // ----
+// Warning 4661: (224-238): BMC: Assertion violation happens here.
 // 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/out_of_bounds/array_2d_4.sol

@@ -24,4 +24,4 @@ contract C {
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
 // Warning 2661: (184-197): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (228-244): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.