Add --halt-symex-on-bug flag

When doing path exploration, one sometimes wants CBMC to halt symbolic
execution as soon as it encounters a single bug, rather than exploring
for all bugs. This flag enables that behaviour.

This flag differs from --stop-on-fail in that --stop-on-fail explores
all paths but halts on the first property violation, while
--halt-symex-on-bug doesn't bother exploring any more paths as soon as a
buggy one is found.

Author: karkhaz

src/cbmc/bmc.cpp

@@ -588,6 +588,12 @@ int bmct::do_language_agnostic_bmc(
       if(driver_configure_bmc)
         driver_configure_bmc(bmc, symbol_table);
       tmp_result = bmc.run(model);
+
+      if(
+        tmp_result == safety_checkert::resultt::UNSAFE &&
+        opts.get_bool_option("halt-symex-on-bug"))
+        return CPROVER_EXIT_VERIFICATION_UNSAFE;
+
       if(tmp_result != safety_checkert::resultt::PAUSED)
         final_result = tmp_result;
     }
@@ -637,6 +643,12 @@ int bmct::do_language_agnostic_bmc(
       if(driver_configure_bmc)
         driver_configure_bmc(pe, symbol_table);
       tmp_result = pe.run(model);
+
+      if(
+        tmp_result == safety_checkert::resultt::UNSAFE &&
+        opts.get_bool_option("halt-symex-on-bug"))
+        return CPROVER_EXIT_VERIFICATION_UNSAFE;
+
       if(tmp_result != safety_checkert::resultt::PAUSED)
         final_result &= tmp_result;
       worklist->pop();

src/cbmc/bmc.h

@@ -304,6 +304,7 @@ class path_explorert : public bmct
   "(no-pretty-names)"                                                          \
   "(no-self-loops-to-assumptions)"                                             \
   "(partial-loops)"                                                            \
+  "(halt-symex-on-bug)"                                                        \
   "(paths):"                                                                   \
   "(show-symex-strategies)"                                                    \
   "(depth):"                                                                   \
@@ -326,6 +327,7 @@ 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"            \
+  " --halt-symex-on-bug          with --paths, halt on first buggy path\n"     \
   " --no-self-loops-to-assumptions\n"                                          \
   "                              do not simplify while(1){} to assume(0)\n"    \
   " --no-pretty-names            do not simplify identifiers\n"                \

src/goto-symex/path_storage.cpp

@@ -98,6 +98,9 @@ void path_strategy_choosert::set_path_strategy_options(
       exit(CPROVER_EXIT_USAGE_ERROR);
     }
     options.set_option("exploration-strategy", strategy);
+
+    if(cmdline.isset("halt-symex-on-bug"))
+      options.set_option("halt-symex-on-bug", true);
   }
   else
     options.set_option("exploration-strategy", default_strategy());

unit/path_strategies.cpp

@@ -223,6 +223,39 @@ SCENARIO("path strategies")
         symex_eventt::resume(symex_eventt::enumt::JUMP, 9),
         symex_eventt::result(symex_eventt::enumt::FAILURE),
       });
+
+    GIVEN("program to check for halt-symex-on-bug")
+    {
+      std::function<void(optionst &)> halt_callback = [](optionst &opts) {
+        opts.set_option("halt-symex-on-bug", true);
+      };
+      std::function<void(optionst &)> no_halt_callback = [](optionst &opts) {};
+
+      c =
+        "/*  1 */  int main()      \n"
+        "/*  2 */  {               \n"
+        "/*  3 */    int x, y;     \n"
+        "/*  4 */    if(x)         \n"
+        "/*  5 */      y = 5 / 0;  \n"
+        "/*  6 */    else          \n"
+        "/*  7 */      y = 5 / 0;  \n"
+        "/*  8 */  }               \n";
+
+      check_with_strategy(
+        "lifo",
+        no_halt_callback,
+        c,
+        {symex_eventt::resume(symex_eventt::enumt::NEXT, 4),
+         symex_eventt::result(symex_eventt::enumt::FAILURE),
+         symex_eventt::resume(symex_eventt::enumt::NEXT, 6),
+         symex_eventt::result(symex_eventt::enumt::FAILURE)});
+      check_with_strategy(
+        "lifo",
+        halt_callback,
+        c,
+        {symex_eventt::resume(symex_eventt::enumt::NEXT, 4),
+         symex_eventt::result(symex_eventt::enumt::FAILURE)});
+    }
   }
 }