Add option to generate function body to goto-instrument

regression/goto-instrument/generate-function-body/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+void should_not_be_replaced(void)
+{
+  __CPROVER_assume(0);
+}
+
+void should_be_generated(void);
+
+int main(void)
+{
+  int flag;
+  int does_not_get_reached = 0;
+  if(flag)
+  {
+    should_not_be_replaced();
+    assert(does_not_get_reached);
+  }
+  should_be_generated();
+  return 0;
+}

regression/goto-instrument/generate-function-body/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body '(?!__).*' --replace-function-body-options assert-false
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.assertion.1\] assertion does_not_get_reached: SUCCESS$
+^\[should_be_generated.assertion.1\] assertion FALSE: FAILURE$

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

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+void crashes_program(void);
+
+int main(void)
+{
+  int flag;
+  if(flag)
+  {
+    crashes_program();
+    assert(0);
+  }
+  return 0;
+}

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

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-function-body crashes_program --replace-function-body-options assert-false-assume-false
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.assertion.1\] assertion 0: SUCCESS$
+^\[crashes_program.assertion.1\] assertion FALSE: FAILURE$

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, [email protected]
 #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,30 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       throw 0;
   }
 
+  if(
+    cmdline.isset("replace-function-body") ||
+    cmdline.isset("generate-function-body"))
+  {
+    if(
+      cmdline.isset("replace-function-body") &&
+      cmdline.isset("generate-function-body"))
+    {
+      throw "Can only use one of --replace-function-body or --generate-function-body";
+    }
+    bool only_generate = cmdline.isset("generate-function-body");
+    std::regex function_regex = std::regex(
+      only_generate ? cmdline.get_value("generate-function-body")
+                    : cmdline.get_value("replace-function-body"));
+    status() << "Replacing function bodies" << eom;
+    replace_function_bodies(
+      goto_model.goto_functions,
+      goto_model.symbol_table,
+      function_regex,
+      only_generate,
+      cmdline.get_value("replace-function-body-options"),
+      *this);
+  }
+
   // recalculate numbers, etc.
   goto_model.goto_functions.update();
 }
@@ -1521,9 +1546,21 @@ void goto_instrument_parse_optionst::help()
     " --check-invariant function   instruments invariant checking function\n"
     " --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(*)
+    " --undefined-function-is-assume-false\n"
     // 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"
+    " --replace-function-body <regex>\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    "                              Replace bodies of function matching regex\n"
+    " --generate-function-body <regex>\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    "                              Like replace-function-body, but ignore functions that already have bodies\n"
+    " --replace-function-body-options <option>\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    "                              One of empty, assert-false, assume-false, nondet-return\n"
+    "                              assert-false-assume-false and\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    "                              havoc[,params:<regex>][,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,11 @@ Author: Daniel Kroening, [email protected]
   "(show-threaded)(list-calls-args)(print-path-lengths)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
-  "(splice-call):"
+  "(splice-call):" \
+  "(replace-function-body):" \
+  "(generate-function-body):" \
+  "(replace-function-body-options):"
+
 // clang-format on
 
 class goto_instrument_parse_optionst: