Merge pull request #3237 from karkhaz/kk-thrifty-model-checking

tautschnig · web-flow · commit 3ab83715be93 · 2018-10-30T08:20:25.000Z
Only safety-check paths when new VCCs get added
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -153,9 +153,14 @@ bmct::run_decision_procedure(prop_convt &prop_conv)
 
 void bmct::report_success()
 {
-  result() << bold << "VERIFICATION SUCCESSFUL" << reset << eom;
+  report_success(*this, ui_message_handler);
+}
 
-  switch(ui_message_handler.get_ui())
+void bmct::report_success(messaget &log, ui_message_handlert &handler)
+{
+  log.result() << log.bold << "VERIFICATION SUCCESSFUL" << log.reset << log.eom;
+
+  switch(handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     break;
@@ -164,25 +169,30 @@ void bmct::report_success()
     {
       xmlt xml("cprover-status");
       xml.data="SUCCESS";
-      result() << xml;
+      log.result() << xml;
     }
     break;
 
   case ui_message_handlert::uit::JSON_UI:
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("success");
-      result() << json_result;
+      log.result() << json_result;
     }
     break;
   }
 }
 
 void bmct::report_failure()
 {
-  result() << bold << "VERIFICATION FAILED" << reset << eom;
+  report_failure(*this, ui_message_handler);
+}
 
-  switch(ui_message_handler.get_ui())
+void bmct::report_failure(messaget &log, ui_message_handlert &handler)
+{
+  log.result() << log.bold << "VERIFICATION FAILED" << log.reset << log.eom;
+
+  switch(handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     break;
@@ -191,15 +201,15 @@ void bmct::report_failure()
     {
       xmlt xml("cprover-status");
       xml.data="FAILURE";
-      result() << xml;
+      log.result() << xml;
     }
     break;
 
   case ui_message_handlert::uit::JSON_UI:
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("failure");
-      result() << json_result;
+      log.result() << json_result;
     }
     break;
   }
@@ -260,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.
@@ -272,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);
     }
@@ -318,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;
@@ -329,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)
@@ -396,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(
@@ -484,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;
@@ -544,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,
@@ -603,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;
   }
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
@@ -208,6 +208,9 @@ class bmct:public safety_checkert
   virtual void report_success();
   virtual void report_failure();
 
+  static void report_success(messaget &, ui_message_handlert &);
+  static void report_failure(messaget &, ui_message_handlert &);
+
   virtual void error_trace();
   void output_graphml(resultt result);
 
diff --git a/src/goto-programs/safety_checker.h b/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:
diff --git a/src/goto-symex/goto_symex.h b/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
   ///
diff --git a/src/goto-symex/symex_main.cpp b/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;
 
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
diff --git a/unit/path_strategies.h b/unit/path_strategies.h

Original file line number	Diff line number	Diff line change
`@@ -52,6 +52,7 @@ void goto_symext::vcc(`
`52`	`52`	`statet &state)`
`53`	`53`	`{`
`54`	`54`	`state.total_vccs++;`
	`55`	`+ path_segment_vccs++;`
`55`	`56`
`56`	`57`	`exprt expr=vcc_expr;`
`57`	`58`