Merge pull request #2006 from tautschnig/opt-no-self-loops

[SV-COMP'18 17/19] Add option not to transform self-loops into assumes

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -152,6 +152,11 @@ 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);
 

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,8 @@
+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

@@ -84,6 +84,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)
@@ -292,6 +294,7 @@ class path_explorert : public bmct
   "(unwinding-assertions)"                                                     \
   "(no-unwinding-assertions)"                                                  \
   "(no-pretty-names)"                                                          \
+  "(no-self-loops-to-assumptions)"                                             \
   "(partial-loops)"                                                            \
   "(paths):"                                                                   \
   "(show-symex-strategies)"                                                    \
@@ -315,6 +318,8 @@ class path_explorert : public bmct
   " --unwinding-assertions       generate unwinding assertions (cannot be\n"   \
   "                              used with --cover or --partial-loops)\n"      \
   " --partial-loops              permit paths with partial loops\n"            \
+  " --no-self-loops-to-assumptions\n"                                          \
+  "                              do not simplify while(1){} to assume(0)\n"    \
   " --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

@@ -227,6 +227,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("no-propagation"))
     options.set_option("propagation", false);
 
+  // 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

@@ -57,6 +57,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),
@@ -202,6 +203,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,11 @@ 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