Refactor function filter for coverage instrumentation.

This will make it possible to create filters that depend on more
elaborate properties of functions, as opposed to the current behaviour
when we could basically just filter using function's name.

Author: Vojtech Forejt

src/goto-instrument/cover.cpp

@@ -253,12 +253,12 @@ 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_symbol: symbol of the function to be instrumented
 /// \param function: function to instrument
 /// \param message_handler: log output
 static void instrument_cover_goals(
   const cover_configt &cover_config,
-  const irep_idt &function_id,
+  const symbolt &function_symbol,
   goto_functionst::goto_functiont &function,
   message_handlert &message_handler)
 {
@@ -284,10 +284,10 @@ static void instrument_cover_goals(
 
   bool changed = false;
 
-  if(cover_config.function_filters(function_id, function))
+  if(cover_config.function_filters(function_symbol, function))
   {
     instrument_cover_goals(
-      function_id,
+      function_symbol.name,
       function.body,
       cover_config.cover_instrumenters,
       cover_config.mode,
@@ -297,9 +297,9 @@ static void instrument_cover_goals(
 
   if(
     cover_config.traces_must_terminate &&
-    function_id == goto_functionst::entry_point())
+    function_symbol.name == goto_functionst::entry_point())
   {
-    cover_instrument_end_of_function(function_id, function.body);
+    cover_instrument_end_of_function(function_symbol.name, function.body);
     changed = true;
   }
 
@@ -316,9 +316,11 @@ void instrument_cover_goals(
   goto_model_functiont &function,
   message_handlert &message_handler)
 {
+  const symbolt function_symbol =
+    function.get_symbol_table().lookup_ref(function.get_function_id());
   instrument_cover_goals(
     cover_config,
-    function.get_function_id(),
+    function_symbol,
     function.get_goto_function(),
     message_handler);
 
@@ -356,9 +358,10 @@ bool instrument_cover_goals(
 
   Forall_goto_functions(f_it, goto_functions)
   {
-    cover_config->mode = symbol_table.lookup(f_it->first)->mode;
+    const symbolt function_symbol = symbol_table.lookup_ref(f_it->first);
+    cover_config->mode = function_symbol.mode;
     instrument_cover_goals(
-      *cover_config, f_it->first, f_it->second, message_handler);
+      *cover_config, function_symbol, f_it->second, message_handler);
   }
   goto_functions.compute_location_numbers();
 

src/goto-instrument/cover_filter.cpp

@@ -16,24 +16,24 @@ Author: Peter Schrammel
 #include <linking/static_lifetime_init.h>
 
 /// Filter out functions that are not considered provided by the user
-/// \param function_id: a function name
+/// \param function: the function under consideration
 /// \param goto_function: a goto function
 /// \return returns true if function is considered user-provided
 bool internal_functions_filtert::operator()(
-  const irep_idt &function_id,
+  const symbolt &function,
   const goto_functionst::goto_functiont &goto_function) const
 {
-  if(function_id == goto_functionst::entry_point())
+  if(function.name == goto_functionst::entry_point())
     return false;
 
-  if(function_id == INITIALIZE_FUNCTION)
+  if(function.name == INITIALIZE_FUNCTION)
     return false;
 
   if(goto_function.is_hidden())
     return false;
 
   // ignore Java built-ins (synthetic functions)
-  if(has_prefix(id2string(function_id), "java::array["))
+  if(has_prefix(id2string(function.name), "java::array["))
     return false;
 
   // ignore if built-in library
@@ -45,33 +45,34 @@ bool internal_functions_filtert::operator()(
   return true;
 }
 
-/// Filter functions whose name match the regex
-/// \param function_id: a function name
+/// Filter functions whose name matches the regex
+/// \param function: the function under consideration
 /// \param goto_function: a goto function
 /// \return returns true if the function name matches
 bool include_pattern_filtert::operator()(
-  const irep_idt &function_id,
+  const symbolt &function,
   const goto_functionst::goto_functiont &goto_function) const
 {
   (void)goto_function; // unused parameter
   std::smatch string_matcher;
   return std::regex_match(
-    id2string(function_id), string_matcher, regex_matcher);
+    id2string(function.name), 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 function_id: name of \p goto_function
+/// \param function: function symbol for function corresponding
+/// to \p goto_function
 /// \param goto_function: a goto function
 /// \return returns true if non-trivial
 bool trivial_functions_filtert::operator()(
-  const irep_idt &function_id,
+  const symbolt &function,
   const goto_functionst::goto_functiont &goto_function) const
 {
-  (void)function_id; // unused parameter
+  (void)function; // unused parameter
   unsigned long count_assignments = 0, count_goto = 0;
   forall_goto_program_instructions(i_it, goto_function.body)
   {

src/goto-instrument/cover_filter.h

@@ -15,8 +15,9 @@ Author: Daniel Kroening
 #include <regex>
 #include <memory>
 
-#include <util/message.h>
 #include <util/invariant.h>
+#include <util/message.h>
+#include <util/symbol.h>
 
 #include <goto-programs/goto_model.h>
 
@@ -35,7 +36,7 @@ class function_filter_baset : public messaget
 
   /// Returns true if the function passes the filter criteria
   virtual bool operator()(
-    const irep_idt &identifier,
+    const symbolt &identifier,
     const goto_functionst::goto_functiont &goto_function) const = 0;
 
   /// Can be called after final filter application to report
@@ -85,7 +86,7 @@ class function_filterst
   /// \param identifier: function name
   /// \param goto_function: goto function
   bool operator()(
-    const irep_idt &identifier,
+    const symbolt &identifier,
     const goto_functionst::goto_functiont &goto_function) const
   {
     for(const auto &filter : filters)
@@ -151,7 +152,7 @@ class internal_functions_filtert : public function_filter_baset
   }
 
   bool operator()(
-    const irep_idt &identifier,
+    const symbolt &identifier,
     const goto_functionst::goto_functiont &goto_function) const override;
 };
 
@@ -168,7 +169,7 @@ class include_pattern_filtert : public function_filter_baset
   }
 
   bool operator()(
-    const irep_idt &identifier,
+    const symbolt &identifier,
     const goto_functionst::goto_functiont &goto_function) const override;
 
 private:
@@ -185,7 +186,7 @@ class trivial_functions_filtert : public function_filter_baset
   }
 
   bool operator()(
-    const irep_idt &identifier,
+    const symbolt &identifier,
     const goto_functionst::goto_functiont &goto_function) const override;
 };