Merge pull request #4162 from peterschrammel/fix-trace-truncation

Correctly truncate error traces

Author: tautschnig

regression/cbmc/multiple-goto-traces/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  assert(4 != argc);
+  argc++;
+  argc--;
+  assert(argc >= 1);
+  assert(argc != 4);
+  argc++;
+  argc--;
+  assert(argc + 1 != 5);
+  return 0;
+}

regression/cbmc/multiple-goto-traces/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--trace
+activate-multi-line-match
+EXIT=10
+SIGNAL=0
+VERIFICATION FAILED
+Trace for main\.assertion\.1:(\n.*){16}  assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){30}  assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){44}  assertion argc \+ 1 != 5
+\*\* 3 of 4 failed
+--
+^warning: ignoring
+--
+We have one counterexample violating multiple properties.
+Make sure the traces are correctly truncated.

src/goto-checker/all_properties_verifier_with_trace_storage.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "goto_verifier.h"
 
+#include "bmc_util.h"
 #include "goto_trace_storage.h"
 #include "incremental_goto_checker.h"
 #include "properties.h"
@@ -37,11 +38,23 @@ class all_properties_verifier_with_trace_storaget : public goto_verifiert
 
   resultt operator()() override
   {
-    while(incremental_goto_checker(properties).progress !=
-          incremental_goto_checkert::resultt::progresst::DONE)
+    while(true)
     {
-      // we've got an error trace; store it and link it to the failed properties
-      (void)traces.insert(incremental_goto_checker.build_trace());
+      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));
+        }
+      }
 
       ++iterations;
     }

src/goto-checker/bmc_util.cpp

@@ -32,19 +32,35 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "symex_bmc.h"
 
+void message_building_error_trace(messaget &log)
+{
+  log.status() << "Building error trace" << messaget::eom;
+}
+
 void build_error_trace(
   goto_tracet &goto_trace,
   const namespacet &ns,
   const symex_target_equationt &symex_target_equation,
   const prop_convt &prop_conv,
   ui_message_handlert &ui_message_handler)
 {
-  messaget msg(ui_message_handler);
-  msg.status() << "Building error trace" << messaget::eom;
+  messaget log(ui_message_handler);
+  message_building_error_trace(log);
 
   build_goto_trace(symex_target_equation, prop_conv, ns, goto_trace);
 }
 
