Skip to content

Remove path strategy chooser from driver #3797

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 2 commits into from
Jan 16, 2019
Merged

Remove path strategy chooser from driver #3797

merged 2 commits into from
Jan 16, 2019

Conversation

peterschrammel
Copy link
Member

@peterschrammel peterschrammel commented Jan 13, 2019 •
edited
Loading

Makes parse_path_strategy_options a function. A BMC-algorithm-specific member shouldn't be owned by *bmc_parse_optionst; only the chosen option should be validated and passed.

  • 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.
  • 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).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj
allredj reviewed Jan 13, 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: eecdb00).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97178570

@smowton
Copy link
Contributor

smowton commented Jan 14, 2019

path_strategy_choosert is actually completely stateless; instead of making one and passing it to do_language_agnostic_bmc, how about simply making them free functions (the map strategies should probably be a static data structure, not a class member)

@peterschrammel
Copy link
Member Author

Yes, right, @smowton. I was a bit lazy and wanted to avoid breaking TG and SS by changing the interface.

@smowton
Copy link
Contributor

smowton commented Jan 14, 2019

I say break them, this is a pretty new interface, so the sooner it's made right the better! Plus I don't believe TG uses do-language-agnostic anyhow.

@peterschrammel
Make parse_path_strategy_options a function
6ce9bf4 
Removes an unnecessary member from *bmc_parse_optionst.

To implement an incremental_goto_checker for --paths,
we have to encapsulate everything algorithm-specfic
inside the incremental_goto_checker.
We can only parse the option in the driver, but
cannot pass on the path_strategy_chooser instance.
@peterschrammel peterschrammel force-pushed the refactor-path-strategy-chooser branch from eecdb00 to 903b059 Compare January 16, 2019 12:13
@peterschrammel
Copy link
Member Author

@smowton, please have a look whether 903b059 is what you envisaged.

@peterschrammel
Refactor path strategy chooser into free functions
50a9ef1 
Since keeping an instance is not an option,
we should avoid having to create an instance on every
stateless function call.
@peterschrammel peterschrammel force-pushed the refactor-path-strategy-chooser branch from 903b059 to 50a9ef1 Compare January 16, 2019 14:47
@smowton
Copy link
Contributor

smowton commented Jan 16, 2019

Yes that looks about right

@peterschrammel
Copy link
Member Author

peterschrammel commented Jan 16, 2019 •
edited
Loading

Yes that looks about right

@smowton, can you approve it?

allredj
allredj reviewed Jan 16, 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.

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

@peterschrammel peterschrammel merged commit 8984eb9 into diffblue:develop Jan 16, 2019
@peterschrammel peterschrammel deleted the refactor-path-strategy-chooser branch January 16, 2019 18:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig approved these changes

@cesaro cesaro Awaiting requested review from cesaro

@cristina-david cristina-david Awaiting requested review from cristina-david

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

@pkesseli pkesseli Awaiting requested review from pkesseli

+2 more reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

Reviewers whose approvals may not affect merge requirements
Assignees

@peterschrammel peterschrammel

Labels
Goto-checker
Projects
None yet
Milestone
No milestone
Development

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