cbmc --symex-coverage-report: Cobertura-compatible coverage output

Author: tautschnig

src/cbmc/Makefile

@@ -2,7 +2,7 @@ SRC = cbmc_main.cpp cbmc_parse_options.cpp bmc.cpp cbmc_dimacs.cpp \
       cbmc_languages.cpp counterexample_beautification.cpp \
       bv_cbmc.cpp symex_bmc.cpp show_vcc.cpp cbmc_solvers.cpp \
       xml_interface.cpp bmc_cover.cpp all_properties.cpp \
-      fault_localization.cpp
+      fault_localization.cpp symex_coverage.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \

src/cbmc/bmc.cpp

@@ -528,6 +528,15 @@ safety_checkert::resultt bmct::run(
                    << " remaining after simplification" << eom;
     }
 
+    // coverage report
+    std::string cov_out=options.get_option("symex-coverage-report");
+    if(!cov_out.empty() &&
+       symex.output_coverage_report(goto_functions, cov_out))
+    {
+      error() << "Failed to write symex coverage report" << eom;
+      return safety_checkert::ERROR;
+    }
+
     if(options.get_bool_option("show-vcc"))
     {
       show_vcc();

src/cbmc/bmc.h

@@ -43,6 +43,8 @@ class bmct:public safety_checkert
     ui(ui_message_handlert::PLAIN)
   {
     symex.constant_propagation=options.get_bool_option("propagation");
+    symex.record_coverage=
+      !options.get_option("symex-coverage-report").empty();
   }
 
   virtual resultt run(const goto_functionst &goto_functions);

src/cbmc/cbmc_parse_options.cpp

@@ -434,6 +434,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("stop-on-fail", true);
     options.set_option("trace", true);
   }
+
+  if(cmdline.isset("symex-coverage-report"))
+    options.set_option(
+      "symex-coverage-report",
+      cmdline.get_value("symex-coverage-report"));
 }
 
 /*******************************************************************\
@@ -1086,6 +1091,7 @@ void cbmc_parse_optionst::help()
     "\n"
     "Analysis options:\n"
     " --show-properties            show the properties, but don't run analysis\n" // NOLINT(*)
+    " --symex-coverage-report f    generate a Cobertura XML coverage report in f\n"
     " --property id                only check one specific property\n"
     " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
     " --trace                      give a counterexample trace for failed properties\n" //NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -46,7 +46,7 @@ class optionst;
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \
   "(version)" \
-  "(cover):" \
+  "(cover):(symex-coverage-report):" \
   "(mm):" \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
   "(ppc-macos)(unsigned-char)" \

src/cbmc/symex_bmc.cpp

@@ -29,7 +29,9 @@ symex_bmct::symex_bmct(
   symbol_tablet &_new_symbol_table,
   symex_targett &_target):
   goto_symext(_ns, _new_symbol_table, _target),
-  max_unwind_is_set(false)
+  record_coverage(false),
+  max_unwind_is_set(false),
+  symex_coverage(_ns)
 {
 }
 
@@ -61,6 +63,10 @@ void symex_bmct::symex_step(
     last_source_location=source_location;
   }
 
+  if(record_coverage &&
+     !state.guard.is_false())
+    symex_coverage.covered(state.source.pc);
+
   goto_symext::symex_step(goto_functions, state);
 }
 

src/cbmc/symex_bmc.h

@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-symex/goto_symex.h>
 
+#include "symex_coverage.h"
+
 class symex_bmct:
   public goto_symext,
   public messaget
@@ -49,6 +51,15 @@ class symex_bmct:
     loop_limits[id]=limit;
   }
 
+  bool output_coverage_report(
+    const goto_functionst &goto_functions,
+    const std::string &path) const
+  {
+    return symex_coverage.generate_report(goto_functions, path);
+  }
+
+  bool record_coverage;
+
 protected:
   // We have
   // 1) a global limit (max_unwind)
@@ -85,6 +96,8 @@ class symex_bmct:
   virtual void no_body(const irep_idt &identifier);
 
   std::unordered_set<irep_idt, irep_id_hash> body_warnings;
+
+  symex_coveraget symex_coverage;
 };
 
 #endif // CPROVER_CBMC_SYMEX_BMC_H