Add remove-function-body-regex command line option

This extends the existing `remove-function-body` option in
`goto-instrument` with support for regular expressions to specify a
broader set of functions.

Author: tautschnig

doc/man/goto-instrument.1

@@ -748,6 +748,10 @@ cbmc a.out
 \fB\-\-remove\-function\-body\fR \fIf\fR
 remove the implementation of function \fIf\fR (may be repeated)
 .TP
+\fB\-\-remove\-function\-body\-regex\fR \fIregex\fR
+remove the implementation of functions matching regular expression \fIregex\fR
+(may be repeated)
+.TP
 \fB\-\-replace\-calls\fR \fIf\fR:\fIg\fR
 replace calls to \fIf\fR with calls to \fIg\fR
 .TP

regression/goto-instrument/remove-function-body2/main.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+int foo123()
+{
+  int a;
+  assert(a > 0);
+  return a;
+}
+
+int foox()
+{
+  int a;
+  assert(a > 0);
+  return a;
+}
+
+int bar()
+{
+  int b;
+  assert(b > 0);
+  return b;
+}
+
+int main()
+{
+  foo123();
+  foox();
+  bar();
+}

regression/goto-instrument/remove-function-body2/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--remove-function-body-regex '^foo[0-9].*' --remove-function-body-regex '^bar$'
+^foox
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.no-body\.foo123\] line 26 no body for callee foo123: FAILURE$
+^\[main\.no-body\.bar\] line 28 no body for callee bar: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^bar
+^foo123

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1055,6 +1055,14 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       ui_message_handler);
   }
 
+  if(cmdline.isset("remove-function-body-regex"))
+  {
+    remove_functions_regex(
+      goto_model,
+      cmdline.get_values("remove-function-body-regex"),
+      ui_message_handler);
+  }
+
   // we add the library in some cases, as some analyses benefit
 
   if(
@@ -1960,8 +1968,10 @@ void goto_instrument_parse_optionst::help()
     " {y--add-library} \t add models of C library functions\n"
     HELP_CONFIG_LIBRARY
     " {y--model-argc-argv} {un} \t model up to {un} command line arguments\n"
-    " {y--remove-function-body} {uf} remove the implementation of function {uf}"
-    " (may be repeated)\n"
+    " {y--remove-function-body} {uf} \t remove the implementation of function"
+    " {uf} (may be repeated)\n"
+    " {y--remove-function-body-regex} {uregex} \t remove the implementation of"
+    " functions matching regular expression {uregex} (may be repeated)\n"
     HELP_REPLACE_CALLS
     HELP_ANSI_C_LANGUAGE
     "\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -110,7 +110,8 @@ Author: Daniel Kroening, [email protected]
   OPT_ENFORCE_CONTRACT_REC \
   "(show-threaded)(list-calls-args)" \
   "(undefined-function-is-assume-false)" \
-  "(remove-function-body):"\
+  "(remove-function-body):" \
+  "(remove-function-body-regex):" \
   OPT_AGGRESSIVE_SLICER \
   OPT_FLUSH \
   "(splice-call):" \

src/goto-instrument/remove_function.cpp

@@ -17,6 +17,8 @@ Date: April 2017
 
 #include <goto-programs/goto_model.h>
 
+#include <regex>
+
 /// Remove the body of function "identifier" such that an analysis will treat it
 /// as a side-effect free function with non-deterministic return value.
 /// \par parameters: symbol_table  Input symbol table to be modified
@@ -73,3 +75,78 @@ void remove_functions(
   for(const auto &f : names)
     remove_function(goto_model, f, message_handler);
 }
+
+/// Remove functions matching a regular expression pattern
+/// \param goto_model: The goto model to modify
+/// \param pattern: The regex pattern to match function names against
+/// \param pattern_as_str: The string representation of \p pattern
+/// \param message_handler: For status/warning/error messages
+static void remove_functions_regex(
+  goto_modelt &goto_model,
+  const std::regex &pattern,
+  const std::string &pattern_as_str,
+  message_handlert &message_handler)
+{
+  messaget message{message_handler};
+
+  message.debug() << "Removing functions matching pattern: " << pattern_as_str
+                  << messaget::eom;
+
+  // Collect matching function names first to avoid modifying the map while
+  // iterating
+  std::list<irep_idt> matching_functions;
+
+  for(const auto &entry : goto_model.goto_functions.function_map)
+  {
+    const std::string &function_name = id2string(entry.first);
+    if(std::regex_match(function_name, pattern))
+    {
+      matching_functions.push_back(entry.first);
+    }
+  }
+
+  // Now remove all matching functions
+  for(const auto &func : matching_functions)
+  {
+    remove_function(goto_model, func, message_handler);
+  }
+
+  message.debug() << "Removed " << matching_functions.size()
+                  << " function(s) matching pattern: " << pattern_as_str
+                  << messaget::eom;
+}
+
+void remove_functions_regex(
+  goto_modelt &goto_model,
+  const std::list<std::string> &patterns,
+  message_handlert &message_handler)
+{
+  std::string combined_pattern;
+  for(const auto &pattern : patterns)
+  {
+    if(pattern.empty())
+      continue;
+    if(!combined_pattern.empty())
+      combined_pattern += '|';
+    combined_pattern += pattern;
+  }
+
+  if(combined_pattern.empty())
+    return;
+
+  messaget message{message_handler};
+
+  try
+  {
+    std::regex regex_pattern{combined_pattern};
+
+    remove_functions_regex(
+      goto_model, regex_pattern, combined_pattern, message_handler);
+  }
+  catch(const std::regex_error &e)
+  {
+    message.error() << "Invalid regular expression pattern: "
+                    << combined_pattern << " (" << e.what() << ")"
+                    << messaget::eom;
+  }
+}

src/goto-instrument/remove_function.h

@@ -32,4 +32,13 @@ void remove_functions(
   const std::list<std::string> &names,
   message_handlert &);
 
+/// Remove functions matching any of the provided regular expression patterns.
+/// \param goto_model: The goto model to modify
+/// \param patterns: List of regex patterns to match function names against
+/// \param message_handler: For status/warning/error messages
+void remove_functions_regex(
+  goto_modelt &goto_model,
+  const std::list<std::string> &patterns,
+  message_handlert &message_handler);
+
 #endif // CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H