Make --stop-on-fail halt symex early when doing path exploration

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();

src/goto-symex/path_storage.cpp

@@ -43,6 +43,11 @@ std::size_t path_lifot::size() const
   return paths.size();
 }
 
+void path_lifot::clear()
+{
+  paths.clear();
+}
+
 // _____________________________________________________________________________
 // path_fifot
 
@@ -69,6 +74,11 @@ std::size_t path_fifot::size() const
   return paths.size();
 }
 
+void path_fifot::clear()
+{
+  paths.clear();
+}
+
 // _____________________________________________________________________________
 // path_strategy_choosert
 

src/goto-symex/path_storage.h

@@ -50,6 +50,14 @@ class path_storaget
     return private_peek();
   }
 
+  /// \brief Clear all saved paths
+  ///
+  /// This is typically used because we want to terminate symbolic execution
+  /// early. It doesn't matter too much in terms of memory usage since CBMC
+  /// typically exits soon after we do that, however it's nice to have tests
+  /// that check that the worklist is always empty when symex finishes.
+  virtual void clear() = 0;
+
   /// \brief Add paths to resume to the storage
   ///
   /// Symbolic execution is suspended when we reach a conditional goto
@@ -90,6 +98,7 @@ class path_lifot : public path_storaget
 public:
   void push(const patht &, const patht &) override;
   std::size_t size() const override;
+  void clear() override;
 
 protected:
   std::list<path_storaget::patht>::iterator last_peeked;
@@ -106,6 +115,7 @@ class path_fifot : public path_storaget
 public:
   void push(const patht &, const patht &) override;
   std::size_t size() const override;
+  void clear() override;
 
 protected:
   std::list<patht> paths;

unit/path_strategies.cpp

@@ -65,6 +65,8 @@ SCENARIO("path strategies")
   std::string c;
   GIVEN("a simple conditional program")
   {
+    std::function<void(optionst &)> opts_callback = [](optionst &opts) {};
+
     c =
       "/*  1 */  int main()      \n"
       "/*  2 */  {               \n"
@@ -75,28 +77,28 @@ SCENARIO("path strategies")
       "/*  7 */      x = 0;      \n"
       "/*  8 */  }               \n";
 
-    const unsigned unwind_limit = 0U;
-
     check_with_strategy(
       "lifo",
+      opts_callback,
       c,
       {symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
        symex_eventt::result(symex_eventt::enumt::SUCCESS),
        symex_eventt::resume(symex_eventt::enumt::NEXT, 5),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS)},
-      unwind_limit);
+       symex_eventt::result(symex_eventt::enumt::SUCCESS)});
     check_with_strategy(
       "fifo",
+      opts_callback,
       c,
       {symex_eventt::resume(symex_eventt::enumt::NEXT, 5),
        symex_eventt::result(symex_eventt::enumt::SUCCESS),
        symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS)},
-      unwind_limit);
+       symex_eventt::result(symex_eventt::enumt::SUCCESS)});
   }
 
   GIVEN("a program with nested conditionals")
   {
+    std::function<void(optionst &)> opts_callback = [](optionst &opts) {};
+
     c =
       "/*  1 */  int main()            \n"
       "/*  2 */  {                     \n"
@@ -117,10 +119,9 @@ SCENARIO("path strategies")
       "/* 17 */    }                   \n"
       "/* 18 */  }                     \n";
 
-    const unsigned unwind_limit = 0U;
-
     check_with_strategy(
       "lifo",
+      opts_callback,
       c,
       {// Outer else, inner else
        symex_eventt::resume(symex_eventt::enumt::JUMP, 13),
@@ -135,11 +136,11 @@ SCENARIO("path strategies")
        symex_eventt::result(symex_eventt::enumt::SUCCESS),
        // Outer if, inner if
        symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS)},
-      unwind_limit);
+       symex_eventt::result(symex_eventt::enumt::SUCCESS)});
 
     check_with_strategy(
       "fifo",
+      opts_callback,
       c,
       {// Expand outer if, but don't continue depth-first
        symex_eventt::resume(symex_eventt::enumt::NEXT, 6),
@@ -155,12 +156,15 @@ SCENARIO("path strategies")
        symex_eventt::resume(symex_eventt::enumt::NEXT, 14),
        symex_eventt::result(symex_eventt::enumt::SUCCESS),
        symex_eventt::resume(symex_eventt::enumt::JUMP, 16),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS)},
-      unwind_limit);
+       symex_eventt::result(symex_eventt::enumt::SUCCESS)});
   }
 
   GIVEN("a loop program to test functional correctness")
   {
+    std::function<void(optionst &)> opts_callback = [](optionst &opts) {
+      opts.set_option("unwind", 2U);
+    };
+
     c =
       "/*  1 */   int main()                       \n"
       "/*  2 */   {                                \n"
@@ -173,10 +177,9 @@ SCENARIO("path strategies")
       "/*  9 */     assert(x);                     \n"
       "/* 10 */   }                                \n";
 
-    const unsigned unwind_limit = 2U;
-
     check_with_strategy(
       "lifo",
+      opts_callback,
       c,
       {
         // The path where we skip the loop body. Successful because the path is
@@ -194,11 +197,11 @@ SCENARIO("path strategies")
         // infeasible.
         symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
         symex_eventt::result(symex_eventt::enumt::SUCCESS),
-      },
-      unwind_limit);
+      });
 
     check_with_strategy(
       "fifo",
+      opts_callback,
       c,
       {
         // The path where we skip the loop body. Successful because the path is
@@ -219,8 +222,46 @@ SCENARIO("path strategies")
         // executing the loop once, decrementing x to 0; assert(x) should fail.
         symex_eventt::resume(symex_eventt::enumt::JUMP, 9),
         symex_eventt::result(symex_eventt::enumt::FAILURE),
-      },
-      unwind_limit);
+      });
+  }
+
+  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)});
+    }
   }
 }
 
@@ -286,7 +327,7 @@ void symex_eventt::validate_resume(
 void _check_with_strategy(
   const std::string &strategy,
   const std::string &program,
-  const unsigned unwind_limit,
+  std::function<void(optionst &)> opts_callback,
   symex_eventt::listt &events)
 {
   temporary_filet tmp("path-explore_", ".c");
@@ -307,11 +348,7 @@ void _check_with_strategy(
   opts.set_option("paths", true);
   opts.set_option("exploration-strategy", strategy);
 
-  if(unwind_limit)
-  {
-    opts.set_option("unwind", unwind_limit);
-    cmdline.set("unwind", std::to_string(unwind_limit));
-  }
+  opts_callback(opts);
 
   ui_message_handlert mh(cmdline, "path-explore");
   mh.set_verbosity(0);
@@ -337,6 +374,13 @@ 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);
@@ -360,6 +404,13 @@ 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());
 }

unit/path_strategies.h

@@ -45,18 +45,18 @@ struct symex_eventt
 void _check_with_strategy(
   const std::string &strategy,
   const std::string &program,
-  const unsigned unwind_limit,
+  std::function<void(optionst &)>,
   symex_eventt::listt &events);
 
 /// Call this one, not the underscore version
 void check_with_strategy(
   const std::string &strategy,
+  std::function<void(optionst &)> opts_callback,
   const std::string &program,
-  symex_eventt::listt events,
-  const unsigned unwind_limit)
+  symex_eventt::listt events)
 {
   WHEN("strategy is '" + strategy + "'")
-  _check_with_strategy(strategy, program, unwind_limit, events);
+  _check_with_strategy(strategy, program, opts_callback, events);
 }
 
 #endif // CPROVER_PATH_STRATEGIES_H