Integrate fault localizer into goto checker [blocks: 4215]

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -29,8 +29,10 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/ansi_c_language.h>
 
 #include <goto-checker/all_properties_verifier.h>
+#include <goto-checker/all_properties_verifier_with_fault_localization.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
 #include <goto-checker/stop_on_fail_verifier.h>
+#include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/lazy_goto_model.h>
@@ -161,12 +163,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("localize-faults"))
     options.set_option("localize-faults", true);
-  if(cmdline.isset("localize-faults-method"))
-  {
-    options.set_option(
-      "localize-faults-method",
-      cmdline.get_value("localize-faults-method"));
-  }
 
   if(cmdline.isset("unwind"))
     options.set_option("unwind", cmdline.get_value("unwind"));
@@ -613,9 +609,19 @@ int jbmc_parse_optionst::doit()
         }
         else
         {
-          verifier = util_make_unique<
-            stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
-            options, ui_message_handler, goto_model);
+          if(options.get_bool_option("localize-faults"))
+          {
+            verifier =
+              util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
+                java_multi_path_symex_checkert>>(
+                options, ui_message_handler, goto_model);
+          }
+          else
+          {
+            verifier = util_make_unique<
+              stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+          }
         }
       }
       else
@@ -629,10 +635,20 @@ int jbmc_parse_optionst::doit()
         }
         else
         {
-          verifier =
-            util_make_unique<all_properties_verifier_with_trace_storaget<
-              java_multi_path_symex_checkert>>(
-              options, ui_message_handler, goto_model);
+          if(options.get_bool_option("localize-faults"))
+          {
+            verifier =
+              util_make_unique<all_properties_verifier_with_fault_localizationt<
+                java_multi_path_symex_checkert>>(
+                options, ui_message_handler, goto_model);
+          }
+          else
+          {
+            verifier =
+              util_make_unique<all_properties_verifier_with_trace_storaget<
+                java_multi_path_symex_checkert>>(
+                options, ui_message_handler, goto_model);
+          }
         }
       }
     }

jbmc/src/jbmc/jbmc_parse_options.h

@@ -77,7 +77,7 @@ class optionst;
   OPT_FLUSH \
   JAVA_BYTECODE_LANGUAGE_OPTIONS \
   "(java-unwind-enum-static)" \
-  "(localize-faults)(localize-faults-method):" \
+  "(localize-faults)" \
   "(java-threading)" \
   OPT_GOTO_TRACE \
   OPT_VALIDATE \

src/cbmc/cbmc_parse_options.cpp

@@ -34,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 #include <cpp/cprover_library.h>
 
 #include <goto-checker/all_properties_verifier.h>
+#include <goto-checker/all_properties_verifier_with_fault_localization.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
 #include <goto-checker/bmc_util.h>
 #include <goto-checker/cover_goals_verifier_with_trace_storage.h>
@@ -43,6 +44,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/single_path_symex_checker.h>
 #include <goto-checker/single_path_symex_only_checker.h>
 #include <goto-checker/stop_on_fail_verifier.h>
+#include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
@@ -230,12 +232,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("localize-faults"))
     options.set_option("localize-faults", true);
-  if(cmdline.isset("localize-faults-method"))
-  {
-    options.set_option(
-      "localize-faults-method",
-      cmdline.get_value("localize-faults-method"));
-  }
 
   if(cmdline.isset("unwind"))
     options.set_option("unwind", cmdline.get_value("unwind"));
@@ -625,9 +621,19 @@ int cbmc_parse_optionst::doit()
       }
       else
       {
-        verifier =
-          util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
-            options, ui_message_handler, goto_model);
+        if(options.get_bool_option("localize-faults"))
+        {
+          verifier =
+            util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
+              multi_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+        }
+        else
+        {
+          verifier =
+            util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+        }
       }
     }
     else
@@ -639,8 +645,20 @@ int cbmc_parse_optionst::doit()
       }
       else
       {
-        verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
-          multi_path_symex_checkert>>(options, ui_message_handler, goto_model);
+        if(options.get_bool_option("localize-faults"))
+        {
+          verifier =
+            util_make_unique<all_properties_verifier_with_fault_localizationt<
+              multi_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+        }
+        else
+        {
+          verifier =
+            util_make_unique<all_properties_verifier_with_trace_storaget<
+              multi_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+        }
       }
     }
   }

src/cbmc/cbmc_parse_options.h

@@ -76,7 +76,7 @@ class optionst;
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   OPT_FLUSH \
-  "(localize-faults)(localize-faults-method):" \
+  "(localize-faults)" \
   OPT_GOTO_TRACE \
   OPT_VALIDATE \
   OPT_ANSI_C_LANGUAGE \

src/goto-checker/Makefile

@@ -2,6 +2,7 @@ SRC = bmc_util.cpp \
       counterexample_beautification.cpp \
       cover_goals_report_util.cpp \
       incremental_goto_checker.cpp \
+      goto_symex_fault_localizer.cpp \
       goto_symex_property_decider.cpp \
       goto_trace_storage.cpp \
       goto_verifier.cpp \

src/goto-checker/all_properties_verifier_with_fault_localization.h

