From 2a00bcaf86913669018ed50c7f93e6d830e18790 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Apr 2026 06:59:59 +0000 Subject: [PATCH 1/4] Initial plan From 50a66e0531a290ef81386f871241957c9594a8d4 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Apr 2026 07:20:59 +0000 Subject: [PATCH 2/4] Fix: Use may-equality (MayPointTo) when removing locks during unlock 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> --- src/cdomains/symbLocksDomain.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/cdomains/symbLocksDomain.ml b/src/cdomains/symbLocksDomain.ml index 020ac9120e..9e3b89aa11 100644 --- a/src/cdomains/symbLocksDomain.ml +++ b/src/cdomains/symbLocksDomain.ml @@ -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 - 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) + ) st let remove_var v st = S.filter (fun x -> not (Exp.contains_var v x)) st let filter = S.filter From 81076a5738146e2b6be57890e97a82f00343fc7c Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 15 Apr 2026 06:35:33 +0000 Subject: [PATCH 3/4] Remove TODO from 30-symb_lockset_mayunlock.c: race is now detected with 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> --- tests/regression/06-symbeq/30-symb_lockset_mayunlock.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/06-symbeq/30-symb_lockset_mayunlock.c b/tests/regression/06-symbeq/30-symb_lockset_mayunlock.c index 889312dc82..edad06deee 100644 --- a/tests/regression/06-symbeq/30-symb_lockset_mayunlock.c +++ b/tests/regression/06-symbeq/30-symb_lockset_mayunlock.c @@ -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; } From b430e2cecf005237726e7ca5ee7ad87145ac3cd3 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 19 Apr 2026 04:50:39 +0000 Subject: [PATCH 4/4] Use semantic_equal directly for AddrOf(Var) lockset elements in Symbolic.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> --- src/cdomains/symbLocksDomain.ml | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/src/cdomains/symbLocksDomain.ml b/src/cdomains/symbLocksDomain.ml index 9e3b89aa11..7b52a0e499 100644 --- a/src/cdomains/symbLocksDomain.ml +++ b/src/cdomains/symbLocksDomain.ml @@ -359,10 +359,25 @@ struct S.union addrs st 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 -> - let pt_l = ask.f (Queries.MayPointTo l) in - Queries.AD.is_bot (Queries.AD.meet pt_e pt_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