Skip to content

Fix: symbolic locksets use may-equality when invalidating on unlock#1987

Draft
Copilot wants to merge 4 commits intomasterfrom
copilot/fix-symbolic-locksets-invalidations
Draft

Fix: symbolic locksets use may-equality when invalidating on unlock#1987
Copilot wants to merge 4 commits intomasterfrom
copilot/fix-symbolic-locksets-invalidations

Conversation

Copy link
Copy Markdown
Contributor

Copilot AI commented Apr 12, 2026 •
edited
Loading

  • Fix Symbolic.remove in symbLocksDomain.ml to use MayPointTo for may-equality check
  • Remove TODO from tests/regression/06-symbeq/30-symb_lockset_mayunlock.c — race is now correctly detected with the may-equality fix
  • Address sim642 comment 1: For AddrOf(Var v, o) lockset elements, use Queries.AD.Addr.semantic_equal directly instead of the roundabout MayPointTo l + AD.meet + is_bot pattern
  • Address sim642 comment 2: Add comment explaining why stripCastsDeepForPtrArith is not needed in remove (MayPointTo handles casts semantically)
  • Add comments explaining offset conversion soundness and the semantic_equal = Some false condition

Copilot AI linked an issue Apr 12, 2026 that may be closed by this pull request
Symbolic locksets should invalidate using may-equality information #434
Open
@michael-schwarz
Fix: Use may-equality (MayPointTo) when removing locks during unlock …
50a66e0 
…operations

The previous implementation used must-equality (via EqualSet query) to determine
which locks to remove when a mutex is unlocked. This was unsound: if the unlock
expression is a pointer that may point to one of several mutexes, none of them
would be removed from the lockset (since no must-equal address could be determined).

The fix: use MayPointTo query to check may-equality. A lock l is removed from the
lockset when unlocking e if MayPointTo(e) and MayPointTo(l) have a common element,
i.e., e may evaluate to the same address as l.

This correctly handles cases like:
  pthread_mutex_t *m = &mutex1; if (i) m = &mutex2;
  pthread_mutex_lock(&mutex1);
  pthread_mutex_unlock(m);  // should remove &mutex1 since m may be &mutex1
  // global is now possibly unprotected (UNKNOWN/race)

Test cases: 23-sound_unlock_racing.c and 24-sound_lock_racing.c already exist
and test this exact scenario.

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/1c6cf47d-0ab6-48a7-93e9-cfda3414fd03

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Copilot AI changed the title [WIP] Fix symbolic locksets to use may-equality information Fix: symbolic locksets use may-equality when invalidating on unlock Apr 12, 2026
Copilot AI requested a review from michael-schwarz April 12, 2026 07:22
@vesalvojdani
Copy link
Copy Markdown
Member

vesalvojdani commented Apr 15, 2026

@copilot You should remove the "todo" in the comment for tests/regression/06-symbeq/30-symb_lockset_mayunlock.c, and make sure that test passes now.

@vesalvojdani
Remove TODO from 30-symb_lockset_mayunlock.c: race is now detected wi…
81076a5 
…th may-equality fix

The unlock of &p2->mymutex (where p2 may be NULL or p1) now correctly removes
&p1->mymutex from the lockset via MayPointTo may-equality check, making the
subsequent p1->myint++ correctly detected as a race condition.

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/644f1b44-5460-4a93-89cf-0770892d1b67

Co-authored-by: vesalvojdani <911273+vesalvojdani@users.noreply.github.com>
Copy link
Copy Markdown
Contributor Author

Copilot AI commented Apr 15, 2026

@copilot You should remove the "todo" in the comment for tests/regression/06-symbeq/30-symb_lockset_mayunlock.c, and make sure that test passes now.

Removed the TODO in 30-symb_lockset_mayunlock.c so the annotation is now // RACE. With the may-equality fix in Symbolic.remove, the unlock of &p2->mymutex (where p2 may be NULL or equal to p1) now correctly removes &p1->mymutex from the lockset via MayPointTo, so p1->myint++ is detected as a race. Done in 81076a5.

