Skip to content

Maintain nondet and dynamic counters across symex instances [blocks: #3976] #3959

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 1 commit into from
Jan 31, 2019
Merged

Maintain nondet and dynamic counters across symex instances [blocks: #3976] #3959

merged 1 commit into from
Jan 31, 2019

Conversation

tautschnig
Copy link
Collaborator

  • 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 tautschnig mentioned this pull request Jan 26, 2019
Closed
@tautschnig tautschnig force-pushed the fix-3956-bitfields branch 2 times, most recently from bba27e4 to 93ac08f Compare January 27, 2019 10:39
allredj
allredj reviewed Jan 27, 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: 93ac08f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98729940

@tautschnig tautschnig changed the title Maintain nondet and dynamic counters across symex instances Maintain nondet and dynamic counters across symex instances [blocks: #3976] Jan 28, 2019
peterschrammel
peterschrammel approved these changes Jan 28, 2019
View reviewed changes
Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

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

Not for this PR, but maybe worth a performance test in future: Could util/fresh_symbol do the job?

@peterschrammel peterschrammel removed their assignment Jan 28, 2019
romainbrenguier
romainbrenguier suggested changes Jan 29, 2019
View reviewed changes
Copy link
Contributor

@romainbrenguier romainbrenguier left a comment

Choose a reason for hiding this comment

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

I'm not sure why there would be several goto_symext instantiations, which need to share symbols. But please don't introduce global variables.

src/goto-symex/goto_symex.h Outdated
@@ -418,7 +408,7 @@ class goto_symext
virtual void symex_input(statet &, const codet &);
virtual void symex_output(statet &, const codet &);

symex_nondet_generatort build_symex_nondet;
static unsigned nondet_count;
Copy link
Contributor

Choose a reason for hiding this comment

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

👎

@tautschnig
Copy link
Collaborator Author

I'm not sure why there would be several goto_symext instantiations, which need to share symbols.

cbmc --paths (path_explorert) creates a new goto_symext instance for each path.

But please don't introduce global variables.

Ack, but that's just the first commit here, which is a clean revert of your earlier patch. The second commit fixes this. But I can probably also get away without doing that revert and just directly make the modifications done in the second commit.

@tautschnig
Maintain nondet counters across symex instances
321402d 
Use the path storage, which maintains state across different symex
instantiations. While at it, also make the counters std::size_t as using limited
bitwidth is not a meaningful optimisation here.
@tautschnig
Copy link
Collaborator Author

@romainbrenguier I have now largely redone this, avoiding any reverts.

@peterschrammel I have followed your suggestion, and that change is now no longer present in here and #3999 takes care of it instead.

@romainbrenguier
Copy link
Contributor

@tautschnig

cbmc --paths (path_explorert) creates a new goto_symext instance for each path.

But please don't introduce global variables.

Ack, but that's just the first commit here, which is a clean revert of your earlier patch. The second commit fixes this. But I can probably also get away without doing that revert and just directly make the modifications done in the second commit.

Thanks for the explanation and sorry I didn't get this was fixed in the second commit, I think it's clearer without the revert.

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: 321402d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99235044

@tautschnig tautschnig merged commit 595bdaf into diffblue:develop Jan 31, 2019
@tautschnig tautschnig deleted the fix-3956-bitfields branch January 31, 2019 08:11
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

@peterschrammel peterschrammel peterschrammel approved these changes

@romainbrenguier romainbrenguier romainbrenguier approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

Assignees

@romainbrenguier romainbrenguier

Labels
blocker bugfix Symbolic Execution
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@tautschnig @romainbrenguier @peterschrammel @allredj