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%).

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-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
 {