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