Goto function inlining #262

danpoe · 2016-10-21T21:27:12Z

enhanced goto_inlinet to support inlining at the granularity of function calls, specifying whether inlining should be done transitively or non-transitively, and whether to put skip or leave function call on recursion
new option --function-inline for goto-instrument to transitively inline all calls a given function makes

kroening · 2016-10-30T14:17:58Z

May I ask for some reasonable squashing of commits, please?

danpoe · 2016-10-31T11:09:10Z

Ok, done.

kroening · 2016-12-06T12:27:31Z

May I have a rebase, please?

danpoe · 2016-12-13T15:49:48Z

Ok, I've rebased it.

tautschnig

I won't claim to have done a thorough review of the key implementation parts, but do have concerns about the merge that has happened in goto_instrument_parse_options.cpp. Could you please review this?

tautschnig · 2016-12-13T23:32:09Z

src/goto-instrument/goto_instrument_parse_options.h

@@ -51,7 +51,7 @@ Author: Daniel Kroening, [email protected]
  "(show-struct-alignment)(interval-analysis)(show-intervals)" \
  "(show-uninitialized)(show-locations)" \
  "(full-slice)(reachability-slice)" \
-  "(inline)(remove-function-pointers)" \
+  "(inline)(partial-inline)(function-inline):(log):" \


The rebase seems to have introduced a bug here: the "remove-function-pointers" option should not go away!

Yes, that's a bug.

tautschnig · 2016-12-13T23:35:10Z

src/goto-instrument/goto_instrument_parse_options.cpp

+
+    status() << "Inlining calls of function `" << function << "'" << eom;
+
+    if(!cmdline.isset("log"))


The log option is not documented in the help output

For my own record: done.

tautschnig · 2016-12-13T23:36:09Z

src/goto-instrument/goto_instrument_parse_options.cpp

+      }
+      else
+      {
+        std::cout << result << std::endl;


Shouldn't that be status() instead of std::cout?

result is a json object and it should be printed no matter the log level.

Ok, thanks for clarifying!

tautschnig · 2016-12-13T23:37:10Z

src/goto-instrument/goto_instrument_parse_options.cpp

+
+    goto_functions.update();
+    goto_functions.compute_loop_numbers();
+  }


Should this be replaced by a call to do_partial_inlining() ?

The inliner has an option adjust_function which indicates whether the function field of the inlined instructions should be updated to the value of the function they are being inlined into. The behavior of the previous inliner was to not change the function field. do_partial_inlining() still follows this old behavior, whereas here we do adjust the function field.

The reason why the function field has previously not been updated seems to have to do with how loop ids are formed. I would vote to always update the function field and make loop ids independent of that (as suggested in #295). What's your opinion on this?

I'll add my comments in #295; thanks for clarifying why do_partial_inlining wouldn't do the job here.

tautschnig · 2016-12-13T23:37:38Z

src/goto-instrument/goto_instrument_parse_options.cpp

+
+    status() << "Performing full inlining" << eom;
+    goto_inline(goto_functions, ns, ui_message_handler, true);
+  }


I am surprised this code is marked as new, I thought we had had it before already?

Yes that's strange. Only line 1064 is new.

tautschnig · 2016-12-13T23:39:00Z

src/goto-programs/goto_inline.cpp

@@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]

 \*******************************************************************/

+#include <iostream>


Is that really being used here?

tautschnig

See my earlier comments for changes that had been requested. I remain a bit confused by what genuinely is new code vs. what github thinks is new.

danpoe · 2017-01-11T14:34:57Z

Thanks for your help in getting this merged. I checked the diffs and they're mostly reasonable. Code that is marked as new and is based on existing code concerns the following functions:

parameter_assignments()
parameter_destruction()
replace_return()
replace_location()
insert_function_body()
insert_function_nobody()

Those functions are based on previously existing code which I separated out into these functions (with some changes).

tautschnig · 2017-01-11T14:47:09Z

src/goto-programs/goto_inline.cpp

