Only safety-check paths when new VCCs get added

CBMC will no longer bother running safety checks on path segments that
did not generate any new VCCs when running in path-exploration mode.

A "path segment" is a list of instructions between two program branch
points. CBMC would previously pause symbolic execution and run safety
checks at every branch point, which is wasteful when no additional VCCs
have been generated since the last pause. As of this commit, CBMC will
check to see if new VCCs have been added, and only do the safety check
if so.

To support this, the new member goto_symext::path_segment_vccs records
the number of VCCs that were newly generated along this path segment. It
differs from the VCC counters in goto_symex_statet, which hold the
number of VCCs generated along the current path since the start of the
program. goto_symext objects are minted for each path segment, so they
don't hold any information about the VCCs previously along the path.

This commit also removes the "Starting new path" output, since this no
longer makes much sense. On the other hand, there is an additional final
status output; CBMC will report failure after the entire program has
been explored if even a single path contained a failing assertion, and
report success otherwise.

The unit tests have been updated to reflect the fact that CBMC no longer
emits "SUCCESS" at each branch point and at the end of paths, and also
that CBMC makes one final report of the program safety as a whole.

This commit fixes diffblue#2684.

Author: karkhaz

src/cbmc/bmc.cpp

@@ -270,9 +270,6 @@ safety_checkert::resultt bmct::execute(
     const goto_functionst &goto_functions =
       goto_model.get_goto_functions();
 
-    if(symex.should_pause_symex)
-      return safety_checkert::resultt::PAUSED;
-
     // This provides the driver program the opportunity to do things like a
     // symbol-table or goto-functions dump instead of actually running the
     // checker, like show-vcc except driver-program specific.
@@ -282,9 +279,14 @@ safety_checkert::resultt bmct::execute(
     if(driver_callback_after_symex && driver_callback_after_symex())
       return safety_checkert::resultt::SAFE; // to indicate non-error
 
-    // add a partial ordering, if required
     if(equation.has_threads())
     {
+      // When doing path exploration in a concurrent setting, we should avoid
+      // model-checking the program until we reach the end of a path.
+      if(symex.should_pause_symex)
+        return safety_checkert::resultt::PAUSED;
+
+      // add a partial ordering, if required
       memory_model->set_message_handler(get_message_handler());
       (*memory_model)(equation);
     }
@@ -328,6 +330,8 @@ safety_checkert::resultt bmct::execute(
       !options.get_bool_option("program-only") &&
       symex.get_remaining_vccs() == 0)
     {
+      if(options.is_set("paths"))
+        return safety_checkert::resultt::PAUSED;
       report_success();
       output_graphml(resultt::SAFE);
       return safety_checkert::resultt::SAFE;
@@ -339,7 +343,10 @@ safety_checkert::resultt bmct::execute(
       return safety_checkert::resultt::SAFE;
     }
 
-    return decide(goto_functions, prop_conv);
+    if(!options.is_set("paths") || symex.path_segment_vccs > 0)
+      return decide(goto_functions, prop_conv);
+
+    return safety_checkert::resultt::PAUSED;
   }
 
   catch(const std::string &error_str)
@@ -406,6 +413,10 @@ void bmct::slice()
   statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
                << symex.get_remaining_vccs()
                << " remaining after simplification" << eom;
+
+  if(options.is_set("paths"))
+    statistics() << "Generated " << symex.path_segment_vccs
+                 << " new VCC(s) along current path segment" << eom;
 }
 
 safety_checkert::resultt bmct::run(
@@ -494,8 +505,8 @@ int bmct::do_language_agnostic_bmc(
   std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
   std::function<bool(void)> callback_after_symex)
 {
-  safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN;
-  safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN;
+  safety_checkert::resultt final_result = safety_checkert::resultt::SAFE;
+  safety_checkert::resultt tmp_result = safety_checkert::resultt::SAFE;
   const symbol_tablet &symbol_table = model.get_symbol_table();
   messaget message(ui);
   std::unique_ptr<path_storaget> worklist;
@@ -554,11 +565,6 @@ int bmct::do_language_agnostic_bmc(
 
     while(!worklist->empty())
     {
-      if(tmp_result != safety_checkert::resultt::PAUSED)
-        message.status() << "___________________________\n"
-                         << "Starting new path (" << worklist->size()
-                         << " to go)\n"
-                         << message.eom;
       cbmc_solverst solvers(
         opts,
         symbol_table,
@@ -613,13 +619,15 @@ int bmct::do_language_agnostic_bmc(
   switch(final_result)
   {
   case safety_checkert::resultt::SAFE:
+    if(opts.is_set("paths"))
+      report_success(message, ui);
     return CPROVER_EXIT_VERIFICATION_SAFE;
   case safety_checkert::resultt::UNSAFE:
+    if(opts.is_set("paths"))
+      report_failure(message, ui);
     return CPROVER_EXIT_VERIFICATION_UNSAFE;
   case safety_checkert::resultt::ERROR:
     return CPROVER_EXIT_INTERNAL_ERROR;
-  case safety_checkert::resultt::UNKNOWN:
-    return CPROVER_EXIT_INTERNAL_ERROR;
   case safety_checkert::resultt::PAUSED:
     UNREACHABLE;
   }

src/goto-programs/safety_checker.h

@@ -42,10 +42,6 @@ class safety_checkert:public messaget
     /// doing path exploration; the symex state has been saved, and symex should
     /// be resumed by the caller.
     PAUSED,
-    /// We haven't yet assigned a safety check result to this object. A value of
-    /// UNKNOWN can be used to initialize a resultt object, and that object may
-    /// then safely be used with the |= and &= operators.
-    UNKNOWN
   };
 
   // check whether all assertions in goto_functions are safe
@@ -76,9 +72,6 @@ operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
     b != safety_checkert::resultt::PAUSED);
   switch(a)
   {
-  case safety_checkert::resultt::UNKNOWN:
-    a = b;
-    return a;
   case safety_checkert::resultt::ERROR:
     return a;
   case safety_checkert::resultt::SAFE:
@@ -107,9 +100,6 @@ operator|=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
     b != safety_checkert::resultt::PAUSED);
   switch(a)
   {
-  case safety_checkert::resultt::UNKNOWN:
-    a = b;
-    return a;
   case safety_checkert::resultt::SAFE:
     return a;
   case safety_checkert::resultt::ERROR:

src/goto-symex/goto_symex.h

@@ -70,6 +70,7 @@ class goto_symext
       log(mh),
       guard_identifier("goto_symex::\\guard"),
       path_storage(path_storage),
+      path_segment_vccs(0),
       _total_vccs(std::numeric_limits<unsigned>::max()),
       _remaining_vccs(std::numeric_limits<unsigned>::max())
   {
@@ -464,6 +465,18 @@ class goto_symext
 
   path_storaget &path_storage;
 
+public:
+  /// \brief Number of VCCs generated during the run of this goto_symext object
+  ///
+  /// This member is always initialized to `0` upon construction of this object.
+  /// It therefore differs from goto_symex_statet::total_vccs, which persists
+  /// across the creation of several goto_symext objects. When CBMC is run in
+  /// path-exploration mode, the meaning of this member is "the number of VCCs
+  /// generated between the last branch point and the current instruction,"
+  /// while goto_symex_statet::total_vccs records the total number of VCCs
+  /// generated along the entire path from the beginning of the program.
+  std::size_t path_segment_vccs;
+
 protected:
   /// @{\name Statistics
   ///

src/goto-symex/symex_main.cpp

@@ -52,6 +52,7 @@ void goto_symext::vcc(
   statet &state)
 {
   state.total_vccs++;
+  path_segment_vccs++;
 
   exprt expr=vcc_expr;
 

unit/path_strategies.cpp

@@ -81,15 +81,13 @@ SCENARIO("path strategies")
       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)});
     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)});
   }
@@ -125,14 +123,11 @@ SCENARIO("path strategies")
       {// Outer else, inner else
        symex_eventt::resume(symex_eventt::enumt::JUMP, 13),
        symex_eventt::resume(symex_eventt::enumt::JUMP, 16),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
        // Outer else, inner if
        symex_eventt::resume(symex_eventt::enumt::NEXT, 14),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
        // Outer if, inner else
        symex_eventt::resume(symex_eventt::enumt::NEXT, 6),
        symex_eventt::resume(symex_eventt::enumt::JUMP, 9),
-       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)});
@@ -147,13 +142,9 @@ SCENARIO("path strategies")
        symex_eventt::resume(symex_eventt::enumt::JUMP, 13),
        // Expand inner if of the outer if
        symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