@@ -0,0 +1,109 @@
+/*******************************************************************\
+
+Module: Goto Verifier for Verifying all Properties and Localizing Faults
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto verifier for verifying all properties that stores traces
+/// and localizes faults
+
+#ifndef CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_FAULT_LOCALIZATION_H
+#define CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_FAULT_LOCALIZATION_H
+
+#include "goto_verifier.h"
+
+#include "fault_localization_provider.h"
+#include "goto_trace_storage.h"
+#include "incremental_goto_checker.h"
+#include "properties.h"
+#include "report_util.h"
+
+/// Requires an incremental goto checker that is a
+/// `goto_trace_providert` and `fault_localization_providert`.
+template <class incremental_goto_checkerT>
+class all_properties_verifier_with_fault_localizationt : public goto_verifiert
+{
+public:
+  all_properties_verifier_with_fault_localizationt(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler,
+    abstract_goto_modelt &goto_model)
+    : goto_verifiert(options, ui_message_handler),
+      goto_model(goto_model),
+      incremental_goto_checker(options, ui_message_handler, goto_model),
+      traces(incremental_goto_checker.get_namespace())
+  {
+    properties = initialize_properties(goto_model);
+  }
+
+  resultt operator()() override
+  {
+    while(true)
+    {
+      const auto result = incremental_goto_checker(properties);
+      if(result.progress == incremental_goto_checkert::resultt::progresst::DONE)
+        break;
+
+      // we've got an error trace
+      message_building_error_trace(log);
+      for(const auto &property_id : result.updated_properties)
+      {
+        if(properties.at(property_id).status == property_statust::FAIL)
+        {
+          // get correctly truncated error trace for property and store it
+          (void)traces.insert(
+            incremental_goto_checker.build_trace(property_id));
+
+          fault_locations.insert(
+            {property_id,
+             incremental_goto_checker.localize_fault(property_id)});
+        }
+      }
+
+      ++iterations;
+    }
+
+    return determine_result(properties);
+  }
+
+  void report() override
+  {
+    if(
+      options.get_bool_option("trace") ||
+      // currently --trace only affects plain text output
+      ui_message_handler.get_ui() != ui_message_handlert::uit::PLAIN)
+    {
+      const trace_optionst trace_options(options);
+      output_properties_with_traces_and_fault_localization(
+        properties,
+        traces,
+        trace_options,
+        fault_locations,
+        iterations,
+        ui_message_handler);
+    }
+    else
+    {
+      output_properties_with_fault_localization(
+        properties, fault_locations, iterations, ui_message_handler);
+    }
+    output_overall_result(determine_result(properties), ui_message_handler);
+  }
+
+  const goto_trace_storaget &get_traces() const
+  {
+    return traces;
+  }
+
+protected:
+  abstract_goto_modelt &goto_model;
+  incremental_goto_checkerT incremental_goto_checker;
+  std::size_t iterations = 1;
+  goto_trace_storaget traces;
+  std::unordered_map<irep_idt, fault_location_infot> fault_locations;
+};
+
+#endif // CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_FAULT_LOCALIZATION_H

src/goto-checker/bmc_util.cpp

@@ -102,6 +102,19 @@ void output_error_trace(
   }
 }
 
+void freeze_guards(
+  const symex_target_equationt &equation,
+  prop_convt &prop_conv)
+{
+  for(const auto &step : equation.SSA_steps)
+  {
+    if(!step.guard_literal.is_constant())
+      prop_conv.set_frozen(step.guard_literal);
+    if(step.is_assert() && !step.cond_literal.is_constant())
+      prop_conv.set_frozen(step.cond_literal);
+  }
+}
+
 /// outputs an error witness in graphml format
 void output_graphml(
   const goto_tracet &goto_trace,

src/goto-checker/bmc_util.h

@@ -57,6 +57,8 @@ void output_error_trace(
   const trace_optionst &,
   ui_message_handlert &);
 
+void freeze_guards(const symex_target_equationt &, prop_convt &);
+
 void output_graphml(const goto_tracet &, const namespacet &, const optionst &);
 void output_graphml(
   const symex_target_equationt &,

src/goto-checker/fault_localization_provider.h

@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module: Interface for Goto Checkers to provide Fault Localization
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Interface for Goto Checkers to provide Fault Localization
+
+#ifndef CPROVER_GOTO_CHECKER_FAULT_LOCALIZATION_PROVIDER_H
+#define CPROVER_GOTO_CHECKER_FAULT_LOCALIZATION_PROVIDER_H
+
+#include <map>
+
+#include <goto-programs/goto_program.h>
+
+class goto_tracet;
+class namespacet;
+
+struct fault_location_infot
+{
+  typedef std::map<goto_programt::const_targett, std::size_t> score_mapt;
+  score_mapt scores;
+};
+
+/// An implementation of `incremental_goto_checkert`
+/// may implement this interface to provide fault localization information.
+class fault_localization_providert
+{
+public:
+  /// Returns the most likely fault locations
+  /// for the given FAILed \p property_id
+  virtual fault_location_infot
+  localize_fault(const irep_idt &property_id) const = 0;
+
+  virtual ~fault_localization_providert() = default;
+};
+
+#endif // CPROVER_GOTO_CHECKER_FAULT_LOCALIZATION_PROVIDER_H