L1 renaming at each declaration #3980

tautschnig · 2019-01-28T16:05:18Z

~~I still need to review why the second commit is necessary, thus marking work-in-progress.~~

Each commit message has a non-empty body, explaining why the change was made.
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.

tautschnig · 2019-01-28T16:10:23Z

Actually marking this RFC: the second commit makes perfect sense, it's odd that previously the suffix was not included. Could TG people (@thk123, @allredj, @peterschrammel, or anyone else) let me know whether this breaks anything on your end?

smowton · 2019-01-28T16:52:08Z

Would you mind elaborating briefly what kind of thing previously went wrong? I get the vague idea but just want to check my understanding. Some of that explanation might usefully make its way into comments in symex_decl.

Also am I right in thinking the symex_dead changes are purely cleanup and don't change behaviour?

tautschnig · 2019-01-28T17:20:20Z

Yes, I need to add a lot more documentation here/in the commit message. The (observable) problem is that objects declared in loops got the same L1 name, which implies they had the same address. Thus objects were spuriously reported as dead when their address was taken, because a pointer to the latest (live) object would be the same as one to an earlier (genuinely dead) object. A problem not yet fully fixed is regression/cbmc/vla3, which still fails despite the work here.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 205baa8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98894303
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.

tautschnig · 2019-01-30T18:46:08Z

I have cleaned up the changes a bit and made the commit messages clearer.

allredj

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

allredj

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

allredj

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

allredj

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

src/goto-symex/goto_symex_state.cpp

src/goto-symex/symex_decl.cpp

src/goto-symex/symex_function_call.cpp

romainbrenguier · 2019-02-18T11:48:24Z

src/goto-symex/path_storage.h

+    auto entry = unique_index_map.emplace(id, minimum_index);
+
+    if(!entry.second)
+      entry.first->second = std::max(entry.first->second + 1, minimum_index);


It looks like we could avoid the if condition if the function is always called with the same minimum index, I don't know if that's always the case.

No, even right now we (intentionally) use 0 for L1 indices when setting up new threads, but elsewhere use 1. And also that facility is rather general, we could as well use it for non-det counters any maybe others.

allredj

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

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 9f9c8b8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102972059
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 2777f85).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102999251
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: a382218).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103000236
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 3dbd7ba).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103022135
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: d165461).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103065221
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

src/goto-symex/goto_symex_state.h

src/goto-symex/path_storage.h

Try to make clearer what we can(not) remove from renaming maps. Also do small cleanups of the code.

This was done up until c8f0f7b. The (observable) problem tackled here is that objects declared in loops got the same L1 name, which implies they had the same address. Thus objects were spuriously reported as dead when their address was taken, because a pointer to the latest (live) object would be the same as one to an earlier (genuinely dead) object. A side effect of this change is objects generated for test suites now have L1 indices, as witnessed in the pointer-function-parameters test.

allredj

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

tautschnig added bugfix work in progress labels Jan 28, 2019

tautschnig requested review from kroening, peterschrammel, pkesseli and smowton as code owners January 28, 2019 16:05

tautschnig added RFC Request for comment and removed work in progress labels Jan 28, 2019

tautschnig assigned smowton, thk123, kroening, peterschrammel and allredj Jan 28, 2019

tautschnig force-pushed the block-scope branch from e57ec80 to 205baa8 Compare January 28, 2019 22:59

allredj reviewed Jan 29, 2019

View reviewed changes

tautschnig force-pushed the block-scope branch from 205baa8 to ed73813 Compare January 30, 2019 18:45

allredj reviewed Jan 31, 2019

View reviewed changes

tautschnig force-pushed the block-scope branch from ed73813 to 953e2d0 Compare January 31, 2019 08:21

tautschnig removed the RFC Request for comment label Jan 31, 2019

allredj reviewed Jan 31, 2019

View reviewed changes

tautschnig force-pushed the block-scope branch from 953e2d0 to 1bab7c1 Compare January 31, 2019 16:41

allredj reviewed Jan 31, 2019

View reviewed changes

tautschnig added the Symbolic Execution label Feb 4, 2019

tautschnig force-pushed the block-scope branch from 1bab7c1 to 83e58f3 Compare February 5, 2019 09:59

allredj reviewed Feb 5, 2019

View reviewed changes

tautschnig force-pushed the block-scope branch from 83e58f3 to 9f90b20 Compare February 15, 2019 15:13

romainbrenguier reviewed Feb 18, 2019

View reviewed changes

tautschnig unassigned smowton Feb 21, 2019

tautschnig added the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Feb 21, 2019

tautschnig force-pushed the block-scope branch from 450aca6 to f4c2262 Compare February 21, 2019 12:58

tautschnig force-pushed the block-scope branch from f4c2262 to 9806ccd Compare March 2, 2019 07:19

tautschnig assigned tautschnig and unassigned thk123, kroening, peterschrammel and allredj Mar 2, 2019

allredj reviewed Mar 2, 2019

View reviewed changes

tautschnig force-pushed the block-scope branch from 9806ccd to 9f9c8b8 Compare March 3, 2019 21:41

allredj reviewed Mar 3, 2019

View reviewed changes

tautschnig force-pushed the block-scope branch 2 times, most recently from 2777f85 to a382218 Compare March 4, 2019 07:48

allredj reviewed Mar 4, 2019

View reviewed changes

tautschnig force-pushed the block-scope branch 2 times, most recently from 3885343 to 3dbd7ba Compare March 4, 2019 10:28

allredj reviewed Mar 4, 2019

View reviewed changes

tautschnig force-pushed the block-scope branch from 3dbd7ba to d165461 Compare March 4, 2019 14:13

allredj reviewed Mar 4, 2019

View reviewed changes

romainbrenguier approved these changes Mar 6, 2019

View reviewed changes

src/goto-symex/goto_symex_state.h Outdated Show resolved Hide resolved

src/goto-symex/path_storage.h Show resolved Hide resolved

tautschnig added 2 commits March 6, 2019 22:36

Clarify comments in symex_dead

365f246

Try to make clearer what we can(not) remove from renaming maps. Also do small cleanups of the code.

tautschnig force-pushed the block-scope branch from d165461 to a397a58 Compare March 6, 2019 22:53

tautschnig merged commit 28dc3d7 into diffblue:develop Mar 7, 2019

tautschnig deleted the block-scope branch March 7, 2019 00:21

allredj reviewed Mar 7, 2019

View reviewed changes

tautschnig mentioned this pull request Apr 13, 2019

[SV-COMP'18 7/19] Ensure that local declarations do not introduce spurious dead warnings #1996

Closed

L1 renaming at each declaration #3980

L1 renaming at each declaration #3980

Uh oh!

Conversation

tautschnig commented Jan 28, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Jan 28, 2019

Uh oh!

smowton commented Jan 28, 2019

Uh oh!

tautschnig commented Jan 28, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 30, 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!

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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

romainbrenguier Feb 18, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 21, 2019

Choose a reason for hiding this comment

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!

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!

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!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig commented Jan 28, 2019 •

edited

Loading