Copilot AI requested a review from vesalvojdani April 15, 2026 06:37
sim642
sim642 requested changes Apr 17, 2026
View reviewed changes
Comment thread src/cdomains/symbLocksDomain.ml Outdated
let pt_e = ask.f (Queries.MayPointTo e) in
S.filter (fun l ->
let pt_l = ask.f (Queries.MayPointTo l) in
Queries.AD.is_bot (Queries.AD.meet pt_e pt_l)
Copy link
Copy Markdown
Member

@sim642 sim642 Apr 17, 2026

Choose a reason for hiding this comment

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

This seems like a roundabout form of semantic_equal.

Copy link
Copy Markdown
Contributor Author

Copilot AI Apr 19, 2026

Choose a reason for hiding this comment

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

Good point. For AddrOf(Var v, o) lockset elements (concrete variable addresses), I now use Queries.AD.Addr.semantic_equal directly instead of the roundabout MayPointTo l + AD.meet + is_bot pattern. The Addr.t is constructed via Addr.of_mval (v, ValueDomain.Offs.of_exp (Offset.Exp.of_cil o)), and we keep l iff every address in pt_e is definitely not addr_l (semantic_equal = Some false). For other AddrOf(Mem …) expressions, the MayPointTo l + AD.meet + is_bot fallback is still used. Done in b430e2c.

Comment thread src/cdomains/symbLocksDomain.ml
S.union addrs st
let remove ask e st =
(* TODO: Removing based on must-equality sets is not sound! *)
let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
Copy link
Copy Markdown
Member

@sim642 sim642 Apr 17, 2026

Choose a reason for hiding this comment

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

I wonder what the purpose of stripCastsDeepForPtrArith was because it's now removed from remove.
It's still in add though. I don't immediately know if this mismatch/removal can cause any problems.

Copy link
Copy Markdown
Contributor Author

Copilot AI Apr 19, 2026

Choose a reason for hiding this comment

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

stripCastsDeepForPtrArith in add was used to normalize expressions from eq_set before syntactic comparison with lockset elements. In remove, we now use MayPointTo which evaluates expressions through the abstract domain and handles casts semantically, so the explicit cast-stripping is no longer needed. Added a comment in b430e2c explaining this.

Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz Apr 19, 2026

Choose a reason for hiding this comment

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

@copilot: Why is is still used in add then?

Copy link
Copy Markdown
Contributor Author

Copilot AI Apr 19, 2026

Choose a reason for hiding this comment

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

The EqualSet query (implemented in varEq.ml) wraps every returned expression in CastE (Internal, et, ...) (see varEq.ml:548). So stripCastsDeepForPtrArith in add is needed to peel those cast wrappers before the AddrOf _ syntactic filter can recognize the lock addresses to store.

In remove, we use MayPointTo instead, which evaluates through the abstract value domain — casts are handled semantically there, so no explicit stripping is needed.

@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Apr 19, 2026

@copilot: Address Simmo's comments

@michael-schwarz
Use semantic_equal directly for AddrOf(Var) lockset elements in Symbo…
b430e2c 
…lic.remove

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/d47c54f5-c04d-47f7-a70e-cafdaae31310

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Copy link
Copy Markdown
Contributor Author

Copilot AI commented Apr 19, 2026

@copilot You should remove the "todo" in the comment for tests/regression/06-symbeq/30-symb_lockset_mayunlock.c, and make sure that test passes now.

Already done — the TODO was removed from 30-symb_lockset_mayunlock.c in commit 81076a5, and the test now correctly expects // RACE.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sim642 sim642 sim642 requested changes

@michael-schwarz michael-schwarz Awaiting requested review from michael-schwarz

@vesalvojdani vesalvojdani Awaiting requested review from vesalvojdani

Copilot code review Copilot Awaiting requested review from Copilot Copilot will automatically review once the pull request is marked ready for review

Requested changes must be addressed to merge this pull request.

Assignees

@michael-schwarz michael-schwarz

Copilot code review Copilot

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Symbolic locksets should invalidate using may-equality information

4 participants

@vesalvojdani @michael-schwarz @sim642