Update after remove returns #4151

tautschnig · 2019-02-11T07:19:18Z

This reverts #4147 and instead introduces a local update. This yields a much simpler protocol, as the size of the change also shows.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 66e0b75).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100406202
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: e362c86).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100411075

chrisr-diffblue · 2019-02-11T09:50:48Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1447,9 +1443,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
  {
    do_indirect_call_and_rtti_removal();

-    // recalculate numbers, etc.
-    goto_model.goto_functions.update();


Is this actually still needed, seeing as this follows from do_indirect_call_and_rtti_removal, not do_return_removal ?

Well, this commit just reverts that earlier change, I don't think it ever was needed.

kroening · 2019-02-11T09:58:50Z

Note that the location numbers are global, not local to a function. The global update is too expensive to be performed after every transformation.

What needs to be done here is to clean up goto_instrument to have a concept of 'steps', which can then imply a next step or require a previous step.

tautschnig · 2019-02-11T10:10:38Z

Note that the location numbers are global, not local to a function. The global update is too expensive to be performed after every transformation.

The proposed change here only does a single-function update, not the global one. It will not ensure globally unique numbers, but will ensure we have increasing numbers per function. We could instead use the facility from goto_functionst that does permit incremental numbering.

What needs to be done here is to clean up goto_instrument to have a concept of 'steps', which can then imply a next step or require a previous step.

That might work for goto-instrument, but would then still leave any other users of remove_returns at risk to be broken. Can we please please please avoid those implicit obligations and instead make things usable as building blocks where requirements are preferably guaranteed or at bare minimum documented?

kroening · 2019-02-11T10:17:55Z

I agree on the pain point entirely.
I think the right thing to do is to get rid of the location number altogether. I'll look into it.

kroening · 2019-02-11T10:36:14Z

The (relatively) easy thing to appears to be to change the location number to be locally unique, not globally.

smowton · 2019-02-11T12:13:50Z

Could I suggest passing goto_model_functiont to the pass instead of goto_programt? That wraps a goto_programt but also provides a back-pointer to its enclosing model for numbering purposes: https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/goto_model.h#L165

tautschnig · 2019-02-24T23:41:56Z

As removal of location numbers is a larger task that may not be completed in the near future I have followed @smowton's suggestion, which did not require many changes at all.

smowton

Looks good except I think you should remove every occurrence of ! from the PR ;)

smowton · 2019-02-25T11:49:24Z

src/goto-programs/remove_returns.cpp

@@ -142,10 +142,14 @@ void remove_returnst::replace_returns(
 /// \param function_is_stub: function (irep_idt -> bool) that determines whether
 ///   a given function ID is a stub
 /// \param goto_program: program to transform
-void remove_returnst::do_function_calls(
+/// \return False if, and only if, instructions have been inserted. In that case


Surely returning true if something has been done would be more intuitive? I appreciate there are various cbmc functions using the unix shell "zero = success" pattern, but I don't think this is a success/failure return.

I couldn't decide... - so I'll happily take the guidance that you and @thk123 provided and will amend this.

thk123

I note the original PR didn't have any tests, so it'd be great if possible to add one here?

I also strongly support @smowton's suggestion to return true if something happened. This is consistent with STL things where returning true indicates that something was inserted in to the set, for example. If also removes all the ! you have to put in at the callsite

tautschnig · 2019-02-25T12:50:44Z

I note the original PR didn't have any tests, so it'd be great if possible to add one here?

To be honest, I have no idea how to create a regression test for this (a unit test would seem possible, of course): In #4147 @kroening claimed that #4001 (which has since been merged) would fail without the fix, but even when using just the revert without the fix I cannot make any test fail. All of the code paths in goto-instrument take care of updating location numbers before any output is generated.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 845d60d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102161974
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

kroening · 2019-02-26T08:14:47Z

@tautschnig The failure was on Windows only, which made it really hard to diagnose.

kroening · 2019-02-26T08:16:00Z

The problem with this PR is still that it kills the global uniqueness of the location numbers?
If this is what we want, it needs a bigger audit.

tautschnig · 2019-02-26T09:32:53Z

@tautschnig The failure was on Windows only, which made it really hard to diagnose.

I'll try to reproduce it. Marking this PR work-in-progress for the moment.

The problem with this PR is still that it kills the global uniqueness of the location numbers?

No, goto_functionst maintains a counter and will only ever assign previously unused numbers. As a result there may be gaps, but numbers will be globally unique, and strictly monotone and contiguous per-function.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: db63e03).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102299143

This reverts commit abbb389. In diffblue#2089 a broad cleanup of redundant calls to .update() was done. Let's stay in this spirit and call .update() when necessary, and not "just to be safe."

remove_returnst::do_function_calls may introduce new instructions. Doing so requires a call to compute_location_numbers to ensure instruction numbers are assigned. To avoid recomputing location numbers across all goto functions, the facility from goto_functionst is used, which will ensure globally unique location numbers (though they might not be globally contiguous).

tautschnig · 2019-02-26T11:28:39Z

I'll try to reproduce it. Marking this PR work-in-progress for the moment.

It seems that removing the bug fix does not actually make any tests fail. I'll refrain from doing more debugging as certainly there is a possible problem, but we seemingly have a number of mitigations in place.

Putting this PR back in ready-for-review.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: cdab267).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102315448

