Merge pull request #2705 from danpoe/feature/replace-function-calls

Replace function calls with calls to other functions

Author: Daniel Kroening

regression/goto-instrument/replace-calls-01/main.c

@@ -0,0 +1,17 @@
+int f(int a)
+{
+  return a;
+}
+
+int g(int b)
+{
+  return b + 1;
+}
+
+int main()
+{
+  int r;
+
+  r = f(0);
+  assert(r == 1);
+}

regression/goto-instrument/replace-calls-01/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-calls f:g
+g\(0\);
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+f\(0\);
+^warning: ignoring

regression/goto-instrument/replace-calls-02/main.c

@@ -0,0 +1,30 @@
+int f()
+{
+  return 0;
+}
+
+int g()
+{
+  return 1;
+}
+
+int h()
+{
+  return 2;
+}
+
+int i()
+{
+  return 3;
+}
+
+int main()
+{
+  int r;
+
+  r = f();
+  assert(r == 1);
+
+  r = h();
+  assert(r == 3);
+}

regression/goto-instrument/replace-calls-02/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-calls f:g --replace-calls h:i
+g\(\);
+i\(\);
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+f\(\);
+h\(\);
+^warning: ignoring

regression/goto-instrument/replace-calls-03/main.c

@@ -0,0 +1,14 @@
+int f()
+{
+  return 0;
+}
+
+char g()
+{
+  return 1;
+}
+
+int main()
+{
+  f();
+}

regression/goto-instrument/replace-calls-03/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-calls f:g
+Functions f and g are not type-compatible
+^EXIT=11$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-instrument/replace-calls-04/main.c

@@ -0,0 +1,14 @@
+void f(int a)
+{
+  return 0;
+}
+
+void g(unsigned a)
+{
+  return 1;
+}
+
+int main()
+{
+  f(0);
+}

regression/goto-instrument/replace-calls-04/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-calls f:g
+Functions f and g are not type-compatible
+^EXIT=11$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-instrument/replace-calls-05/main.c

@@ -0,0 +1,8 @@
+void g()
+{
+}
+
+int main()
+{
+  return 0;
+}

regression/goto-instrument/replace-calls-05/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-calls f:g --replace-calls h:f
+Function f cannot both be replaced and be a replacement
+^EXIT=11$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-instrument/replace-calls-06/main.c

@@ -0,0 +1,23 @@
+int f()
+{
+  return 0;
+}
+
+int g()
+{
+  return 1;
+}
+
+int main()
+{
+  int (*h)(void);
+
+  h = g;
+  h = f;
+
+  int r;
+  r = h();
+  assert(r == 1);
+
+  return 0;
+}

regression/goto-instrument/replace-calls-06/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--replace-calls f:g
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+f\(\);
+^warning: ignoring

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1063,6 +1063,14 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     do_remove_const_function_pointers_only();
   }
 
+  if(cmdline.isset("replace-calls"))
+  {
+    do_indirect_call_and_rtti_removal();
+
+    replace_callst replace_calls;
+    replace_calls(goto_model, cmdline.get_values("replace-calls"));
+  }
+
   if(cmdline.isset("function-inline"))
   {
     std::string function=cmdline.get_value("function-inline");
@@ -1628,6 +1636,7 @@ void goto_instrument_parse_optionst::help()
     " --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"
+    HELP_REPLACE_CALLS
     "\n"
     "Other options:\n"
     " --no-system-headers          with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/remove_calls_no_body.h>
 #include <goto-programs/remove_const_function_pointers.h>
+#include <goto-programs/replace_calls.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
@@ -97,7 +98,9 @@ Author: Daniel Kroening, [email protected]
   OPT_REMOVE_CALLS_NO_BODY \
   OPT_REPLACE_FUNCTION_BODY \
   OPT_GOTO_PROGRAM_STATS \
-  "(show-local-safe-pointers)(show-safe-dereferences)"
+  "(show-local-safe-pointers)(show-safe-dereferences)" \
+  OPT_REPLACE_CALLS \
+  // empty last line
 
 // clang-format on
 

src/goto-programs/Makefile

@@ -6,7 +6,7 @@ SRC = adjust_float_expressions.cpp \
       destructor.cpp \
       elf_reader.cpp \
       format_strings.cpp \
-      initialize_goto_model.cpp \
+      generate_function_bodies.cpp \
       goto_asm.cpp \
       goto_clean_expr.cpp \
       goto_convert.cpp \
@@ -16,12 +16,13 @@ SRC = adjust_float_expressions.cpp \
       goto_convert_side_effect.cpp \
       goto_function.cpp \
       goto_functions.cpp \
-      goto_inline.cpp \
       goto_inline_class.cpp \
+      goto_inline.cpp \
       goto_program.cpp \
       goto_program_template.cpp \
       goto_trace.cpp \
       graphml_witness.cpp \
+      initialize_goto_model.cpp \
       instrument_preconditions.cpp \
       interpreter.cpp \
       interpreter_evaluate.cpp \
@@ -50,7 +51,7 @@ SRC = adjust_float_expressions.cpp \
       remove_unused_functions.cpp \
       remove_vector.cpp \
       remove_virtual_functions.cpp \
-      generate_function_bodies.cpp \
+      replace_calls.cpp \
       resolve_inherited_component.cpp \
       safety_checker.cpp \
       set_properties.cpp \