Add new function to inline calls in a goto_program

Author: Remi Delmas

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, [email protected]
 
 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,26 @@ void goto_inlinet::goto_inline(
     force_full);
 }
 
+/// Inline specified calls in a given program.
+/// \param call_list : calls to inline in the program.
+/// \param goto_function : to program to inline in.
+/// \param force_full : true to break recursion with a SKIP,
+///   false means detecting recursion is an error.
+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,15 @@ class goto_inlinet
     const inline_mapt &inline_map,
     const bool force_full=false);
 
+  /// Inline specified calls in a goto_program.
+  /// force_full:
+  /// - true:  put skip on recursion and issue warning
+  /// - false: leave call on recursion
+  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,