diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 3c4e5bd57de..eec4574ff5d 100644 --- a/jbmc/unit/Makefile +++ b/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) \ diff --git a/regression/cbmc-cover/assertion1/test.desc b/regression/cbmc-cover/assertion1/test.desc index 0463c5e110c..dc140c5a2b0 100644 --- a/regression/cbmc-cover/assertion1/test.desc +++ b/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 diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 17b0f86b0ef..4a8a6931aa7 100644 --- a/src/cbmc/Makefile +++ b/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 \ diff --git a/src/cbmc/c_test_input_generator.cpp b/src/cbmc/c_test_input_generator.cpp new file mode 100644 index 00000000000..0e2e2f2a219 --- /dev/null +++ b/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 + +#include + +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include + +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; + } +} diff --git a/src/cbmc/c_test_input_generator.h b/src/cbmc/c_test_input_generator.h new file mode 100644 index 00000000000..8c139ed90c2 --- /dev/null +++ b/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 + +#include + +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 diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 1557a727fde..c431aeede89 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -73,6 +74,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#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 + 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 verifier = nullptr; if( @@ -607,6 +622,7 @@ int cbmc_parse_optionst::doit() resultt result = (*verifier)(); verifier->report(); + return result_to_exit_code(result); } diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index da5ce406e31..ea625131c9c 100644 --- a/src/goto-checker/Makefile +++ b/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 \ diff --git a/src/goto-checker/README.md b/src/goto-checker/README.md index 1f4f062d184..8c1ef5978cd 100644 --- a/src/goto-checker/README.md +++ b/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 diff --git a/src/goto-checker/cover_goals_report_util.cpp b/src/goto-checker/cover_goals_report_util.cpp new file mode 100644 index 00000000000..4804dfbada3 --- /dev/null +++ b/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 + +#include +#include +#include +#include +#include + +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); +} diff --git a/src/goto-checker/cover_goals_report_util.h b/src/goto-checker/cover_goals_report_util.h new file mode 100644 index 00000000000..1e99504ecea --- /dev/null +++ b/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 diff --git a/src/goto-checker/cover_goals_verifier_with_trace_storage.h b/src/goto-checker/cover_goals_verifier_with_trace_storage.h new file mode 100644 index 00000000000..95d058c009b --- /dev/null +++ b/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 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 diff --git a/src/goto-checker/goto_trace_storage.cpp b/src/goto-checker/goto_trace_storage.cpp index 7febf158afb..9a95ac82e6a 100644 --- a/src/goto-checker/goto_trace_storage.cpp +++ b/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_trace_storaget::all() const { return traces; diff --git a/src/goto-checker/goto_trace_storage.h b/src/goto-checker/goto_trace_storage.h index e8ff75126e0..4fdf3aaa77b 100644 --- a/src/goto-checker/goto_trace_storage.h +++ b/src/goto-checker/goto_trace_storage.h @@ -20,8 +20,12 @@ class goto_trace_storaget 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 &all() const; const goto_tracet &operator[](const irep_idt &property_id) const; diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 8d69f672de3..78afb9a66ef 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/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 goto_tracet::get_all_property_ids() const +{ + std::vector property_ids; + for(const auto &step : steps) + { + if(step.is_assert()) + property_ids.push_back(step.property_id); + } + return property_ids; +} diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 108bb52bf86..ea138c9f2e6 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -181,11 +181,14 @@ class goto_tracet // 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 get_all_property_ids() const; + // delete all steps after (not including) s void trim_after(stepst::iterator s) { diff --git a/unit/Makefile b/unit/Makefile index d6a49237bf7..1d77dccc5d5 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -95,6 +95,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) \