Skip to content

boolbv_width: distinguish zero from unknown size #6862

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
Jun 7, 2022
Merged

boolbv_width: distinguish zero from unknown size #6862

merged 1 commit into from
Jun 7, 2022

Conversation

tautschnig
Copy link
Collaborator

Use optionalt to distinguish types of known-zero size from those with
unknown size, which previously had the default value of zero.

  • 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.
  • 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 self-assigned this May 17, 2022
@tautschnig tautschnig changed the title boolbv_width: distinguish zero from unknown size [depends-on: #6825, #6860, #6861] boolbv_width: distinguish zero from unknown size [depends-on: #6825, #6861] May 19, 2022
@tautschnig tautschnig changed the title boolbv_width: distinguish zero from unknown size [depends-on: #6825, #6861] boolbv_width: distinguish zero from unknown size [depends-on: #6825] May 24, 2022
@tautschnig tautschnig force-pushed the cleanup/optional-size branch 2 times, most recently from 63a980e to ca634a3 Compare May 24, 2022 11:17
@codecov
Copy link

codecov bot commented May 24, 2022 •
edited
Loading

Codecov Report

Merging #6862 (6685497) into develop (13d0c18) will increase coverage by 0.02%.
The diff coverage is 74.28%.

@@             Coverage Diff             @@
##           develop    #6862      +/-   ##
===========================================
+ Coverage    77.76%   77.78%   +0.02%     
===========================================
  Files         1568     1568              
  Lines       180318   180269      -49     
===========================================
- Hits        140231   140230       -1     
+ Misses       40087    40039      -48
Impacted Files Coverage Δ
src/cbmc/cbmc_parse_options.cpp 80.00% <ø> (+0.09%) ⬆️
src/goto-cc/gcc_cmdline.cpp 79.23% <ø> (ø)
src/solvers/flattening/boolbv_abs.cpp 83.33% <ø> (+3.33%) ⬆️
src/solvers/flattening/boolbv_add_sub.cpp 48.27% <ø> (-0.06%) ⬇️
src/solvers/flattening/boolbv_bitreverse.cpp 100.00% <ø> (+14.28%) ⬆️
src/solvers/flattening/boolbv_bitwise.cpp 93.75% <ø> (+2.57%) ⬆️
src/solvers/flattening/boolbv_case.cpp 0.00% <ø> (ø)
src/solvers/flattening/boolbv_complex.cpp 0.00% <ø> (ø)
src/solvers/flattening/boolbv_concatenation.cpp 100.00% <ø> (+5.88%) ⬆️
src/solvers/flattening/boolbv_cond.cpp 0.00% <ø> (ø)
... and 35 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 3b340ad...6685497. Read the comment docs.

@tautschnig tautschnig force-pushed the cleanup/optional-size branch 3 times, most recently from 904b131 to 2124b9b Compare May 31, 2022 19:10
@tautschnig tautschnig changed the title boolbv_width: distinguish zero from unknown size [depends-on: #6825] boolbv_width: distinguish zero from unknown size May 31, 2022
@tautschnig tautschnig marked this pull request as ready for review May 31, 2022 19:10
@tautschnig tautschnig assigned kroening and unassigned tautschnig May 31, 2022
@kroening
Copy link
Member

kroening commented Jun 1, 2022

I got somewhat confused by the fact that a boolbv_widtht cache entry no longer has type entryt but optional<entryt>.

@tautschnig tautschnig force-pushed the cleanup/optional-size branch from 2124b9b to 28d7d3b Compare June 1, 2022 06:46
@tautschnig
Copy link
Collaborator Author

I got somewhat confused by the fact that a boolbv_widtht cache entry no longer has type entryt but optional<entryt>.

If it weren't optionalt, then we'd either need a Boolean flag in there ("invalid") or else types that don't have a width couldn't be cached. I'm happy to adjust the implementation to do either of these if that's deemed easier to follow.

@tautschnig tautschnig force-pushed the cleanup/optional-size branch from 28d7d3b to 3e70324 Compare June 1, 2022 06:55
@kroening
Copy link
Member

kroening commented Jun 1, 2022

If it weren't optionalt, then we'd either need a Boolean flag in there ("invalid") or else types that don't have a width couldn't be cached. I'm happy to adjust the implementation to do either of these if that's deemed easier to follow.

How about s.th. like using entryt = optionalt<entry_structt>

@tautschnig tautschnig force-pushed the cleanup/optional-size branch from 3e70324 to 1c27840 Compare June 1, 2022 13:01
@tautschnig
Copy link
Collaborator Author

If it weren't optionalt, then we'd either need a Boolean flag in there ("invalid") or else types that don't have a width couldn't be cached. I'm happy to adjust the implementation to do either of these if that's deemed easier to follow.

How about s.th. like using entryt = optionalt<entry_structt>

Done (I chose to use defined_entryt instead of entry_structt).

@tautschnig tautschnig force-pushed the cleanup/optional-size branch from 1c27840 to ca225ec Compare June 1, 2022 13:03
peterschrammel
peterschrammel approved these changes Jun 7, 2022
View reviewed changes
src/solvers/flattening/boolbv.cpp Outdated
@@ -85,8 +85,11 @@ bvt boolbvt::conversion_failed(const exprt &expr)
ignoring(expr);

// try to make it free bits
std::size_t width=boolbv_width(expr.type());
return prop.new_variables(width);
// TODO we likely end up in this path when an earlier call to boolbv_width
Copy link
Member

Choose a reason for hiding this comment

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

Does the TODO mean that something needs to be done or that we don't understand why this piece of code exists?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thank you for reminding me of this 😊 I have now audited all uses of conversion_failed, several of which were in response to calls to boolbv_width failing. That, however, would have resulted in the call to boolbv_width in here failing, making the code path really dangerous in the way it previously was (we would not have generated the correct number of free variables), and useless the way I changed it (making the CHECK_RETURN in here fail). All of these instances are now turned into early failures.

@peterschrammel peterschrammel removed their assignment Jun 7, 2022
@tautschnig tautschnig assigned tautschnig and unassigned martin-cs Jun 7, 2022
@tautschnig
boolbv_width: distinguish zero from unknown size
6685497 
Use optionalt to distinguish types of known-zero size from those with
unknown size, which previously had the default value of zero.

This makes it possible to support index expressions over zero bitwidth
arrays without mistaking the situation for an unknown size. (There is
not really anything wrong in having empty bitvectors, which we otherwise
already support (as of e021eef).)
@tautschnig tautschnig force-pushed the cleanup/optional-size branch from ca225ec to 6685497 Compare June 7, 2022 20:39
@tautschnig tautschnig merged commit 31e4ddf into diffblue:develop Jun 7, 2022
@tautschnig tautschnig deleted the cleanup/optional-size branch June 7, 2022 22:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kroening kroening kroening approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

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

@thomasspriggs thomasspriggs Awaiting requested review from thomasspriggs

@NlightNFotis NlightNFotis Awaiting requested review from NlightNFotis

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

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

Assignees

@tautschnig tautschnig

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@tautschnig @kroening @peterschrammel @martin-cs