Option --replace-calls to replace function calls with calls to other given functions

Author: danpoe

regression/cbmc/replace-calls-01/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int f(int a)
+{
+  return a;
+}
+
+int g(int b)
+{
+  return b + 1;
+}
+
+int main()
+{
+  int r;
+
+  r = f(0);
+  assert(r == 1);
+}

regression/cbmc/replace-calls-01/test.desc

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

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

@@ -0,0 +1,18 @@
+
+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,31 @@
+
+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,15 @@
+
+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,15 @@
+
+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,5 @@
+
+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

src/cbmc/cbmc_parse_options.cpp

@@ -193,6 +193,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("nondet-static"))
     options.set_option("nondet-static", true);
 
+  if(cmdline.isset("replace-calls"))
+    options.set_option("replace-calls", cmdline.get_values("replace-calls"));
+
   if(cmdline.isset("no-simplify"))
     options.set_option("simplify", false);
 
@@ -730,6 +733,12 @@ bool cbmc_parse_optionst::process_goto_program(
       goto_model,
       options.get_bool_option("pointer-check"));
 
+    if(options.is_set("replace-calls"))
+    {
+      replace_callst replace_calls;
+      replace_calls(goto_model, options.get_list_option("replace-calls"));
+    }
+
     mm_io(goto_model);
 
     // instrument library preconditions
@@ -945,6 +954,7 @@ void cbmc_parse_optionst::help()
     "Semantic transformations:\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --nondet-static              add nondeterministic initialization of variables with static lifetime\n"
+    HELP_REPLACE_CALLS
     "\n"
     "BMC options:\n"
     HELP_BMC

src/cbmc/cbmc_parse_options.h

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/goto_check.h>
 
 #include <goto-programs/goto_trace.h>
+#include <goto-programs/replace_calls.h>
 
 #include "bmc.h"
 #include "xml_interface.h"
@@ -73,6 +74,7 @@ class optionst;
   OPT_FLUSH \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
+  OPT_REPLACE_CALLS \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 

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,8 @@ 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
 
 // clang-format on
 

src/goto-programs/Makefile

@@ -67,6 +67,7 @@ SRC = adjust_float_expressions.cpp \
       wp.cpp \
       write_goto_binary.cpp \
       xml_goto_trace.cpp \
+      replace_calls.cpp \
       # Empty last line
 
 INCLUDES= -I ..