Merge pull request #3831 from tautschnig/function-coverage

Coverage instrumentation now passes a function identifier [blocks: #3126]

Author: tautschnig

src/goto-instrument/cover.cpp

@@ -25,12 +25,14 @@ Date: May 2016
 #include "cover_basic_blocks.h"
 
 /// Applies instrumenters to given goto program
+/// \param function_id: name of \p goto_program
 /// \param goto_program: the goto program
 /// \param instrumenters: the instrumenters
 /// \param mode: mode of the function to instrument (for instance ID_C or
 ///   ID_java)
 /// \param message_handler: a message handler
 void instrument_cover_goals(
+  const irep_idt &function_id,
   goto_programt &goto_program,
   const cover_instrumenterst &instrumenters,
   const irep_idt &mode,
@@ -42,12 +44,14 @@ void instrument_cover_goals(
                     : std::unique_ptr<cover_blocks_baset>(
                         new cover_basic_blockst(goto_program));
 
-  basic_blocks->report_block_anomalies(goto_program, message_handler);
-  instrumenters(goto_program, *basic_blocks);
+  basic_blocks->report_block_anomalies(
+    function_id, goto_program, message_handler);
+  instrumenters(function_id, goto_program, *basic_blocks);
 }
 
 /// Instruments goto program for a given coverage criterion
 /// \param symbol_table: the symbol table
+/// \param function_id: name of \p goto_program
 /// \param goto_program: the goto program
 /// \param criterion: the coverage criterion
 /// \param message_handler: a message handler
@@ -57,6 +61,7 @@ void instrument_cover_goals(
 DEPRECATED("use instrument_cover_goals(goto_programt &...) instead")
 void instrument_cover_goals(
   const symbol_tablet &symbol_table,
+  const irep_idt &function_id,
   goto_programt &goto_program,
   coverage_criteriont criterion,
   message_handlert &message_handler)
@@ -68,7 +73,7 @@ void instrument_cover_goals(
   instrumenters.add_from_criterion(criterion, symbol_table, goal_filters);
 
   instrument_cover_goals(
-    goto_program, instrumenters, ID_unknown, message_handler);
+    function_id, goto_program, instrumenters, ID_unknown, message_handler);
 }
 
 /// Create and add an instrumenter based on the given criterion
@@ -249,7 +254,7 @@ std::unique_ptr<cover_configt> get_cover_config(
 /// Instruments a single goto program based on the given configuration
 /// \param cover_config: configuration, produced using get_cover_config
 /// \param function_id: function name
-/// \param function: function function to instrument
+/// \param function: function to instrument
 /// \param message_handler: log output
 static void instrument_cover_goals(
   const cover_configt &cover_config,
@@ -281,6 +286,7 @@ static void instrument_cover_goals(
   if(cover_config.function_filters(function_id, function))
   {
     instrument_cover_goals(
+      function_id,
       function.body,
       cover_config.cover_instrumenters,
       cover_config.mode,

src/goto-instrument/cover_basic_blocks.cpp

@@ -109,6 +109,7 @@ cover_basic_blockst::source_location_of(const std::size_t block_nr) const
 }
 
 void cover_basic_blockst::report_block_anomalies(
+  const irep_idt &function_id,
   const goto_programt &goto_program,
   message_handlert &message_handler)
 {
@@ -133,7 +134,7 @@ void cover_basic_blockst::report_block_anomalies(
       block_info.source_location.is_nil())
     {
       msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
-                    << it->location_number << " " << it->function
+                    << it->location_number << " " << function_id
                     << " (missing source location)" << messaget::eom;
     }
     // The location numbers printed here are those

src/goto-instrument/cover_basic_blocks.h

@@ -43,13 +43,16 @@ class cover_blocks_baset
   virtual void output(std::ostream &out) const = 0;
 
   /// Output warnings about ignored blocks
+  /// \param function_id: name of \p goto_program
   /// \param goto_program: The goto program
   /// \param message_handler: The message handler
   virtual void report_block_anomalies(
+    const irep_idt &function_id,
     const goto_programt &goto_program,
     message_handlert &message_handler)
   {
     // unused parameters
+    (void)function_id;
     (void)goto_program;
     (void)message_handler;
   }
@@ -78,9 +81,11 @@ class cover_basic_blockst final : public cover_blocks_baset
   source_location_of(std::size_t block_nr) const override;
 
   /// Output warnings about ignored blocks
+  /// \param function_id: name of \p goto_program
   /// \param goto_program: The goto program
   /// \param message_handler: The message handler
   void report_block_anomalies(
+    const irep_idt &function_id,
     const goto_programt &goto_program,
     message_handlert &message_handler) override;
 

src/goto-instrument/cover_filter.cpp

@@ -14,24 +14,24 @@ Author: Peter Schrammel
 #include <linking/static_lifetime_init.h>
 
 /// Filter out functions that are not considered provided by the user
-/// \param identifier: a function name
+/// \param function_id: a function name
 /// \param goto_function: a goto function
 /// \return returns true if function is considered user-provided
 bool internal_functions_filtert::operator()(
-  const irep_idt &identifier,
+  const irep_idt &function_id,
   const goto_functionst::goto_functiont &goto_function) const
 {
-  if(identifier == goto_functionst::entry_point())
+  if(function_id == goto_functionst::entry_point())
     return false;
 
-  if(identifier == INITIALIZE_FUNCTION)
+  if(function_id == INITIALIZE_FUNCTION)
     return false;
 
   if(goto_function.is_hidden())
     return false;
 
   // ignore Java built-ins (synthetic functions)
-  if(has_prefix(id2string(identifier), "java::array["))
+  if(has_prefix(id2string(function_id), "java::array["))
     return false;
 
   // ignore if built-in library
@@ -44,31 +44,32 @@ bool internal_functions_filtert::operator()(
 }
 
 /// Filter functions whose name match the regex
-/// \param identifier: a function name
+/// \param function_id: a function name
 /// \param goto_function: a goto function
 /// \return returns true if the function name matches
 bool include_pattern_filtert::operator()(
-  const irep_idt &identifier,
+  const irep_idt &function_id,
   const goto_functionst::goto_functiont &goto_function) const
 {
   (void)goto_function; // unused parameter
   std::smatch string_matcher;
-  return std::regex_match(id2string(identifier), string_matcher, regex_matcher);
+  return std::regex_match(
+    id2string(function_id), string_matcher, regex_matcher);
 }
 
 /// Call a goto_program non-trivial if it has:
 ///  * Any declarations
 ///  * At least 2 branches
 ///  * At least 5 assignments
 /// These criteria are arbitrarily chosen.
-/// \param identifier: a function name
+/// \param function_id: name of \p goto_function
 /// \param goto_function: a goto function
 /// \return returns true if non-trivial
 bool trivial_functions_filtert::operator()(
-  const irep_idt &identifier,
+  const irep_idt &function_id,
   const goto_functionst::goto_functiont &goto_function) const
 {
-  (void)identifier; // unused parameter
+  (void)function_id; // unused parameter
   unsigned long count_assignments = 0, count_goto = 0;
   forall_goto_program_instructions(i_it, goto_function.body)
   {

src/goto-instrument/cover_instrument.h

@@ -37,15 +37,17 @@ class cover_instrumenter_baset
   }
 
   /// Instruments a goto program
+  /// \param function_id: name of \p goto_program
   /// \param goto_program: a goto program
   /// \param basic_blocks: detected basic blocks
   virtual void operator()(
+    const irep_idt &function_id,
     goto_programt &goto_program,
     const cover_blocks_baset &basic_blocks) const
   {
     Forall_goto_program_instructions(i_it, goto_program)
     {
-      instrument(goto_program, i_it, basic_blocks);
+      instrument(function_id, goto_program, i_it, basic_blocks);
     }
   }
 
@@ -58,20 +60,21 @@ class cover_instrumenter_baset
 
   /// Override this method to implement an instrumenter
   virtual void instrument(
+    const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const = 0;
 
   void initialize_source_location(
     goto_programt::targett t,
     const std::string &comment,
-    const irep_idt &function) const
+    const irep_idt &function_id) const
   {
     t->source_location.set_comment(comment);
     t->source_location.set(ID_coverage_criterion, coverage_criterion);
     t->source_location.set_property_class(property_class);
-    t->source_location.set_function(function);
-    t->function = function;
+    t->source_location.set_function(function_id);
+    t->function = function_id;
   }
 
   bool is_non_cover_assertion(goto_programt::const_targett t) const
@@ -91,14 +94,16 @@ class cover_instrumenterst
     const goal_filterst &);
 
   /// Applies all instrumenters to the given goto program
+  /// \param function_id: name of \p goto_program
   /// \param goto_program: a goto program
   /// \param basic_blocks: detected basic blocks of the goto program
   void operator()(
+    const irep_idt &function_id,
     goto_programt &goto_program,
     const cover_blocks_baset &basic_blocks) const
   {
     for(const auto &instrumenter : instrumenters)
-      (*instrumenter)(goto_program, basic_blocks);
+      (*instrumenter)(function_id, goto_program, basic_blocks);
   }
 
 private:
@@ -118,6 +123,7 @@ class cover_location_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -136,6 +142,7 @@ class cover_branch_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -154,6 +161,7 @@ class cover_condition_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -172,6 +180,7 @@ class cover_decision_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -190,6 +199,7 @@ class cover_mcdc_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -208,6 +218,7 @@ class cover_path_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -226,6 +237,7 @@ class cover_assertion_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -244,13 +256,14 @@ class cover_cover_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
 };
 
 void cover_instrument_end_of_function(
-  const irep_idt &function,
+  const irep_idt &function_id,
   goto_programt &goto_program);
 
 #endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H

src/goto-instrument/cover_instrument_branch.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening
 #include "cover_basic_blocks.h"
 
 void cover_branch_instrumentert::instrument(
+  const irep_idt &function_id,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
   const cover_blocks_baset &basic_blocks) const
@@ -31,7 +32,7 @@ void cover_branch_instrumentert::instrument(
     goto_programt::targett t = goto_program.insert_before(i_it);
     t->make_assertion(false_exprt());
     t->source_location = source_location;
-    initialize_source_location(t, comment, i_it->function);
+    initialize_source_location(t, comment, function_id);
   }
 
   if(
@@ -44,18 +45,17 @@ void cover_branch_instrumentert::instrument(
     std::string false_comment = "block " + b + " branch false";
 
     exprt guard = i_it->guard;
-    const irep_idt function = i_it->function;
     source_locationt source_location = i_it->source_location;
 
     goto_program.insert_before_swap(i_it);
     i_it->make_assertion(not_exprt(guard));
     i_it->source_location = source_location;
-    initialize_source_location(i_it, true_comment, function);
+    initialize_source_location(i_it, true_comment, function_id);
 
     goto_program.insert_before_swap(i_it);
     i_it->make_assertion(guard);
     i_it->source_location = source_location;
-    initialize_source_location(i_it, false_comment, function);
+    initialize_source_location(i_it, false_comment, function_id);
 
     std::advance(i_it, 2);
   }

src/goto-instrument/cover_instrument_condition.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening
 #include "cover_basic_blocks.h"
 
 void cover_condition_instrumentert::instrument(
+  const irep_idt &function_id,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
   const cover_blocks_baset &) const
@@ -33,20 +34,19 @@ void cover_condition_instrumentert::instrument(
 
     for(const auto &c : conditions)
     {
-      const std::string c_string = from_expr(ns, i_it->function, c);
+      const std::string c_string = from_expr(ns, function_id, c);
 
       const std::string comment_t = "condition `" + c_string + "' true";
-      const irep_idt function = i_it->function;
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(c);
       i_it->source_location = source_location;
-      initialize_source_location(i_it, comment_t, function);
+      initialize_source_location(i_it, comment_t, function_id);
 
       const std::string comment_f = "condition `" + c_string + "' false";
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(not_exprt(c));
       i_it->source_location = source_location;
-      initialize_source_location(i_it, comment_f, function);
+      initialize_source_location(i_it, comment_f, function_id);
     }
 
     for(std::size_t i = 0; i < conditions.size() * 2; i++)