new option --no-caching for use with inlining to disable caching of intermediate results

Author: danpoe

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

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

src/goto-programs/goto_inline_class.cpp

@@ -682,6 +682,12 @@ void goto_inlinet::expand_function_call(
         function,
         arguments,
         constrain);
+
+      if(!caching)
+      {
+        inline_log.cleanup(cached.body);
+        cache.erase(identifier);
+      }
     }
     else
     {
@@ -1146,6 +1152,29 @@ void goto_inlinet::output_inline_map(
 
 /*******************************************************************\
 
+Function: output_cache
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void goto_inlinet::output_cache(std::ostream &out) const
+{
+  for(auto it=cache.begin(); it!=cache.end(); it++)
+  {
+    if(it!=cache.begin())
+      out << ", ";
+
+    out << it->first << "\n";
+  }
+}
+
+/*******************************************************************\
+
 Function: cleanup
 
   Inputs:
@@ -1257,8 +1286,9 @@ void goto_inlinet::goto_inline_logt::copy_from(
     assert(it1->location_number==it2->location_number);
 
     log_mapt::const_iterator l_it=log_map.find(it1);
-    if(l_it!=log_map.end())
+    if(l_it!=log_map.end()) // a segment starts here
     {
+      // as 'to' is a fresh copy
       assert(log_map.find(it2)==log_map.end());
 
       goto_inline_log_infot info=l_it->second;

src/goto-programs/goto_inline_class.h

@@ -24,11 +24,13 @@ class goto_inlinet:public messaget
     goto_functionst &goto_functions,
     const namespacet &ns,
     message_handlert &message_handler,
-    bool adjust_function):
+    bool adjust_function,
+    bool caching=true):
     messaget(message_handler),
     goto_functions(goto_functions),
     ns(ns),
-    adjust_function(adjust_function)
+    adjust_function(adjust_function),
+    caching(caching)
   {
   }
 
@@ -64,6 +66,8 @@ class goto_inlinet:public messaget
     std::ostream &out,
     const inline_mapt &inline_map);
 
+  void output_cache(std::ostream &out) const;
+
   // call after goto_functions.update()!
   jsont output_inline_log_json()
   {
@@ -127,6 +131,8 @@ class goto_inlinet:public messaget
   const namespacet &ns;
 
   const bool adjust_function;
+  const bool caching;
+
   goto_inline_logt inline_log;
 
   void goto_inline_nontransitive(