Replace function calls

danpoe · danpoe · commit d6147f521a25 · 2018-08-10T13:35:17.000+01:00
Adds an option --replace-calls f:g (can be repeated) to goto-instrument which
replaces calls to function f by calls to function g. A use case is to replace
certain functions by simpler stubs for analysis.
diff --git a/regression/goto-instrument/replace-calls-01/main.c b/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);
+}
diff --git a/regression/goto-instrument/replace-calls-01/test.desc b/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
diff --git a/regression/goto-instrument/replace-calls-02/main.c b/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);
+}
diff --git a/regression/goto-instrument/replace-calls-02/test.desc b/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
diff --git a/regression/goto-instrument/replace-calls-03/main.c b/regression/goto-instrument/replace-calls-03/main.c
@@ -0,0 +1,14 @@
+int f()
+{
+  return 0;
+}
+
+char g()
+{
+  return 1;
+}
+
+int main()
+{
+  f();
+}
diff --git a/regression/goto-instrument/replace-calls-03/test.desc b/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
diff --git a/regression/goto-instrument/replace-calls-04/main.c b/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);
+}
diff --git a/regression/goto-instrument/replace-calls-04/test.desc b/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
diff --git a/regression/goto-instrument/replace-calls-05/main.c b/regression/goto-instrument/replace-calls-05/main.c
@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}
diff --git a/regression/goto-instrument/replace-calls-05/test.desc b/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
diff --git a/regression/goto-instrument/replace-calls-06/main.c b/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;
+}
diff --git a/regression/goto-instrument/replace-calls-06/test.desc b/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
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <analyses/goto_check.h>
 
 #include <goto-programs/goto_trace.h>
+#include <goto-programs/replace_calls.h>
 
 #include "bmc.h"
 #include "xml_interface.h"
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/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(*)
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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>
 
@@ -98,6 +99,7 @@ Author: Daniel Kroening, kroening@kroening.com
   OPT_REPLACE_FUNCTION_BODY \
   OPT_GOTO_PROGRAM_STATS \
   "(show-local-safe-pointers)(show-safe-dereferences)" \
+  OPT_REPLACE_CALLS \
   // empty last line
 
 // clang-format on
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
@@ -51,6 +51,7 @@ SRC = adjust_float_expressions.cpp \
       remove_unused_functions.cpp \
       remove_vector.cpp \
       remove_virtual_functions.cpp \
+      replace_calls.cpp \
       resolve_inherited_component.cpp \
       safety_checker.cpp \
       set_properties.cpp \
