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 all 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
27 changes: 22 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,28 @@ 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 =
(* No stripCastsDeepForPtrArith needed: MayPointTo handles casts semantically. *)
let pt_e = ask.f (Queries.MayPointTo e) in
S.filter (fun l ->
match l with
| AddrOf (Var v, o) ->
(* For concrete variable addresses, use semantic_equal directly without
a MayPointTo query on l.
Offset.Exp.of_cil converts the CIL offset to an exp-indexed offset;
ValueDomain.Offs.of_exp then abstracts it (non-constant indices become
top), which is sound: an unknown index may alias anything.
We keep l iff every address in pt_e is *definitely* not addr_l
(semantic_equal = Some false); when equality is unknown (None) or
definite (Some true), l is conservatively removed. *)
let addr_l = Queries.AD.Addr.of_mval (v, ValueDomain.Offs.of_exp (Offset.Exp.of_cil o)) in
Queries.AD.for_all (fun ae ->
Queries.AD.Addr.semantic_equal ae addr_l = Some false
) pt_e
| _ ->
Queries.AD.is_bot (Queries.AD.meet pt_e (ask.f (Queries.MayPointTo l)))
) 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