goto-symex: use function and called_function fields [blocks: #3126] #3844

tautschnig · 2019-01-18T20:03:46Z

goto_programt::instructionst::instructiont::function is going to go away, use
the fields that are already available within goto-symex.

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

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

kroening · 2019-01-19T10:25:43Z

src/goto-symex/symex_goto.cpp

-      frame.loop_iterations[goto_programt::loop_id(*state.source.pc)].count;
+    const auto &loop_id =
+      goto_programt::loop_id(state.source.function, *state.source.pc);
+


goto_programt::loop_id returns a temporary, so I would not use a reference here.

Done, and I've now added a second commit to make sure we use goto_programt::loop_id everywhere.

allredj

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

peterschrammel

Consider #3828 (comment)

allredj

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

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 67507db).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97969840
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-20T22:53:14Z

@peterschrammel It's perfectly possible that the TG failure is genuine and caused by renaming the function member to function_id. Could you please take a look and possibly create a suitable bump?

Marking this as do-not-merge for now.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 92ec183).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98122649
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 · 2019-01-24T10:01:25Z

TG update: https://github.com/diffblue/test-gen/pull/2852

allredj · 2019-01-24T10:11:20Z

@tautschnig could you please rebase this PR onto develop (or at least on top of #3876) so that I can compile with TG?

goto_programt::instructionst::instructiont::function is going to go away, use the fields that are already available within goto-symex.

This ensures we build loop identifiers in the same way everywhere.

"function" is too ambiguous and "function_identifier" is too long, and mixing them is even worse.

tautschnig · 2019-01-24T10:13:37Z

@allredj Rebase done.

allredj · 2019-01-24T12:58:52Z

@tautschnig thanks. TG bump passing.

allredj · 2019-01-24T12:59:34Z

Shall I merge?

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: f33f64e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98458367
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-24T13:10:29Z

@allredj Thanks a lot, was away from my desk - merge done. Please merge the corresponding TG update.

tautschnig added the blocker label Jan 18, 2019

tautschnig requested review from chrisr-diffblue, kroening, peterschrammel, pkesseli and smowton as code owners January 18, 2019 20:03

allredj reviewed Jan 18, 2019

View reviewed changes

kroening reviewed Jan 19, 2019

View reviewed changes

tautschnig force-pushed the function-symex branch from fb5bdcf to 08504ec Compare January 19, 2019 11:04

tautschnig requested a review from martin-cs as a code owner January 19, 2019 11:04

kroening approved these changes Jan 19, 2019

View reviewed changes

smowton approved these changes Jan 19, 2019

View reviewed changes

tautschnig force-pushed the function-symex branch from 08504ec to 91c66b4 Compare January 19, 2019 13:44

tautschnig assigned peterschrammel, martin-cs and chrisr-diffblue Jan 19, 2019

allredj reviewed Jan 19, 2019

View reviewed changes

peterschrammel approved these changes Jan 20, 2019

View reviewed changes

peterschrammel assigned tautschnig and unassigned peterschrammel Jan 20, 2019

tautschnig force-pushed the function-symex branch 4 times, most recently from c6bdc44 to 67507db Compare January 20, 2019 21:25

allredj reviewed Jan 20, 2019

View reviewed changes

tautschnig added the do not merge label Jan 20, 2019

tautschnig unassigned tautschnig and martin-cs Jan 20, 2019

tautschnig assigned peterschrammel and unassigned chrisr-diffblue Jan 20, 2019

tautschnig force-pushed the function-symex branch from 67507db to 92ec183 Compare January 22, 2019 06:55

allredj reviewed Jan 22, 2019

View reviewed changes

peterschrammel assigned allredj and unassigned peterschrammel Jan 23, 2019

tautschnig added 3 commits January 24, 2019 10:13

goto-symex: use function and called_function fields

3d2efc0

goto_programt::instructionst::instructiont::function is going to go away, use the fields that are already available within goto-symex.

Use goto_programt::loop_id

b7222de

This ensures we build loop identifiers in the same way everywhere.

symex: Consistently use function_id

f33f64e

"function" is too ambiguous and "function_identifier" is too long, and mixing them is even worse.

tautschnig force-pushed the function-symex branch from 92ec183 to f33f64e Compare January 24, 2019 10:13

allredj reviewed Jan 24, 2019

View reviewed changes

tautschnig merged commit e2cd2f3 into diffblue:develop Jan 24, 2019

tautschnig deleted the function-symex branch January 24, 2019 13:10

goto-symex: use function and called_function fields [blocks: #3126] #3844

goto-symex: use function and called_function fields [blocks: #3126] #3844

Uh oh!

Conversation

tautschnig commented Jan 18, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

kroening Jan 19, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 19, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel 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!

tautschnig commented Jan 20, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj commented Jan 24, 2019

Uh oh!

allredj commented Jan 24, 2019

Uh oh!

tautschnig commented Jan 24, 2019

Uh oh!

allredj commented Jan 24, 2019

Uh oh!

allredj commented Jan 24, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 24, 2019

Uh oh!

Uh oh!