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.

Author: tautschnig

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
 

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",

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$

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

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"))
   {

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" \

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)
         {

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()));

src/goto-instrument/unwind.h

@@ -26,6 +26,7 @@ class goto_unwindt
     CONTINUE,
     PARTIAL,
     ASSERT_ASSUME,
+    ASSERT_PARTIAL,
     ASSUME
   };
 

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());
     }