+ssa_step_predicatet
+ssa_step_matches_failing_property(const irep_idt &property_id)
+{
+  return [property_id](
+           symex_target_equationt::SSA_stepst::const_iterator step,
+           const prop_convt &prop_conv) {
+    return step->is_assert() && step->get_property_id() == property_id &&
+           prop_conv.l_get(step->cond_literal).is_false();
+  };
+}
+
 void output_error_trace(
   const goto_tracet &goto_trace,
   const namespacet &ns,

src/goto-checker/bmc_util.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <memory>
 
 #include <goto-programs/safety_checker.h>
+#include <goto-symex/build_goto_trace.h>
 #include <goto-symex/path_storage.h>
 
 #include "properties.h"
@@ -35,6 +36,14 @@ void convert_symex_target_equation(
   prop_convt &,
   message_handlert &);
 
+/// Returns a function that checks whether an SSA step is an assertion
+/// with \p property_id. Usually used for `build_goto_trace`.
+ssa_step_predicatet
+ssa_step_matches_failing_property(const irep_idt &property_id);
+
+/// Outputs a message that an error trace is being built
+void message_building_error_trace(messaget &);
+
 void build_error_trace(
   goto_tracet &,
   const namespacet &,

src/goto-checker/cover_goals_verifier_with_trace_storage.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "goto_verifier.h"
 
+#include "bmc_util.h"
 #include "cover_goals_report_util.h"
 #include "goto_trace_storage.h"
 #include "incremental_goto_checker.h"
@@ -41,7 +42,8 @@ class cover_goals_verifier_with_trace_storaget : public goto_verifiert
           incremental_goto_checkert::resultt::progresst::DONE)
     {
       // we've got a trace; store it and link it to the covered goals
-      (void)traces.insert_all(incremental_goto_checker.build_trace());
+      message_building_error_trace(log);
+      (void)traces.insert_all(incremental_goto_checker.build_full_trace());
 
       ++iterations;
     }

src/goto-checker/goto_trace_provider.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
 #define CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
 
+#include <util/irep.h>
+
 class goto_tracet;
 class namespacet;
 
@@ -20,8 +22,15 @@ class namespacet;
 class goto_trace_providert
 {
 public:
-  /// Builds and returns a trace
-  virtual goto_tracet build_trace() const = 0;
+  /// Builds and returns the complete trace
+  virtual goto_tracet build_full_trace() const = 0;
+
+  /// Builds and returns the trace up to the first failed property
+  virtual goto_tracet build_shortest_trace() const = 0;
+
+  /// Builds and returns the trace for the FAILed property
+  /// with the given \p property_id
+  virtual goto_tracet build_trace(const irep_idt &property_id) const = 0;
 
   /// Returns the namespace associated with the traces
   virtual const namespacet &get_namespace() const = 0;

src/goto-checker/multi_path_symex_checker.cpp

@@ -109,20 +109,44 @@ operator()(propertiest &properties)
   return result;
 }
 
-goto_tracet multi_path_symex_checkert::build_trace() const
+goto_tracet multi_path_symex_checkert::build_full_trace() const
+{
+  goto_tracet goto_trace;
+  build_goto_trace(
+    equation,
+    equation.SSA_steps.end(),
+    property_decider.get_solver(),
+    ns,
+    goto_trace);
+
+  return goto_trace;
+}
+
+goto_tracet multi_path_symex_checkert::build_shortest_trace() const
 {
   if(options.get_bool_option("beautify"))
   {
     counterexample_beautificationt()(
       dynamic_cast<boolbvt &>(property_decider.get_solver()), equation);
   }
+
   goto_tracet goto_trace;
-  ::build_error_trace(
-    goto_trace,
-    ns,
+  build_goto_trace(equation, property_decider.get_solver(), ns, goto_trace);
+
+  return goto_trace;
+}
+
+goto_tracet
+multi_path_symex_checkert::build_trace(const irep_idt &property_id) const
+{
+  goto_tracet goto_trace;
+  build_goto_trace(
     equation,
+    ssa_step_matches_failing_property(property_id),
     property_decider.get_solver(),
-    ui_message_handler);
+    ns,
+    goto_trace);
+
   return goto_trace;
 }
 

src/goto-checker/multi_path_symex_checker.h

@@ -39,7 +39,9 @@ class multi_path_symex_checkert : public multi_path_symex_only_checkert,
   ///   in P_i. Such additional properties will be ignored.
   resultt operator()(propertiest &) override;
 
-  goto_tracet build_trace() const override;
+  goto_tracet build_full_trace() const override;
+  goto_tracet build_shortest_trace() const override;
+  goto_tracet build_trace(const irep_idt &) const override;
   const namespacet &get_namespace() const override;
 
   void output_error_witness(const goto_tracet &) override;

src/goto-checker/report_util.cpp

@@ -175,14 +175,9 @@ static void output_single_property_plain(
                << messaget::eom;
 }
 
-static void
-output_properties_plain(const propertiest &properties, messaget &log)
+static std::vector<propertiest::const_iterator>
+get_sorted_properties(const propertiest &properties)
 {
-  if(properties.empty())
-    return;
-
-  log.result() << "\n** Results:" << messaget::eom;
-  // collect properties in a vector
   std::vector<propertiest::const_iterator> sorted_properties;
   for(auto p_it = properties.begin(); p_it != properties.end(); p_it++)
     sorted_properties.push_back(p_it);
@@ -204,6 +199,17 @@ output_properties_plain(const propertiest &properties, messaget &log)
       else
         return id2string(pit1->first) < id2string(pit2->first);
     });
