From accc4124cc9c00f6c70ab8461e18ce6fdb73f9d2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 10 Apr 2017 14:31:03 +0100 Subject: [PATCH] goto-instrument --remove-function-body Removes the implementation of a function (but not its declaration or its call sites) from a goto program. This enables stubbing of possibly costly functions, such as custom memset implementations. --- CHANGELOG | 1 + .../remove-function-body1/main.c | 21 +++++ .../remove-function-body1/test.desc | 10 ++ src/goto-instrument/Makefile | 1 + .../goto_instrument_parse_options.cpp | 12 +++ .../goto_instrument_parse_options.h | 3 +- src/goto-instrument/remove_function.cpp | 94 +++++++++++++++++++ src/goto-instrument/remove_function.h | 35 +++++++ 8 files changed, 176 insertions(+), 1 deletion(-) create mode 100644 regression/goto-instrument/remove-function-body1/main.c create mode 100644 regression/goto-instrument/remove-function-body1/test.desc create mode 100644 src/goto-instrument/remove_function.cpp create mode 100644 src/goto-instrument/remove_function.h diff --git a/CHANGELOG b/CHANGELOG index 1718d32243d..44ac745be0d 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -7,6 +7,7 @@ * GOTO-INSTRUMENT: New option --print-path-lenghts * GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions * GOTO-INSTRUMENT: New option --undefined-function-is-assume-false +* GOTO-INSTRUMENT: New option --remove-function-body 5.7 diff --git a/regression/goto-instrument/remove-function-body1/main.c b/regression/goto-instrument/remove-function-body1/main.c new file mode 100644 index 00000000000..14e576db99f --- /dev/null +++ b/regression/goto-instrument/remove-function-body1/main.c @@ -0,0 +1,21 @@ +#include + +int foo() +{ + int a; + assert(a>0); + return a; +} + +int bar() +{ + int b; + assert(b>0); + return b; +} + +int main() +{ + foo(); + bar(); +} diff --git a/regression/goto-instrument/remove-function-body1/test.desc b/regression/goto-instrument/remove-function-body1/test.desc new file mode 100644 index 00000000000..45369a31184 --- /dev/null +++ b/regression/goto-instrument/remove-function-body1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--remove-function-body foo --remove-function-body bar +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +^bar +^foo diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 4b74d173ff7..bc3cb10f1b3 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -42,6 +42,7 @@ SRC = accelerate/accelerate.cpp \ points_to.cpp \ race_check.cpp \ reachability_slicer.cpp \ + remove_function.cpp \ rw_set.cpp \ show_locations.cpp \ skip_loops.cpp \ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 9c30bae5612..34b4f789027 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -90,6 +90,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "unwind.h" #include "model_argc_argv.h" #include "undefined_functions.h" +#include "remove_function.h" /*******************************************************************\ @@ -1034,6 +1035,15 @@ void goto_instrument_parse_optionst::instrument_goto_program() throw 0; } + if(cmdline.isset("remove-function-body")) + { + remove_functions( + symbol_table, + goto_functions, + cmdline.get_values("remove-function-body"), + get_message_handler()); + } + // we add the library in some cases, as some analyses benefit if(cmdline.isset("add-library") || @@ -1634,6 +1644,8 @@ void goto_instrument_parse_optionst::help() HELP_REMOVE_CONST_FUNCTION_POINTERS " --add-library add models of C library functions\n" " --model-argc-argv model up to command line arguments\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --remove-function-body remove the implementation of function (may be repeated)\n" "\n" "Other options:\n" " --use-system-headers with --dump-c/--dump-cpp: generate C source with includes\n" // NOLINT(*) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 788bf543953..2f015c13d5c 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -72,7 +72,8 @@ Author: Daniel Kroening, kroening@kroening.com "(z3)(add-library)(show-dependence-graph)" \ "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ "(show-threaded)(list-calls-args)(print-path-lengths)" \ - "(undefined-function-is-assume-false)" + "(undefined-function-is-assume-false)" \ + "(remove-function-body):" class goto_instrument_parse_optionst: public parse_options_baset, diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp new file mode 100644 index 00000000000..2f72455a3df --- /dev/null +++ b/src/goto-instrument/remove_function.cpp @@ -0,0 +1,94 @@ +/*******************************************************************\ + +Module: Remove function definition + +Author: Michael Tautschnig + +Date: April 2017 + +\*******************************************************************/ + +#include "remove_function.h" + +#include + +#include + +/*******************************************************************\ + +Function: remove_function + + Inputs: + symbol_table Input symbol table to be modified + goto_functions Input functions to be modified + identifier Function to be removed + message_handler Error/status output + + Outputs: + + Purpose: Remove the body of function "identifier" such that an + analysis will treat it as a side-effect free function with + non-deterministic return value. + +\*******************************************************************/ + +void remove_function( + symbol_tablet &symbol_table, + goto_functionst &goto_functions, + const irep_idt &identifier, + message_handlert &message_handler) +{ + messaget message(message_handler); + + goto_functionst::function_mapt::iterator entry= + goto_functions.function_map.find(identifier); + + if(entry==goto_functions.function_map.end()) + { + message.error() << "No function " << identifier + << " in goto program" << messaget::eom; + return; + } + else if(entry->second.is_inlined()) + { + message.warning() << "Function " << identifier << " is inlined, " + << "instantiations will not be removed" + << messaget::eom; + } + + if(entry->second.body_available()) + { + message.status() << "Removing body of " << identifier + << messaget::eom; + entry->second.clear(); + symbol_table.lookup(identifier).value.make_nil(); + } +} + +/*******************************************************************\ + +Function: remove_functions + + Inputs: + symbol_table Input symbol table to be modified + goto_functions Input functions to be modified + names List of functions to be removed + message_handler Error/status output + + Outputs: + + Purpose: Remove the body of all functions listed in "names" such that + an analysis will treat it as a side-effect free function with + non-deterministic return value. + +\*******************************************************************/ + +void remove_functions( + symbol_tablet &symbol_table, + goto_functionst &goto_functions, + const std::list &names, + message_handlert &message_handler) +{ + for(const auto &f : names) + remove_function(symbol_table, goto_functions, f, message_handler); +} diff --git a/src/goto-instrument/remove_function.h b/src/goto-instrument/remove_function.h new file mode 100644 index 00000000000..c8983025457 --- /dev/null +++ b/src/goto-instrument/remove_function.h @@ -0,0 +1,35 @@ +/*******************************************************************\ + +Module: Remove function definition + +Author: Michael Tautschnig + +Date: April 2017 + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H +#define CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H + +#include +#include + +#include + +class goto_functionst; +class message_handlert; +class symbol_tablet; + +void remove_function( + symbol_tablet &symbol_table, + goto_functionst &goto_functions, + const irep_idt &identifier, + message_handlert &message_handler); + +void remove_functions( + symbol_tablet &symbol_table, + goto_functionst &goto_functions, + const std::list &names, + message_handlert &message_handler); + +#endif // CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H