Skip to content

symex: source is not optional #3890

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 3 commits into from
Feb 12, 2019
Merged

symex: source is not optional #3890

merged 3 commits into from
Feb 12, 2019

Conversation

kroening
Copy link
Member

@kroening kroening commented Jan 22, 2019 •
edited
Loading

This is probably the worst case of use of unitialised data that we have. Most parts of the code base assume that source.pc is a valid iterator, yet the interface explicitly allows it to be uninitialised.

  • 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.

@kroening kroening requested review from smowton and thk123 January 22, 2019 11:49
@kroening kroening force-pushed the source-is-not-optional branch from 8dae6fe to b071672 Compare January 22, 2019 11:51
tautschnig
tautschnig approved these changes Jan 22, 2019
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I approve of the general direction, but I would suggest that the two commits be squashed (and some further work is necessary as CI is failing) as neither of them makes sense without the other.

@kroening
Copy link
Member Author

The first one works by itself, and could be seen as an improvement.
The second then removes dead code.
The CI issue is that slice_by_trace wants to produce SSA_steps without source, and there isn't an obvious one to use.

@tautschnig
Copy link
Collaborator

The CI issue is that slice_by_trace wants to produce SSA_steps without source, and there isn't an obvious one to use.

One could be solved by storing a source in the merge_map_back, the other could probably just use the source from the front element (before emplacing a new element at the front)?

@tautschnig tautschnig changed the title symex: source is not optional symex: source is not optional [depends-on: #3971] Jan 28, 2019
@tautschnig
Copy link
Collaborator

This one should be easy once #3971 has been merged.

@kroening
Copy link
Member Author

This one should be easy once #3971 has been merged.

Indeed!

@tautschnig tautschnig force-pushed the source-is-not-optional branch from b071672 to b563adb Compare January 29, 2019 08:04
@tautschnig tautschnig changed the title symex: source is not optional [depends-on: #3971] symex: source is not optional Jan 29, 2019
@tautschnig
Copy link
Collaborator

Rebased as #3971 has been merged.

@kroening kroening force-pushed the source-is-not-optional branch from b563adb to 707efb6 Compare January 29, 2019 09:27
@tautschnig tautschnig force-pushed the source-is-not-optional branch from 707efb6 to 2cd585a Compare January 31, 2019 08:09
allredj
allredj reviewed Jan 31, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@tautschnig tautschnig force-pushed the source-is-not-optional branch from 2cd585a to 9d3d87b Compare February 5, 2019 20:16
allredj
allredj reviewed Feb 5, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@tautschnig tautschnig force-pushed the source-is-not-optional branch from 9d3d87b to 58d7bcf Compare February 9, 2019 10:04
allredj
allredj reviewed Feb 9, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Daniel Kroening and others added 3 commits February 12, 2019 16:45
@tautschnig
Ensure goto_symex_statet::source is always set
09de169 
sourcet contains an interator, and the interface explicitly allows it to be
uninitialised.  However, most parts of the code base access source.pc
without checking.
@tautschnig
Refactor goto_symext initialisation API
4302619 
Avoid doing the same start_function set-up three times, and avoid redundant work
between different initialize* functions when one always calls the other.
@tautschnig
remove the trivial constructor from symex_targett::sourcet
9e0c5a3 
sourcet contains an interator, and the current interface explicitly allows
it to be uninitialised.  However, most parts of the code base access
source.pc without checking.  This commit removes the option to leave the
source uninitialized.
@tautschnig tautschnig force-pushed the source-is-not-optional branch from 58d7bcf to 9e0c5a3 Compare February 12, 2019 17:39
@tautschnig tautschnig merged commit e3ff246 into develop Feb 12, 2019
@tautschnig tautschnig deleted the source-is-not-optional branch February 12, 2019 19:22
allredj
allredj reviewed Feb 12, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@tautschnig tautschnig tautschnig approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@smowton smowton Awaiting requested review from smowton

@thk123 thk123 Awaiting requested review from thk123

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@danpoe danpoe Awaiting requested review from danpoe

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Awaiting requested review from hannes-steffenhagen-diffblue

Assignees

@tautschnig tautschnig

Labels
bugfix
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@kroening @tautschnig @peterschrammel @allredj @martin-cs @chrisr-diffblue