Merge pull request #654 from danpoe/inlining-no-caching

Option to disable caching for inlining

Author: kroening

regression/goto-instrument/inline_13/main.c

@@ -0,0 +1,18 @@
+
+int x;
+
+void g()
+{
+  x = 1;
+}
+
+void f()
+{
+  g();
+}
+
+int main()
+{
+  f();
+}
+

regression/goto-instrument/inline_13/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function-inline main --log -
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/inline_14/main.c

@@ -0,0 +1,23 @@
+
+int x;
+
+void h()
+{
+  x = 1;
+}
+
+void g()
+{
+  h();
+}
+
+void f()
+{
+  g();
+}
+
+int main()
+{
+  f();
+}
+

regression/goto-instrument/inline_14/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function-inline main --log - --no-caching
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/inline_15/main.c

@@ -0,0 +1,23 @@
+
+int x;
+
+void h()
+{
+  x = 1;
+}
+
+void g()
+{
+  h();
+}
+
+void f()
+{
+  g();
+}
+
+int main()
+{
+  f();
+}
+

regression/goto-instrument/inline_15/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function-inline main --log - --no-caching --verbosity 9
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1052,6 +1052,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     std::string function=cmdline.get_value("function-inline");
     assert(!function.empty());
 
+    bool caching=!cmdline.isset("no-caching");
+
     do_indirect_call_and_rtti_removal();
 
     status() << "Inlining calls of function `" << function << "'" << eom;
@@ -1063,7 +1065,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         function,
         ns,
         ui_message_handler,
-        true);
+        true,
+        caching);
     }
     else
     {
@@ -1076,7 +1079,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
           function,
           ns,
           ui_message_handler,
-          true);
+          true,
+          caching);
 
       if(have_file)
       {
@@ -1548,6 +1552,7 @@ void goto_instrument_parse_optionst::help()
     " --inline                     perform full inlining\n"
     " --partial-inline             perform partial inlining\n"
     " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
+    " --no-caching                 disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
     " --log <file>                 log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
     " --remove-function-pointers   replace function pointers by case statement over function calls\n" // NOLINT(*)
     " --add-library                add models of C library functions\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -53,7 +53,7 @@ Author: Daniel Kroening, [email protected]
   "(show-struct-alignment)(interval-analysis)(show-intervals)" \
   "(show-uninitialized)(show-locations)" \
   "(full-slice)(reachability-slice)(slice-global-inits)" \
-  "(inline)(partial-inline)(function-inline):(log):" \
+  "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
   "(remove-function-pointers)" \
   "(show-claims)(show-properties)(property):" \
   "(show-symbol-table)(show-points-to)(show-rw-set)" \

src/goto-programs/goto_inline.cpp

@@ -273,13 +273,15 @@ void goto_function_inline(
   const irep_idt function,
   const namespacet &ns,
   message_handlert &message_handler,
-  bool adjust_function)
+  bool adjust_function,
+  bool caching)
 {
   goto_inlinet goto_inline(
     goto_functions,
     ns,
     message_handler,
-    adjust_function);
+    adjust_function,
+    caching);
 
   goto_functionst::function_mapt::iterator f_it=
     goto_functions.function_map.find(function);
@@ -327,13 +329,15 @@ jsont goto_function_inline_and_log(
   const irep_idt function,
   const namespacet &ns,
   message_handlert &message_handler,
-  bool adjust_function)
+  bool adjust_function,
+  bool caching)
 {
   goto_inlinet goto_inline(
     goto_functions,
     ns,
     message_handler,
-    adjust_function);
+    adjust_function,
+    caching);
 
   goto_functionst::function_mapt::iterator f_it=
     goto_functions.function_map.find(function);
@@ -349,6 +353,7 @@ jsont goto_function_inline_and_log(
   // gather all calls
   goto_inlinet::inline_mapt inline_map;
 
+  // create empty call list
   goto_inlinet::call_listt &call_list=inline_map[f_it->first];
 
   goto_programt &goto_program=goto_function.body;

src/goto-programs/goto_inline.h

@@ -50,20 +50,23 @@ void goto_function_inline(
   goto_modelt &goto_model,
   const irep_idt function,
   message_handlert &message_handler,
-  bool adjust_function=false);
+  bool adjust_function=false,
+  bool caching=true);
 
 void goto_function_inline(
   goto_functionst &goto_functions,
   const irep_idt function,
   const namespacet &ns,
   message_handlert &message_handler,
-  bool adjust_function=false);
+  bool adjust_function=false,
+  bool caching=true);
 
 jsont goto_function_inline_and_log(
   goto_functionst &goto_functions,
   const irep_idt function,
   const namespacet &ns,
   message_handlert &message_handler,
-  bool adjust_function=false);
+  bool adjust_function=false,
+  bool caching=true);
 
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H