Skip to content

Use expected_width parameter in flattening/boolbv_if to simplify error handling #3043

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

Use expected_width parameter in flattening/boolbv_if to simplify error handling #3043

merged 2 commits into from
Sep 26, 2018

Conversation

@hannes-steffenhagen-diffblue
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue commented Sep 25, 2018 •
edited
Loading

  • Each commit message has a non-empty body, explaining why the change was made.
  • My contribution is formatted in line with CODING_STANDARD.md.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • 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) (not applicable).
  • 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 Sep 25, 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: 3779e52).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85890465

tautschnig
tautschnig requested changes Sep 25, 2018
View reviewed changes
src/solvers/flattening/boolbv_if.cpp Outdated
const bvt &false_case_bv = convert_bv(expr.false_case());

if(op1_bv.size()!=width || op2_bv.size()!=width)
if(true_case_bv.size() != width || false_case_bv.size() != width)
Copy link
Collaborator

@tautschnig tautschnig Sep 25, 2018

Choose a reason for hiding this comment

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

I think width should just be passed as second argument to convert_bv thanks to your earlier work?!

Copy link
Contributor

@NlightNFotis NlightNFotis Sep 26, 2018

Choose a reason for hiding this comment

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

@hannes-steffenhagen-diffblue convert_bv in boolbv.cpp was changed recently to take an optional size. https://github.com/diffblue/cbmc/blob/develop/src/solvers/flattening/boolbv.cpp#L114 That makes the invariant present here as well unnecessary.

NlightNFotis
NlightNFotis suggested changes Sep 26, 2018
View reviewed changes
Copy link
Contributor

@NlightNFotis NlightNFotis left a comment

Choose a reason for hiding this comment

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

The data invariant is not needed, just pass the width as an extra argument to convert_bv. The invariant is being enforced inside convert_bv now.

@hannes-steffenhagen-diffblue
Copy link
Contributor Author

hannes-steffenhagen-diffblue commented Sep 26, 2018

Apologies, the changes to convert_bv hadn't been made when I committed these changes. I'll revise them.

@hannes-steffenhagen-diffblue
Rename variables in boolbv_if for easier legibility
b5b989d
@hannes-steffenhagen-diffblue
Use convert_bv expected_width parameter in boolbv_if
2ab7ac7 
The second parameter to convert_bv will cause to function to fail if the
resulting bitvector doesn't have the width we say it should have. We use this to
avoid doing an explicit check in this file.
@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue force-pushed the feature-invariant_cleanup-flattening-if branch from 3779e52 to 2ab7ac7 Compare September 26, 2018 13:56
@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue changed the title Invariant cleanup in flattening/boolbv_if Use expected_width parameter in flattening/boolbv_if to simplify error handling Sep 26, 2018
@hannes-steffenhagen-diffblue
Copy link
Contributor Author

hannes-steffenhagen-diffblue commented Sep 26, 2018

@NlightNFotis @tautschnig I believe I've addresses your comments, can you rereview?

NlightNFotis
NlightNFotis approved these changes Sep 26, 2018
View reviewed changes
Copy link
Contributor

@NlightNFotis NlightNFotis left a comment

Choose a reason for hiding this comment

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

Looks good to me.

allredj
allredj reviewed Sep 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: 2ab7ac7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86025732

@NlightNFotis NlightNFotis merged commit 6b6302e into diffblue:develop Sep 26, 2018
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

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

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

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

+2 more reviewers

@allredj allredj allredj left review comments

@NlightNFotis NlightNFotis NlightNFotis approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@hannes-steffenhagen-diffblue @tautschnig @NlightNFotis @allredj