value_sets now have function identifiers [blocks: #3126] #3865

tautschnig · 2019-01-20T22:37:22Z

We are working towards removing the "function" field from
goto_programt::instructionst::instructiont, and thus need to pass the identifier
of the function whenever it actually is required.

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.

tautschnig · 2019-01-21T12:16:05Z

No, in the latest incarnation there isn't actually a member - where needed the function_id is passed in.

danpoe · 2019-01-21T12:17:17Z

@tautschnig Sounds good! Sorry, I accidentally closed the PR when I tried to comment.

smowton · 2019-01-21T14:28:42Z

src/analyses/flow_insensitive_analysis.cpp

-    new_data = state.transform(ns, t, l_next) || new_data;
+    bool new_data =
+      state.transform(ns, calling_function, l_call, f_it->first, r);
+    new_data = state.transform(ns, f_it->first, r, f_it->first, t) || new_data;


While you're editing this code, might be sensible to annotate these as "callsite -> head of function" and "callsite -> callsite successor" and so on, explaining the different function names we're passing in

smowton · 2019-01-21T14:33:04Z

src/goto-instrument/race_check.cpp

  L_M_ARG(const goto_functionst::goto_functiont &goto_function)
-  goto_programt &goto_program,
+    goto_programt &goto_program,


dodgy indent

Good catch! I've added a clang-format off/on.

allredj

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

allredj

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

martin-cs

I think this does what is claimed. I'm still not sure I see why removing the function field is needed but I recognise that this is part of a larger effort.

src/analyses/flow_insensitive_analysis.cpp

peterschrammel · 2019-01-28T20:44:11Z

src/analyses/flow_insensitive_analysis.cpp

-  fixedpoint(goto_functions);
+  initialize(goto_program);
+  goto_functionst goto_functions;
+  fixedpoint(function_id, goto_program, goto_functions);


What are the goto_functions used for?

They are used to resolve function calls in do_function_call_rec (though in this case it will just fail to resolve any function calls). That said, I have cleaned up the patch so that this change doesn't even show up anymore, because it was only an artefact of reordering functions in the file.

allredj

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

We are working towards removing the "function" field from goto_programt::instructionst::instructiont, and thus need to pass the identifier of the function whenever it actually is required.

allredj

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

tautschnig added the blocker label Jan 20, 2019

tautschnig requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, smowton and thk123 as code owners January 20, 2019 22:37

tautschnig changed the title ~~value_sets now have function identifiers [blocks: #3126]~~ value_sets now have function identifiers [depends-on: #3863, blocks: #3126] Jan 21, 2019

tautschnig added the dependent - do not merge label Jan 21, 2019

tautschnig force-pushed the function-value_sets branch from 368b11f to aa6aba7 Compare January 21, 2019 09:19

danpoe closed this Jan 21, 2019

danpoe reopened this Jan 21, 2019

smowton approved these changes Jan 21, 2019

View reviewed changes

tautschnig force-pushed the function-value_sets branch 2 times, most recently from ded3d24 to 5f4bb28 Compare January 21, 2019 16:31

tautschnig self-assigned this Jan 23, 2019

tautschnig force-pushed the function-value_sets branch from 5f4bb28 to b9b0a91 Compare January 23, 2019 18:37

tautschnig changed the title ~~value_sets now have function identifiers [depends-on: #3863, blocks: #3126]~~ value_sets now have function identifiers [blocks: #3126] Jan 23, 2019

tautschnig removed the dependent - do not merge label Jan 23, 2019

tautschnig assigned kroening, peterschrammel, martin-cs and chrisr-diffblue and unassigned tautschnig Jan 23, 2019

tautschnig force-pushed the function-value_sets branch from b9b0a91 to 5671835 Compare January 23, 2019 20:00

allredj reviewed Jan 23, 2019

View reviewed changes

tautschnig force-pushed the function-value_sets branch 2 times, most recently from cf046ed to 56d5cbb Compare January 26, 2019 20:44

tautschnig force-pushed the function-value_sets branch from 56d5cbb to d3576d4 Compare January 27, 2019 10:40

allredj reviewed Jan 27, 2019

View reviewed changes

martin-cs approved these changes Jan 27, 2019

View reviewed changes

src/analyses/flow_insensitive_analysis.cpp Show resolved Hide resolved

tautschnig unassigned martin-cs and chrisr-diffblue Jan 28, 2019

peterschrammel approved these changes Jan 28, 2019

View reviewed changes

peterschrammel removed their assignment Jan 28, 2019

tautschnig assigned tautschnig and unassigned kroening Jan 29, 2019

tautschnig force-pushed the function-value_sets branch from d3576d4 to cb1aeae Compare January 29, 2019 09:11

allredj reviewed Jan 29, 2019

View reviewed changes

value_sets now have function identifiers

61557dc

We are working towards removing the "function" field from goto_programt::instructionst::instructiont, and thus need to pass the identifier of the function whenever it actually is required.

tautschnig force-pushed the function-value_sets branch from cb1aeae to 61557dc Compare January 29, 2019 18:14

allredj reviewed Jan 30, 2019

View reviewed changes

tautschnig merged commit 04fac41 into diffblue:develop Jan 30, 2019

tautschnig deleted the function-value_sets branch January 30, 2019 07:48

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

value_sets now have function identifiers [blocks: #3126] #3865

value_sets now have function identifiers [blocks: #3126] #3865

Uh oh!

tautschnig commented Jan 20, 2019

Uh oh!

tautschnig commented Jan 21, 2019

Uh oh!

danpoe commented Jan 21, 2019

Uh oh!

smowton Jan 21, 2019

Uh oh!

tautschnig Jan 21, 2019

Uh oh!

smowton Jan 21, 2019

Uh oh!

tautschnig Jan 21, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

martin-cs left a comment

Uh oh!

Uh oh!

peterschrammel Jan 28, 2019

Uh oh!

tautschnig Jan 29, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

value_sets now have function identifiers [blocks: #3126] #3865

value_sets now have function identifiers [blocks: #3126] #3865

Uh oh!

Conversation

tautschnig commented Jan 20, 2019

Uh oh!

tautschnig commented Jan 21, 2019

Uh oh!

danpoe commented Jan 21, 2019

Uh oh!

smowton Jan 21, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 21, 2019

Choose a reason for hiding this comment

Uh oh!

smowton Jan 21, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 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!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

peterschrammel Jan 28, 2019

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!