diff --git a/src/goto-programs/replace_calls.cpp b/src/goto-programs/replace_calls.cpp
@@ -0,0 +1,158 @@
+/*******************************************************************\
+
+Module: Replace calls
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+/// \file
+/// Replace calls to given functions with calls to other given
+/// functions
+
+#include "replace_calls.h"
+
+#include <goto-programs/remove_returns.h>
+
+#include <util/base_type.h>
+#include <util/invariant.h>
+#include <util/irep.h>
+#include <util/string_utils.h>
+#include <util/suffix.h>
+
+/// Replace function calls with calls to other functions
+/// \param goto_model: goto model to modify
+/// \param replacement_list: list of strings, with each string f:g denoting a
+///   mapping between functions names; a mapping f -> g indicates that calls to
+///   f should be replaced by calls to g
+void replace_callst::operator()(
+  goto_modelt &goto_model,
+  const replacement_listt &replacement_list) const
+{
+  replacement_mapt replacement_map = parse_replacement_list(replacement_list);
+  (*this)(goto_model, replacement_map);
+}
+
+/// Replace function calls with calls to other functions
+/// \param goto_model: goto model to modify
+/// \param replacement_map: mapping between function names; a mapping f -> g
+///   indicates that calls to f should be replaced by calls to g
+void replace_callst::operator()(
+  goto_modelt &goto_model,
+  const replacement_mapt &replacement_map) const
+{
+  check_replacement_map(replacement_map);
+
+  const namespacet ns(goto_model.symbol_table);
+  goto_functionst &goto_functions = goto_model.goto_functions;
+
+  for(auto &p : goto_functions.function_map)
+  {
+    goto_functionst::goto_functiont &goto_function = p.second;
+    goto_programt &goto_program = goto_function.body;
+
+    (*this)(goto_program, goto_functions, ns, replacement_map);
+  }
+}
+
+void replace_callst::operator()(
+  goto_programt &goto_program,
+  const goto_functionst &goto_functions,
+  const namespacet &ns,
+  const replacement_mapt &replacement_map) const
+{
+  Forall_goto_program_instructions(it, goto_program)
+  {
+    goto_programt::instructiont &ins = *it;
+
+    if(!ins.is_function_call())
+      continue;
+
+    code_function_callt &cfc = to_code_function_call(ins.code);
+    exprt &function = cfc.function();
+
+    PRECONDITION(function.id() == ID_symbol);
+
+    symbol_exprt &se = to_symbol_expr(function);
+    const irep_idt &id = se.get_identifier();
+
+    auto f_it1 = goto_functions.function_map.find(id);
+
+    INVARIANT(
+      f_it1 != goto_functions.function_map.end(),
+      "Called functions need to be present");
+
+    replacement_mapt::const_iterator r_it = replacement_map.find(id);
+
+    if(r_it == replacement_map.end())
+      continue;
+
+    const irep_idt &new_id = r_it->second;
+
+    auto f_it2 = goto_functions.function_map.find(new_id);
+
+    if(f_it2 == goto_functions.function_map.end())
+      throw "Replacement function " + id2string(new_id) +
+        " needs to be present";
+
+    const goto_functionst::goto_functiont &cur_goto_function = f_it1->second;
+    const goto_functionst::goto_functiont &new_goto_function = f_it2->second;
+
+    if(!base_type_eq(cur_goto_function.type, new_goto_function.type, ns))
+      throw "Functions " + id2string(id) + " and " + id2string(new_id) +
+        " are not type-compatible";
+
+    // check that returns have not been removed
+    goto_programt::const_targett next_it = std::next(it);
+    if(next_it != goto_program.instructions.end() && next_it->is_assign())
+    {
+      const code_assignt &ca = to_code_assign(next_it->code);
+      const exprt &rhs = ca.rhs();
+
+      if(rhs.id() == ID_symbol)
+      {
+        const symbol_exprt &se = to_symbol_expr(rhs);
+        if(has_suffix(id2string(se.get_identifier()), RETURN_VALUE_SUFFIX))
+          throw "Returns must not be removed before replacing calls";
+      }
+    }
+
+    // Finally modify the call
+    function.type() = new_goto_function.type;
+    se.set_identifier(new_id);
+  }
+}
+
+replace_callst::replacement_mapt replace_callst::parse_replacement_list(
+  const replacement_listt &replacement_list) const
+{
+  replacement_mapt replacement_map;
+
+  for(const std::string &s : replacement_list)
+  {
+    std::string original;
+    std::string replacement;
+
+    split_string(s, ':', original, replacement, true);
+
+    const auto r =
+      replacement_map.insert(std::make_pair(original, replacement));
+
+    if(!r.second)
+      throw "Conflicting replacement for function " + original;
+  }
+
+  return replacement_map;
+}
+
+void replace_callst::check_replacement_map(
+  const replacement_mapt &replacement_map) const
+{
+  for(const auto &p : replacement_map)
+  {
+    if(replacement_map.find(p.second) != replacement_map.end())
+      throw "Function " + id2string(p.second) +
+        " cannot both be replaced and "
+        "be a replacement";
+  }
+}
diff --git a/src/goto-programs/replace_calls.h b/src/goto-programs/replace_calls.h

-Original file line number
+Diff line change
@@ @@ -0,0 +1,4 @@ @@
 +int main()
 +{
 +  return 0;
 +}