From 6574c10f2589d868ab7e2846d990807ebd2fd0e7 Mon Sep 17 00:00:00 2001 From: Pawel Gebal Date: Thu, 27 Jul 2023 18:16:35 +0200 Subject: [PATCH] SMTChecker: Visit the condition in for and while loops after loop is unrolled --- Changelog.md | 1 + libsolidity/formal/BMC.cpp | 47 +++++++++++++++---- libsolidity/formal/BMC.h | 2 +- .../loops/do_while_bmc_iterations_7.sol | 19 ++++++++ .../do_while_bmc_iterations_semantics_1.sol | 2 +- .../do_while_bmc_iterations_semantics_2.sol | 9 ++-- .../do_while_bmc_iterations_semantics_3.sol | 8 ++-- .../do_while_bmc_iterations_semantics_4.sol | 4 +- .../loops/for_loop_bmc_iterations_10.sol | 19 ++++++++ .../for_loop_bmc_iterations_semantics_1.sol | 6 +-- .../for_loop_bmc_iterations_semantics_2.sol | 10 ++-- .../for_loop_bmc_iterations_semantics_3.sol | 10 ++-- .../loops/while_bmc_iterations_8.sol | 18 +++++++ .../while_bmc_iterations_semantics_1.sol | 8 ++-- .../while_bmc_iterations_semantics_2.sol | 11 +++-- .../while_bmc_iterations_semantics_3.sol | 10 ++-- .../out_of_bounds/array_2d_4.sol | 2 +- 17 files changed, 142 insertions(+), 44 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_7.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_10.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_8.sol diff --git a/Changelog.md b/Changelog.md index 377b5f9ce..4f74b2dea 100644 --- a/Changelog.md +++ b/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) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index dcaffbdb6..220f6411a 100644 --- a/libsolidity/formal/BMC.cpp +++ b/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 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 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) diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 3abaac1bd..dfd4169e2 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -190,7 +190,7 @@ private: smtutil::CheckResult checkSatisfiable(); //@} - std::tuple mergeVariablesFromLoopCheckpoints(); + smtutil::Expression mergeVariablesFromLoopCheckpoints(); bool isInsideLoop() const; std::unique_ptr m_interface; diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_7.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_7.sol new file mode 100644 index 000000000..81d94e1b9 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_1.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_1.sol index 665681780..4d1112ac0 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_1.sol +++ b/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 } diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_2.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_2.sol index f1e296a00..9db49261c 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_2.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_3.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_3.sol index 70edda38b..e5e03d3d6 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_3.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_4.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_4.sol index bf814ab76..04d197045 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_4.sol +++ b/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 } diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_10.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_10.sol new file mode 100644 index 000000000..5c91d2ce5 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_1.sol index 915c0e690..d3a6c825f 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_1.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_2.sol index 337515c9a..720f621df 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_2.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_3.sol index 5ff9d1778..00cd3a5ce 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_3.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_8.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_8.sol new file mode 100644 index 000000000..b7ad4e2ec --- /dev/null +++ b/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 +// ---- diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_1.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_1.sol index eb497be7c..7de8b8146 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_1.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_2.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_2.sol index 90682c7f7..a50acf4d2 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_2.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_3.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_3.sol index 992ac7f80..6ead58142 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_3.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/array_2d_4.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/array_2d_4.sol index ee7ab8bcc..2a9f39d1a 100644 --- a/test/libsolidity/smtCheckerTests/out_of_bounds/array_2d_4.sol +++ b/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.