Merge pull request #5714 from tautschnig/cover-trace

CBMC/JBMC --cover: only store traces with --trace to avoid memory exhaustion

Author: tautschnig

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

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$

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\)

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+)?=[^,]*)$

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;
   }

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;
     }

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,10 +44,14 @@ 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();
 }
 
-const std::vector<goto_tracet> &goto_trace_storaget::all() const
+const std::list<goto_tracet> &goto_trace_storaget::all() const
 {
   return traces;
 }
@@ -53,8 +61,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

src/goto-checker/goto_trace_storage.h

@@ -14,6 +14,10 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-programs/goto_trace.h>
 
+#include <util/merge_irep.h>
+
+#include <list>
+
 class goto_trace_storaget
 {
 public:
@@ -28,7 +32,7 @@ class goto_trace_storaget
   ///   are mapped to the given trace.
   const goto_tracet &insert_all(goto_tracet &&);
 
-  const std::vector<goto_tracet> &all() const;
+  const std::list<goto_tracet> &all() const;
   const goto_tracet &operator[](const irep_idt &property_id) const;
 
   const namespacet &get_namespace() const;
@@ -38,10 +42,13 @@ class goto_trace_storaget
   const namespacet &ns;
 
   /// stores the traces
-  std::vector<goto_tracet> traces;
+  std::list<goto_tracet> traces;
 
   // maps property ID to index in traces
   std::unordered_map<irep_idt, std::size_t> property_id_to_trace_index;
+
+  /// irep container for shared ireps
+  merge_irept merge_ireps;
 };
 
 #endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_STORAGE_H

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.

src/goto-instrument/cover.h

@@ -24,15 +24,18 @@ 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 "   \
   "CC\n"                                                                       \
   " --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
 {