Skip to content

Change Offset.MakeLattice.to_index to return bytes, not bits #1679

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

Merged
merged 3 commits into from
Feb 17, 2025

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Feb 13, 2025

Follow-up to #1676 (comment).
A TODO in LockDomain also anticipated this: (* TODO: is this bits or bytes? *).

Fixes Offset.MakeLattice.to_index to return bytes instead of bits, as per documentation:

val to_index: ?typ:GoblintCil.typ -> t -> idx
(** Physical memory offset in bytes of the entire offset.
Used for {!semantic_equal}.
@param typ base type. *)

Also extracts a few other similar utility functions for offsets and sizes in bytes, not bits. These now assert divisibility by 8 before doing so. Usually this is fine because points to bitfields are impossible.
However, to_index violates it in some memOutOfBounds bitfield tests because the analysis also refers to things accessed more directly, not just those whose addresses have been taken. To handle that, an interval from floor to ceil division is constructed.

Theoretically, doing it in bits is more precise than after having rounded to bytes, but I don't know if this has practical relevance.
The blind division by 8 from #1676 and others wouldn't have done it correctly either for bitfields spanning multiple bytes.

@sim642 sim642 added cleanup Refactoring, clean-up bug unsound labels Feb 13, 2025
@michael-schwarz michael-schwarz self-requested a review February 13, 2025 22:10
@sim642 sim642 added this to the v2.6.0 milestone Feb 17, 2025
@sim642 sim642 merged commit 8dd4762 into master Feb 17, 2025
21 checks passed
@sim642 sim642 deleted the offset-to_index-bytes branch February 17, 2025 08:33
jerhard added a commit that referenced this pull request Feb 17, 2025
Do to PR #1679, where offsets are now computed in bytes in the Offset Domain, and C2PO calculating with bits, a helper function is introduced to perform the conversion from bytes to bits.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug cleanup Refactoring, clean-up unsound
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants