From 61bd09f054a521f25498089eb7fe68b573cec2e4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 12 Sep 2025 12:47:23 +0000 Subject: [PATCH] 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. --- doc/man/goto-instrument.1 | 3 + .../remove-function-body2/main.c | 29 +++++++++ .../remove-function-body2/test.desc | 13 ++++ .../goto_instrument_parse_options.cpp | 14 ++++- .../goto_instrument_parse_options.h | 3 +- src/goto-instrument/remove_function.cpp | 62 +++++++++++++++++++ src/goto-instrument/remove_function.h | 9 +++ 7 files changed, 130 insertions(+), 3 deletions(-) create mode 100644 regression/goto-instrument/remove-function-body2/main.c create mode 100644 regression/goto-instrument/remove-function-body2/test.desc diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index f787ab7f26d..5d971063565 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -748,6 +748,9 @@ 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 +.TP \fB\-\-replace\-calls\fR \fIf\fR:\fIg\fR replace calls to \fIf\fR with calls to \fIg\fR .TP diff --git a/regression/goto-instrument/remove-function-body2/main.c b/regression/goto-instrument/remove-function-body2/main.c new file mode 100644 index 00000000000..6cf3a52a732 --- /dev/null +++ b/regression/goto-instrument/remove-function-body2/main.c @@ -0,0 +1,29 @@ +#include + +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(); +} diff --git a/regression/goto-instrument/remove-function-body2/test.desc b/regression/goto-instrument/remove-function-body2/test.desc new file mode 100644 index 00000000000..eeaf24160c0 --- /dev/null +++ b/regression/goto-instrument/remove-function-body2/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--remove-function-body-regex '^(foo[0-9].*|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 diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 3675390972f..570554155b4 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/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_value("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}\n" HELP_REPLACE_CALLS HELP_ANSI_C_LANGUAGE "\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 1927f49e2bc..8e49a495c54 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -110,7 +110,8 @@ Author: Daniel Kroening, kroening@kroening.com 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):" \ diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp index 02056d81d61..2b7ab9119b8 100644 --- a/src/goto-instrument/remove_function.cpp +++ b/src/goto-instrument/remove_function.cpp @@ -17,6 +17,8 @@ Date: April 2017 #include +#include + /// 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,63 @@ 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 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::string &pattern, + message_handlert &message_handler) +{ + messaget message{message_handler}; + + try + { + std::regex regex_pattern{pattern}; + + remove_functions_regex(goto_model, regex_pattern, pattern, message_handler); + } + catch(const std::regex_error &e) + { + message.error() << "Invalid regular expression pattern: " << pattern << " (" + << e.what() << ")" << messaget::eom; + } +} diff --git a/src/goto-instrument/remove_function.h b/src/goto-instrument/remove_function.h index 3c88b8ce803..9130908af17 100644 --- a/src/goto-instrument/remove_function.h +++ b/src/goto-instrument/remove_function.h @@ -32,4 +32,13 @@ void remove_functions( const std::list &names, message_handlert &); +/// Remove functions matching any of the provided regular expression patterns. +/// \param goto_model: The goto model to modify +/// \param pattern: 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::string &pattern, + message_handlert &message_handler); + #endif // CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H