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

@@ -161,7 +161,9 @@ to the later assertion, use the option
 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.
+may be spurious, that is, it may not exist in the original program. If
+`--unwinding-assertions` is also used and all unwinding assertions pass,
+then no counterexample involved such a spurious path.
 
 ### Depth-based Unwinding
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -252,14 +252,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

@@ -160,14 +160,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

@@ -184,17 +184,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());
     }

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