Invoke goto_functions.update() after inlining #6493
Conversation
| goto_function_inline( | ||
| goto_functions, function_name, ns, log.get_message_handler()); | ||
| goto_functions.update(); |
There was a problem hiding this comment.
If one should always call them together, wouldn't be safer to add a proper API with both calls? It'd certainly help us to avoid these mistakes.
There was a problem hiding this comment.
Maybe. The problem is the cost of these calls. If you're making multiple modifications to goto programs and don't depend on unique instruction numbers, loop numbering in between, then you should not need to invoke it. There are, in fact, a lot more places in the contracts instrumentation code where such updates need to be considered.
There was a problem hiding this comment.
Could we at least mention in the goto_inline.h doc that it breaks the internal consistency of the goto model / function and that a call to goto_functionst::update is needed to restore it? Or maybe in the preconditions of natural_loops ?
What type of modifications require calls to update ?
There was a problem hiding this comment.
Hmm, I am wondering where to best document (or implement!) this. Any operations that add or remove instructions for a goto program require calls to update. I realise that goto_programt::validate does not actually check for these properties (as documented with the location_number and loop_number members of goto_programt::instructiont).
tautschnig
force-pushed
the
followup-6473
branch
from
7a3f2e6 to
62f4b81
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6493 +/- ##
===========================================
- Coverage 76.06% 76.06% -0.01%
===========================================
Files 1546 1546
Lines 165584 165618 +34
===========================================
+ Hits 125951 125975 +24
- Misses 39633 39643 +10
Continue to review full report at Codecov.
|
tautschnig
force-pushed
the
followup-6473
branch
2 times, most recently
from
2a96d8c to
2d691ea
Compare
Inlining will alter location (instruction) numbers, which need to be updated to once again be globally unique. With this change, invar_check_large requires an assigns clause for the loop as the local may alias analysis returns "UNKNOWN." The previous result was actually unsound, because the automatically computed assigns set did not include arr0, arr1, arr2, arr3, arr4. This also demonstrated that the implementation in the test was incorrect: it would not terminate when: *(arr[h]) == pivot && *(arr[l]) == pivot && h != r && l != r.
tautschnig
force-pushed
the
followup-6473
branch
from
2d691ea to
3af4718
Compare
Inlining will alter location (instruction) numbers, which need to be
updated to once again be globally unique.
This is a follow-up to #6473.