Add option to generate function body to goto-instrument

Author: hannes-steffenhagen-diffblue

regression/goto-instrument/replace-function-body-assert-false/main.c

@@ -0,0 +1,6 @@
+void do_not_call_this(void);
+
+int main(void)
+{
+  do_not_call_this();
+}

regression/goto-instrument/replace-function-body-assert-false/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-function-body do_not_call_this --replace-function-body-options assert-false
+^EXIT=10$
+^SIGNAL=0$
+^\[do_not_call_this.assertion.1\] assertion FALSE: FAILURE$
+--
+^warning: ignoring

regression/goto-instrument/replace-function-body-assume-false/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+void will_not_return(void);
+
+int main(void)
+{
+  will_not_return();
+  assert(0);
+}

regression/goto-instrument/replace-function-body-assume-false/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-function-body will_not_return --replace-function-body-options assume-false
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/replace-function-body-havoc-globals/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int global = 10;
+const int constant_global = 10;
+
+void touches_globals(void);
+
+int main(void)
+{
+  touches_globals();
+  assert(global == 10);
+  assert(constant_global == 10);
+}

regression/goto-instrument/replace-function-body-havoc-globals/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-function-body touches_globals --replace-function-body-options 'havoc,globals:(?!__).*'
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.assertion.1\] assertion global == 10: FAILURE$
+^\[main.assertion.2\] assertion constant_global == 10: SUCCESS$
+--
+^warning: ignoring

regression/goto-instrument/replace-function-body-havoc-params/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void touches_parameter(int *param, const int *const_param);
+
+int main(void)
+{
+  int parameter = 10;
+  int constant_parameter = 10;
+  touches_parameter(&parameter, &constant_parameter);
+  assert(parameter == 10);
+  assert(constant_parameter == 10);
+}

regression/goto-instrument/replace-function-body-havoc-params/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-function-body touches_parameter --replace-function-body-options havoc,params
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.assertion.1\] assertion parameter == 10: FAILURE$
+^\[main.assertion.2\] assertion constant_parameter == 10: SUCCESS$
+--
+^warning: ignoring

regression/goto-instrument/replace-function-body-nondet-return/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int this_returns_ten(void)
+{
+  return 10;
+}
+
+int main(void)
+{
+  assert(this_returns_ten() == 10);
+}

regression/goto-instrument/replace-function-body-nondet-return/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-function-body this_returns_ten --replace-function-body-options nondet-return
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-instrument/Makefile

@@ -61,6 +61,7 @@ SRC = accelerate/accelerate.cpp \
       undefined_functions.cpp \
       uninitialized.cpp \
       unwind.cpp \
+      replace_function_bodies.cpp \
       wmm/abstract_event.cpp \
       wmm/cycle_collection.cpp \
       wmm/data_dp.cpp \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -99,6 +99,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "undefined_functions.h"
 #include "remove_function.h"
 #include "splice_call.h"
+#include "replace_function_bodies.h"
 
 void goto_instrument_parse_optionst::eval_verbosity()
 {
@@ -1447,6 +1448,16 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       throw 0;
   }
 
+  if(cmdline.isset("replace-function-body"))
+  {
+    status() << "Replacing function bodies" << eom;
+    replace_function_bodies(
+      goto_model.goto_functions,
+      goto_model.symbol_table,
+      std::regex(cmdline.get_value("replace-function-body")),
+      cmdline.get_value("replace-function-body-options"));
+  }
+
   // recalculate numbers, etc.
   goto_model.goto_functions.update();
 }
@@ -1522,8 +1533,13 @@ void goto_instrument_parse_optionst::help()
     " --remove-pointers            converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
     " --splice-call caller,callee  prepends a call to callee in the body of caller\n"  // NOLINT(*)
     // NOLINTNEXTLINE(whitespace/line_length)
-    " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length)
-    "                              convert each call to an undefined function to assume(false)\n"
+    " --undefined-function-is-assume-false\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --replace-function-body <regex> Replace bodies of function matching regex\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --replace-function-body-options <option> One of assert-false, assume-false, nondet-return and\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    "                                          havoc[,params][,globals:<regex>]"
     "\n"
     "Loop transformations:\n"
     " --k-induction <k>            check loops with k-induction\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -84,7 +84,10 @@ Author: Daniel Kroening, kroening@kroening.com
   "(show-threaded)(list-calls-args)(print-path-lengths)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
-  "(splice-call):"
+  "(splice-call):" \
+  "(replace-function-body):" \
+  "(replace-function-body-options):"
+
 // clang-format on
 
 class goto_instrument_parse_optionst: