From 836f04b86acb104f31bf5ccbdb7d96a6de2d4309 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 2 Feb 2022 12:44:29 +0000 Subject: [PATCH] Unwinding options --unwinding-assertions and --partial-loops do not conflict By default, bounded loop unwinding will yield an assumption to ensure that all counterexamples are genuine. Option --unwinding-assertions requests that an additional assertion be generated, which will furthermore ensure that successful verification does not constitute spurious proof. Option --partial-loops disables generating the unwinding assumption. Therefore, --unwinding-assertions and --partial-loops each control (not) generating one instruction, but there is no overlap in the instructions that they are (not) generating. It is, thus, safe to use these options together. --- doc/cprover-manual/cbmc-unwinding.md | 3 +++ jbmc/src/jbmc/jbmc_parse_options.cpp | 8 ------- .../cbmc-concurrency/recursion1/test.desc | 2 +- .../unwind-assert2/partial.desc | 10 ++++++++ src/cbmc/cbmc_parse_options.cpp | 8 ------- src/goto-checker/bmc_util.h | 2 +- .../goto_instrument_parse_options.cpp | 19 +++++++++++---- src/goto-instrument/unwind.cpp | 5 +++- src/goto-instrument/unwind.h | 1 + src/goto-symex/symex_function_call.cpp | 11 +++------ src/goto-symex/symex_goto.cpp | 24 +++++++------------ 11 files changed, 46 insertions(+), 47 deletions(-) create mode 100644 regression/goto-instrument/unwind-assert2/partial.desc diff --git a/doc/cprover-manual/cbmc-unwinding.md b/doc/cprover-manual/cbmc-unwinding.md index 52ad1d6e536..76756f31980 100644 --- a/doc/cprover-manual/cbmc-unwinding.md +++ b/doc/cprover-manual/cbmc-unwinding.md @@ -162,6 +162,9 @@ This option will allow paths that execute loops only partially, enabling a counterexample for the assertion above even for small unwinding bounds. The disadvantage of using this option is that the resulting path may be spurious, that is, it may not exist in the original program. +If `--unwinding-assertions` is also used, and the particular counterexample +trace does not include a report of a violated unwinding assertion, then that +counterexample is not impacted by insufficient loop unwinding. ### Depth-based Unwinding diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index f4e40d5812a..842891608cc 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -241,14 +241,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) "partial-loops", cmdline.isset("partial-loops")); - if(options.get_bool_option("partial-loops") && - options.get_bool_option("unwinding-assertions")) - { - log.error() << "--partial-loops and --unwinding-assertions " - << "must not be given together" << messaget::eom; - exit(1); // should contemplate EX_USAGE from sysexits.h - } - // remove unused equations options.set_option( "slice-formula", diff --git a/regression/cbmc-concurrency/recursion1/test.desc b/regression/cbmc-concurrency/recursion1/test.desc index 1d5f74efc45..52c9db329a9 100644 --- a/regression/cbmc-concurrency/recursion1/test.desc +++ b/regression/cbmc-concurrency/recursion1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 1 --partial-loops --depth 100 +--unwind 1 --partial-loops --unwinding-assertions --depth 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/goto-instrument/unwind-assert2/partial.desc b/regression/goto-instrument/unwind-assert2/partial.desc new file mode 100644 index 00000000000..b8267ab082b --- /dev/null +++ b/regression/goto-instrument/unwind-assert2/partial.desc @@ -0,0 +1,10 @@ +CORE +main.c +--unwind 9 --unwinding-assertions --partial-loops +^\[main.assertion.1\] line 6 fails when fully unwinding the loop: FAILURE$ +^\*\* 2 of 2 failed +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b9a4d5edaae..4062028b6ef 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -159,14 +159,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("no-array-field-sensitivity", true); } - if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions")) - { - log.error() - << "--partial-loops and --unwinding-assertions must not be given " - << "together" << messaget::eom; - exit(CPROVER_EXIT_USAGE_ERROR); - } - if(cmdline.isset("reachability-slice") && cmdline.isset("reachability-slice-fb")) { diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index c6ee131fefe..c2f34a5686d 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -234,7 +234,7 @@ void run_property_decider( " --show-vcc show the verification conditions\n" \ " --slice-formula remove assignments unrelated to property\n" \ " --unwinding-assertions generate unwinding assertions (cannot be\n" \ - " used with --cover or --partial-loops)\n" \ + " used with --cover)\n" \ " --partial-loops permit paths with partial loops\n" \ " --no-self-loops-to-assumptions\n" \ " do not simplify while(1){} to assume(0)\n" \ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 8c17f1da60e..abd4808a8ff 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -182,17 +182,26 @@ int goto_instrument_parse_optionst::doit() bool unwinding_assertions=cmdline.isset("unwinding-assertions"); bool partial_loops=cmdline.isset("partial-loops"); bool continue_as_loops=cmdline.isset("continue-as-loops"); - - if(unwinding_assertions+partial_loops+continue_as_loops>1) - throw "more than one of --unwinding-assertions,--partial-loops," - "--continue-as-loops selected"; + if(continue_as_loops) + { + if(unwinding_assertions) + { + throw "unwinding assertions cannot be used with " + "--continue-as-loops"; + } + else if(partial_loops) + throw "partial loops cannot be used with --continue-as-loops"; + } goto_unwindt::unwind_strategyt unwind_strategy= goto_unwindt::unwind_strategyt::ASSUME; if(unwinding_assertions) { - unwind_strategy = goto_unwindt::unwind_strategyt::ASSERT_ASSUME; + if(partial_loops) + unwind_strategy = goto_unwindt::unwind_strategyt::ASSERT_PARTIAL; + else + unwind_strategy = goto_unwindt::unwind_strategyt::ASSERT_ASSUME; } else if(partial_loops) { diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index dcfca5417d6..35add96a40f 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -130,6 +130,7 @@ void goto_unwindt::unwind( { PRECONDITION( unwind_strategy == unwind_strategyt::ASSERT_ASSUME || + unwind_strategy == unwind_strategyt::ASSERT_PARTIAL || unwind_strategy == unwind_strategyt::ASSUME); goto_programt::const_targett t=loop_exit; @@ -148,7 +149,9 @@ void goto_unwindt::unwind( exit_cond = loop_head->get_condition(); } - if(unwind_strategy == unwind_strategyt::ASSERT_ASSUME) + if( + unwind_strategy == unwind_strategyt::ASSERT_ASSUME || + unwind_strategy == unwind_strategyt::ASSERT_PARTIAL) { goto_programt::targett assertion = rest_program.add( goto_programt::make_assertion(exit_cond, loop_head->source_location())); diff --git a/src/goto-instrument/unwind.h b/src/goto-instrument/unwind.h index 812d73c0b54..bd8aad59509 100644 --- a/src/goto-instrument/unwind.h +++ b/src/goto-instrument/unwind.h @@ -26,6 +26,7 @@ class goto_unwindt CONTINUE, PARTIAL, ASSERT_ASSUME, + ASSERT_PARTIAL, ASSUME }; diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index da047c50625..096fe555ee4 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -245,15 +245,10 @@ void goto_symext::symex_function_call_post_clean( // see if it's too much if(stop_recursing) { - if(symex_config.partial_loops) + if(symex_config.unwinding_assertions) + vcc(false_exprt(), "recursion unwinding assertion", state); + if(!symex_config.partial_loops) { - // it's ok, ignore - } - else - { - if(symex_config.unwinding_assertions) - vcc(false_exprt(), "recursion unwinding assertion", state); - // Rule out this path: symex_assume_l2(state, false_exprt()); } diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index d4485b6a89d..0ac08cd361a 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -932,25 +932,19 @@ void goto_symext::loop_bound_exceeded( else negated_cond=not_exprt(guard); - if(!symex_config.partial_loops) + if(symex_config.unwinding_assertions) { - if(symex_config.unwinding_assertions) - { - // Generate VCC for unwinding assertion. - vcc( - negated_cond, - "unwinding assertion loop " + std::to_string(loop_number), - state); - } + // Generate VCC for unwinding assertion. + vcc( + negated_cond, + "unwinding assertion loop " + std::to_string(loop_number), + state); + } + if(!symex_config.partial_loops) + { // generate unwinding assumption, unless we permit partial loops symex_assume_l2(state, negated_cond); - - if(symex_config.unwinding_assertions) - { - // add to state guard to prevent further assignments - state.guard.add(negated_cond); - } } }