Merge pull request #7524 from qinheping/loop-contract-unwind

CONTRACTS: Add an option to not unwind transformed loops after applying loop contracts

Author: tautschnig

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

doc/man/goto-synthesizer.1

@@ -17,6 +17,9 @@ program transformation for the synthesized contracts, and then writes the
 resulting program as GOTO binary on disk.
 .SH OPTIONS
 .TP
+\fB\-loop\-contracts\-no\-unwind\fR
+Do not unwind transformed loops after applying the synthesized loop contracts.
+.TP
 \fB\-\-dump\-loop\-contracts
 Dump the synthesized loop contracts as JSON.
 .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"                      \
@@ -75,7 +80,7 @@ class code_contractst
   /// with an assertion that the `requires` clause holds followed by an
   /// assumption that the `ensures` clause holds. In order to ensure that `F`
   /// actually abides by its `ensures` and `requires` clauses, you should
-  /// separately call `code_constractst::enforce_contracts()` on `F` and verify
+  /// separately call `code_contractst::enforce_contracts()` on `F` and verify
   /// it using `cbmc --function F`.
   void replace_calls(const std::set<std::string> &to_replace);
 
@@ -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;
@@ -159,7 +167,7 @@ class code_contractst
   std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
     original_loop_number_map;
 
-  /// Loop havoc instructions instrumneted during applying loop contracts.
+  /// Loop havoc instructions instrumented during applying loop contracts.
   std::unordered_set<goto_programt::const_targett, const_target_hash>
     loop_havoc_set;
 

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, [email protected]
   "(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 \

src/goto-synthesizer/cegis_verifier.cpp

@@ -610,6 +610,7 @@ optionalt<cext> cegis_verifiert::verify()
 
   // Apply loop contracts we annotated.
   code_contractst cont(goto_model, log);
+  cont.unwind_transformed_loops = false;
   cont.apply_loop_contracts();
   original_loop_number_map = cont.get_original_loop_number_map();
   loop_havoc_set = cont.get_loop_havoc_set();

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -110,6 +110,8 @@ int goto_synthesizer_parse_optionst::doit()
     cmdline.get_values("nondet-static-exclude").begin(),
     cmdline.get_values("nondet-static-exclude").end());
   code_contractst contracts(goto_model, log);
+  contracts.unwind_transformed_loops =
+    !cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND);
   contracts.apply_loop_contracts(to_exclude_from_nondet_static);
 
   // recalculate numbers, etc.
@@ -183,6 +185,7 @@ void goto_synthesizer_parse_optionst::help()
     "\n"
     "Main options:\n"
     HELP_DUMP_LOOP_CONTRACTS
+    HELP_LOOP_CONTRACTS_NO_UNWIND
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"