Add option not to transform self-loops into assumes

This allows disabling an optimisation in goto-symex
which is not compatible with termination checking.

Author: peterschrammel

regression/cbmc/self_loops_to_assumptions1/default.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--unwind 1 --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc/self_loops_to_assumptions1/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  while(1) {}
+
+  return 0;
+}

regression/cbmc/self_loops_to_assumptions1/no-assume.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--unwind 1 --unwinding-assertions --no-self-loops-to-assumptions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

src/cbmc/bmc.h

@@ -90,6 +90,8 @@ class bmct:public safety_checkert
     symex.constant_propagation=options.get_bool_option("propagation");
     symex.record_coverage=
       !options.get_option("symex-coverage-report").empty();
+    symex.self_loops_to_assumptions =
+      options.get_bool_option("self-loops-to-assumptions");
   }
 
   virtual resultt run(const goto_functionst &goto_functions)
@@ -303,6 +305,7 @@ class path_explorert : public bmct
   "(unwinding-assertions)"                                                     \
   "(no-unwinding-assertions)"                                                  \
   "(no-pretty-names)"                                                          \
+  "(no-self-loops-to-assumptions)"                                             \
   "(partial-loops)"                                                            \
   "(paths)"                                                                    \
   "(depth):"                                                                   \
@@ -323,6 +326,8 @@ class path_explorert : public bmct
   " --slice-formula              remove assignments unrelated to property\n"   \
   " --unwinding-assertions       generate unwinding assertions\n"              \
   " --partial-loops              permit paths with partial loops\n"            \
+  " --no-self-loops-to-assumptions                                             \
+  "                              do not simplify while(1) {} to assume(false)  \
   " --no-pretty-names            do not simplify identifiers\n"                \
   " --graphml-witness filename   write the witness in GraphML format to "      \
   "filename\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.cpp

@@ -187,6 +187,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   else
     options.set_option("propagation", true);
 
+  // transform self loops to assumptions
+  options.set_option(
+    "self-loops-to-assumptions", cmdline.isset("no-self-loops-to-assumptions"));
+
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 

src/goto-symex/goto_symex.h

@@ -74,6 +74,7 @@ class goto_symext
     : total_vccs(0),
       remaining_vccs(0),
       constant_propagation(true),
+      self_loops_to_assumptions(true),
       language_mode(),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
@@ -210,6 +211,7 @@ class goto_symext
   unsigned total_vccs, remaining_vccs;
 
   bool constant_propagation;
+  bool self_loops_to_assumptions;
 
   optionst options;
 

src/goto-symex/symex_goto.cpp

@@ -58,9 +58,10 @@ void goto_symext::symex_goto(statet &state)
   if(!forward) // backwards?
   {
     // is it label: goto label; or while(cond); - popular in SV-COMP
-    if(goto_target==state.source.pc ||
-       (instruction.incoming_edges.size()==1 &&
-        *instruction.incoming_edges.begin()==goto_target))
+    if(self_loops_to_assumptions &&
+       (goto_target==state.source.pc ||
+        (instruction.incoming_edges.size()==1 &&
+         *instruction.incoming_edges.begin()==goto_target)))
     {
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto

src/jbmc/jbmc_parse_options.cpp

@@ -154,6 +154,10 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   else
     options.set_option("propagation", true);
 
+  // transform self loops to assumptions
+  options.set_option(
+    "self-loops-to-assumptions", cmdline.isset("no-self-loops-to-assumptions"));
+
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);