From f15b82643193ce05e41c0e602bb8cfbcb140f857 Mon Sep 17 00:00:00 2001 From: Pawel Gebal Date: Thu, 23 Feb 2023 19:22:46 +0100 Subject: [PATCH] Add optional bounds to unroll loops in BMC model checker --- Changelog.md | 1 + libsolidity/formal/BMC.cpp | 259 ++++++++++++------ libsolidity/formal/BMC.h | 22 +- libsolidity/formal/ModelCheckerSettings.h | 2 + libsolidity/formal/SMTEncoder.h | 2 + libsolidity/interface/StandardCompiler.cpp | 12 +- solc/CommandLineParser.cpp | 21 +- .../model_checker_bmc_loop_iterations/args | 1 + .../model_checker_bmc_loop_iterations/err | 11 + .../input.sol | 12 + .../args | 1 + .../err | 1 + .../exit | 1 + .../input.sol | 0 .../args | 1 + .../err | 1 + .../exit | 1 + .../input.sol | 0 .../input.json | 29 ++ .../output.json | 22 ++ .../input.json | 29 ++ .../output.json | 12 + test/libsolidity/SMTCheckerTest.cpp | 3 + test/libsolidity/SMTCheckerTest.h | 2 + .../functions_trivial_condition_for.sol | 8 - .../functions_trivial_condition_while.sol | 8 - ...e_1_false_positives.sol => do_while_1.sol} | 0 .../loops/do_while_bmc_iterations_1.sol | 16 ++ .../loops/do_while_bmc_iterations_2.sol | 20 ++ .../loops/do_while_bmc_iterations_3.sol | 18 ++ .../loops/do_while_bmc_iterations_4.sol | 15 + .../loops/do_while_bmc_iterations_5.sol | 22 ++ ...while_bmc_iterations_assertion_fails_1.sol | 17 ++ ...while_bmc_iterations_assertion_fails_2.sol | 19 ++ ...while_bmc_iterations_assertion_fails_3.sol | 17 ++ .../loops/do_while_bmc_iterations_break_1.sol | 17 ++ .../loops/do_while_bmc_iterations_break_2.sol | 17 ++ .../loops/do_while_bmc_iterations_break_3.sol | 19 ++ .../loops/do_while_bmc_iterations_break_4.sol | 19 ++ .../loops/do_while_bmc_iterations_break_5.sol | 19 ++ .../loops/do_while_bmc_iterations_break_6.sol | 23 ++ .../loops/do_while_bmc_iterations_break_7.sol | 23 ++ .../loops/do_while_bmc_iterations_break_8.sol | 17 ++ ..._while_bmc_iterations_break_continue_1.sol | 21 ++ ..._while_bmc_iterations_break_continue_2.sol | 22 ++ .../do_while_bmc_iterations_continue_1.sol | 19 ++ .../do_while_bmc_iterations_continue_2.sol | 25 ++ .../do_while_bmc_iterations_continue_3.sol | 24 ++ .../do_while_bmc_iterations_continue_4.sol | 25 ++ .../loops/do_while_bmc_iterations_nested.sol | 22 ++ .../do_while_bmc_iterations_nested_break.sol | 24 ++ ...o_while_bmc_iterations_nested_continue.sol | 24 ++ .../do_while_bmc_iterations_semantics_1.sol | 20 ++ .../do_while_bmc_iterations_semantics_2.sol | 20 ++ .../do_while_bmc_iterations_semantics_3.sol | 20 ++ ...do_while_bmc_iterations_shallow_unroll.sol | 19 ++ .../smtCheckerTests/loops/for_1_fail.sol | 19 -- .../loops/for_1_false_positive.sol | 2 +- .../loops/for_loop_bmc_iterations_1.sol | 15 + .../loops/for_loop_bmc_iterations_2.sol | 15 + .../loops/for_loop_bmc_iterations_3.sol | 16 ++ .../loops/for_loop_bmc_iterations_4.sol | 15 + .../loops/for_loop_bmc_iterations_5.sol | 14 + .../loops/for_loop_bmc_iterations_6.sol | 16 ++ .../loops/for_loop_bmc_iterations_7.sol | 23 ++ .../loops/for_loop_bmc_iterations_8.sol | 31 +++ ..._loop_bmc_iterations_assertion_fails_1.sol | 16 ++ ..._loop_bmc_iterations_assertion_fails_2.sol | 19 ++ ..._loop_bmc_iterations_assertion_fails_3.sol | 17 ++ .../loops/for_loop_bmc_iterations_break_1.sol | 19 ++ .../loops/for_loop_bmc_iterations_break_2.sol | 18 ++ .../loops/for_loop_bmc_iterations_break_3.sol | 18 ++ .../loops/for_loop_bmc_iterations_break_4.sol | 18 ++ .../loops/for_loop_bmc_iterations_break_5.sol | 23 ++ .../loops/for_loop_bmc_iterations_break_6.sol | 23 ++ .../loops/for_loop_bmc_iterations_break_7.sol | 17 ++ .../loops/for_loop_bmc_iterations_break_8.sol | 18 ++ .../loops/for_loop_bmc_iterations_break_9.sol | 17 ++ ...r_loop_bmc_iterations_break_continue_1.sol | 22 ++ ...r_loop_bmc_iterations_break_continue_2.sol | 23 ++ ...r_loop_bmc_iterations_break_continue_3.sol | 22 ++ .../for_loop_bmc_iterations_continue_1.sol | 18 ++ .../for_loop_bmc_iterations_continue_2.sol | 23 ++ .../for_loop_bmc_iterations_continue_3.sol | 24 ++ .../for_loop_bmc_iterations_continue_4.sol | 24 ++ .../for_loop_bmc_iterations_continue_5.sol | 17 ++ ...for_loop_bmc_iterations_false_positive.sol | 16 ++ .../loops/for_loop_bmc_iterations_nested.sol | 17 ++ .../for_loop_bmc_iterations_nested_break.sol | 22 ++ ...or_loop_bmc_iterations_nested_continue.sol | 20 ++ .../for_loop_bmc_iterations_semantics_1.sol | 19 ++ .../for_loop_bmc_iterations_semantics_2.sol | 19 ++ .../for_loop_bmc_iterations_semantics_3.sol | 19 ++ ...for_loop_bmc_iterations_shallow_unroll.sol | 17 ++ .../loops/for_loop_trivial_condition_1.sol | 1 - .../loops/for_loop_trivial_condition_2.sol | 1 - .../loops/for_loop_unreachable_1.sol | 13 - .../loops/while_bmc_iterations_1.sol | 18 ++ .../loops/while_bmc_iterations_2.sol | 19 ++ .../loops/while_bmc_iterations_3.sol | 17 ++ .../loops/while_bmc_iterations_4.sol | 15 + .../loops/while_bmc_iterations_5.sol | 15 + .../loops/while_bmc_iterations_7.sol | 22 ++ ...while_bmc_iterations_assertion_fails_1.sol | 17 ++ ...while_bmc_iterations_assertion_fails_2.sol | 18 ++ ...while_bmc_iterations_assertion_fails_3.sol | 17 ++ .../loops/while_bmc_iterations_break_1.sol | 16 ++ .../loops/while_bmc_iterations_break_2.sol | 17 ++ .../loops/while_bmc_iterations_break_3.sol | 19 ++ .../loops/while_bmc_iterations_break_4.sol | 19 ++ .../loops/while_bmc_iterations_break_5.sol | 19 ++ .../loops/while_bmc_iterations_break_6.sol | 23 ++ .../loops/while_bmc_iterations_break_7.sol | 23 ++ .../loops/while_bmc_iterations_break_8.sol | 19 ++ .../loops/while_bmc_iterations_break_9.sol | 18 ++ .../while_bmc_iterations_break_continue_1.sol | 21 ++ .../while_bmc_iterations_break_continue_2.sol | 22 ++ .../loops/while_bmc_iterations_continue_1.sol | 19 ++ .../loops/while_bmc_iterations_continue_2.sol | 24 ++ .../loops/while_bmc_iterations_nested.sol | 22 ++ .../while_bmc_iterations_nested_break.sol | 23 ++ .../while_bmc_iterations_nested_continue.sol | 23 ++ .../while_bmc_iterations_semantics_1.sol | 20 ++ .../while_bmc_iterations_semantics_2.sol | 21 ++ .../while_bmc_iterations_semantics_3.sol | 20 ++ .../while_bmc_iterations_shallow_unroll.sol | 17 ++ .../loops/while_break_direct.sol | 4 +- .../out_of_bounds/array_2d_4.sol | 2 +- .../try_catch/try_inside_while.sol | 1 - test/solc/CommandLineParser.cpp | 4 +- test/tools/fuzzer_common.cpp | 1 + 131 files changed, 2200 insertions(+), 146 deletions(-) create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations/args create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations/err create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations/input.sol create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/args create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/err create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/exit create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/input.sol create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/args create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/err create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/exit create mode 100644 test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/input.sol create mode 100644 test/cmdlineTests/standard_model_checker_bmc_loop_iterations/input.json create mode 100644 test/cmdlineTests/standard_model_checker_bmc_loop_iterations/output.json create mode 100644 test/cmdlineTests/standard_model_checker_bmc_loop_iterations_invalid_arg/input.json create mode 100644 test/cmdlineTests/standard_model_checker_bmc_loop_iterations_invalid_arg/output.json delete mode 100644 test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol delete mode 100644 test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol rename test/libsolidity/smtCheckerTests/loops/{do_while_1_false_positives.sol => do_while_1.sol} (100%) create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_4.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_5.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_4.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_5.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_6.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_7.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_8.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_continue_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_continue_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_4.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_nested.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_nested_break.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_nested_continue.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_shallow_unroll.sol delete mode 100644 test/libsolidity/smtCheckerTests/loops/for_1_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_4.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_5.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_6.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_7.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_8.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_4.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_5.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_6.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_7.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_8.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_9.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_continue_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_continue_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_continue_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_4.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_5.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_false_positive.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_nested.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_nested_break.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_nested_continue.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_shallow_unroll.sol delete mode 100644 test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_4.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_5.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_7.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_4.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_5.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_6.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_7.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_8.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_9.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_continue_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_continue_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_continue_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_continue_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_nested.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_nested_break.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_nested_continue.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_1.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_3.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_shallow_unroll.sol diff --git a/Changelog.md b/Changelog.md index 7624358ee..62806a5e1 100644 --- a/Changelog.md +++ b/Changelog.md @@ -32,6 +32,7 @@ Compiler Features: * NatSpec: Include NatSpec from events that are emitted by a contract but defined outside of it in userdoc and devdoc output. * Optimizer: Re-implement simplified version of ``UnusedAssignEliminator`` and ``UnusedStoreEliminator``. It can correctly remove some unused assignments in deeply nested loops that were ignored by the old version. * Parser: Unary plus is no longer recognized as a unary operator in the AST and triggers an error at the parsing stage (rather than later during the analysis). + * SMTChecker: Add CLI option ``--model-checker-bmc-loop-iterations`` and a JSON option ``settings.modelChecker.bmcLoopIterations`` that specify how many loop iterations the BMC engine should unroll. Note that false negatives are possible when unrolling loops. This is due to the possibility that bmc loop iteration setting is less than actual number of iterations needed to complete a loop. * SMTChecker: Group all messages about unsupported language features in a single warning. The CLI option ``--model-checker-show-unsupported`` and the JSON option ``settings.modelChecker.showUnsupported`` can be enabled to show the full list. * SMTChecker: Properties that are proved safe are now reported explicitly at the end of analysis. By default, only the number of safe properties is shown. The CLI option ``--model-checker-show-proved-safe`` and the JSON option ``settings.modelChecker.showProvedSafe`` can be enabled to show the full list of safe properties. * Standard JSON Interface: Add experimental support for importing ASTs via Standard JSON. diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index b72e8451a..be29000fe 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -18,7 +18,6 @@ #include -#include #include #include @@ -26,6 +25,8 @@ #include #include +#include + #ifdef HAVE_Z3_DLOPEN #include #endif @@ -245,7 +246,7 @@ bool BMC::visit(IfStatement const& _node) // We ignore called functions here because they have // specific input values. - if (isRootFunction()) + if (isRootFunction() && !isInsideLoop()) addVerificationTarget( VerificationTargetType::ConstantCondition, expr(_node.condition()), @@ -280,7 +281,7 @@ bool BMC::visit(Conditional const& _op) m_context.pushSolver(); _op.condition().accept(*this); - if (isRootFunction()) + if (isRootFunction() && !isInsideLoop()) addVerificationTarget( VerificationTargetType::ConstantCondition, expr(_op.condition()), @@ -294,109 +295,172 @@ bool BMC::visit(Conditional const& _op) 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. +// Unrolls while or do-while loop bool BMC::visit(WhileStatement const& _node) { - auto indicesBeforeLoop = copyVariableIndices(); - m_context.resetVariables(touchedVariables(_node)); - decltype(indicesBeforeLoop) indicesAfterLoop; + unsigned int bmcLoopIterations = m_settings.bmcLoopIterations.value_or(1); + smtutil::Expression broke(false); + smtutil::Expression loopCondition(true); if (_node.isDoWhile()) { - indicesAfterLoop = visitBranch(&_node.body()).first; - // TODO the assertions generated in the body should still be active in the condition - _node.condition().accept(*this); - if (isRootFunction()) - addVerificationTarget( - VerificationTargetType::ConstantCondition, - expr(_node.condition()), - &_node.condition() - ); - } - else - { - _node.condition().accept(*this); - if (isRootFunction()) - addVerificationTarget( - VerificationTargetType::ConstantCondition, - expr(_node.condition()), - &_node.condition() + for (unsigned int i = 0; i < bmcLoopIterations; ++i) + { + m_loopCheckpoints.emplace(); + + auto indicesBefore = copyVariableIndices(); + _node.body().accept(*this); + + auto [continues, brokeInCurrentIteration] = mergeVariablesFromLoopCheckpoints(); + + auto indicesBreak = copyVariableIndices(); + _node.condition().accept(*this); + mergeVariables( + !brokeInCurrentIteration, + copyVariableIndices(), + indicesBreak ); - indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition())).first; + mergeVariables( + broke || !loopCondition, + indicesBefore, + copyVariableIndices() + ); + loopCondition = expr(_node.condition()); + broke = broke || brokeInCurrentIteration; + m_loopCheckpoints.pop(); + } } + else { + smtutil::Expression loopConditionOnPreviousIteration(true); + for (unsigned int i = 0; i < bmcLoopIterations; ++i) + { + m_loopCheckpoints.emplace(); + auto indicesBefore = copyVariableIndices(); + _node.condition().accept(*this); + loopCondition = expr(_node.condition()); - // 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); + auto indicesAfterCondition = copyVariableIndices(); - mergeVariables(expr(_node.condition()), indicesAfterLoop, copyVariableIndices()); + pushPathCondition(loopCondition); + _node.body().accept(*this); + popPathCondition(); + auto [continues, brokeInCurrentIteration] = mergeVariablesFromLoopCheckpoints(); + + // merges indices modified when accepting loop condition that no longer holds + mergeVariables( + !loopCondition, + indicesAfterCondition, + copyVariableIndices() + ); + + // handles breaks in previous iterations + // 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, + indicesBefore, + copyVariableIndices() + ); + m_loopCheckpoints.pop(); + broke = broke || brokeInCurrentIteration; + loopConditionOnPreviousIteration = loopCondition; + } + } + if (bmcLoopIterations > 0) + m_context.addAssertion(not(loopCondition) || broke); m_loopExecutionHappened = true; return false; } -// Here we consider the execution of two branches similar to WhileStatement. +// Unrolls for loop bool BMC::visit(ForStatement const& _node) { if (_node.initializationExpression()) _node.initializationExpression()->accept(*this); - auto indicesBeforeLoop = copyVariableIndices(); - - // Do not reset the init expression part. - auto touchedVars = touchedVariables(_node.body()); - if (_node.condition()) - touchedVars += touchedVariables(*_node.condition()); - if (_node.loopExpression()) - touchedVars += touchedVariables(*_node.loopExpression()); - - m_context.resetVariables(touchedVars); - - if (_node.condition()) + smtutil::Expression broke(false); + smtutil::Expression forCondition(true); + smtutil::Expression forConditionOnPreviousIteration(true); + unsigned int bmcLoopIterations = m_settings.bmcLoopIterations.value_or(1); + for (unsigned int i = 0; i < bmcLoopIterations; ++i) { - _node.condition()->accept(*this); - if (isRootFunction()) - addVerificationTarget( - VerificationTargetType::ConstantCondition, - expr(*_node.condition()), - _node.condition() + auto indicesBefore = copyVariableIndices(); + if (_node.condition()) + { + _node.condition()->accept(*this); + // values in loop condition might change during loop iteration + forCondition = expr(*_node.condition()); + } + m_loopCheckpoints.emplace(); + auto indicesAfterCondition = copyVariableIndices(); + + pushPathCondition(forCondition); + _node.body().accept(*this); + + auto [continues, brokeInCurrentIteration] = mergeVariablesFromLoopCheckpoints(); + + // accept loop expression if there was no break + if (_node.loopExpression()) + { + auto indicesBreak = copyVariableIndices(); + _node.loopExpression()->accept(*this); + mergeVariables( + !brokeInCurrentIteration, + copyVariableIndices(), + indicesBreak ); + } + popPathCondition(); + + // merges indices modified when accepting loop condition that does no longer hold + mergeVariables( + !forCondition, + indicesAfterCondition, + copyVariableIndices() + ); + + // handles breaks in previous iterations + // 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, + indicesBefore, + copyVariableIndices() + ); + m_loopCheckpoints.pop(); + broke = broke || brokeInCurrentIteration; + forConditionOnPreviousIteration = forCondition; } - - m_context.pushSolver(); - if (_node.condition()) - m_context.addAssertion(expr(*_node.condition())); - _node.body().accept(*this); - if (_node.loopExpression()) - _node.loopExpression()->accept(*this); - m_context.popSolver(); - - 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()) : smtutil::Expression(true); - mergeVariables(forCondition, indicesAfterLoop, copyVariableIndices()); - + if (bmcLoopIterations > 0) + m_context.addAssertion(not(forCondition) || broke); m_loopExecutionHappened = true; return false; } +std::tuple BMC::mergeVariablesFromLoopCheckpoints() +{ + smtutil::Expression continues(false); + smtutil::Expression brokeInCurrentIteration(false); + for (auto const& loopControl: m_loopCheckpoints.top()) + { + // use SSAs associated with this break statement only if + // loop didn't break or continue earlier in the iteration + // loop condition is included in break path conditions + mergeVariables( + !brokeInCurrentIteration && !continues && loopControl.pathConditions, + loopControl.variableIndices, + copyVariableIndices() + ); + if (loopControl.kind == LoopControlKind::Break) + brokeInCurrentIteration = + brokeInCurrentIteration || loopControl.pathConditions; + else if (loopControl.kind == LoopControlKind::Continue) + continues = continues || loopControl.pathConditions; + } + return std::pair(continues, brokeInCurrentIteration); +} + bool BMC::visit(TryStatement const& _tryStatement) { FunctionCall const* externalCall = dynamic_cast(&_tryStatement.externalCall()); @@ -428,6 +492,28 @@ bool BMC::visit(TryStatement const& _tryStatement) return false; } +bool BMC::visit(Break const&) +{ + LoopControl control = { + LoopControlKind::Break, + currentPathConditions(), + copyVariableIndices() + }; + m_loopCheckpoints.top().emplace_back(control); + return false; +} + +bool BMC::visit(Continue const&) +{ + LoopControl control = { + LoopControlKind::Continue, + currentPathConditions(), + copyVariableIndices() + }; + m_loopCheckpoints.top().emplace_back(control); + return false; +} + void BMC::endVisit(UnaryOperation const& _op) { SMTEncoder::endVisit(_op); @@ -535,7 +621,7 @@ void BMC::visitRequire(FunctionCall const& _funCall) auto const& args = _funCall.arguments(); solAssert(args.size() >= 1, ""); solAssert(args.front()->annotation().type->category() == Type::Category::Bool, ""); - if (isRootFunction()) + if (isRootFunction() && !isInsideLoop()) addVerificationTarget( VerificationTargetType::ConstantCondition, expr(*args.front()), @@ -960,7 +1046,7 @@ void BMC::checkCondition( vector expressionsToEvaluate; vector expressionNames; tie(expressionsToEvaluate, expressionNames) = _modelExpressions; - if (_callStack.size()) + if (!_callStack.empty()) if (_additionalValue) { expressionsToEvaluate.emplace_back(*_additionalValue); @@ -973,8 +1059,9 @@ void BMC::checkCondition( string extraComment = SMTEncoder::extraComment(); if (m_loopExecutionHappened) extraComment += - "\nNote that some information is erased after the execution of loops.\n" - "You can re-introduce information using require()."; + "False negatives are possible when unrolling loops.\n" + "This is due to the possibility that the BMC loop iteration setting is" + " smaller than the actual number of iterations needed to complete a loop."; if (m_externalFunctionCallHappened) extraComment += "\nNote that external function calls are not inlined," @@ -1145,3 +1232,7 @@ void BMC::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& )); } +bool BMC::isInsideLoop() const +{ + return !m_loopCheckpoints.empty(); +} diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 9a8242047..3abaac1bd 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -100,6 +100,8 @@ private: void endVisit(FunctionCall const& _node) override; void endVisit(Return const& _node) override; bool visit(TryStatement const& _node) override; + bool visit(Break const& _node) override; + bool visit(Continue const& _node) override; //@} /// Visitor helpers. @@ -188,6 +190,9 @@ private: smtutil::CheckResult checkSatisfiable(); //@} + std::tuple mergeVariablesFromLoopCheckpoints(); + bool isInsideLoop() const; + std::unique_ptr m_interface; /// Flags used for better warning messages. @@ -204,6 +209,21 @@ private: /// Number of verification conditions that could not be proved. size_t m_unprovedAmt = 0; -}; + enum class LoopControlKind + { + Continue, + Break + }; + + // Current path conditions and SSA indices for break or continue statement + struct LoopControl { + LoopControlKind kind; + smtutil::Expression pathConditions; + VariableIndices variableIndices; + }; + + // Loop control statements for every loop + std::stack> m_loopCheckpoints; +}; } diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h index fafb2cdac..d190116d9 100644 --- a/libsolidity/formal/ModelCheckerSettings.h +++ b/libsolidity/formal/ModelCheckerSettings.h @@ -157,6 +157,7 @@ struct ModelCheckerExtCalls struct ModelCheckerSettings { + std::optional bmcLoopIterations; ModelCheckerContracts contracts = ModelCheckerContracts::Default(); /// Currently division and modulo are replaced by multiplication with slack vars, such that /// a / b <=> a = b * k + m @@ -179,6 +180,7 @@ struct ModelCheckerSettings bool operator==(ModelCheckerSettings const& _other) const noexcept { return + bmcLoopIterations == _other.bmcLoopIterations && contracts == _other.contracts && divModNoSlacks == _other.divModNoSlacks && engine == _other.engine && diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index c16569686..726f16ef6 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -168,7 +168,9 @@ protected: void endVisit(IndexAccess const& _node) override; void endVisit(IndexRangeAccess const& _node) override; bool visit(InlineAssembly const& _node) override; + bool visit(Break const&) override { return false; } void endVisit(Break const&) override {} + bool visit(Continue const&) override { return false; } void endVisit(Continue const&) override {} bool visit(TryCatchClause const&) override { return true; } void endVisit(TryCatchClause const&) override {} diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 972c04ba9..f18c618e9 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -430,7 +430,7 @@ std::optional checkSettingsKeys(Json::Value const& _input) std::optional checkModelCheckerSettingsKeys(Json::Value const& _input) { - static set keys{"contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showProvedSafe", "showUnproved", "showUnsupported", "solvers", "targets", "timeout"}; + static set keys{"bmcLoopIterations", "contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showProvedSafe", "showUnproved", "showUnsupported", "solvers", "targets", "timeout"}; return checkKeys(_input, keys, "modelChecker"); } @@ -1013,6 +1013,16 @@ std::variant StandardCompiler: ret.modelCheckerSettings.engine = *engine; } + if (modelCheckerSettings.isMember("bmcLoopIterations")) + { + if (!ret.modelCheckerSettings.engine.bmc) + return formatFatalError(Error::Type::JSONError, "settings.modelChecker.bmcLoopIterations requires the BMC engine to be enabled."); + if (modelCheckerSettings["bmcLoopIterations"].isUInt()) + ret.modelCheckerSettings.bmcLoopIterations = modelCheckerSettings["bmcLoopIterations"].asUInt(); + else + return formatFatalError(Error::Type::JSONError, "settings.modelChecker.bmcLoopIterations must be an unsigned integer."); + } + if (modelCheckerSettings.isMember("extCalls")) { if (!modelCheckerSettings["extCalls"].isString()) diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index da818411e..aab6b6710 100644 --- a/solc/CommandLineParser.cpp +++ b/solc/CommandLineParser.cpp @@ -76,6 +76,7 @@ static string const g_strModelCheckerShowUnsupported = "model-checker-show-unsup static string const g_strModelCheckerSolvers = "model-checker-solvers"; static string const g_strModelCheckerTargets = "model-checker-targets"; static string const g_strModelCheckerTimeout = "model-checker-timeout"; +static string const g_strModelCheckerBMCLoopIterations = "model-checker-bmc-loop-iterations"; static string const g_strNone = "none"; static string const g_strNoOptimizeYul = "no-optimize-yul"; static string const g_strOptimize = "optimize"; @@ -861,17 +862,23 @@ General Information)").c_str(), ( g_strModelCheckerTargets.c_str(), po::value()->value_name("default,all,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray,outOfBounds")->default_value("default"), - "Select model checker verification targets. " + "Select model checker verification targets." "Multiple targets can be selected at the same time, separated by a comma and no spaces." " By default all targets except underflow and overflow are selected." ) ( g_strModelCheckerTimeout.c_str(), po::value()->value_name("ms"), - "Set model checker timeout per query in milliseconds. " - "The default is a deterministic resource limit. " + "Set model checker timeout per query in milliseconds." + "The default is a deterministic resource limit." "A timeout of 0 means no resource/time restrictions for any query." ) + ( + g_strModelCheckerBMCLoopIterations.c_str(), + po::value(), + "Set loop unrolling depth for BMC engine." + "Default is 1." + ) ; desc.add(smtCheckerOptions); @@ -965,6 +972,7 @@ void CommandLineParser::processArgs() {g_strModelCheckerInvariants, {InputMode::Compiler, InputMode::CompilerWithASTImport}}, {g_strModelCheckerSolvers, {InputMode::Compiler, InputMode::CompilerWithASTImport}}, {g_strModelCheckerTimeout, {InputMode::Compiler, InputMode::CompilerWithASTImport}}, + {g_strModelCheckerBMCLoopIterations, {InputMode::Compiler, InputMode::CompilerWithASTImport}}, {g_strModelCheckerContracts, {InputMode::Compiler, InputMode::CompilerWithASTImport}}, {g_strModelCheckerTargets, {InputMode::Compiler, InputMode::CompilerWithASTImport}} }; @@ -1337,6 +1345,13 @@ void CommandLineParser::processArgs() if (m_args.count(g_strModelCheckerTimeout)) m_options.modelChecker.settings.timeout = m_args[g_strModelCheckerTimeout].as(); + if (m_args.count(g_strModelCheckerBMCLoopIterations)) + { + if (!m_options.modelChecker.settings.engine.bmc) + solThrow(CommandLineValidationError, "BMC loop unrolling requires the BMC engine to be enabled"); + m_options.modelChecker.settings.bmcLoopIterations = m_args[g_strModelCheckerBMCLoopIterations].as(); + } + m_options.metadata.literalSources = (m_args.count(g_strMetadataLiteral) > 0); m_options.modelChecker.initialize = m_args.count(g_strModelCheckerContracts) || diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations/args b/test/cmdlineTests/model_checker_bmc_loop_iterations/args new file mode 100644 index 000000000..3761421e9 --- /dev/null +++ b/test/cmdlineTests/model_checker_bmc_loop_iterations/args @@ -0,0 +1 @@ +--model-checker-engine bmc --model-checker-bmc-loop-iterations 3 \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations/err b/test/cmdlineTests/model_checker_bmc_loop_iterations/err new file mode 100644 index 000000000..cbb2b0f9d --- /dev/null +++ b/test/cmdlineTests/model_checker_bmc_loop_iterations/err @@ -0,0 +1,11 @@ +Warning: BMC: Assertion violation happens here. + --> model_checker_bmc_loop_iterations/input.sol:10:3: + | +10 | assert(x == 3); + | ^^^^^^^^^^^^^^ +Note: Counterexample: + x = 2 + +Note: Callstack: +Note: False negatives are possible when unrolling loops. +This is due to the possibility that the BMC loop iteration setting is smaller than the actual number of iterations needed to complete a loop. diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations/input.sol b/test/cmdlineTests/model_checker_bmc_loop_iterations/input.sol new file mode 100644 index 000000000..3722e46cf --- /dev/null +++ b/test/cmdlineTests/model_checker_bmc_loop_iterations/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C +{ + function f(uint x) public pure { + require(x == 0); + do { + ++x; + } while (x < 2); + assert(x == 3); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/args b/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/args new file mode 100644 index 000000000..32b6eb05b --- /dev/null +++ b/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/args @@ -0,0 +1 @@ +--model-checker-engine bmc --model-checker-bmc-loop-iterations bmc \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/err b/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/err new file mode 100644 index 000000000..0f0fbaf8b --- /dev/null +++ b/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/err @@ -0,0 +1 @@ +the argument ('bmc') for option '--model-checker-bmc-loop-iterations' is invalid \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/exit b/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/exit new file mode 100644 index 000000000..56a6051ca --- /dev/null +++ b/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/exit @@ -0,0 +1 @@ +1 \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/input.sol b/test/cmdlineTests/model_checker_bmc_loop_iterations_invalid_arg/input.sol new file mode 100644 index 000000000..e69de29bb diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/args b/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/args new file mode 100644 index 000000000..aad7e026c --- /dev/null +++ b/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/args @@ -0,0 +1 @@ +--model-checker-engine bmc --model-checker-bmc-loop-iterations \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/err b/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/err new file mode 100644 index 000000000..9b59a4eb8 --- /dev/null +++ b/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/err @@ -0,0 +1 @@ +the argument ('model_checker_bmc_loop_iterations_no_argument/input.sol') for option '--model-checker-bmc-loop-iterations' is invalid diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/exit b/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/exit new file mode 100644 index 000000000..56a6051ca --- /dev/null +++ b/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/exit @@ -0,0 +1 @@ +1 \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/input.sol b/test/cmdlineTests/model_checker_bmc_loop_iterations_no_argument/input.sol new file mode 100644 index 000000000..e69de29bb diff --git a/test/cmdlineTests/standard_model_checker_bmc_loop_iterations/input.json b/test/cmdlineTests/standard_model_checker_bmc_loop_iterations/input.json new file mode 100644 index 000000000..e7d2d09bb --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_bmc_loop_iterations/input.json @@ -0,0 +1,29 @@ +{ + "language": "Solidity", + "sources": + { + "Source": + { + "content": "// SPDX-License-Identifier: GPL-3.0 + pragma solidity >=0.0; + contract C + { + function f(uint x) public pure { + require(x == 0); + do { + ++x; + } while (x < 2); + assert(x == 2); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "bmc", + "bmcLoopIterations": 3 + } + } +} \ No newline at end of file diff --git a/test/cmdlineTests/standard_model_checker_bmc_loop_iterations/output.json b/test/cmdlineTests/standard_model_checker_bmc_loop_iterations/output.json new file mode 100644 index 000000000..139b0825b --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_bmc_loop_iterations/output.json @@ -0,0 +1,22 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "6002", + "formattedMessage": "Info: BMC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them. + +", + "message": "BMC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.", + "severity": "info", + "type": "Info" + } + ], + "sources": + { + "Source": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_bmc_loop_iterations_invalid_arg/input.json b/test/cmdlineTests/standard_model_checker_bmc_loop_iterations_invalid_arg/input.json new file mode 100644 index 000000000..8c5fa65cd --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_bmc_loop_iterations_invalid_arg/input.json @@ -0,0 +1,29 @@ +{ + "language": "Solidity", + "sources": + { + "Source": + { + "content": "// SPDX-License-Identifier: GPL-3.0 + pragma solidity >=0.0; + contract C + { + function f(uint x) public pure { + require(x == 0); + do { + ++x; + } while (x < 2); + assert(x == 2); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "bmc", + "bmcLoopIterations": "bmc" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_bmc_loop_iterations_invalid_arg/output.json b/test/cmdlineTests/standard_model_checker_bmc_loop_iterations_invalid_arg/output.json new file mode 100644 index 000000000..971973d85 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_bmc_loop_iterations_invalid_arg/output.json @@ -0,0 +1,12 @@ +{ + "errors": + [ + { + "component": "general", + "formattedMessage": "settings.modelChecker.bmcLoopIterations must be an unsigned integer.", + "message": "settings.modelChecker.bmcLoopIterations must be an unsigned integer.", + "severity": "error", + "type": "JSONError" + } + ] +} diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp index 949589527..288527e04 100644 --- a/test/libsolidity/SMTCheckerTest.cpp +++ b/test/libsolidity/SMTCheckerTest.cpp @@ -122,6 +122,9 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E m_shouldRun = false; #endif } + + auto const& bmcLoopIterations = m_reader.sizetSetting("BMCLoopIterations", 1); + m_modelCheckerSettings.bmcLoopIterations = std::optional{bmcLoopIterations}; } TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted) diff --git a/test/libsolidity/SMTCheckerTest.h b/test/libsolidity/SMTCheckerTest.h index 54d23c74f..965705f30 100644 --- a/test/libsolidity/SMTCheckerTest.h +++ b/test/libsolidity/SMTCheckerTest.h @@ -55,6 +55,8 @@ protected: Set in m_modelCheckerSettings. SMTSolvers: `all`, `cvc4`, `z3`, `none`, where the default is `all`. Set in m_modelCheckerSettings. + BMCLoopIterations: number of loop iterations for BMC engine, the default is 1. + Set in m_modelCheckerSettings. */ ModelCheckerSettings m_modelCheckerSettings; diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol deleted file mode 100644 index 681d42aef..000000000 --- a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol +++ /dev/null @@ -1,8 +0,0 @@ -contract C -{ - function f(bool x) public pure { require(x); for (;x;) {} } -} -// ==== -// SMTEngine: all -// ---- -// Warning 6838: (65-66): BMC: Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol deleted file mode 100644 index 91bfd981c..000000000 --- a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol +++ /dev/null @@ -1,8 +0,0 @@ -contract C -{ - function f(bool x) public pure { require(x); while (x) {} } -} -// ==== -// SMTEngine: all -// ---- -// Warning 6838: (66-67): BMC: Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1.sol similarity index 100% rename from test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol rename to test/libsolidity/smtCheckerTests/loops/do_while_1.sol diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_1.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_1.sol new file mode 100644 index 000000000..bff046b06 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_1.sol @@ -0,0 +1,16 @@ +contract C +{ + function f(uint x) public pure { + require(x == 0); + do { + ++x; + } while (x < 2); + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_2.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_2.sol new file mode 100644 index 000000000..92cbc1bea --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_2.sol @@ -0,0 +1,20 @@ +contract C +{ + function f() public pure { + uint x; + do { + ++x; + { + ++x; + ++x; + } + } while (x < 3); + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 4 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_3.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_3.sol new file mode 100644 index 000000000..d4a37786c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_3.sol @@ -0,0 +1,18 @@ +contract C +{ + function f() public pure { + uint x; + do { + if (x >= 2) + ++x; + ++x; + } while (x < 3); + assert(x == 4); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_4.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_4.sol new file mode 100644 index 000000000..cce896b70 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_4.sol @@ -0,0 +1,15 @@ +contract C { + function f() public pure { + uint x; + do { + ++x; + } while (true); + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 1 +// ---- +// Info 6002: BMC: 2 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_5.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_5.sol new file mode 100644 index 000000000..6f25a4f5c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_5.sol @@ -0,0 +1,22 @@ +contract C { + uint x; + + function condition() private returns(bool) { + ++x; + return x < 3; + } + + function f() public { + require(x == 0); + do { + } while (condition()); + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 5 +// ---- +// Warning 2661: (77-80): 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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_1.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_1.sol new file mode 100644 index 000000000..54ede91c2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_1.sol @@ -0,0 +1,17 @@ +contract C +{ + function f(uint x) public pure { + require(x == 0); + do { + ++x; + } while (x < 2); + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Warning 4661: (102-116): BMC: Assertion violation happens here. +// 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_assertion_fails_2.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_2.sol new file mode 100644 index 000000000..8c742b749 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_2.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x; + do { + ++x; + break; + } while (x < 3); + assert(x == 0); + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 2 +// ---- +// Warning 5740: (87-92): Unreachable code. +// Warning 4661: (97-111): 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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_3.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_3.sol new file mode 100644 index 000000000..0742c5cdc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_assertion_fails_3.sol @@ -0,0 +1,17 @@ +contract C { + function f() public pure { + uint x; + do { + ++x; + continue; + } while (x < 2); + assert(x == 0); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 2 +// ---- +// Warning 4661: (100-114): BMC: Assertion violation happens here. +// 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_break_1.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_1.sol new file mode 100644 index 000000000..e7bb9d145 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_1.sol @@ -0,0 +1,17 @@ +contract C { + function f() public pure { + uint x; + do { + ++x; + break; + } while (x < 3); + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Warning 5740: (87-92): Unreachable code. +// Info 6002: BMC: 2 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_break_2.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_2.sol new file mode 100644 index 000000000..9dec60544 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_2.sol @@ -0,0 +1,17 @@ +contract C { + function f() public pure { + uint x = 0; + do { + if (x > 0) + break; + ++x; + } while (x < 3); + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_break_3.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_3.sol new file mode 100644 index 000000000..0f1c7d033 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_3.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x = 0; + do { + if (x >= 0) { + ++x; + break; + } + ++x; + } while (x < 3); + assert(x == 1); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_4.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_4.sol new file mode 100644 index 000000000..c2c046809 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_4.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x = 0; + do { + if (x > 0) { + ++x; + break; + } + ++x; + } while (x < 3); + assert(x == 2); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_5.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_5.sol new file mode 100644 index 000000000..4379d4f61 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_5.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x = 0; + do { + ++x; + if (x > 1) { + ++x; + break; + } + } while (x < 3); + assert(x == 3); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_6.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_6.sol new file mode 100644 index 000000000..d0a917fa9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_6.sol @@ -0,0 +1,23 @@ +contract C { + function f() public pure { + uint x; + do { + ++x; + if (x > 0) { + x = 2; + break; + } + if (x > 1) { + x = 3; + break; + } + } while (x < 3); + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_break_7.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_7.sol new file mode 100644 index 000000000..52c3270ba --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_7.sol @@ -0,0 +1,23 @@ +contract C { + function f() public pure { + uint x; + do { + ++x; + if (x > 1) { + x = 3; + break; + } + if (x > 0) { + x = 2; + break; + } + } while (x < 3); + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_break_8.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_8.sol new file mode 100644 index 000000000..c25f98212 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_8.sol @@ -0,0 +1,17 @@ +contract C { + function f() public pure { + uint x; + do { + break; + } while (++x < 2); + // loop condition is not executed after break + assert(x == 0); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Warning 5740: (79-86): Unreachable code. +// Info 6002: BMC: 2 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_break_continue_1.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_continue_1.sol new file mode 100644 index 000000000..53ce958fa --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_continue_1.sol @@ -0,0 +1,21 @@ +contract C { + function f() public pure { + uint x; + do { + if (x > 1) { + break; + } + if (x >= 0) { + x = 10; + continue; + } + } while (x < 3); + assert(x == 10); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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_break_continue_2.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_continue_2.sol new file mode 100644 index 000000000..12d6fff6f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_break_continue_2.sol @@ -0,0 +1,22 @@ +contract C { + function f() public pure { + uint x; + do { + if (x > 1) { + x = 3; + break; + } + if (x >= 0) { + x = 2; + continue; + } + } while (x < 4); + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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_continue_1.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_1.sol new file mode 100644 index 000000000..aa69cb90c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_1.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x = 0; + do { + ++x; + if (x == 3) { + continue; + } + ++x; + } while (x < 3); + assert(x == 3); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_2.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_2.sol new file mode 100644 index 000000000..83826575d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_2.sol @@ -0,0 +1,25 @@ +contract C { + function f() public pure { + uint x = 0; + uint y = 0; + do { + ++x; + if (x == 2) { + ++x; + y = 1; + continue; + } + if (x == 3) { + y = 2; + continue; + } + } while (x < 3); + assert(y == 1); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_3.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_3.sol new file mode 100644 index 000000000..1afe9034e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_3.sol @@ -0,0 +1,24 @@ +contract C { + function f() public pure { + uint x = 0; + uint y = 0; + do { + ++x; + if (x > 0) { + y = 1; + continue; + } + if (x > 0) { + y = 2; + continue; + } + } while (x < 3); + assert(y == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 2 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_continue_4.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_4.sol new file mode 100644 index 000000000..69ad6529c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_continue_4.sol @@ -0,0 +1,25 @@ +contract C +{ + function f(uint x) public pure { + require(x == 0); + uint i; + do { + ++i; + if (i == 2) { + x = 2; + continue; + } + if (i == 1) { + x = 1; + continue; + } + } while (i < 3); + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 2 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_nested.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_nested.sol new file mode 100644 index 000000000..62d1b793d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_nested.sol @@ -0,0 +1,22 @@ +contract C +{ + function f(uint z) public pure { + uint x = 0; + require(z == 0); + do { + uint y = 0; + do { + ++z; + ++y; + } while (y < 2); + ++x; + } while (x < 2); + assert(z == 4); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 4 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_nested_break.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_nested_break.sol new file mode 100644 index 000000000..267e18ec6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_nested_break.sol @@ -0,0 +1,24 @@ +contract C +{ + function f(uint z) public pure { + uint x = 0; + require(z == 0); + do { + uint y = 0; + do { + if (y > 0) + break; + ++z; + ++y; + } while (y < 2); + ++x; + } while (x < 2); + assert(z == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 4 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_nested_continue.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_nested_continue.sol new file mode 100644 index 000000000..42ef9bccc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_nested_continue.sol @@ -0,0 +1,24 @@ +contract C +{ + function f(uint z) public pure { + uint x = 0; + require(z == 0); + do { + uint y = 0; + do { + ++y; + if (y > 0) + continue; + ++z; + } while (y < 2); + ++x; + } while (x < 2); + assert(z == 0); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 4 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 new file mode 100644 index 000000000..665681780 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_1.sol @@ -0,0 +1,20 @@ +contract C { + function f() public pure { + uint x = 0; + int y = 0; + do { + if (x >= 3) + y = 1; + ++x; + } while (x < 3 || 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 + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 1 +// ---- +// 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_2.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_2.sol new file mode 100644 index 000000000..b98bba18a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_2.sol @@ -0,0 +1,20 @@ +contract C { + function f() public pure { + uint x = 0; + int y = 0; + do { + if (x >= 3) + y = 1; + ++x; + } 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 + } +} +// ==== +// 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. 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 new file mode 100644 index 000000000..2a5866e16 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_semantics_3.sol @@ -0,0 +1,20 @@ +contract C { + function f() public pure { + uint x = 0; + int y = 0; + do { + if (x >= 3) + 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 == 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. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_shallow_unroll.sol b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_shallow_unroll.sol new file mode 100644 index 000000000..449d41c67 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_bmc_iterations_shallow_unroll.sol @@ -0,0 +1,19 @@ +contract C { + function f(uint x) public pure { + require(x == 0); + uint y; + do { + ++y; + if (y == 2) + x = 3; + } while (y < 3); + // nothing is reported because loop condition is true after unrolling the loop one time + assert(x == 4); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 1 +// ---- +// Info 6002: BMC: 2 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_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol deleted file mode 100644 index 7d179aa10..000000000 --- a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol +++ /dev/null @@ -1,19 +0,0 @@ -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); - } -} -// ==== -// SMTEngine: all -// SMTSolvers: z3 -// ---- -// Warning 4984: (143-148): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6328: (156-170): CHC: Assertion violation happens here. -// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 2661: (143-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol index 46694d785..0b4ac7e68 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -14,4 +14,4 @@ contract C // ---- // Warning 4984: (106-111): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 2661: (106-111): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. +// 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_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_1.sol new file mode 100644 index 000000000..a352b6e38 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_1.sol @@ -0,0 +1,15 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 2; ++i) + ++x; + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_2.sol new file mode 100644 index 000000000..d460ea770 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_2.sol @@ -0,0 +1,15 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 3; ++i) + x = i; + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_3.sol new file mode 100644 index 000000000..63b434668 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_3.sol @@ -0,0 +1,16 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 3; ++i) + if (i > 1) + x = 10; + assert(x == 10); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_4.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_4.sol new file mode 100644 index 000000000..e3fea509a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_4.sol @@ -0,0 +1,15 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 0; ++i) + ++x; + assert(x == 0); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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_5.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_5.sol new file mode 100644 index 000000000..38437fce2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_5.sol @@ -0,0 +1,14 @@ +contract C +{ + function f() public pure { + uint x; + for (; x < 0; ++x) {} + assert(x == 0); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 1 +// ---- +// Info 6002: BMC: 2 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_6.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_6.sol new file mode 100644 index 000000000..cdbc41485 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_6.sol @@ -0,0 +1,16 @@ +contract C +{ + function f() public pure { + uint x = 0; + for (uint i = 1; i < 3;) { + x = i; + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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_7.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_7.sol new file mode 100644 index 000000000..834529b32 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_7.sol @@ -0,0 +1,23 @@ +contract C +{ + uint x; + + function condition() private returns(bool) { + ++x; + return x < 3; + } + + function f() public { + require(x == 0); + for (; condition();) { + } + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 5 +// ---- +// Warning 2661: (71-74): 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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_8.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_8.sol new file mode 100644 index 000000000..421c965e1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_8.sol @@ -0,0 +1,31 @@ +contract C +{ + uint x; + uint y; + + function condition() private returns(bool) { + ++x; + return x < 3; + } + + function expression() private { + ++y; + } + + function f() public { + require(x == 0); + require(y == 0); + for (; condition(); expression()) { + } + assert(x == 3); + assert(y == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 5 +// ---- +// Warning 2661: (80-83): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 2661: (140-143): 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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_1.sol new file mode 100644 index 000000000..67290785b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_1.sol @@ -0,0 +1,16 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 2; ++i) + ++x; + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Warning 4661: (92-106): 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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_2.sol new file mode 100644 index 000000000..cd1ae918f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_2.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x; + for (uint i = 0; i < 2; ++i) { + ++x; + break; + } + assert(x == 0); + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Warning 5740: (77-80): Unreachable code. +// Warning 4661: (108-122): 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_assertion_fails_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_3.sol new file mode 100644 index 000000000..8e1cb97bc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_assertion_fails_3.sol @@ -0,0 +1,17 @@ +contract C { + function f() public pure { + uint x; + for (uint i = 0; i < 2; ++i) { + ++x; + continue; + } + assert(x == 0); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Warning 4661: (111-125): 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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_1.sol new file mode 100644 index 000000000..26958bf1d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_1.sol @@ -0,0 +1,19 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 3; ++i) { + break; + ++x; + } + assert(x == 0); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Warning 5740: (77-80): Unreachable code. +// Warning 5740: (97-100): Unreachable code. +// 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_break_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_2.sol new file mode 100644 index 000000000..cada2d851 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_2.sol @@ -0,0 +1,18 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 3; ++i) { + ++x; + break; + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Warning 5740: (77-80): Unreachable code. +// 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_break_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_3.sol new file mode 100644 index 000000000..eb947d555 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_3.sol @@ -0,0 +1,18 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 3; ++i) { + if (i > 0) + break; + ++x; + } + assert(x == 1); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_4.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_4.sol new file mode 100644 index 000000000..3d4855abf --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_4.sol @@ -0,0 +1,18 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 3; ++i) { + ++x; + if (i > 0) + break; + } + assert(x == 2); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_5.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_5.sol new file mode 100644 index 000000000..f21255502 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_5.sol @@ -0,0 +1,23 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 3; ++i) { + if (i > 1) { + x = 1; + break; + } + if (i > 1) { + x = 2; + break; + } + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 2 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_break_6.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_6.sol new file mode 100644 index 000000000..401491e90 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_6.sol @@ -0,0 +1,23 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 3; ++i) { + if (i > 1) { + x = 1; + break; + } + if (i >= 1) { + x = 2; + break; + } + } + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 2 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_break_7.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_7.sol new file mode 100644 index 000000000..4bb4ffdf0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_7.sol @@ -0,0 +1,17 @@ +contract C +{ + function f() public pure { + uint x; + for (;;) { + ++x; + break; + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 2 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_break_8.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_8.sol new file mode 100644 index 000000000..a88a031e7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_8.sol @@ -0,0 +1,18 @@ +contract C +{ + function f() public pure { + uint x; + for (;;) { + break; + ++x; + } + assert(x == 0); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Warning 5740: (78-81): Unreachable code. +// Info 6002: BMC: 2 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_break_9.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_9.sol new file mode 100644 index 000000000..4ce3d9268 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_9.sol @@ -0,0 +1,17 @@ +contract C +{ + function f() public pure { + uint x; + for (;x < 2;) { + ++x; + break; + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_break_continue_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_continue_1.sol new file mode 100644 index 000000000..b999f9cf6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_continue_1.sol @@ -0,0 +1,22 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 3; ++i) { + if (i > 1) { + break; + } + if (i >= 0) { + x = 10; + continue; + } + } + assert(x == 10); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_break_continue_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_continue_2.sol new file mode 100644 index 000000000..0da0f5d99 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_continue_2.sol @@ -0,0 +1,23 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 2; ++i) { + if (i > 0) { + x = 1; + break; + } + if (i >= 0) { + x = 2; + continue; + } + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 2 +// ---- +// Info 6002: BMC: 2 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_break_continue_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_continue_3.sol new file mode 100644 index 000000000..9f762bb43 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_break_continue_3.sol @@ -0,0 +1,22 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 3; ++i) { + if (i > 0) { + x = 1; + break; + } else { + x = 2; + continue; + } + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_continue_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_1.sol new file mode 100644 index 000000000..44983ecdd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_1.sol @@ -0,0 +1,18 @@ +contract C +{ + function f(uint x) public pure { + require(x == 0); + for (uint i = 0; i < 3; ++i) { + if (i > 1) + continue; + ++x; + } + assert(x == 2); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_2.sol new file mode 100644 index 000000000..2c7fc1236 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_2.sol @@ -0,0 +1,23 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 2; ++i) { + if (i == 1) { + x = 1; + continue; + } + if (i == 0) { + x = 2; + continue; + } + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 2 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_continue_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_3.sol new file mode 100644 index 000000000..b74709e48 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_3.sol @@ -0,0 +1,24 @@ +contract C +{ + function f(uint x) public pure { + require(x == 0); + for (uint i = 0; i < 3; ++i) { + if (x > 1) { + x = 10; + continue; + } + if (x > 0) { + x = 11; + continue; + } + ++x; + } + assert(x == 10); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_4.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_4.sol new file mode 100644 index 000000000..246aa74c9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_4.sol @@ -0,0 +1,24 @@ +contract C +{ + function f() public pure { + uint x; + for (; x < 2; ++x) { + if (x > 1) { + x = 10; + continue; + } + if (x > 0) { + x = 11; + continue; + } + } + // x > 0 branch triggers x = 11 and continue triggers ++x loop expression + assert(x == 12); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 2 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_continue_5.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_5.sol new file mode 100644 index 000000000..270d8d4df --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_continue_5.sol @@ -0,0 +1,17 @@ +contract C +{ + function f() public pure { + uint x; + for (; x < 2; ++x) { + continue; + } + // loop expression is executed after continue + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 2 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_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_false_positive.sol new file mode 100644 index 000000000..20071a64a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_false_positive.sol @@ -0,0 +1,16 @@ +contract C +{ + function f() public pure { + uint x = 0; + for (;;) { + x = 1; + } + assert(x == 1000); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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_nested.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_nested.sol new file mode 100644 index 000000000..d63e2ca5c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_nested.sol @@ -0,0 +1,17 @@ +contract C +{ + function f() public pure { + uint x; + for (uint i = 0; i < 2; ++i) { + for (uint j = 0; j < 2; ++j) + ++x; + } + assert(x == 4); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 4 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_nested_break.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_nested_break.sol new file mode 100644 index 000000000..c302decaf --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_nested_break.sol @@ -0,0 +1,22 @@ +contract C +{ + function f(uint x) public pure { + require(x == 0); + for (uint i = 0; i < 2; ++i) { + for (uint j = 0; j < 2; ++j) { + x = x + 1; + break; + } + break; + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Warning 5740: (92-95): Unreachable code. +// Warning 5740: (126-129): Unreachable code. +// Info 6002: BMC: 4 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_nested_continue.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_nested_continue.sol new file mode 100644 index 000000000..8c07d096a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_nested_continue.sol @@ -0,0 +1,20 @@ +contract C +{ + function f() public pure { + uint x = 0; + for (uint i = 0; i < 2; ++i) { + for (uint j = 0; j < 2; ++j) { + if (i > 0) + continue; + ++x; + } + } + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 4 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 new file mode 100644 index 000000000..915c0e690 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_1.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x = 0; + int y = 0; + for (; x < 3 || y == 1; ++x) { + if (x >= 3) + 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 + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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 new file mode 100644 index 000000000..337515c9a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_2.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x = 0; + int y = 0; + for (; x < 3 || y == 1; ++x) { + 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 + } +} +// ==== +// 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. 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 new file mode 100644 index 000000000..5ff9d1778 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_semantics_3.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x = 0; + int y = 0; + for (; x < 3 || y == 1; ++x) { + 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 + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_shallow_unroll.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_shallow_unroll.sol new file mode 100644 index 000000000..8bfecdfa5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_bmc_iterations_shallow_unroll.sol @@ -0,0 +1,17 @@ +contract C +{ + function f() public pure { + uint x = 0; + for (uint i = 0; i < 2; ++i) { + ++x; + } + // nothing is reported because loop condition is still true after BMCLoopIterations + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 1 +// ---- +// 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_trivial_condition_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol index d667a55c8..36af4f9b4 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol @@ -10,4 +10,3 @@ contract C { // SMTSolvers: z3 // ---- // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 6838: (90-96): BMC: Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol index 65caca982..0847066a0 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol @@ -13,4 +13,3 @@ contract C { // SMTSolvers: z3 // ---- // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 6838: (106-112): BMC: Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol deleted file mode 100644 index 4fdaa6bcf..000000000 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol +++ /dev/null @@ -1,13 +0,0 @@ -contract C { - function f(uint x) public pure { - require(x == 2); - for (; x > 2;) {} - assert(x == 2); - } -} -// ==== -// SMTEngine: all -// SMTSolvers: z3 -// ---- -// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 6838: (90-95): BMC: Condition is always false. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_1.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_1.sol new file mode 100644 index 000000000..11a4e7587 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_1.sol @@ -0,0 +1,18 @@ +contract C { + function f(uint x) public pure { + require(x == 0); + uint y; + while (y < 3) { + ++y; + if (y == 2) + x = 3; + } + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 2 +// ---- +// Info 6002: BMC: 2 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_2.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_2.sol new file mode 100644 index 000000000..075e342ea --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_2.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + ++x; + { + ++x; + ++x; + } + } + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 4 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_3.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_3.sol new file mode 100644 index 000000000..2596af24f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_3.sol @@ -0,0 +1,17 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + if (x >= 2) + ++x; + ++x; + } + assert(x == 4); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_4.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_4.sol new file mode 100644 index 000000000..8bfbe32d1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_4.sol @@ -0,0 +1,15 @@ +contract C { + function f(uint x) public pure { + x = 0; + while (x < 1) { + ++x; + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_5.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_5.sol new file mode 100644 index 000000000..f3166cee8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_5.sol @@ -0,0 +1,15 @@ +contract C { + function f() public pure { + uint x; + while (true) { + ++x; + } + assert(x == 1000); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 1 +// ---- +// Info 6002: BMC: 2 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_7.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_7.sol new file mode 100644 index 000000000..3f6a5b4bf --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_7.sol @@ -0,0 +1,22 @@ +contract C { + uint x; + + function condition() private returns(bool) { + ++x; + return x < 3; + } + + function f() public { + require(x == 0); + while (condition()) { + } + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 5 +// ---- +// Warning 2661: (77-80): 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. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_1.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_1.sol new file mode 100644 index 000000000..a43c7489e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_1.sol @@ -0,0 +1,17 @@ +contract C +{ + function f(uint x) public pure { + require(x == 0); + while (x < 2) { + ++x; + } + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Warning 4661: (98-112): BMC: Assertion violation happens here. +// 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/while_bmc_iterations_assertion_fails_2.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_2.sol new file mode 100644 index 000000000..c16f755b6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_2.sol @@ -0,0 +1,18 @@ +contract C { + function f() public pure { + uint x; + while (x < 2) { + ++x; + break; + } + assert(x == 0); + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 2 +// ---- +// Warning 4661: (93-107): 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. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_3.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_3.sol new file mode 100644 index 000000000..acaf4f9a3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_assertion_fails_3.sol @@ -0,0 +1,17 @@ +contract C { + function f() public pure { + uint x; + while (x < 2) { + ++x; + continue; + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Warning 4661: (96-110): BMC: Assertion violation happens here. +// 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/while_bmc_iterations_break_1.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_1.sol new file mode 100644 index 000000000..c8b45bac0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_1.sol @@ -0,0 +1,16 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + ++x; + break; + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_break_2.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_2.sol new file mode 100644 index 000000000..c4a8c2f39 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_2.sol @@ -0,0 +1,17 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + if (x > 0) + break; + ++x; + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_break_3.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_3.sol new file mode 100644 index 000000000..c089b906b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_3.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + if (x > 0) { + ++x; + break; + } + ++x; + } + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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_break_4.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_4.sol new file mode 100644 index 000000000..d1939871b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_4.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + ++x; + if (x > 0) { + ++x; + break; + } + } + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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_break_5.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_5.sol new file mode 100644 index 000000000..f7ba610a6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_5.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + ++x; + if (x > 1) { + ++x; + break; + } + } + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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_break_6.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_6.sol new file mode 100644 index 000000000..0546e48c0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_6.sol @@ -0,0 +1,23 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + ++x; + if (x > 0) { + x = 2; + break; + } + if (x > 1) { + x = 3; + break; + } + } + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_break_7.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_7.sol new file mode 100644 index 000000000..8e4d3b626 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_7.sol @@ -0,0 +1,23 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + ++x; + if (x > 1) { + x = 3; + break; + } + if (x > 0) { + x = 2; + break; + } + } + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 2 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_break_8.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_8.sol new file mode 100644 index 000000000..be6b04bb2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_8.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x = 0; + while (x < 3) { + if (x >= 0) { + ++x; + break; + } + ++x; + } + assert(x == 1); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_9.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_9.sol new file mode 100644 index 000000000..caaa4f570 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_9.sol @@ -0,0 +1,18 @@ +contract C { + function f() public pure { + uint x = 0; + while (x < 3) { + ++x; + break; + ++x; + } + assert(x == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Warning 5740: (94-97): Unreachable code. +// 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_break_continue_1.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_continue_1.sol new file mode 100644 index 000000000..bb9554523 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_continue_1.sol @@ -0,0 +1,21 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + if (x > 1) { + break; + } + if (x >= 0) { + x = 10; + continue; + } + } + assert(x == 10); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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/while_bmc_iterations_break_continue_2.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_continue_2.sol new file mode 100644 index 000000000..b65404e22 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_break_continue_2.sol @@ -0,0 +1,22 @@ +contract C { + function f() public pure { + uint x; + while (x < 3) { + if (x > 1) { + x = 3; + break; + } + if (x >= 0) { + x = 2; + continue; + } + } + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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/while_bmc_iterations_continue_1.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_continue_1.sol new file mode 100644 index 000000000..e17fa3037 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_continue_1.sol @@ -0,0 +1,19 @@ +contract C { + function f() public pure { + uint x; + uint i; + while (i < 3) { + ++i; + if (i > 1) + continue; + ++x; + } + assert(x == 1); + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_continue_2.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_continue_2.sol new file mode 100644 index 000000000..3670f8dac --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_continue_2.sol @@ -0,0 +1,24 @@ +contract C { + function f(uint x) public pure { + require(x == 0); + uint i; + while (i < 3) { + ++i; + if (i == 2) { + x = 2; + continue; + } + if (i == 1) { + x = 1; + continue; + } + } + assert(x == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 2 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_nested.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_nested.sol new file mode 100644 index 000000000..887ce60f7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_nested.sol @@ -0,0 +1,22 @@ +contract C { + function f(uint z) public pure { + uint x = 0; + require(z == 0); + while (x < 2) { + uint y = 0; + while (y < 2) { + ++z; + ++y; + } + ++x; + } + assert(z == 4); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 4 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_nested_break.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_nested_break.sol new file mode 100644 index 000000000..170c5a3c3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_nested_break.sol @@ -0,0 +1,23 @@ +contract C { + function f(uint z) public pure { + uint x = 0; + require(z == 0); + while (x < 2) { + uint y = 0; + while (y < 2) { + if (y > 0) + break; + ++z; + ++y; + } + ++x; + } + assert(z == 2); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// Info 6002: BMC: 4 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_nested_continue.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_nested_continue.sol new file mode 100644 index 000000000..66ad2081b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_nested_continue.sol @@ -0,0 +1,23 @@ +contract C { + function f() public pure { + uint x; + uint i; + while (i < 3) { + ++i; + uint j; + while (j < 3) { + ++j; + if (i > 1) + continue; + ++x; + } + } + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// Info 6002: BMC: 4 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_1.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_1.sol new file mode 100644 index 000000000..eb497be7c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_1.sol @@ -0,0 +1,20 @@ +contract C { + function f() public pure { + uint x = 0; + int y = 0; + while (x < 3 || y == 1) { + if (x >= 3) + y = 1; + ++x; + } + // BMC loop iteration setting is not enough to leave the loop + assert(x == 3); + assert(y == 1); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 3 +// ---- +// 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 new file mode 100644 index 000000000..90682c7f7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_2.sol @@ -0,0 +1,21 @@ +contract C { + function f() public pure { + uint x = 0; + int y = 0; + while (x < 3 || y == 1) { + if (x >= 3) + y = 1; + ++x; + } + // BMC loop iteration setting is just enough to leave the loop + assert(x == 3); // should hold + assert(y == 1); // should fail + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 4 +// ---- +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_3.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_3.sol new file mode 100644 index 000000000..992ac7f80 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_semantics_3.sol @@ -0,0 +1,20 @@ +contract C { + function f() public pure { + uint x = 0; + int y = 0; + while (x < 3 || y == 1) { + if (x >= 3) + 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 + } +} +// ==== +// 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. diff --git a/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_shallow_unroll.sol b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_shallow_unroll.sol new file mode 100644 index 000000000..3134e35c4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_shallow_unroll.sol @@ -0,0 +1,17 @@ +contract C { + function f() public pure { + uint x = 0; + while (x < 5) { + x = x + 1; + } + // nothing is reported because loop condition is true after unrolling the loop one time + assert(x == 5); + assert(x == 3); + } +} +// ==== +// SMTEngine: bmc +// SMTSolvers: z3 +// BMCLoopIterations: 1 +// ---- +// 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_break_direct.sol b/test/libsolidity/smtCheckerTests/loops/while_break_direct.sol index 783a2f268..4a6245b0f 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_break_direct.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_break_direct.sol @@ -1,5 +1,4 @@ -contract C -{ +contract C { function f(uint x) public pure { x = 0; while (x < 10) @@ -12,4 +11,3 @@ contract C // SMTSolvers: z3 // ---- // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 6838: (65-71): BMC: Condition is always true. 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 2a9f39d1a..ee7ab8bcc 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: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol b/test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol index 8d54f103f..63976d59f 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol @@ -11,4 +11,3 @@ contract C { // SMTEngine: all // ---- // Warning 6321: (43-47): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6838: (59-63): BMC: Condition is always true. diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index 1b5d8da49..30a8b2830 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -142,6 +142,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--optimize", "--optimize-runs=1000", "--yul-optimizations=agf", + "--model-checker-bmc-loop-iterations=2", "--model-checker-contracts=contract1.yul:A,contract2.yul:B", "--model-checker-div-mod-no-slacks", "--model-checker-engine=bmc", @@ -152,7 +153,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--model-checker-show-unsupported", "--model-checker-solvers=z3,smtlib2", "--model-checker-targets=underflow,divByZero", - "--model-checker-timeout=5", + "--model-checker-timeout=5" }; if (inputMode == InputMode::CompilerWithASTImport) @@ -210,6 +211,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) expectedOptions.modelChecker.initialize = true; expectedOptions.modelChecker.settings = { + 2, {{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}}, true, {true, false}, diff --git a/test/tools/fuzzer_common.cpp b/test/tools/fuzzer_common.cpp index 60b871cf7..531fc3c17 100644 --- a/test/tools/fuzzer_common.cpp +++ b/test/tools/fuzzer_common.cpp @@ -105,6 +105,7 @@ void FuzzerUtil::testCompiler( { forceSMT(_input); compiler.setModelCheckerSettings({ + /*bmcLoopIterations*/1, frontend::ModelCheckerContracts::Default(), /*divModWithSlacks*/true, frontend::ModelCheckerEngine::All(),