Skip to content

IsMultiple in MallocWrapper: Check uniqueness of allocating(!) thread #1720

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 1 commit into from
Mar 27, 2025

Conversation

michael-schwarz
Copy link
Member

@michael-schwarz michael-schwarz commented Mar 26, 2025

To determine uniqueness of a malloced object, Goblint is supposed to perform the following logic:

  • A: Check that is assigned a counter value (numbering mallocs within a thread) other than top
  • B: Check that the allocating thread is unique

Unfortunately, the logic for (B) is broken: It checks whether the thread making a uniqueness query for the blob is unique, instead of the thread which allocated the memory in the first place.

The added testcase is a precision issue, but it also is a soundness problem.

If the querying thread happens to be unique but the allocating one is not, we give the wrong answer here. Because of various internals (always spawning the unique copy of a thread in a loop too), getting Goblint to actually surface the unsoundness was beyond me, though.

SV-COMP: After this blunder is removed, we might benefit in MemSafety and it may also be interesting to re-check if one should enable the malloc uniqueness for races (CC @karoliineh): With --set ana.malloc.unique_address_count 1, we now succeed on sv-comp/sv-benchmarks/c/pthread/twostage_3.i.

Closes #1719

@michael-schwarz michael-schwarz added bug unsound sv-comp SV-COMP (analyses, results), witnesses precision labels Mar 26, 2025
@michael-schwarz michael-schwarz added this to the v2.6.0 milestone Mar 26, 2025
Copy link
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

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

I have deja vu that we've had a similar issue somewhere in the past, but couldn't easily find it.

@michael-schwarz michael-schwarz merged commit 4e30a22 into master Mar 27, 2025
21 checks passed
@michael-schwarz michael-schwarz deleted the issue_1719 branch March 27, 2025 08:34
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 unsound
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Goblint cannot handle even simple cases of malloc'ed mutexes
2 participants