From 4743cb93d9453ab5cdb0e25c876aaefd6bd0ece2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 3 Jan 2021 17:07:43 +0000 Subject: [PATCH 1/3] goto trace storage: use a list instead of a vector goto traces consume a lot of memory, and re-allocating them for each incremental addition of a goto trace does not seem to be a good approach. This is at the expense of more costly indexed access, which now requires iterator increments. --- src/goto-checker/goto_trace_storage.cpp | 5 +++-- src/goto-checker/goto_trace_storage.h | 6 ++++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/goto-checker/goto_trace_storage.cpp b/src/goto-checker/goto_trace_storage.cpp index 38f01afd12f..da54751ae7f 100644 --- a/src/goto-checker/goto_trace_storage.cpp +++ b/src/goto-checker/goto_trace_storage.cpp @@ -43,7 +43,7 @@ const goto_tracet &goto_trace_storaget::insert_all(goto_tracet &&trace) return traces.back(); } -const std::vector &goto_trace_storaget::all() const +const std::list &goto_trace_storaget::all() const { return traces; } @@ -53,8 +53,9 @@ operator[](const irep_idt &property_id) const { const auto trace_found = property_id_to_trace_index.find(property_id); PRECONDITION(trace_found != property_id_to_trace_index.end()); + CHECK_RETURN(trace_found->second < traces.size()); - return traces.at(trace_found->second); + return *(std::next(traces.begin(), trace_found->second)); } const namespacet &goto_trace_storaget::get_namespace() const diff --git a/src/goto-checker/goto_trace_storage.h b/src/goto-checker/goto_trace_storage.h index 52d0cd1d1de..51a131bbf83 100644 --- a/src/goto-checker/goto_trace_storage.h +++ b/src/goto-checker/goto_trace_storage.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, Peter Schrammel #include +#include + class goto_trace_storaget { public: @@ -28,7 +30,7 @@ class goto_trace_storaget /// are mapped to the given trace. const goto_tracet &insert_all(goto_tracet &&); - const std::vector &all() const; + const std::list &all() const; const goto_tracet &operator[](const irep_idt &property_id) const; const namespacet &get_namespace() const; @@ -38,7 +40,7 @@ class goto_trace_storaget const namespacet &ns; /// stores the traces - std::vector traces; + std::list traces; // maps property ID to index in traces std::unordered_map property_id_to_trace_index; From e4d4ff44edb8c8abcad9429eb8c8ac01f135cd0f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 19 Jan 2021 12:34:16 +0000 Subject: [PATCH 2/3] Enable merge_ireps for goto traces A goto trace includes freshly constructed expressions, which thus lack sharing. This results in excessive memory use when storing multiple traces, as is done for coverage computation. On a particular benchmark, coverage computation previously ran out of memory at 768 GB. This same benchmark can now be run with just 80 GB of memory. --- src/goto-checker/goto_trace_storage.cpp | 8 ++++++++ src/goto-checker/goto_trace_storage.h | 5 +++++ src/goto-programs/goto_trace.cpp | 15 +++++++++++++++ src/goto-programs/goto_trace.h | 6 ++++++ 4 files changed, 34 insertions(+) diff --git a/src/goto-checker/goto_trace_storage.cpp b/src/goto-checker/goto_trace_storage.cpp index da54751ae7f..dfb8c572080 100644 --- a/src/goto-checker/goto_trace_storage.cpp +++ b/src/goto-checker/goto_trace_storage.cpp @@ -27,6 +27,10 @@ const goto_tracet &goto_trace_storaget::insert(goto_tracet &&trace) emplace_result.second, "cannot associate more than one error trace with property " + id2string(last_step.property_id)); + + for(auto &step : traces.back().steps) + step.merge_ireps(merge_ireps); + return traces.back(); } @@ -40,6 +44,10 @@ const goto_tracet &goto_trace_storaget::insert_all(goto_tracet &&trace) { property_id_to_trace_index.emplace(property_id, traces.size() - 1); } + + for(auto &step : traces.back().steps) + step.merge_ireps(merge_ireps); + return traces.back(); } diff --git a/src/goto-checker/goto_trace_storage.h b/src/goto-checker/goto_trace_storage.h index 51a131bbf83..36c1596fdc3 100644 --- a/src/goto-checker/goto_trace_storage.h +++ b/src/goto-checker/goto_trace_storage.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, Peter Schrammel #include +#include + #include class goto_trace_storaget @@ -44,6 +46,9 @@ class goto_trace_storaget // maps property ID to index in traces std::unordered_map property_id_to_trace_index; + + /// irep container for shared ireps + merge_irept merge_ireps; }; #endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 581028eaa3b..1d9152571d9 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening #include #include #include +#include #include #include #include @@ -133,6 +134,20 @@ void goto_trace_stept::output( out << '\n'; } + +void goto_trace_stept::merge_ireps(merge_irept &dest) +{ + dest(cond_expr); + dest(full_lhs); + dest(full_lhs_value); + + for(auto &io_arg : io_args) + dest(io_arg); + + for(auto &function_arg : function_arguments) + dest(function_arg); +} + /// Returns the numeric representation of an expression, based on /// options. The default is binary without a base-prefix. Setting /// options.hex_representation to be true outputs hex format. Setting diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 1d6e63904a5..d499ef98546 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -24,6 +24,8 @@ Date: July 2005 #include +class merge_irept; + /// Step of the trace of a GOTO program /// /// A step is either: @@ -162,6 +164,10 @@ class goto_trace_stept full_lhs_value.make_nil(); cond_expr.make_nil(); } + + /// Use \p dest to establish sharing among ireps. + /// \param [out] dest: irep storage container. + void merge_ireps(merge_irept &dest); }; /// Trace of a GOTO program. From 87e844067843b464db5ecfcae9fec673fd82c87e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Jan 2021 23:33:15 +0000 Subject: [PATCH 3/3] CBMC --cover: only store traces with --show-test-suite Not everyone needs test inputs, especially when programs lack INPUT instructions anyway. Test inputs are found via goto traces, and computing those is expensive in both time and memory required. On one benchmark, not building goto traces reduced the overall time from 36000 seconds to 2800 seconds (a saving of 92%). --- doc/cprover-manual/test-suite.md | 5 +++-- regression/cbmc-cover/branch-loop1/test.desc | 2 +- .../pointer-function-parameters-2/test.desc | 2 +- .../cbmc-cover/pointer-function-parameters/test.desc | 2 +- src/cbmc/cbmc_parse_options.cpp | 7 +++++-- .../cover_goals_verifier_with_trace_storage.h | 11 ++++++++--- src/goto-instrument/cover.cpp | 2 ++ src/goto-instrument/cover.h | 7 +++++-- 8 files changed, 26 insertions(+), 12 deletions(-) diff --git a/doc/cprover-manual/test-suite.md b/doc/cprover-manual/test-suite.md index 2bbcc2f6274..31765b61055 100644 --- a/doc/cprover-manual/test-suite.md +++ b/doc/cprover-manual/test-suite.md @@ -128,10 +128,11 @@ and outputs of interest for generating test suites. To demonstrate the automatic test suite generation in CBMC, we call the following command: - cbmc pid.c --cover mcdc --unwind 6 --xml-ui + cbmc pid.c --cover mcdc --show-test-suite --unwind 6 --xml-ui We'll describe those command line options one by one. The option `--cover mcdc` -specifies the code coverage criterion. There +specifies the code coverage criterion, and --show-test-suite requests that a +test suite be printed. There are four conditional statements in the PID function: in lines 41, 44, 48, and 49. To satisfy MC/DC, the test suite has to meet multiple requirements. For instance, each conditional statement needs to diff --git a/regression/cbmc-cover/branch-loop1/test.desc b/regression/cbmc-cover/branch-loop1/test.desc index 978d1bd0aee..24e8813872b 100644 --- a/regression/cbmc-cover/branch-loop1/test.desc +++ b/regression/cbmc-cover/branch-loop1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---xml-ui --cover branch +--xml-ui --cover branch --show-test-suite activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-cover/pointer-function-parameters-2/test.desc b/regression/cbmc-cover/pointer-function-parameters-2/test.desc index 60a0c1b3785..c107c04e1ce 100644 --- a/regression/cbmc-cover/pointer-function-parameters-2/test.desc +++ b/regression/cbmc-cover/pointer-function-parameters-2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---function fun --cover branch +--function fun --cover branch --show-test-suite ^\*\* 7 of 7 covered \(100.0%\)$ ^Test suite:$ a=\(\(signed int \*\*\)NULL\) diff --git a/regression/cbmc-cover/pointer-function-parameters/test.desc b/regression/cbmc-cover/pointer-function-parameters/test.desc index 46e8ef03507..3f159e8234b 100644 --- a/regression/cbmc-cover/pointer-function-parameters/test.desc +++ b/regression/cbmc-cover/pointer-function-parameters/test.desc @@ -1,6 +1,6 @@ CORE main.c ---function fun --cover branch +--function fun --cover branch --show-test-suite ^\*\* 5 of 5 covered \(100\.0%\)$ ^Test suite:$ ^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 48ff28ae69e..d9f6a884ba2 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -726,8 +726,11 @@ int cbmc_parse_optionst::doit() (void)verifier(); verifier.report(); - c_test_input_generatort test_generator(ui_message_handler, options); - test_generator(verifier.get_traces()); + if(options.get_bool_option("show-test-suite")) + { + c_test_input_generatort test_generator(ui_message_handler, options); + test_generator(verifier.get_traces()); + } return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-checker/cover_goals_verifier_with_trace_storage.h b/src/goto-checker/cover_goals_verifier_with_trace_storage.h index 771b18812be..ff62445d81d 100644 --- a/src/goto-checker/cover_goals_verifier_with_trace_storage.h +++ b/src/goto-checker/cover_goals_verifier_with_trace_storage.h @@ -41,9 +41,14 @@ class cover_goals_verifier_with_trace_storaget : public goto_verifiert 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 - message_building_error_trace(log); - (void)traces.insert_all(incremental_goto_checker.build_full_trace()); + if( + options.get_bool_option("show-test-suite") || + options.get_bool_option("trace")) + { + // we've got a trace; store it and link it to the covered goals + message_building_error_trace(log); + (void)traces.insert_all(incremental_goto_checker.build_full_trace()); + } ++iterations; } diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 3103f3e3269..a03ba66d9e1 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -166,6 +166,8 @@ void parse_cover_options(const cmdlinet &cmdline, optionst &options) cmdline.isset("cover-traces-must-terminate")); options.set_option( "cover-failed-assertions", cmdline.isset("cover-failed-assertions")); + + options.set_option("show-test-suite", cmdline.isset("show-test-suite")); } /// Build data structures controlling coverage from command-line options. diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 585dede7674..82da5193c40 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -24,7 +24,8 @@ class optionst; #define OPT_COVER \ "(cover):" \ - "(cover-failed-assertions)" + "(cover-failed-assertions)" \ + "(show-test-suite)" #define HELP_COVER \ " --cover CC create test-suite with coverage criterion " \ @@ -32,7 +33,9 @@ class optionst; " --cover-failed-assertions do not stop coverage checking at failed " \ "assertions\n" \ " (this is the default for --cover " \ - "assertions)\n" + "assertions)\n" \ + " --show-test-suite print test suite for coverage criterion " \ + "(requires --cover)" enum class coverage_criteriont {