Skip to content

Evaluating sizeof over __CPROVER_bool requires special cases #3183

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
Oct 29, 2018
Merged

Evaluating sizeof over __CPROVER_bool requires special cases #3183

merged 1 commit into from
Oct 29, 2018

Conversation

tautschnig
Copy link
Collaborator

__CPROVER_bool is just a single bit, and not part of any language standard
describing the semantics of sizeof. We can declare arrays of __CPROVER_bool,
which will thus have elements that are not aligned on byte boundaries. Using
sizeof with such an array thus requires specific handling.

  • 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.
  • 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 Oct 15, 2018
Merged
3 tasks
allredj
allredj reviewed Oct 15, 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.

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

allredj
allredj reviewed Oct 15, 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.

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

smowton
smowton approved these changes Oct 17, 2018
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

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

In some places you align to config.ansi_c.char_width and in others to 8; check if we're using the right one in the right place? Otherwise just one nitpick to attend.

src/util/pointer_offset_size.cpp Outdated
++bit_field_bits;
const std::size_t bytes = bit_field_bits / 8;
bit_field_bits %= 8;
result = plus_exprt(result, from_integer(bytes, result.type()));
Copy link
Contributor

Choose a reason for hiding this comment

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

Perhaps check for bytes == 0 to avoid creating a needless stack of +0s that will needlessly obscure what we're doing if not simplified away yet?

allredj
allredj reviewed Oct 22, 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: 8f299c7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88745816

kroening
kroening reviewed Oct 26, 2018
View reviewed changes
src/ansi-c/c_typecheck_expr.cpp
@@ -979,7 +979,7 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)

exprt new_expr;

if(type.id()==ID_c_bit_field)
if(type.id() == ID_c_bit_field || type.id() == ID_bool)
{
err_location(expr);
error() << "sizeof cannot be applied to bit fields" << eom;
Copy link
Member

Choose a reason for hiding this comment

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

The error message may be a bit confusing -- I'd give this a separate case.

kroening
kroening reviewed Oct 26, 2018
View reviewed changes
src/ansi-c/c_typecheck_expr.cpp Outdated
@@ -1733,7 +1733,7 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr)

exprt &op=expr.op0();

if(op.type().id()==ID_c_bit_field)
if(op.type().id() == ID_c_bit_field || op.type().id() == ID_bool)
{
err_location(expr);
error() << "cannot take address of a bit field" << eom;
Copy link
Member

Choose a reason for hiding this comment

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

Same here.

@kroening kroening assigned tautschnig and unassigned kroening Oct 26, 2018
@tautschnig
Evaluating sizeof over __CPROVER_bool requires special cases
3124621 
__CPROVER_bool is just a single bit, and not part of any language standard
describing the semantics of sizeof. We can declare arrays of __CPROVER_bool,
which will thus have elements that are not aligned on byte boundaries. Using
sizeof with such an array thus requires specific handling.
@tautschnig tautschnig merged commit 7fd6f21 into diffblue:develop Oct 29, 2018
@tautschnig tautschnig deleted the cprover_bool-sizeof branch October 29, 2018 16:58
allredj
allredj reviewed Oct 29, 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: 3124621).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89538458

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

@smowton smowton smowton approved these changes

@kroening kroening kroening approved these changes

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

@pkesseli pkesseli Awaiting requested review from pkesseli

Assignees

@tautschnig tautschnig

Labels
bugfix C Front End
Projects
None yet
Milestone
No milestone
Development

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