+  return sorted_properties;
+}
+
+static void output_properties_plain(
+  const std::vector<propertiest::const_iterator> &sorted_properties,
+  messaget &log)
+{
+  if(sorted_properties.empty())
+    return;
+
+  log.result() << "\n** Results:" << messaget::eom;
   // now show in the order we have determined
   irep_idt previous_function;
   irep_idt current_file;
@@ -253,7 +259,8 @@ void output_properties(
   {
   case ui_message_handlert::uit::PLAIN:
   {
-    output_properties_plain(properties, log);
+    const auto sorted_properties = get_sorted_properties(properties);
+    output_properties_plain(sorted_properties, log);
     output_iterations(properties, iterations, log);
     break;
   }
@@ -292,18 +299,19 @@ void output_properties_with_traces(
   {
   case ui_message_handlert::uit::PLAIN:
   {
-    output_properties_plain(properties, log);
-    for(const auto &property_pair : properties)
+    const auto sorted_properties = get_sorted_properties(properties);
+    output_properties_plain(sorted_properties, log);
+    for(const auto &property_it : sorted_properties)
     {
-      if(property_pair.second.status == property_statust::FAIL)
+      if(property_it->second.status == property_statust::FAIL)
       {
         log.result() << "\n"
-                     << "Trace for " << property_pair.first << ":"
+                     << "Trace for " << property_it->first << ":"
                      << "\n";
         show_goto_trace(
           log.result(),
           traces.get_namespace(),
-          traces[property_pair.first],
+          traces[property_it->first],
           trace_options);
         log.result() << messaget::eom;
       }

src/goto-checker/single_path_symex_checker.cpp

@@ -110,21 +110,49 @@ operator()(propertiest &properties)
   return result;
 }
 
-goto_tracet single_path_symex_checkert::build_trace() const
+goto_tracet single_path_symex_checkert::build_full_trace() const
+{
+  goto_tracet goto_trace;
+  build_goto_trace(
+    property_decider->get_equation(),
+    property_decider->get_equation().SSA_steps.end(),
+    property_decider->get_solver(),
+    ns,
+    goto_trace);
+
+  return goto_trace;
+}
+
+goto_tracet single_path_symex_checkert::build_shortest_trace() const
 {
   if(options.get_bool_option("beautify"))
   {
     counterexample_beautificationt()(
       dynamic_cast<boolbvt &>(property_decider->get_solver()),
       property_decider->get_equation());
   }
+
   goto_tracet goto_trace;
-  ::build_error_trace(
-    goto_trace,
+  build_goto_trace(
+    property_decider->get_equation(),
+    property_decider->get_solver(),
     ns,
+    goto_trace);
+
+  return goto_trace;
+}
+
+goto_tracet
+single_path_symex_checkert::build_trace(const irep_idt &property_id) const
+{
+  goto_tracet goto_trace;
+  build_goto_trace(
     property_decider->get_equation(),
+    ssa_step_matches_failing_property(property_id),
     property_decider->get_solver(),
-    ui_message_handler);
+    ns,
+    goto_trace);
+
   return goto_trace;
 }
 

src/goto-checker/single_path_symex_checker.h

@@ -34,7 +34,9 @@ class single_path_symex_checkert : public single_path_symex_only_checkert,
 
   resultt operator()(propertiest &) override;
 
-  goto_tracet build_trace() const override;
+  goto_tracet build_full_trace() const override;
+  goto_tracet build_shortest_trace() const override;
+  goto_tracet build_trace(const irep_idt &) const override;
   const namespacet &get_namespace() const override;
 
   void output_error_witness(const goto_tracet &) override;

src/goto-checker/stop_on_fail_verifier.h

@@ -50,7 +50,8 @@ class stop_on_fail_verifiert : public goto_verifiert
 
     case resultt::FAIL:
     {
-      goto_tracet goto_trace = incremental_goto_checker.build_trace();
+      message_building_error_trace(log);
+      goto_tracet goto_trace = incremental_goto_checker.build_shortest_trace();
       output_error_trace(
         goto_trace,
         incremental_goto_checker.get_namespace(),