Skip to content

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

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.

Sign up for GitHub

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

Draft
Copilot wants to merge 4 commits into
base: master
Choose a base branch
from
+23 −6
Draft

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

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2a00bca
Initial plan
Copilot Apr 12, 2026
50a66e0
Fix: Use may-equality (MayPointTo) when removing locks during unlock …
Copilot Apr 12, 2026
81076a5
Remove TODO from 30-symb_lockset_mayunlock.c: race is now detected wi…
Copilot Apr 15, 2026
b430e2c
Use semantic_equal directly for AddrOf(Var) lockset elements in Symbo…
Copilot Apr 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions src/cdomains/symbLocksDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -357,11 +357,13 @@ struct
let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
let addrs = S.filter (function AddrOf _ -> true | _ -> false) no_casts in
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.

let addrs = S.filter (function AddrOf _ -> true | _ -> false) no_casts in
S.diff st addrs

let remove (ask: Queries.ask) e st =
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.

) st
let remove_var v st = S.filter (fun x -> not (Exp.contains_var v x)) st

let filter = S.filter
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/06-symbeq/30-symb_lockset_mayunlock.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void *foo(void *arg) {
pthread_mutex_lock(&p1->mymutex);
if (__VERIFIER_nondet_int()) p2 = NULL;
pthread_mutex_unlock(&p2->mymutex);
p1->myint++; // TODO RACE
p1->myint++; // RACE

return NULL;
}
Expand Down
Loading