Skip to content

prohibit pointers to bit-vectors that are not byte-aligned #7444

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
Dec 16, 2022
Merged

prohibit pointers to bit-vectors that are not byte-aligned #7444

merged 1 commit into from
Dec 16, 2022

Conversation

kroening
Copy link
Member

This adds checks to the C front-end that prohibit taking the address of objects that cannot be addressed with byte-granularity pointers. This includes proper Booleans (not to be confused with _Bool) and __CPROVER_bitvector-typed objects whose width is not a multiple of 8.

Fixes #7104.

  • 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).
  • 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 approved these changes Dec 16, 2022
View reviewed changes
src/ansi-c/c_typecast.cpp Outdated
Comment on lines 793 to 796
if(width % config.ansi_c.char_width != 0)
return std::string(
"bitvector must have width that is a multiple of CHAR_BIT");
else
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: braces around multi-line body

src/ansi-c/c_typecast.cpp Outdated
Comment on lines 787 to 788
if(
type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
type.id() == ID_bv || type.id() == ID_floatbv)
{
Copy link
Collaborator

Choose a reason for hiding this comment

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

Perhaps can_cast_type<bitvector_typet> (which has several more cases that also seem legitimate).

src/ansi-c/c_typecheck_expr.cpp Outdated
Comment on lines 1196 to 1198
error().source_location = expr.source_location();
error() << *error_opt << eom;
throw 0;
Copy link
Collaborator

Choose a reason for hiding this comment

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

throw invalid_source_file_exceptiont{*error_opt, expr.source_location()};

src/ansi-c/c_typecheck_expr.cpp Outdated
Comment on lines 1728 to 1730
error().source_location = expr.source_location();
error() << "cannot take address of a single bit" << eom;
error() << *error_opt << eom;
throw 0;
Copy link
Collaborator

Choose a reason for hiding this comment

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

throw invalid_source_file_exceptiont{*error_opt, expr.source_location()};

@tautschnig tautschnig assigned kroening and unassigned tautschnig Dec 16, 2022
@codecov
Copy link

codecov bot commented Dec 16, 2022 •
edited
Loading

Codecov Report

Base: 78.41% // Head: 78.42% // Increases project coverage by +0.01% 🎉

Coverage data is based on head (52bb522) compared to base (206cf2a).
Patch coverage: 76.55% of modified lines in pull request are covered.

❗ Current head 52bb522 differs from pull request most recent head 0aba4e8. Consider uploading reports for the commit 0aba4e8 to get more accurate results

Additional details and impacted files 
@@             Coverage Diff             @@
##           develop    #7444      +/-   ##
===========================================
+ Coverage    78.41%   78.42%   +0.01%     
===========================================
  Files         1659     1660       +1     
  Lines       190382   190371      -11     
===========================================
+ Hits        149280   149304      +24     
+ Misses       41102    41067      -35
Impacted Files Coverage Δ
...src/java_bytecode/java_bytecode_convert_method.cpp 97.67% <ø> (ø)
jbmc/src/java_bytecode/java_bytecode_language.cpp 92.60% <ø> (ø)
src/analyses/invariant_set.cpp 0.00% <0.00%> (ø)
src/ansi-c/c_typecast.h 75.00% <ø> (ø)
src/ansi-c/c_typecheck_base.h 100.00% <ø> (ø)
src/cprover/simplify_state_expr.cpp 91.59% <ø> (ø)
src/goto-cc/as86_cmdline.cpp 0.00% <0.00%> (ø)
src/goto-cc/as_cmdline.cpp 0.00% <0.00%> (ø)
src/goto-cc/as_mode.cpp 0.00% <0.00%> (ø)
src/goto-cc/bcc_cmdline.cpp 0.00% <0.00%> (ø)
... and 136 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

@kroening
prohibit pointers to bit-vectors that are not byte-aligned
0aba4e8 
This adds checks to the C front-end that prohibit taking the address of
objects that cannot be addressed with byte-granularity pointers.  This
includes proper Booleans (not to be confused with _Bool) and
__CPROVER_bitvector-typed objects whose width is not a multiple of 8.

Fixes #7104.
@kroening kroening marked this pull request as ready for review December 16, 2022 14:54
@kroening kroening merged commit f872937 into develop Dec 16, 2022
@kroening kroening deleted the pointer-to-bit branch December 16, 2022 16:02
@NlightNFotis NlightNFotis mentioned this pull request Dec 16, 2022
Closed
7 tasks
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

@peterschrammel peterschrammel peterschrammel approved these changes

@chris-ryder chris-ryder Awaiting requested review from chris-ryder

@remi-delmas-3000 remi-delmas-3000 Awaiting requested review from remi-delmas-3000 remi-delmas-3000 is a code owner

Assignees

@kroening kroening

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Unexpected assertion result with arrays of __CPROVER_bitvector
3 participants
@kroening @tautschnig @peterschrammel