Skip to content
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.

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

Introduce bitst and bytest to avoid bit/byte mix-up #7413

Open
wants to merge 2 commits into
base: develop
Choose a base branch
from

Conversation

tautschnig
Copy link
Collaborator

Use mp_integers with a unit to clarify when an mp_integer holds a number
of bits or a number of bytes. This makes sure that type-inconsistent
comparisons as fixed in #7411 result in compile-time errors.

  • 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 Dec 5, 2022
@tautschnig tautschnig changed the title Introduce bitst and bytest to avoid bit/byte mix-up [depends-on: #7411, #7412] Introduce bitst and bytest to avoid bit/byte mix-up Dec 6, 2022
@tautschnig tautschnig marked this pull request as ready for review December 6, 2022 12:40
@codecov
Copy link

codecov bot commented Dec 6, 2022

Codecov Report

Attention: Patch coverage is 91.94396% with 46 lines in your changes missing coverage. Please review.

Project coverage is 78.36%. Comparing base (2ffc4c9) to head (b533d00).

Files Patch % Lines
src/cprover/bv_pointers_wide.cpp 55.55% 8 Missing ⚠️
src/goto-programs/interpreter_evaluate.cpp 33.33% 6 Missing ⚠️
src/solvers/flattening/bv_pointers.cpp 73.33% 4 Missing ⚠️
src/util/pointer_offset_size.cpp 91.66% 4 Missing ⚠️
src/ansi-c/expr2c.cpp 25.00% 3 Missing ⚠️
src/ansi-c/padding.cpp 93.87% 3 Missing ⚠️
src/pointer-analysis/value_set.cpp 80.00% 3 Missing ⚠️
src/analyses/goto_rw.cpp 77.77% 2 Missing ⚠️
src/goto-synthesizer/cegis_evaluator.cpp 60.00% 2 Missing ⚠️
src/memory-analyzer/analyze_symbol.cpp 89.47% 2 Missing ⚠️
... and 8 more
Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #7413      +/-   ##
===========================================
+ Coverage    78.09%   78.36%   +0.27%     
===========================================
  Files         1726     1727       +1     
  Lines       189039   188491     -548     
  Branches     18399    18442      +43     
===========================================
+ Hits        147629   147717      +88     
+ Misses       41410    40774     -636     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@thomasspriggs
Copy link
Contributor

Have you seen the approach taken to strong types here? https://www.fluentcpp.com/2016/12/08/strong-types-for-strong-interfaces/

This approach appears to have the following advantages -

  • Templates are used to avoid needing a full cut-and-paste definition for each of the strong / unit associated types.
  • Values are stored using containership rather than inheritance. This could side-step some of the potential issues with implicit upcasting.

@tautschnig
Copy link
Collaborator Author

Have you seen the approach taken to strong types here? https://www.fluentcpp.com/2016/12/08/strong-types-for-strong-interfaces/

This approach appears to have the following advantages -

* Templates are used to avoid needing a full cut-and-paste definition for each of the strong / unit associated types.

* Values are stored using containership rather than inheritance. This could side-step some of the potential issues with implicit upcasting.

Thank you for alerting me to this! This will require implementing more methods, but that's ok. I'll try this route.

@tautschnig tautschnig self-assigned this Dec 6, 2022
@tautschnig tautschnig force-pushed the feature/bits-bytes branch 3 times, most recently from 4279119 to c14cb4a Compare December 14, 2022 08:47
@tautschnig tautschnig removed their assignment Dec 14, 2022
@tautschnig tautschnig force-pushed the feature/bits-bytes branch from e592d27 to 117e4d6 Compare May 15, 2023 11:46
@tautschnig tautschnig assigned tautschnig and unassigned tautschnig May 15, 2023
@tautschnig tautschnig self-assigned this May 31, 2023
@tautschnig tautschnig force-pushed the feature/bits-bytes branch from 117e4d6 to 7cd034d Compare June 1, 2023 18:28
@tautschnig tautschnig removed their assignment Jun 1, 2023
@tautschnig tautschnig force-pushed the feature/bits-bytes branch from 7cd034d to 98d642f Compare July 19, 2023 05:51
@tautschnig tautschnig force-pushed the feature/bits-bytes branch 2 times, most recently from 656f15d to 2cc9ef7 Compare November 20, 2023 21:00
@tautschnig tautschnig self-assigned this Jan 22, 2024
@tautschnig tautschnig assigned feliperodri and unassigned tautschnig Jan 22, 2024
Copy link
Collaborator

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

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

LGTM.

@feliperodri feliperodri removed their assignment Jan 22, 2024
@tautschnig tautschnig self-assigned this Jan 22, 2024
@tautschnig tautschnig removed their assignment Jan 23, 2024
@tautschnig tautschnig force-pushed the feature/bits-bytes branch 2 times, most recently from a6df679 to 3dad36d Compare May 8, 2024 11:32
The upper bound for lowering a union to a sequence of bytes is the
byte-width of the widest member, not the bit width.
Use mp_integers with a unit to clarify when an mp_integer holds a number
of bits or a number of bytes. This makes sure that type-inconsistent
comparisons as fixed in diffblue#7411 result in compile-time errors.
@tautschnig tautschnig force-pushed the feature/bits-bytes branch from 3dad36d to b533d00 Compare June 20, 2024 08:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

8 participants