tautschnig assigned kroening and peterschrammel Feb 11, 2019

tautschnig requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli and smowton as code owners February 11, 2019 07:19

tautschnig force-pushed the update-after-remove-returns branch from 66e0b75 to e362c86 Compare February 11, 2019 07:51

allredj reviewed Feb 11, 2019

View reviewed changes

chrisr-diffblue reviewed Feb 11, 2019

View reviewed changes

peterschrammel assigned tautschnig and unassigned kroening and peterschrammel Feb 12, 2019

tautschnig force-pushed the update-after-remove-returns branch from e362c86 to 989ffad Compare February 24, 2019 23:40

tautschnig assigned smowton, kroening and peterschrammel and unassigned tautschnig Feb 24, 2019

smowton approved these changes Feb 25, 2019

View reviewed changes

thk123 reviewed Feb 25, 2019

View reviewed changes

tautschnig unassigned smowton Feb 25, 2019

tautschnig force-pushed the update-after-remove-returns branch from 989ffad to 845d60d Compare February 25, 2019 12:56

allredj reviewed Feb 25, 2019

View reviewed changes

allredj approved these changes Feb 25, 2019

View reviewed changes

tautschnig force-pushed the update-after-remove-returns branch from 845d60d to db63e03 Compare February 26, 2019 09:27

tautschnig assigned tautschnig and unassigned kroening and peterschrammel Feb 26, 2019

tautschnig added do not merge work in progress labels Feb 26, 2019

allredj reviewed Feb 26, 2019

View reviewed changes

tautschnig added 2 commits February 26, 2019 11:27

Revert "bugfix: must do .update() after remove_returns"

2694ac5

This reverts commit abbb389. In diffblue#2089 a broad cleanup of redundant calls to .update() was done. Let's stay in this spirit and call .update() when necessary, and not "just to be safe."

tautschnig force-pushed the update-after-remove-returns branch from db63e03 to cdab267 Compare February 26, 2019 11:28

tautschnig removed do not merge work in progress labels Feb 26, 2019

tautschnig assigned kroening and peterschrammel and unassigned tautschnig Feb 26, 2019

allredj reviewed Feb 26, 2019

View reviewed changes

tautschnig merged commit ee11014 into diffblue:develop Mar 2, 2019

tautschnig deleted the update-after-remove-returns branch March 2, 2019 06:19

tautschnig restored the update-after-remove-returns branch December 27, 2020 06:43

Update after remove returns #4151

Update after remove returns #4151

Uh oh!

Conversation

tautschnig commented Feb 11, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue Feb 11, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 11, 2019

Choose a reason for hiding this comment

Uh oh!

kroening commented Feb 11, 2019

Uh oh!

tautschnig commented Feb 11, 2019

Uh oh!

kroening commented Feb 11, 2019

Uh oh!

kroening commented Feb 11, 2019

Uh oh!

smowton commented Feb 11, 2019

Uh oh!

tautschnig commented Feb 24, 2019

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

smowton Feb 25, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 25, 2019

Choose a reason for hiding this comment

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 25, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Feb 26, 2019

Uh oh!

kroening commented Feb 26, 2019

Uh oh!

tautschnig commented Feb 26, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 26, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!