Merge pull request #6644 from tautschnig/feature/partial-loops

Unwinding options --unwinding-assertions and --partial-loops do not conflict

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

@@ -238,14 +238,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());
     }

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