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

@@ -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

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

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

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

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 \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -90,6 +90,7 @@ Author: Daniel Kroening, [email protected]
 #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 <n>        model up to <n> command line arguments\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
     "\n"
     "Other options:\n"
     " --use-system-headers         with --dump-c/--dump-cpp: generate C source with includes\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -72,7 +72,8 @@ Author: Daniel Kroening, [email protected]
   "(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,

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 <util/message.h>
+
+#include <goto-programs/goto_functions.h>
+
+/*******************************************************************\
+
+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<std::string> &names,
+  message_handlert &message_handler)
+{
+  for(const auto &f : names)
+    remove_function(symbol_table, goto_functions, f, message_handler);
+}

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 <list>
+#include <string>
+
+#include <util/irep.h>
+
+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<std::string> &names,
+  message_handlert &message_handler);
+
+#endif // CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H