Skip to content

Conversation

@karoliineh
Copy link
Member

@karoliineh karoliineh commented Feb 12, 2025

Looking through Goblint logs for the SV-COMP MemSafety tasks revealed several issues that are fixed in this PR:

  1. Pointers wrapped in TNamed were not recognized and considered as pointers
  2. Bytes were compared to bits
  3. In some edge cases, equality between pointers wrapped in TNamed was not working

Additional fixes:

  • The comparison ID.lt casted_es casted_offs requires subtracting 1 from casted_es, but the corresponding log message about the size of casted_es was misleading because of the subtraction. The log message now displays the actual size before the subtraction to prevent confusion.

@karoliineh karoliineh added bug sv-comp SV-COMP (analyses, results), witnesses precision labels Feb 12, 2025
@karoliineh karoliineh added this to the SV-COMP 2026 milestone Feb 12, 2025
@michael-schwarz michael-schwarz self-requested a review February 12, 2025 17:22
@karoliineh karoliineh marked this pull request as ready for review February 13, 2025 14:32
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
Copy link
Member

Choose a reason for hiding this comment

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

Nice catch, I guess this tended to kill us almost all of the time.

Copy link
Member

Choose a reason for hiding this comment

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

There's also a documentation problem (by me) that might've contributed to this:

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. *)

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 sim642 merged commit 39dc63e into master Feb 13, 2025
21 checks passed
@sim642 sim642 deleted the memsafety-bugs branch February 13, 2025 15:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug precision sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants