Merge pull request #7550 from remi-delmas-3000/inline-program

Add new function to inline a list of calls in a goto_program

src/goto-programs/goto_inline.cpp

@@ -354,3 +354,36 @@ jsont goto_function_inline_and_log(
 
   return goto_inline.output_inline_log_json();
 }
+
+/// Transitively inline all function calls found in a particular program.
+/// Caller is responsible for calling update(), compute_loop_numbers(), etc.
+/// \param goto_functions: The function map to use to find function bodies.
+/// \param goto_program: The program whose calls to inline.
+/// \param ns: Namespace used by goto_inlinet.
+/// \param message_handler: Message handler used by goto_inlinet.
+/// \param adjust_function: Replace location in inlined function with call site.
+/// \param caching: Tell goto_inlinet to cache.
+void goto_program_inline(
+  goto_functionst &goto_functions,
+  goto_programt &goto_program,
+  const namespacet &ns,
+  message_handlert &message_handler,
+  bool adjust_function,
+  bool caching)
+{
+  goto_inlinet goto_inline(
+    goto_functions, ns, message_handler, adjust_function, caching);
+
+  // gather all calls found in the program
+  goto_inlinet::call_listt call_list;
+
+  Forall_goto_program_instructions(i_it, goto_program)
+  {
+    if(!i_it->is_function_call())
+      continue;
+
+    call_list.push_back(goto_inlinet::callt(i_it, true));
+  }
+
+  goto_inline.goto_inline(call_list, goto_program, true);
+}

src/goto-programs/goto_inline.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class goto_functionst;
 class goto_modelt;
+class goto_programt;
 class message_handlert;
 class namespacet;
 
@@ -74,4 +75,12 @@ jsont goto_function_inline_and_log(
   bool adjust_function=false,
   bool caching=true);
 
+void goto_program_inline(
+  goto_functionst &goto_functions,
+  goto_programt &goto_program,
+  const namespacet &ns,
+  message_handlert &message_handler,
+  bool adjust_function = false,
+  bool caching = true);
+
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H

src/goto-programs/goto_inline_class.cpp

@@ -488,6 +488,21 @@ void goto_inlinet::goto_inline(
     force_full);
 }
 
+void goto_inlinet::goto_inline(
+  const goto_inlinet::call_listt &call_list,
+  goto_programt &goto_program,
+  const bool force_full)
+{
+  recursion_set.clear();
+  for(const auto &call : call_list)
+  {
+    // each top level call in the program gets its own fresh inline map
+    const inline_mapt inline_map;
+    expand_function_call(
+      goto_program, inline_map, call.second, force_full, call.first);
+  }
+}
+
 void goto_inlinet::goto_inline_nontransitive(
   const irep_idt identifier,
   goto_functiont &goto_function,

src/goto-programs/goto_inline_class.h

@@ -69,6 +69,16 @@ class goto_inlinet
     const inline_mapt &inline_map,
     const bool force_full=false);
 
+  /// \brief Inline specified calls in a given program.
+  /// \param call_list : calls to inline in the `goto_program`.
+  /// \param goto_program : goto program to inline `calls_list` in.
+  /// \param force_full : true to break recursion with a SKIP,
+  ///   false means detecting recursion is an error.
+  void goto_inline(
+    const goto_inlinet::call_listt &call_list,
+    goto_programt &goto_program,
+    const bool force_full = false);
+
   // handle all functions
   void goto_inline(
     const inline_mapt &inline_map,

unit/Makefile

@@ -66,6 +66,7 @@ SRC += analyses/ai/ai.cpp \
        goto-programs/goto_program_declaration.cpp \
        goto-programs/goto_program_function_call.cpp \
        goto-programs/goto_program_goto_target.cpp \
+       goto-programs/goto_program_goto_program_inline.cpp \
        goto-programs/goto_program_symbol_type_table_consistency.cpp \
        goto-programs/goto_program_table_consistency.cpp \
        goto-programs/goto_program_validate.cpp \

unit/goto-programs/goto_program_goto_program_inline.cpp

@@ -0,0 +1,67 @@
+/*******************************************************************\
+
+Module: Inline calls in program unit tests
+
+Author: Remi Delmas
+
+\*******************************************************************/
+
+#include <util/message.h>
+
+#include <goto-programs/goto_inline.h>
+
+#include <testing-utils/get_goto_model_from_c.h>
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("Goto program inline", "[core][goto-programs][goto_program_inline]")
+{
+  const std::string code = R"(
+    int x;
+    int y;
+    void f() { y = 0; }
+    void g() { x = 0; f(); }
+    void h() { g(); }
+    void main() { h(); }
+  )";
+
+  goto_modelt goto_model = get_goto_model_from_c(code);
+
+  auto &function = goto_model.goto_functions.function_map.at("h");
+
+  null_message_handlert message_handler;
+  goto_program_inline(
+    goto_model.goto_functions,
+    function.body,
+    namespacet(goto_model.symbol_table),
+    message_handler);
+
+  static int assign_count = 0;
+  for_each_instruction_if(
+    function,
+    [&](goto_programt::const_targett it) {
+      return it->is_function_call() || it->is_assign();
+    },
+    [&](goto_programt::const_targett it) {
+      if(it->is_function_call())
+      {
+        // there are no calls left
+        FAIL();
+      }
+
+      if(it->is_assign())
+      {
+        // the two assignments were inlined
+        const auto &lhs = it->assign_lhs();
+        if(assign_count == 0)
+        {
+          REQUIRE(to_symbol_expr(lhs).get_identifier() == "x");
+        }
+        else if(assign_count == 1)
+        {
+          REQUIRE(to_symbol_expr(lhs).get_identifier() == "y");
+        }
+        assign_count++;
+      }
+    });
+  REQUIRE(assign_count == 2);
+}