beginnings of instrumentation-based coverage

Author: Daniel Kroening

src/cbmc/Makefile

@@ -19,6 +19,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../pointer-analysis/goto_program_dereference$(OBJEXT) \
       ../goto-instrument/full_slicer$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
+      ../goto-instrument/cover$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \

src/cbmc/cbmc_parse_options.cpp

@@ -37,9 +37,11 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/string_instrumentation.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/link_to_library.h>
+#include <goto-programs/remove_skip.h>
 
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
+#include <goto-instrument/cover.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
 
@@ -909,16 +911,43 @@ bool cbmc_parse_optionst::process_goto_program(
 
     // recalculate numbers, etc.
     goto_functions.update();
-
+    
     // add loop ids
     goto_functions.compute_loop_numbers();
 
-    // if we aim to cover assertions, replace
-    // all assertions by false to prevent simplification
+    // instrument cover goals
 
-    if(cmdline.isset("cover") &&
-       cmdline.get_value("cover")=="assertions")
-      make_assertions_false(goto_functions);
+    if(cmdline.isset("cover"))
+    {
+      std::string criterion=cmdline.get_value("cover");
+      
+      coverage_criteriont c;
+
+      if(criterion=="assertion" || criterion=="assertions")
+        c=coverage_criteriont::ASSERTION;
+      else if(criterion=="path" || criterion=="paths")
+        c=coverage_criteriont::PATH;
+      else if(criterion=="branch" || criterion=="branches")
+        c=coverage_criteriont::BRANCH;
+      else if(criterion=="location" || criterion=="locations")
+        c=coverage_criteriont::LOCATION;
+      else if(criterion=="decision" || criterion=="decisions")
+        c=coverage_criteriont::DECISION;
+      else if(criterion=="condition" || criterion=="conditions")
+        c=coverage_criteriont::CONDITION;
+      else if(criterion=="mcdc")
+        c=coverage_criteriont::MCDC;
+      else
+      {
+        error() << "unknown coverage criterion" << eom;
+        return false;
+      }
+          
+      instrument_cover_goals(symbol_table, goto_functions, c);
+    }
+      
+    // remove skips
+    remove_skip(goto_functions);
 
     // show it?
     if(cmdline.isset("show-loops"))

src/goto-instrument/Makefile

@@ -23,7 +23,7 @@ SRC = goto_instrument_parse_options.cpp rw_set.cpp \
       wmm/event_graph.cpp wmm/pair_collection.cpp \
       goto_instrument_main.cpp horn_encoding.cpp \
       thread_instrumentation.cpp skip_loops.cpp loop_utils.cpp \
-      code_contracts.cpp
+      code_contracts.cpp cover.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \

src/goto-instrument/cover.cpp

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Coverage Instrumentation
+
+Author: Daniel Kroening
+
+Date: May 2016
+
+\*******************************************************************/
+
+#include "cover.h"
+
+void instrument_cover_goals(
+  const symbol_tablet &symbol_table,
+  goto_programt &goto_program,
+  coverage_criteriont criterion)
+{
+}
+
+void instrument_cover_goals(
+  const symbol_tablet &symbol_table,
+  goto_functionst &goto_functions,
+  coverage_criteriont criterion)
+{
+}

src/goto-instrument/cover.h

@@ -0,0 +1,30 @@
+/*******************************************************************\
+
+Module: Coverage Instrumentation
+
+Author: Daniel Kroening
+
+Date: May 2016
+
+\*******************************************************************/
+
+#ifndef CPROVER_COVER_H
+#define CPROVER_COVER_H
+
+#include <goto-programs/goto_model.h>
+
+enum class coverage_criteriont {
+  LOCATION, BRANCH, DECISION, CONDITION,
+  PATH, MCDC, ASSERTION };
+
+void instrument_cover_goals(
+  const symbol_tablet &symbol_table,
+  goto_programt &goto_program,
+  coverage_criteriont);
+
+void instrument_cover_goals(
+  const symbol_tablet &symbol_table,
+  goto_functionst &goto_functions,
+  coverage_criteriont);
+
+#endif

src/goto-programs/goto_convert_functions.cpp

@@ -17,7 +17,6 @@ Date: June 2003
 
 #include "goto_convert_functions.h"
 #include "goto_inline.h"
-#include "remove_skip.h"
 
 /*******************************************************************\
 
@@ -294,11 +293,6 @@ void goto_convert_functionst::convert_function(const irep_idt &identifier)
   Forall_goto_program_instructions(i_it, f.body)
     i_it->function=identifier;
 
-  // remove_skip depends on the target numbers
-  f.body.compute_target_numbers();
-
-  remove_skip(f.body);
-
   f.body.update();
 
   if(hide(f.body))

src/goto-programs/remove_skip.cpp

@@ -41,8 +41,10 @@ static bool is_skip(goto_programt::instructionst::iterator it)
     goto_programt::instructionst::iterator next_it=it;
     next_it++;
 
-    // a branch to the next instruction is a skip
-    return it->targets.front()==next_it;
+    // A branch to the next instruction is a skip
+    // We also require the guard to be 'true'
+    return it->guard.is_true() &&
+           it->targets.front()==next_it;
   }
 
   if(it->is_other())