-       // No more branch points, so complete the path
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
-       // Continue BFSing
+       // No more branch points, so complete the path. Then continue BFSing
        symex_eventt::resume(symex_eventt::enumt::JUMP, 9),
-       symex_eventt::result(symex_eventt::enumt::SUCCESS),
        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)});
   }
@@ -196,6 +187,9 @@ SCENARIO("path strategies")
         // infeasible.
         symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
         symex_eventt::result(symex_eventt::enumt::SUCCESS),
+
+        // Overall we fail.
+        symex_eventt::result(symex_eventt::enumt::FAILURE),
       });
 
     check_with_strategy(
@@ -221,6 +215,9 @@ 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),
+
+        // Overall we fail.
+        symex_eventt::result(symex_eventt::enumt::FAILURE),
       });
   }
 
@@ -250,7 +247,10 @@ SCENARIO("path strategies")
         {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)});
+         symex_eventt::result(symex_eventt::enumt::FAILURE),
+         // Overall result
+         symex_eventt::result(symex_eventt::enumt::FAILURE)
+        });
     }
     GIVEN("stopping on failure")
     {
@@ -259,7 +259,10 @@ SCENARIO("path strategies")
         halt_callback,
         c,
         {symex_eventt::resume(symex_eventt::enumt::JUMP, 7),
-         symex_eventt::result(symex_eventt::enumt::FAILURE)});
+         symex_eventt::result(symex_eventt::enumt::FAILURE),
+         // Overall result
+         symex_eventt::result(symex_eventt::enumt::FAILURE)
+        });
     }
   }
 }