+  catch(const char *e)
+  {
+    goto_inline.error() << e << messaget::eom;
+    throw 0;


Applies above as well: calling error() here makes it impossible to include/report a source location. Couldn't you invoke error() at place where an exception is thrown at present, and then throw 0; in those places?

tautschnig · 2017-01-11T14:48:20Z

src/goto-programs/goto_inline.cpp


-  goto_inline.smallfunc_limit=_smallfunc_limit;
+  goto_functionst::function_mapt::iterator f_it
+    =goto_functions.function_map.find(function);


assignment operator on preceding line

tautschnig · 2017-01-11T14:49:10Z

src/goto-programs/goto_inline_class.cpp

+
+//#define DEBUG
+
+#include <iostream>


Should not be necessary

tautschnig · 2017-01-11T14:49:53Z

src/goto-programs/goto_inline_class.cpp

+  for(code_typet::parameterst::const_iterator
+      it2=parameter_types.begin();
+      it2!=parameter_types.end();
+      it2++)


My understanding is that this is existing code. In future, this should be moved to a ranged for.

tautschnig · 2017-01-11T15:52:04Z

src/goto-instrument/goto_instrument_parse_options.cpp

+
+    status() << "Inlining calls of function `" << function << "'" << eom;
+
+    if(!cmdline.isset("log"))


For my own record: done.

martin-cs · 2017-01-12T13:04:34Z

@danpoe There are a page or so of linter errors; please could you fix ASAP.

@kroening Merging this will help speed up work on the Toyota project. Michael has signed it off; please can you merge it?

danpoe · 2017-01-13T11:03:19Z

Ok, the linter issues are also fixed now.

peterschrammel · 2017-01-17T13:10:51Z

@kroening, this looks mergeable now.

…avis_config Update Travis config to reflect upstream changes

Include GOTO guard expressions in variable sensitivity data dependencies

kroening self-assigned this Oct 30, 2016

kroening added the enhancement label Oct 30, 2016

danpoe force-pushed the goto-function-inlining branch from 3204cf1 to 70a0ae3 Compare October 31, 2016 11:06

danpoe force-pushed the goto-function-inlining branch from 3f66250 to 983c080 Compare November 17, 2016 16:50

danpoe force-pushed the goto-function-inlining branch 2 times, most recently from 69fa5d1 to 9ddfb85 Compare December 13, 2016 15:47

tautschnig requested changes Dec 13, 2016

View reviewed changes

tautschnig assigned danpoe and unassigned kroening Dec 13, 2016

danpoe force-pushed the goto-function-inlining branch from 9ddfb85 to 3095608 Compare December 19, 2016 22:24

tautschnig requested changes Jan 11, 2017

View reviewed changes

tautschnig reviewed Jan 11, 2017

View reviewed changes

danpoe force-pushed the goto-function-inlining branch from 3095608 to a5faba6 Compare January 11, 2017 15:50

tautschnig approved these changes Jan 11, 2017

View reviewed changes

danpoe force-pushed the goto-function-inlining branch 3 times, most recently from b162e12 to d83ca14 Compare January 13, 2017 11:02

danpoe force-pushed the goto-function-inlining branch from d83ca14 to 5150c62 Compare January 17, 2017 12:12

goto function inlining at function call granularity

05f19bf

danpoe force-pushed the goto-function-inlining branch from 5150c62 to 05f19bf Compare January 17, 2017 14:03

kroening merged commit c655301 into diffblue:master Jan 17, 2017

danpoe deleted the goto-function-inlining branch January 17, 2017 17:46

smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018

Merge pull request diffblue#262 from diffblue/smowton/admin/update_tr…

87bc2f0

…avis_config Update Travis config to reflect upstream changes

chrisr-diffblue added a commit to chrisr-diffblue/cbmc that referenced this pull request Aug 24, 2018

Merge pull request diffblue#262 from diffblue/issue259

1cc3158

Include GOTO guard expressions in variable sensitivity data dependencies

FrNecas mentioned this pull request Mar 11, 2021

Update to CBMC 5.7 diffblue/2ls#148

Merged


		status() << "Inlining calls of function `" << function << "'" << eom;

		if(!cmdline.isset("log"))

		@@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]

		\*******************************************************************/

		#include <iostream>

Goto function inlining #262

Goto function inlining #262

Uh oh!

Conversation

danpoe commented Oct 21, 2016

Uh oh!

kroening commented Oct 30, 2016

Uh oh!

danpoe commented Oct 31, 2016

Uh oh!

kroening commented Dec 6, 2016

Uh oh!

danpoe commented Dec 13, 2016

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

danpoe commented Jan 11, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Jan 12, 2017

Uh oh!

danpoe commented Jan 13, 2017

Uh oh!

peterschrammel commented Jan 17, 2017

Uh oh!

Uh oh!