--stop-on-fail now stops on failed path

When doing path exploration, one sometimes wants CBMC to halt symbolic
execution as soon as it encounters a single bug, rather than continuing
to explore the program for all bugs. This behaviour can now be enabled
by passing the --stop-on-fail flag together with the --paths flag.

Prior to this commit, the --stop-on-fail flag --- which was written with
model-checking rather than path exploration in mind --- would explore
all paths, but only print out a single failed property, which isn't
terribly useful because it uses just as much time as printing out all
properties. This commit makes this flag more useful when used in
conjunction with --paths, while not changing its behaviour for model
checking.

Author: karkhaz

src/cbmc/bmc.cpp

@@ -588,6 +588,15 @@ 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("stop-on-fail") && opts.is_set("paths"))
+      {
+        worklist->clear();
+        return CPROVER_EXIT_VERIFICATION_UNSAFE;
+      }
+
       if(tmp_result != safety_checkert::resultt::PAUSED)
         final_result = tmp_result;
     }
@@ -637,6 +646,15 @@ 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("stop-on-fail") && opts.is_set("paths"))
+      {
+        worklist->clear();
+        return CPROVER_EXIT_VERIFICATION_UNSAFE;
+      }
+
       if(tmp_result != safety_checkert::resultt::PAUSED)
         final_result &= tmp_result;
       worklist->pop();

unit/path_strategies.cpp

@@ -224,6 +224,45 @@ SCENARIO("path strategies")
         symex_eventt::result(symex_eventt::enumt::FAILURE),
       });
   }
+
+    GIVEN("program to check for stop-on-fail with path exploration")
+    {
+      std::function<void(optionst &)> halt_callback = [](optionst &opts) {
+        opts.set_option("stop-on-fail", 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 */      assert(0);  \n"
+        "/*  6 */    else          \n"
+        "/*  7 */      assert(0);  \n"
+        "/*  8 */  }               \n";
+
+      GIVEN("no stopping on failure")
+      {
+        check_with_strategy(
+          "lifo",
+          no_halt_callback,
+          c,
+          {symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
+           symex_eventt::result(symex_eventt::enumt::FAILURE),
+           symex_eventt::resume(symex_eventt::enumt::NEXT, 5),
+           symex_eventt::result(symex_eventt::enumt::FAILURE)});
+      }
+      GIVEN("stopping on failure")
+      {
+        check_with_strategy(
+          "lifo",
+          halt_callback,
+          c,
+          {symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
+           symex_eventt::result(symex_eventt::enumt::FAILURE)});
+      }
+    }
 }
 
 // In theory, there should be no need to change the code below when adding new
@@ -334,6 +373,11 @@ void _check_with_strategy(
   safety_checkert::resultt result = bmc.run(gm);
   symex_eventt::validate_result(events, result);
 
+  if(
+    result == safety_checkert::resultt::UNSAFE &&
+    opts.get_bool_option("stop-on-fail") && opts.is_set("paths"))
+    worklist->clear();
+
   while(!worklist->empty())
   {
     cbmc_solverst solvers(opts, gm.get_symbol_table(), mh);
@@ -357,6 +401,11 @@ void _check_with_strategy(
 
     symex_eventt::validate_result(events, result);
     worklist->pop();
+
+    if(
+      result == safety_checkert::resultt::UNSAFE &&
+      opts.get_bool_option("stop-on-fail"))
+      worklist->clear();
   }
   REQUIRE(events.empty());
 }