Expand the documentation for goto-inline #6136
Conversation
martin-cs
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6136 +/- ##
===========================================
+ Coverage 67.40% 75.59% +8.18%
===========================================
Files 1157 1454 +297
Lines 95236 159745 +64509
===========================================
+ Hits 64197 120757 +56560
- Misses 31039 38988 +7949
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
martin-cs
force-pushed
the
fix/inline-documentation
branch
2 times, most recently
from
e4209b3 to
fdc3f54
Compare
|
Only CI failure is the incremental diff which I don't think is a problem. However I have run into a question -- should inlining be before or after return removal? cbmc/src/goto-programs/goto_inline_class.cpp Line 158 in 78a08ce checks for return instructions which implies that can be run before return removal. However not jumping to the end of the inlined function feels like a bug, likewise generating an The code-base seems inconsistent on the matter, in some places inlining is before return removal: but in others it is not: I would very much appreciate your thoughts on this. |
I'm adding some thoughts and observations here as invited. I am not sure I understand all of the subtleties enough to be considered an authority on this though (caveats end here). I've also rearranged and cut parts of the original to make my thoughts clearer.
I agree this looks suspect and the creation of the new
I don't recall exactly what happened before unifying the code path between different programs. I know some parts were changed (hence the bug on the
This one is under another condition and so (I guess) not always done before the "full inlining". This one does remove all the returns but is only doing partial inlining. Here this appears to be related to the Regardless of the above, there is always a call to |
|
On Tue, 2021-05-25 at 02:17 -0700, TGWDB wrote:
> I would very much appreciate your thoughts on this.
I'm adding some thoughts and observations here as invited. I am not
sure I understand all of the subtleties enough to be considered an
authority on this though (caveats end here).
I've also rearranged and cut parts of the original to make my
thoughts clearer.
All thoughts appreciated :-)
There is a long-standing issue with there being undocumented
assumptions made about which of the transformed / normal forms for
goto-programs various transformations work on.
> checks for return instructions which implies that can be run before
> return removal. However not jumping to the end of the inlined
> function feels like a bug, likewise generating an `OTHER`
> instruction is a bit suspect. So I am not sure this code actually
> works correctly without return removal.
I agree this looks suspect and the creation of the new `OTHER`
instructions does not inspire much confidence. I guess it would be
nice to try and find an example that can demonstrate a bug (or in the
process discover there is no bug/error).
Inlining something like...
```
inline int f00(int x) {
int ret = 0;
if (x == 0) {
return ret;
}
ret = 1;
return ret;
}
...
assert(f00(0) == 0);
...
```
/before/ return removal should show if there is an issue with the
inlining not processing returns correctly. What is harder is finding
the set of options / paths that will trigger this problem in an
externally visible way.
> The code-base seems inconsistent on the matter, in some places
> inlining is before return removal:
>
> https://github.com/diffblue/cbmc/blob/78a08ce28328ad0c15ca4e92ea15837856db833e/src/goto-programs/process_goto_program.cpp#L57
I don't recall exactly what happened before unifying the code path
between different programs. I know some parts were changed (hence the
bug on the `instrument_preconditions` locations). This might be an
artefact from that unification rather than the "correct" approach.
I tried to be very careful to respect ordering when unifying the
processing, so if it is possible now it should have been possible in at
least one of the tools before.
That said, returns are always removed after inlining even if they are
(also) removed before inlining.
My concern is not about whether it happens, it is when it happens. I
/think/ that inlining is buggy if it is done before return removal. If
this is the case then it should really be documented and the places
that it is done should be fixed OR we should fix goto-inline so it
works with either.
> https://github.com/diffblue/cbmc/blob/78a08ce28328ad0c15ca4e92ea15837856db833e/src/goto-instrument/goto_instrument_parse_options.cpp#L1132
This one does remove all the returns but is only doing partial
inlining.
Partial inlining uses the same code and thus should have the same issue
(assuming that it is triggered).
Here this appears to be related to the `escape-analysis` flag rather
than explicit inlining.
Yeah; this is what makes it hard to come up with a concrete bug.
Regardless of the above, there is always a call to
`goto_model.goto_functions.update()` (line 1609) that also does the
removal of returns, so it appears to always happen regardless of
whether an earlier pass may (also) do this.
I don't think that does return removal:
https://github.com/diffblue/cbmc/blob/6e7d38d368b75470248adffaa1c95ee7e7642795/src/goto-programs/goto_functions.h#L81
|
I guess we're finding the assumptions, or maybe the bugs that indicate the assumptions. :)
I was mostly hoping there was an easy way to find those flags/conditions.
It may be that these are subtle bugs that always existed and we're finding them now. I didn't see any mistakes in that re-arrangement (but was focusing on the locations at the time), and that bug was significantly more complex than simply merging the code paths alone would easily expose.
Agree on all of the above.
Correct, my mistake. I was still thinking of locations and other goto_model updates. |
|
On Wed, 2021-05-26 at 00:28 -0700, TGWDB wrote:
> All thoughts appreciated :-) There is a long-standing issue with
> there being undocumented assumptions made about which of the
> transformed / normal forms for goto-programs various
> transformations work on.
I guess we're finding the assumptions, or maybe the bugs that
indicate the assumptions. :)
Exactly!
> Inlining something like... ``` inline int f00(int x) { int ret = 0;
> if (x == 0) { return ret; } ret = 1; return ret; } ...
> assert(f00(0) == 0); ... ``` /before/ return removal should show if
> there is an issue with the inlining not processing returns
> correctly. What is harder is finding the set of options / paths
> that will trigger this problem in an externally visible way.
I was mostly hoping there was an easy way to find those
flags/conditions.
Find all the calls to inlining, trace back which do return removal
first and which don't, try the same code on different paths, if it
gives incorrect results then work out if it is caused by the inlining
or whether it was broken anyway (in the case of some of the more
obscure paths in goto-instrument).
OR, just try it our by modifying process_goto_programs. I suspect this
is what I will do when I have a little time.
> I tried to be very careful to respect ordering when unifying the
> processing, so if it is possible now it should have been possible
> in at least one of the tools before.
It may be that these are subtle bugs that always existed and we're
finding them now. I didn't see any mistakes in that re-arrangement
(but was focusing on the locations at the time), and that bug was
significantly more complex than simply merging the code paths alone
would easily expose.
Yes; there are (I suspect) many of the subtle interactions that we have
avoided more by luck than intent. Normalising the preprocessing is one
way to find / remove these.
If I had the time / when I have the time to try to de-tangle goto-
instrument, what we really need is a way of marking which
normalisations / transforms a goto-modelt has been through and then
adding pre/post conditions to each of the transforms for what they
require / ensure.
|
martin-cs
force-pushed
the
fix/inline-documentation
branch
from
fdc3f54 to
65034b8
Compare
|
( I haven't had time to dig into the ordering issues. I am inclined to merge this PR without comments about ordering and then have a go at sorting out the ordering of passes another time. ) |
martin-cs
force-pushed
the
fix/inline-documentation
branch
from
65034b8 to
2bd6f72
Compare
Some comments I wrote while working out the interfaces to the inlining code and how it can be used.