Add an option to not unwind tranformed loops after applying loop contracts

Author: qinheping

doc/man/goto-instrument.1

@@ -999,6 +999,9 @@ force aggressive slicer to preserve all direct paths
 \fB\-\-apply\-loop\-contracts\fR
 check and use loop contracts when provided
 .TP
+\fB\-loop\-contracts\-no\-unwind\fR
+do not unwind transformed loops
+.TP
 \fB\-\-replace\-call\-with\-contract\fR \fIfun\fR
 replace calls to \fIfun\fR with \fIfun\fR's contract
 .TP

regression/contracts/loop_contracts_no_unwind/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 0;
+
+  while(x < 10)
+    __CPROVER_loop_invariant(0 <= x && x <= 10);
+  {
+    x++;
+  }
+
+  assert(x == 10);
+}

regression/contracts/loop_contracts_no_unwind/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--apply-loop-contracts --loop-contracts-no-unwind _ --unwind 1 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+\[main.unwind.\d+\] line \d+ unwinding assertion loop 0: FAILURE
+^VERIFICATION FAILED$
+--
+--
+Check that transformed loop will not be unwound with flag --loop-contracts-no-unwind.

src/goto-instrument/contracts/contracts.cpp

@@ -1445,10 +1445,13 @@ void code_contractst::apply_loop_contracts(
   nondet_static(goto_model, to_exclude_from_nondet_init);
 
   // unwind all transformed loops twice.
-  unwindsett unwindset{goto_model};
-  unwindset.parse_unwindset(loop_names, log.get_message_handler());
-  goto_unwindt goto_unwind;
-  goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);
+  if(unwind_transformed_loops)
+  {
+    unwindsett unwindset{goto_model};
+    unwindset.parse_unwindset(loop_names, log.get_message_handler());
+    goto_unwindt goto_unwind;
+    goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);
+  }
 
   remove_skip(goto_model);
 

src/goto-instrument/contracts/contracts.h

@@ -35,6 +35,11 @@ Date: February 2016
   " --apply-loop-contracts\n"                                                  \
   "                              check and use loop contracts when provided\n"
 
+#define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind"
+#define HELP_LOOP_CONTRACTS_NO_UNWIND                                          \
+  " --loop-contracts-no-unwind\n"                                              \
+  "                              do not unwind transformed loops\n"
+
 #define FLAG_REPLACE_CALL "replace-call-with-contract"
 #define HELP_REPLACE_CALL                                                      \
   " --replace-call-with-contract <function>[/contract]\n"                      \
@@ -139,6 +144,9 @@ class code_contractst
 
   namespacet ns;
 
+  // Unwind transformed loops after applying loop contracts or not.
+  bool unwind_transformed_loops = true;
+
 protected:
   goto_modelt &goto_model;
   symbol_tablet &symbol_table;

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1237,7 +1237,17 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     contracts.enforce_contracts(to_enforce, to_exclude_from_nondet_static);
 
     if(cmdline.isset(FLAG_LOOP_CONTRACTS))
+    {
+      if(cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND))
+      {
+        contracts.unwind_transformed_loops = false;
+        log.warning() << "**** WARNING: transformed loops will not be unwound "
+                      << "after applying loop contracts. Remember to unwind "
+                      << "them at least twice to pass unwinding-assertions."
+                      << messaget::eom;
+      }
       contracts.apply_loop_contracts(to_exclude_from_nondet_static);
+    }
   }
 
   if(cmdline.isset("value-set-fi-fp-removal"))
@@ -1966,6 +1976,7 @@ void goto_instrument_parse_optionst::help()
     "Code contracts:\n"
     HELP_DFCC
     HELP_LOOP_CONTRACTS
+    HELP_LOOP_CONTRACTS_NO_UNWIND
     HELP_REPLACE_CALL
     HELP_ENFORCE_CONTRACT
     HELP_ENFORCE_CONTRACT_REC

src/goto-instrument/goto_instrument_parse_options.h

@@ -97,6 +97,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(horn)(skip-loops):(model-argc-argv):" \
   OPT_DFCC \
   "(" FLAG_LOOP_CONTRACTS ")" \
+  "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
   "(" FLAG_REPLACE_CALL "):" \
   "(" FLAG_ENFORCE_CONTRACT "):" \
   OPT_ENFORCE_CONTRACT_REC \