Merge pull request #3968 from peterschrammel/cover-verifier

Add cover goals verifier [blocks: 3969]

jbmc/unit/Makefile

@@ -85,9 +85,7 @@ java-testing-utils-clean:
 BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \
           $(CPROVER_DIR)/src/jsil/expr2jsil$(OBJEXT) \
           $(CPROVER_DIR)/src/jsil/jsil_convert$(OBJEXT) \
           $(CPROVER_DIR)/src/jsil/jsil_entry_point$(OBJEXT) \

regression/cbmc-cover/assertion1/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover assertion
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 9 function main: SATISFIED$
-^\[main.coverage.2\] file main.c line 13 function main: SATISFIED$
+^\[main.coverage.1\] file main.c line 9 function main assertion: SATISFIED$
+^\[main.coverage.2\] file main.c line 13 function main assertion: SATISFIED$
 --
 ^warning: ignoring

src/cbmc/Makefile

@@ -1,6 +1,7 @@
 SRC = all_properties.cpp \
       bmc.cpp \
       bmc_cover.cpp \
+      c_test_input_generator.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
       cbmc_parse_options.cpp \

src/cbmc/c_test_input_generator.cpp

@@ -0,0 +1,164 @@
+/*******************************************************************\
+
+Module: Test Input Generator for C
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Test Input Generator for C
+
+#include "c_test_input_generator.h"
+
+#include <goto-checker/goto_trace_storage.h>
+
+#include <langapi/language_util.h>
+
+#include <util/json.h>
+#include <util/json_irep.h>
+#include <util/options.h>
+#include <util/string_utils.h>
+#include <util/xml.h>
+#include <util/xml_irep.h>
+
+#include <goto-programs/json_expr.h>
+#include <goto-programs/json_goto_trace.h>
+#include <goto-programs/xml_expr.h>
+#include <goto-programs/xml_goto_trace.h>
+
+c_test_input_generatort::c_test_input_generatort(
+  ui_message_handlert &ui_message_handler,
+  const optionst &options)
+  : ui_message_handler(ui_message_handler), options(options)
+{
+}
+
+void test_inputst::output_plain_text(
+  std::ostream &out,
+  const namespacet &ns,
+  const goto_tracet &goto_trace) const
+{
+  const auto input_assignments =
+    make_range(goto_trace.steps)
+      .filter([](const goto_trace_stept &step) { return step.is_input(); })
+      .map([ns](const goto_trace_stept &step) {
+        return id2string(step.io_id) + '=' +
+               from_expr(ns, step.function_id, step.io_args.front());
+      });
+  join_strings(out, input_assignments.begin(), input_assignments.end(), ", ");
+  out << '\n';
+}
+
+json_objectt test_inputst::to_json(
+  const namespacet &ns,
+  const goto_tracet &goto_trace,
+  bool print_trace) const
+{
+  json_objectt json_result;
+  json_arrayt &json_inputs = json_result["inputs"].make_array();
+
+  for(const auto &step : goto_trace.steps)
+  {
+    if(step.is_input())
+    {
+      json_objectt json_input({{"id", json_stringt(step.io_id)}});
+      if(step.io_args.size() == 1)
+        json_input["value"] =
+          json(step.io_args.front(), ns, ns.lookup(step.function_id).mode);
+      json_inputs.push_back(std::move(json_input));
+    }
+  }
+
+  json_arrayt goal_refs;
+  for(const auto &goal_id : goto_trace.get_all_property_ids())
+  {
+    goal_refs.push_back(json_stringt(goal_id));
+  }
+  json_result["coveredGoals"] = std::move(goal_refs);
+  return json_result;
+}
+
+xmlt test_inputst::to_xml(
+  const namespacet &ns,
+  const goto_tracet &goto_trace,
+  bool print_trace) const
+{
+  xmlt xml_result("test");
+  if(print_trace)
+  {
+    convert(ns, goto_trace, xml_result.new_element());
+  }
+  else
+  {
+    xmlt &xml_test = xml_result.new_element("inputs");
+
+    for(const auto &step : goto_trace.steps)
+    {
+      if(step.is_input())
+      {
+        xmlt &xml_input = xml_test.new_element("input");
+        xml_input.set_attribute("id", id2string(step.io_id));
+        if(step.io_args.size() == 1)
+          xml_input.new_element("value") = xml(step.io_args.front(), ns);
+      }
+    }
+  }
+
+  for(const auto &goal_id : goto_trace.get_all_property_ids())
+  {
+    xmlt &xml_goal = xml_result.new_element("goal");
+    xml_goal.set_attribute("id", id2string(goal_id));
+  }
+
+  return xml_result;
+}
+
+test_inputst c_test_input_generatort::
+operator()(const goto_tracet &goto_trace, const namespacet &ns)
+{
+  test_inputst test_inputs;
+  return test_inputs;
+}
+
+void c_test_input_generatort::operator()(const goto_trace_storaget &traces)
+{
+  const namespacet &ns = traces.get_namespace();
+  const bool print_trace = options.get_bool_option("trace");
+  messaget log(ui_message_handler);
+  switch(ui_message_handler.get_ui())
+  {
+  case ui_message_handlert::uit::PLAIN:
+    log.result() << "\nTest suite:\n";
+    for(const auto trace : traces.all())
+    {
+      test_inputst test_inputs = (*this)(trace, ns);
+      test_inputs.output_plain_text(log.result(), ns, trace);
+    }
+    log.result() << messaget::eom;
+    break;
+  case ui_message_handlert::uit::JSON_UI:
+  {
+    if(log.status().tellp() > 0)
+      log.status() << messaget::eom; // force end of previous message
+    json_stream_objectt &json_result =
+      ui_message_handler.get_json_stream().push_back_stream_object();
+    json_stream_arrayt &tests_array =
+      json_result.push_back_stream_array("tests");
+
+    for(const auto trace : traces.all())
+    {
+      test_inputst test_inputs = (*this)(trace, ns);
+      tests_array.push_back(test_inputs.to_json(ns, trace, print_trace));
+    }
+    break;
+  }
+  case ui_message_handlert::uit::XML_UI:
+    for(const auto trace : traces.all())
+    {
+      test_inputst test_inputs = (*this)(trace, ns);
+      log.result() << test_inputs.to_xml(ns, trace, print_trace);
+    }
+    break;
+  }
+}

src/cbmc/c_test_input_generator.h

@@ -0,0 +1,67 @@
+/*******************************************************************\
+
+Module: Test Input Generator for C
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Test Input Generator for C
+
+#ifndef CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
+#define CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
+
+#include <iosfwd>
+
+#include <util/ui_message.h>
+
+class goto_tracet;
+class goto_trace_storaget;
+class json_objectt;
+class namespacet;
+class optionst;
+
+class test_inputst
+{
+public:
+  /// Outputs the test inputs in plain text format
+  void output_plain_text(
+    std::ostream &out,
+    const namespacet &ns,
+    const goto_tracet &goto_trace) const;
+
+  /// Returns the test inputs in JSON format
+  /// including the trace if desired
+  json_objectt to_json(
+    const namespacet &ns,
+    const goto_tracet &goto_trace,
+    bool print_trace) const;
+
+  /// Returns the test inputs in XML format
+  /// including the trace if desired
+  xmlt to_xml(
+    const namespacet &ns,
+    const goto_tracet &goto_trace,
+    bool print_trace) const;
+};
+
+class c_test_input_generatort
+{
+public:
+  c_test_input_generatort(
+    ui_message_handlert &ui_message_handler,
+    const optionst &options);
+
+  /// Extracts test inputs for all traces and outputs them
+  void operator()(const goto_trace_storaget &);
+
+protected:
+  ui_message_handlert &ui_message_handler;
+  const optionst &options;
+
+  /// Extracts test inputs from the given \p goto_trace
+  test_inputst operator()(const goto_tracet &goto_trace, const namespacet &ns);
+};
+
+#endif // CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H

src/cbmc/cbmc_parse_options.cpp

@@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-checker/all_properties_verifier.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>
 #include <goto-checker/multi_path_symex_checker.h>
 #include <goto-checker/multi_path_symex_only_checker.h>
 #include <goto-checker/properties.h>
@@ -73,6 +74,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/mode.h>
 
+#include "c_test_input_generator.h"
 #include "xml_interface.h"
 
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
@@ -578,6 +580,19 @@ int cbmc_parse_optionst::doit()
     }
   }
 
+  if(options.is_set("cover"))
+  {
+    cover_goals_verifier_with_trace_storaget<multi_path_symex_checkert>
+      verifier(options, ui_message_handler, goto_model);
+    (void)verifier();
+    verifier.report();
+
+    c_test_input_generatort test_generator(ui_message_handler, options);
+    test_generator(verifier.get_traces());
+
+    return CPROVER_EXIT_SUCCESS;
+  }
+
   std::unique_ptr<goto_verifiert> verifier = nullptr;
 
   if(
@@ -607,6 +622,7 @@ int cbmc_parse_optionst::doit()
 
   resultt result = (*verifier)();
   verifier->report();
+
   return result_to_exit_code(result);
 }
 

src/goto-checker/Makefile

@@ -1,5 +1,6 @@
 SRC = bmc_util.cpp \
       counterexample_beautification.cpp \
+      cover_goals_report_util.cpp \
       incremental_goto_checker.cpp \
       goto_trace_storage.cpp \
       goto_verifier.cpp \

src/goto-checker/README.md

@@ -62,6 +62,12 @@ There are the following variants of goto verifiers at the moment:
   \ref all_properties_verifier_with_trace_storaget,
   \ref all_properties_verifiert does not require to store any traces.
   A trace ends at a violated property.
+* \ref cover_goals_verifier_with_trace_storaget : Determines the status of
+  all properties, but full traces with potentially several failing properties
+  (e.g. coverage goals) are stored and results reported after the
+  verification algorithm has terminated.
+  The reporting uses 'goals' rather than 'property' terminology. I.e.
+  a failing property means 'success' and a passing property 'failed'.
 
 There are the following variants of incremental goto checkers at the moment:
 * \ref multi_path_symex_checkert : The default mode of goto-symex. It explores

src/goto-checker/cover_goals_report_util.cpp

@@ -0,0 +1,136 @@
+/*******************************************************************\
+
+Module: Cover Goals Reporting Utilities
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Cover Goals Reporting Utilities
+
+#include "cover_goals_report_util.h"
+
+#include <iomanip>
+
+#include <util/json.h>
+#include <util/json_irep.h>
+#include <util/ui_message.h>
+#include <util/xml.h>
+#include <util/xml_irep.h>
+
+static void output_goals_iterations(
+  const propertiest &properties,
+  unsigned iterations,
+  messaget &log)
+{
+  const std::size_t goals_covered =
+    count_properties(properties, property_statust::FAIL);
+  log.status() << "** " << goals_covered << " of " << properties.size()
+               << " covered (" << std::fixed << std::setw(1)
+               << std::setprecision(1)
+               << (properties.empty()
+                     ? 100.0
+                     : 100.0 * goals_covered / properties.size())
+               << "%)" << messaget::eom;
+  log.statistics() << "** Used " << iterations << " iteration"
+                   << (iterations == 1 ? "" : "s") << messaget::eom;
+}
+
+static void output_goals_plain(const propertiest &properties, messaget &log)
+{
+  log.result() << "\n** coverage results:" << messaget::eom;
+
+  for(const auto &property_pair : properties)
+  {
+    log.result() << "[" << property_pair.first << "]";
+
+    if(property_pair.second.pc->source_location.is_not_nil())
+      log.result() << ' ' << property_pair.second.pc->source_location;
+
+    if(!property_pair.second.description.empty())
+      log.result() << ' ' << property_pair.second.description;
+
+    log.result() << ": "
+                 << (property_pair.second.status == property_statust::FAIL
+                       ? "SATISFIED"
+                       : "FAILED")
+                 << '\n';
+  }
+
+  log.result() << messaget::eom;
+}
+
+static void output_goals_xml(const propertiest &properties, messaget &log)
+{
+  for(const auto &property_pair : properties)
+  {
+    xmlt xml_result(
+      "goal",
+      {{"id", id2string(property_pair.first)},
+       {"description", property_pair.second.description},
+       {"status",
+        property_pair.second.status == property_statust::FAIL ? "SATISFIED"
+                                                              : "FAILED"}},
+      {});
+
+    if(property_pair.second.pc->source_location.is_not_nil())
+      xml_result.new_element() = xml(property_pair.second.pc->source_location);
+
+    log.result() << xml_result;
+  }
+}
+
+static void output_goals_json(
+  const propertiest &properties,
+  messaget &log,
+  ui_message_handlert &ui_message_handler)
+{
+  if(log.status().tellp() > 0)
+    log.status() << messaget::eom; // force end of previous message
+  json_stream_objectt &json_result =
+    ui_message_handler.get_json_stream().push_back_stream_object();
+  for(const auto &property_pair : properties)
+  {
+    const property_infot &property_info = property_pair.second;
+
+    json_result["status"] = json_stringt(
+      property_info.status == property_statust::FAIL ? "satisfied" : "failed");
+    json_result["goal"] = json_stringt(property_pair.first);
+    json_result["description"] = json_stringt(property_info.description);
+
+    if(property_info.pc->source_location.is_not_nil())
+      json_result["sourceLocation"] = json(property_info.pc->source_location);
+  }
+  json_result["totalGoals"] = json_numbert(std::to_string(properties.size()));
+  const std::size_t goals_covered =
+    count_properties(properties, property_statust::FAIL);
+  json_result["goalsCovered"] = json_numbert(std::to_string(goals_covered));
+}
+
+void output_goals(
+  const propertiest &properties,
+  unsigned iterations,
+  ui_message_handlert &ui_message_handler)
+{
+  messaget log(ui_message_handler);
+  switch(ui_message_handler.get_ui())
+  {
+  case ui_message_handlert::uit::PLAIN:
+  {
+    output_goals_plain(properties, log);
+    break;
+  }
+  case ui_message_handlert::uit::XML_UI:
+  {
+    output_goals_xml(properties, log);
+    break;
+  }
+  case ui_message_handlert::uit::JSON_UI:
+  {
+    output_goals_json(properties, log, ui_message_handler);
+    break;
+  }
+  }
+  output_goals_iterations(properties, iterations, log);
+}

src/goto-checker/cover_goals_report_util.h

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Cover Goals Reporting Utilities
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Cover Goals Reporting Utilities
+
+#ifndef CPROVER_GOTO_CHECKER_COVER_GOALS_REPORT_UTIL_H
+#define CPROVER_GOTO_CHECKER_COVER_GOALS_REPORT_UTIL_H
+
+#include "properties.h"
+
+class ui_message_handlert;
+
+/// Outputs the \p properties interpreted as 'coverage goals'
+/// and the number of goto verifier \p iterations that
+/// were required to compute the properties' status
+void output_goals(
+  const propertiest &properties,
+  unsigned iterations,
+  ui_message_handlert &ui_message_handler);
+
+#endif // CPROVER_GOTO_CHECKER_COVER_GOALS_REPORT_UTIL_H

src/goto-checker/cover_goals_verifier_with_trace_storage.h

@@ -0,0 +1,69 @@
+/*******************************************************************\
+
+Module: Goto Verifier for Covering Goals that stores Traces
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto verifier for covering goals that stores traces
+
+#ifndef CPROVER_GOTO_CHECKER_COVER_GOALS_VERIFIER_WITH_TRACE_STORAGE_H
+#define CPROVER_GOTO_CHECKER_COVER_GOALS_VERIFIER_WITH_TRACE_STORAGE_H
+
+#include "goto_verifier.h"
+
+#include "cover_goals_report_util.h"
+#include "goto_trace_storage.h"
+#include "incremental_goto_checker.h"
+#include "properties.h"
+
+template <class incremental_goto_checkerT>
+class cover_goals_verifier_with_trace_storaget : public goto_verifiert
+{
+public:
+  cover_goals_verifier_with_trace_storaget(
+    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(incremental_goto_checker(properties).progress !=
+          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());
+
+      ++iterations;
+    }
+
+    return determine_result(properties);
+  }
+
+  void report() override
+  {
+    output_goals(properties, iterations, ui_message_handler);
+  }
+
+  const goto_trace_storaget &get_traces() const
+  {
+    return traces;
+  }
+
+protected:
+  abstract_goto_modelt &goto_model;
+  incremental_goto_checkerT incremental_goto_checker;
+  unsigned iterations = 1;
+  goto_trace_storaget traces;
+};
+
+#endif // CPROVER_GOTO_CHECKER_COVER_GOALS_VERIFIER_WITH_TRACE_STORAGE_H

src/goto-checker/goto_trace_storage.cpp

@@ -17,7 +17,7 @@ goto_trace_storaget::goto_trace_storaget(const namespacet &ns) : ns(ns)
 
 const goto_tracet &goto_trace_storaget::insert(goto_tracet &&trace)
 {
-  traces.push_back(trace);
+  traces.push_back(std::move(trace));
   const auto &last_step = traces.back().get_last_step();
   DATA_INVARIANT(
     last_step.is_assert(), "last goto trace step expected to be assertion");
@@ -25,6 +25,19 @@ const goto_tracet &goto_trace_storaget::insert(goto_tracet &&trace)
   return traces.back();
 }
 
+const goto_tracet &goto_trace_storaget::insert_all(goto_tracet &&trace)
+{
+  traces.push_back(std::move(trace));
+  const auto &all_property_ids = traces.back().get_all_property_ids();
+  DATA_INVARIANT(
+    !all_property_ids.empty(), "a trace must violate at least one assertion");
+  for(const auto &property_id : all_property_ids)
+  {
+    property_id_to_trace_index.emplace(property_id, traces.size() - 1);
+  }
+  return traces.back();
+}
+
 const std::vector<goto_tracet> &goto_trace_storaget::all() const
 {
   return traces;

src/goto-checker/goto_trace_storage.h

@@ -20,8 +20,12 @@ public:
   explicit goto_trace_storaget(const namespacet &);
   goto_trace_storaget(const goto_trace_storaget &) = delete;
 
+  /// Store trace that ends in a violated assertion
   const goto_tracet &insert(goto_tracet &&);
 
+  /// Store trace that contains multiple violated assertions
+  const goto_tracet &insert_all(goto_tracet &&);
+
   const std::vector<goto_tracet> &all() const;
   const goto_tracet &operator[](const irep_idt &property_id) const;
 

src/goto-programs/goto_trace.cpp

@@ -777,3 +777,14 @@ void show_goto_trace(
 }
 
 const trace_optionst trace_optionst::default_options = trace_optionst();
+
+std::vector<irep_idt> goto_tracet::get_all_property_ids() const
+{
+  std::vector<irep_idt> property_ids;
+  for(const auto &step : steps)
+  {
+    if(step.is_assert())
+      property_ids.push_back(step.property_id);
+  }
+  return property_ids;
+}

src/goto-programs/goto_trace.h

@@ -181,11 +181,14 @@ public:
 
   // retrieves the final step in the trace for manipulation
   // (used to fill a trace from code, hence non-const)
-  inline goto_trace_stept &get_last_step()
+  goto_trace_stept &get_last_step()
   {
     return steps.back();
   }
 
+  /// Returns the property IDs of all assertions in the trace
+  std::vector<irep_idt> get_all_property_ids() const;
+
   // delete all steps after (not including) s
   void trim_after(stepst::iterator s)
   {

unit/Makefile

@@ -96,6 +96,7 @@ testing-utils-clean:
 BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
           ../src/cbmc/bmc$(OBJEXT) \
           ../src/cbmc/bmc_cover$(OBJEXT) \
+          ../src/cbmc/c_test_input_generator$(OBJEXT) \
           ../src/cbmc/cbmc_languages$(OBJEXT) \
           ../src/cbmc/cbmc_parse_options$(OBJEXT) \
           ../src/cbmc/fault_localization$(OBJEXT) \