Skip to content

Group symex options into symex_config structure #3431

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
Nov 26, 2018
Merged

Group symex options into symex_config structure #3431

merged 2 commits into from
Nov 26, 2018

Conversation

romainbrenguier
Copy link
Contributor

@romainbrenguier romainbrenguier commented Nov 16, 2018 •
edited
Loading

This makes it easy to separate the constant parameters of that class
from the other fields.

  • 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.
  • [na] The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • [na] 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).
  • [na] My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • [na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@romainbrenguier romainbrenguier requested a review from LAJW November 16, 2018 10:51
allredj
allredj reviewed Nov 16, 2018
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: 936fd9c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91653597

LAJW
LAJW approved these changes Nov 16, 2018
View reviewed changes
Copy link
Contributor

@LAJW LAJW left a comment

Choose a reason for hiding this comment

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

The more typed options, the better.

src/goto-symex/goto_symex.h Outdated
@@ -38,6 +38,35 @@ class namespacet;
class side_effect_exprt;
class typecast_exprt;

/// Configuration of the symbolic execution
struct symex_configt
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏ You might've forgotten final.

src/goto-symex/goto_symex.h Outdated
bool partial_loops;
std::string debug_level;

explicit symex_configt(const optionst &options)
Copy link
Contributor

Choose a reason for hiding this comment

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

🤔 I can never decide whether parsing (or doing any operation that can fail) in the constructor is a good or bad idea. I wonder what happens when an option is not specified.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I could have a non-member symex_configt symex_config(const optionst &) function instead. Will try that.

Copy link
Contributor

Choose a reason for hiding this comment

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

Making it a separate function only makes sense if the function can return an empty optional as an error for instance (constructors cannot return empty optionals).

Copy link
Contributor Author

Choose a reason for hiding this comment

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

The result of that is required for the goto_symext constructor anyway so using optional just there wouldn't solve the problem. I would suggest making the goto_symext constructor take a symex_configt instead.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Actually get_option functions have default for when the option is not specified (0 for int, "" for string) so we can go back to using a constructor and there is no reason for it to fail.

Copy link
Contributor

Choose a reason for hiding this comment

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

Not a fan of silent failures, but this seems to be a subject for another time.

@romainbrenguier romainbrenguier force-pushed the refactor/symex-config branch 2 times, most recently from 9745c58 to bf24482 Compare November 16, 2018 14:42
allredj
allredj reviewed Nov 16, 2018
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: bf24482).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91678677

peterschrammel
peterschrammel reviewed Nov 16, 2018
View reviewed changes
src/goto-symex/symex_builtin_functions.cpp Outdated
@@ -458,7 +458,7 @@ void goto_symext::symex_trace(
{
PRECONDITION(code.arguments().size() >= 2);

int debug_thresh = unsafe_string2int(debug_level);
int debug_thresh = unsafe_string2int(symex_config.debug_level);
Copy link
Member

Choose a reason for hiding this comment

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

Why not parse that right away?

@peterschrammel
Copy link
Member

The benefit of this is not obvious, but I'm not strictly opposed.

@romainbrenguier
Copy link
Contributor Author

@peterschrammel

The benefit of this is not obvious, but I'm not strictly opposed.

The benefits I see are that it simplifies the goto_symext class; it makes obvious in the code that a field comes from the configuration and thus is constant (they will all start with symex_config.); it makes clearer what are the options that can be passed to symex through the command line. We could also think of having an extra constructor using symex_configt instead of optiont and it will then be harder to forget about an option (not done in this PR so this argument doesn't really count here).

allredj
allredj reviewed Nov 19, 2018
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: 7de2106).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91842803

allredj
allredj reviewed Nov 19, 2018
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: 1dec39c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91894990

tautschnig
tautschnig approved these changes Nov 24, 2018
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.

Seems like a very good idea. Just a nit pick: there is a typo in the commit message: s/Pares/Parse/

@romainbrenguier
Group symex options into symex_config structure
8e177a5 
This makes it easy to separate the constant parameters of that class
from the other fields.
@romainbrenguier
Parse debug-level at symex_config construction
bf8e58b 
No functional change
allredj
allredj reviewed Nov 26, 2018
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: bf8e58b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92545158

@tautschnig tautschnig merged commit 7a98892 into diffblue:develop Nov 26, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel left review comments

@LAJW LAJW LAJW approved these changes

@allredj allredj allredj left review comments

@tautschnig tautschnig tautschnig approved these changes

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

Assignees

@romainbrenguier romainbrenguier

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

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