Recognize pointers wrapped in TNamed in memOutOfBounds and fix bit-to-byte comparison bug#1676
Merged
Recognize pointers wrapped in TNamed in memOutOfBounds and fix bit-to-byte comparison bug#1676
TNamed in memOutOfBounds and fix bit-to-byte comparison bug#1676Conversation
sim642
reviewed
Feb 13, 2025
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
michael-schwarz
approved these changes
Feb 13, 2025
| let one = intdom_of_int 1 in | ||
| let casted_es = ID.sub casted_es one in | ||
| let casted_offs = ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom in | ||
| let casted_offs = ID.div (ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom) (ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int 8)) in |
Member
There was a problem hiding this comment.
Nice catch, I guess this tended to kill us almost all of the time.
Member
There was a problem hiding this comment.
There's also a documentation problem (by me) that might've contributed to this:
analyzer/src/cdomain/value/cdomains/offset_intf.ml
Lines 92 to 96 in 153ce28
Contrary to the description, it returns the offset in bits (matching what CIL has). It was fine for
semantic_equal because both would be in bits, but not for other uses (this is the only other one I think).
I'll have to open a follow-up PR to fix that. Changing the documentation would be easy, but it's not entirely the right thing: ptrdiff_t is large enough to fit offsets in bytes, but not necessarily in bits (in practice the difference might be irrelevant unless a program actually allocates more than 8th of the address space). Having to_index return bytes would be consistent with ptrdiff_ikind.
sim642
approved these changes
Feb 13, 2025
6 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Looking through Goblint logs for the SV-COMP MemSafety tasks revealed several issues that are fixed in this PR:
TNamedwere not recognized and considered as pointersTNamedwas not workingAdditional fixes:
ID.lt casted_es casted_offsrequires subtracting 1 fromcasted_es, but the corresponding log message about the size ofcasted_eswas misleading because of the subtraction. The log message now displays the actual size before the subtraction to prevent confusion.