@@ -377,14 +380,20 @@ void _check_with_strategy(
   prop_convt &pc = cbmc_solver->prop_conv();
   std::function<bool(void)> callback = []() { return false; };
 
+  safety_checkert::resultt overall_result = safety_checkert::resultt::SAFE;
+  std::size_t expected_results_cnt = 0;
+
   bmct bmc(opts, gm.get_symbol_table(), mh, pc, *worklist, callback);
-  safety_checkert::resultt result = bmc.run(gm);
+  safety_checkert::resultt tmp_result = bmc.run(gm);
 
-  std::size_t expected_results_cnt = 0;
-  symex_eventt::validate_result(events, result, expected_results_cnt);
+  if(tmp_result != safety_checkert::resultt::PAUSED)
+  {
+    symex_eventt::validate_result(events, tmp_result, expected_results_cnt);
+    overall_result &= tmp_result;
+  }
 
   if(
-    result == safety_checkert::resultt::UNSAFE &&
+    overall_result == safety_checkert::resultt::UNSAFE &&
     opts.get_bool_option("stop-on-fail") && opts.is_set("paths"))
   {
     worklist->clear();
@@ -408,17 +417,25 @@ void _check_with_strategy(
       resume.state,
       *worklist,
       callback);
-    result = pe.run(gm);
+    tmp_result = pe.run(gm);
 
-    symex_eventt::validate_result(events, result, expected_results_cnt);
+    if(tmp_result != safety_checkert::resultt::PAUSED)
+    {
+      symex_eventt::validate_result(events, tmp_result, expected_results_cnt);
+      overall_result &= tmp_result;
+    }
     worklist->pop();
 
     if(
-      result == safety_checkert::resultt::UNSAFE &&
+      overall_result == safety_checkert::resultt::UNSAFE &&
       opts.get_bool_option("stop-on-fail"))
     {
       worklist->clear();
     }
   }
+
+  symex_eventt::validate_result(events, overall_result, expected_results_cnt);
+
+  INFO("The expected results list contains " << events.size() << " items");
   REQUIRE(events.empty());
 }