From 7831cbfcd5f923a1269b1d087ad48054fba527a9 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 17 Oct 2025 10:27:09 +0200 Subject: [PATCH 01/95] add inter-procedural lock c files --- .../65-inter-proc-lock1_racefree.c | 26 +++++++++++++++ .../66-inter-proc-lock_racefree.c | 33 +++++++++++++++++++ 2 files changed, 59 insertions(+) create mode 100644 tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c create mode 100644 tests/regression/28-race_reach/66-inter-proc-lock_racefree.c diff --git a/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c b/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c new file mode 100644 index 0000000000..7215219bd2 --- /dev/null +++ b/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c @@ -0,0 +1,26 @@ +//PARAM: --set lib.activated[+] sv-comp +#include +#include "racemacros.h" + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; + +void *t1_fun(void *arg) { + pthread_mutex_lock(&mutex); + assert_racefree(global); // no race + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2_fun(void *arg) { // t2 is protected by mutex locked in main thread + access(global); +} + +int main(void) { + create_threads(t1); + pthread_mutex_lock(&mutex); + create_threads(t2); + join_threads(t2); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c b/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c new file mode 100644 index 0000000000..a687b0e010 --- /dev/null +++ b/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c @@ -0,0 +1,33 @@ +//PARAM: --set lib.activated[+] sv-comp +#include +#include "racemacros.h" + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; + +void *t1child_fun(void* arg) { // t1child is protected by mutex locked in t1 + access(global); + return NULL; +} + +void *tmainchild_fun(void *arg) { // tmainchild is protected by mutex locked in main thread + assert_racefree(global); // NO RACE + return NULL; +} + +void *t1_fun(void *arg) { + pthread_mutex_lock(&mutex); + create_threads(t1child); + join_threads(t1child); + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(void) { + create_threads(t1); + pthread_mutex_lock(&mutex); + create_threads(tmainchild); + join_threads(tmainchild); + pthread_mutex_unlock(&mutex); + return 0; +} From 3ef70824897138d60cfc9b3d4e660b66636209ac Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 17 Oct 2025 10:30:54 +0200 Subject: [PATCH 02/95] add lock-fork hb relationship c file --- .../28-race_reach/67-lock-fork_racefree.c | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tests/regression/28-race_reach/67-lock-fork_racefree.c diff --git a/tests/regression/28-race_reach/67-lock-fork_racefree.c b/tests/regression/28-race_reach/67-lock-fork_racefree.c new file mode 100644 index 0000000000..7a77b91c2c --- /dev/null +++ b/tests/regression/28-race_reach/67-lock-fork_racefree.c @@ -0,0 +1,21 @@ +//PARAM: --set lib.activated[+] sv-comp +#include +#include "racemacros.h" + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex); // must happen after unlock in main + pthread_mutex_unlock(&mutex); + assert_racefree(global); // no race + return NULL; +} + +int main(void) { + pthread_mutex_lock(&mutex); + create_threads(t); + access(global); + pthread_mutex_unlock(&mutex); + return 0; +} From 9d885842fb20bc81bc355ab39e970043b9aca34f Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 5 Nov 2025 18:56:57 +0100 Subject: [PATCH 03/95] use pthread_create() and pthread_join() instead of race macros for inter-proc lock regression tests --- .../65-inter-proc-lock1_racefree.c | 16 +++++++------ .../66-inter-proc-lock_racefree.c | 23 ++++++++++--------- 2 files changed, 21 insertions(+), 18 deletions(-) diff --git a/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c b/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c index 7215219bd2..5bbf405eb1 100644 --- a/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c +++ b/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c @@ -4,23 +4,25 @@ int global = 0; pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; -void *t1_fun(void *arg) { +void *t1(void *arg) { pthread_mutex_lock(&mutex); - assert_racefree(global); // no race + assert_racefree(global); pthread_mutex_unlock(&mutex); return NULL; } -void *t2_fun(void *arg) { // t2 is protected by mutex locked in main thread - access(global); +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + access(global); + return NULL; } int main(void) { - create_threads(t1); + pthread_create(&id1, NULL, t1, NULL); pthread_mutex_lock(&mutex); - create_threads(t2); - join_threads(t2); + pthread_create(&id2, NULL, t2, NULL); + pthread_join(id2, NULL); pthread_mutex_unlock(&mutex); return 0; } diff --git a/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c b/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c index a687b0e010..ba2589ca6c 100644 --- a/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c +++ b/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c @@ -4,30 +4,31 @@ int global = 0; pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t tmain_child, t1, t1_child; -void *t1child_fun(void* arg) { // t1child is protected by mutex locked in t1 - access(global); - return NULL; +void *t1_child(void* arg) { // t1child is protected by mutex locked in t1 + access(global); + return NULL; } -void *tmainchild_fun(void *arg) { // tmainchild is protected by mutex locked in main thread - assert_racefree(global); // NO RACE - return NULL; +void *tmain_child(void *arg) { // tmainchild is protected by mutex locked in main thread + assert_racefree(global); // NORACE + return NULL; } void *t1_fun(void *arg) { pthread_mutex_lock(&mutex); - create_threads(t1child); - join_threads(t1child); + pthread_create(&t1_child, NULL, t1_child, NULL); + pthread_join(t1_child, NULL); pthread_mutex_unlock(&mutex); return NULL; } int main(void) { - create_threads(t1); + pthread_create(&t1, NULL, t1, NULL); pthread_mutex_lock(&mutex); - create_threads(tmainchild); - join_threads(tmainchild); + pthread_create(&tmain_child, NULL, tmain_child, NULL); + pthread_join(tmain_child, NULL); pthread_mutex_unlock(&mutex); return 0; } From b7d0d35671f2102f6f438e0099091a59a05f2798 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 5 Nov 2025 19:07:46 +0100 Subject: [PATCH 04/95] activate creationLockset analysis for inter-threaded lock regressions tests --- tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c | 2 +- tests/regression/28-race_reach/66-inter-proc-lock_racefree.c | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c b/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c index 5bbf405eb1..a3eff997b8 100644 --- a/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c +++ b/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c @@ -1,4 +1,4 @@ -//PARAM: --set lib.activated[+] sv-comp +//PARAM: --set lib.activated[+] sv-comp --set ana.activated[+] creationLockset #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c b/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c index ba2589ca6c..ece2bda785 100644 --- a/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c +++ b/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c @@ -1,4 +1,4 @@ -//PARAM: --set lib.activated[+] sv-comp +//PARAM: --set lib.activated[+] sv-comp --set ana.activated[+] creationLockset #include #include "racemacros.h" From 93a513a83e20dfdb7e87fa9dc448162a4fde672e Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 5 Nov 2025 19:08:27 +0100 Subject: [PATCH 05/95] initial version of creationLockset analysis --- src/analyses/creationLockset.ml | 44 +++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 src/analyses/creationLockset.ml diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml new file mode 100644 index 0000000000..c376d90599 --- /dev/null +++ b/src/analyses/creationLockset.ml @@ -0,0 +1,44 @@ +open Analyses +module TID = ThreadIdDomain.ThreadLifted +module LID = LockDomain.MustLock + +(** + collects for each thread t_n pairs of must-ancestors and locks (t_0,l): + when t_n or a must-ancestor t_1 of t_n was created, the parent t_0 must have held l. + TODO: check if this requirement can be loosened +*) +module Spec = struct + include IdentityUnitContextsSpec (* no context necessary(?) *) + module D = Lattice.Unit (* flow-insensitive analysis *) + + module V = struct + include TID + include StdV + end + + module G = SetDomain.Make (Printable.ProdSimple (TID) (LID)) + (* 2^{T\times L}. TODO: Prod or ProdSimple? *) + + let name () = "creationLockset" + let startstate _ = D.bot () + let exitstate _ = D.bot () + + (* create(t_1) in t_0 with lockset L *) + let threadspawn man ~multiple lval f args fman = + let ask = Analyses.ask_of_man man in + let tid = ask.f Queries.CurrentThreadId in + let child_ask = Analyses.ask_of_man fman in + let child_tid = child_ask.f Queries.CurrentThreadId in + let lockset = ask.f Queries.MustLockset in + (* contribution (t_1, l) to global of t_0 for all l in L: *) + (* TODO also register for transitive descendants of t_1! *) + let contribute_lock lock = man.sideg child_tid (G.singleton (tid, lock)) in + LockDomain.MustLockset.iter contribute_lock lockset + ;; + (* TODO: consider edge cases (most likely in creation lockset analysis)! + - `ana.threads.include-node` is false. Two threads created with different locksets may have the same id that way! + - child thread is not unique and thus could also ancestor of ego thread. In this case, it can also be created with a different lockset! + - more? *) +end + +let _ = MCP.register_analysis ~dep:[ "threadid"; "mutex" ] (module Spec : MCPSpec) From 946536b9ca78f639dc9c1cc42b66dc5010693069 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 7 Nov 2025 12:26:59 +0100 Subject: [PATCH 06/95] AncestorLocksetSpec as common base module --- src/analyses/creationLockset.ml | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index c376d90599..bc2d95a19c 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -2,28 +2,33 @@ open Analyses module TID = ThreadIdDomain.ThreadLifted module LID = LockDomain.MustLock -(** - collects for each thread t_n pairs of must-ancestors and locks (t_0,l): - when t_n or a must-ancestor t_1 of t_n was created, the parent t_0 must have held l. - TODO: check if this requirement can be loosened -*) -module Spec = struct +module AncestorLocksetSpec = struct include IdentityUnitContextsSpec (* no context necessary(?) *) - module D = Lattice.Unit (* flow-insensitive analysis *) + module D = Lattice.Unit module V = struct include TID include StdV end - module G = SetDomain.Make (Printable.ProdSimple (TID) (LID)) + module G = SetDomain.Make (Printable.Prod (TID) (LID)) (* 2^{T\times L}. TODO: Prod or ProdSimple? *) - let name () = "creationLockset" let startstate _ = D.bot () let exitstate _ = D.bot () +end + +(** + collects for each thread t_n pairs of must-ancestors and locks (t_0,l): + when t_n or a must-ancestor t_1 of t_n was created, the parent t_0 must have held l. + TODO: check if this requirement can be loosened +*) +module CreationLocksetSpec = struct + include AncestorLocksetSpec + + let name () = "creationLockset" - (* create(t_1) in t_0 with lockset L *) + (** create(t_1) in t_0 with lockset L *) let threadspawn man ~multiple lval f args fman = let ask = Analyses.ask_of_man man in let tid = ask.f Queries.CurrentThreadId in @@ -41,4 +46,8 @@ module Spec = struct - more? *) end -let _ = MCP.register_analysis ~dep:[ "threadid"; "mutex" ] (module Spec : MCPSpec) +let _ = + MCP.register_analysis + ~dep:[ "threadid"; "mutex" ] + (module CreationLocksetSpec : MCPSpec) +;; From a78e44c37fd196f6ced9efa44d7070afecf70c8e Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 7 Nov 2025 14:36:21 +0100 Subject: [PATCH 07/95] initial version of TaintedCreationLockset analysis --- src/analyses/creationLockset.ml | 46 +++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index bc2d95a19c..d5ccd177d1 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -1,4 +1,6 @@ open Analyses +open GoblintCil +module LF = LibraryFunctions module TID = ThreadIdDomain.ThreadLifted module LID = LockDomain.MustLock @@ -46,8 +48,52 @@ module CreationLocksetSpec = struct - more? *) end +module TaintedCreationLocksetSpec = struct + include AncestorLocksetSpec + + let name () = "taintedCreationLockset" + let eval_exp_addr (a : Queries.ask) exp = a.f (Queries.MayPointTo exp) + + (** stolen from mutexGhost.ml. TODO Maybe add to library? *) + let mustlock_of_addr (addr : LockDomain.Addr.t) : LockDomain.MustLock.t option = + match addr with + | Addr mv when LockDomain.Mval.is_definite mv -> Some (LockDomain.MustLock.of_mval mv) + | _ -> None + ;; + + let event man (e : Events.t) _ = + match e with + | Unlock addr -> + let ask = Analyses.ask_of_man man in + let tid = ask.f Queries.CurrentThreadId in + let may_created_tids = ask.f Queries.CreatedThreads in + let must_joined_tids = ask.f Queries.MustJoinedThreads in + let possibly_running_tids = + ConcDomain.ThreadSet.diff may_created_tids must_joined_tids + in + let contribute_tainted_lock lock child_tid = + man.sideg child_tid (G.singleton (tid, lock)) + in + let lock_opt = mustlock_of_addr addr in + (match lock_opt with + | Some lock -> + (* contribute possibly_running_tids \times \{lock\} *) + ConcDomain.ThreadSet.iter (contribute_tainted_lock lock) possibly_running_tids + | None -> + (* TODO any lock could have been unlocked. Contribute for all possibly_running_tids their full CreationLocksets to invalidate them!! *) + ()) + | _ -> () + ;; +end + let _ = MCP.register_analysis ~dep:[ "threadid"; "mutex" ] (module CreationLocksetSpec : MCPSpec) ;; + +let _ = + MCP.register_analysis + ~dep:[ "threadid"; "mutex" ] + (module TaintedCreationLocksetSpec : MCPSpec) +;; From 8ba90943e2f9bbcb5a4e1ae62e6b1bf907a567fb Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 7 Nov 2025 15:25:41 +0100 Subject: [PATCH 08/95] use thread domain instead of lifted thread domain --- src/analyses/creationLockset.ml | 71 +++++++++++++++++++-------------- 1 file changed, 42 insertions(+), 29 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index d5ccd177d1..ca2845b366 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -1,7 +1,8 @@ open Analyses -open GoblintCil module LF = LibraryFunctions -module TID = ThreadIdDomain.ThreadLifted + +(* TODO use ThreadLifted instead? Are Top or Bot relevant *) +module TID = ThreadIdDomain.Thread module LID = LockDomain.MustLock module AncestorLocksetSpec = struct @@ -18,6 +19,10 @@ module AncestorLocksetSpec = struct let startstate _ = D.bot () let exitstate _ = D.bot () + + let contribute_lock man tid lock child_tid = + man.sideg child_tid (G.singleton (tid, lock)) + ;; end (** @@ -33,14 +38,22 @@ module CreationLocksetSpec = struct (** create(t_1) in t_0 with lockset L *) let threadspawn man ~multiple lval f args fman = let ask = Analyses.ask_of_man man in - let tid = ask.f Queries.CurrentThreadId in - let child_ask = Analyses.ask_of_man fman in - let child_tid = child_ask.f Queries.CurrentThreadId in - let lockset = ask.f Queries.MustLockset in - (* contribution (t_1, l) to global of t_0 for all l in L: *) - (* TODO also register for transitive descendants of t_1! *) - let contribute_lock lock = man.sideg child_tid (G.singleton (tid, lock)) in - LockDomain.MustLockset.iter contribute_lock lockset + let tid_lifted = ask.f Queries.CurrentThreadId in + match tid_lifted with + | `Top | `Bot -> () + | `Lifted tid -> + let child_ask = Analyses.ask_of_man fman in + let child_tid_lifted = child_ask.f Queries.CurrentThreadId in + (match child_tid_lifted with + | `Top | `Bot -> () + | `Lifted child_tid -> + let lockset = ask.f Queries.MustLockset in + (* contribution (t_1, l) to global of t_0 for all l in L: *) + (* TODO also register for transitive descendants of t_1! *) + (* let contribute_lock lock = man.sideg child_tid (G.singleton (tid, lock)) in *) + LockDomain.MustLockset.iter + (fun l -> contribute_lock man tid l child_tid) + lockset) ;; (* TODO: consider edge cases (most likely in creation lockset analysis)! - `ana.threads.include-node` is false. Two threads created with different locksets may have the same id that way! @@ -61,27 +74,27 @@ module TaintedCreationLocksetSpec = struct | _ -> None ;; - let event man (e : Events.t) _ = + let event man e _ = match e with - | Unlock addr -> + | Events.Unlock addr -> let ask = Analyses.ask_of_man man in - let tid = ask.f Queries.CurrentThreadId in - let may_created_tids = ask.f Queries.CreatedThreads in - let must_joined_tids = ask.f Queries.MustJoinedThreads in - let possibly_running_tids = - ConcDomain.ThreadSet.diff may_created_tids must_joined_tids - in - let contribute_tainted_lock lock child_tid = - man.sideg child_tid (G.singleton (tid, lock)) - in - let lock_opt = mustlock_of_addr addr in - (match lock_opt with - | Some lock -> - (* contribute possibly_running_tids \times \{lock\} *) - ConcDomain.ThreadSet.iter (contribute_tainted_lock lock) possibly_running_tids - | None -> - (* TODO any lock could have been unlocked. Contribute for all possibly_running_tids their full CreationLocksets to invalidate them!! *) - ()) + let tid_lifted = ask.f Queries.CurrentThreadId in + (match tid_lifted with + | `Top | `Bot -> () + | `Lifted tid -> + let may_created_tids = ask.f Queries.CreatedThreads in + let must_joined_tids = ask.f Queries.MustJoinedThreads in + let possibly_running_tids = + ConcDomain.ThreadSet.diff may_created_tids must_joined_tids + in + let lock_opt = mustlock_of_addr addr in + (match lock_opt with + | Some lock -> + (* contribute possibly_running_tids \times \{lock\} *) + ConcDomain.ThreadSet.iter (contribute_lock man tid lock) possibly_running_tids + | None -> + (* TODO any lock could have been unlocked. Contribute for all possibly_running_tids their full CreationLocksets to invalidate them!! *) + ())) | _ -> () ;; end From ead4843cec1ea19b96d5ada057dd96474bb979a5 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 7 Nov 2025 15:27:02 +0100 Subject: [PATCH 09/95] add threadJoins as dependency for TaintedCreationLockset analysis --- src/analyses/creationLockset.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index ca2845b366..f58744b49c 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -107,6 +107,6 @@ let _ = let _ = MCP.register_analysis - ~dep:[ "threadid"; "mutex" ] + ~dep:[ "threadid"; "mutex"; "threadJoins" ] (module TaintedCreationLocksetSpec : MCPSpec) ;; From 73e6d9c5e9d5a0049890368d60f0ae7de66ef4d5 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 7 Nov 2025 16:17:02 +0100 Subject: [PATCH 10/95] initial version of transitive descendants analysis --- src/analyses/transitiveDescendants.ml | 37 +++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 src/analyses/transitiveDescendants.ml diff --git a/src/analyses/transitiveDescendants.ml b/src/analyses/transitiveDescendants.ml new file mode 100644 index 0000000000..19e288d116 --- /dev/null +++ b/src/analyses/transitiveDescendants.ml @@ -0,0 +1,37 @@ +open Analyses +module TID = ThreadIdDomain.Thread + +(** flow-insensitive analysis mapping threads to may-sets of descendants *) +module TransitiveDescendants = struct + include IdentityUnitContextsSpec + module D = Lattice.Unit + + module V = struct + include TID + include StdV + end + + module G = SetDomain.Make (TID) + + let name () = "transitiveDescendants" + let startstate _ = D.bot () + let exitstate _ = D.bot () + + let threadspawn man ~multiple lval f args fman = + let ask = Analyses.ask_of_man man in + let tid_lifted = ask.f Queries.CurrentThreadId in + match tid_lifted with + | `Top | `Bot -> () + | `Lifted tid -> + let child_ask = Analyses.ask_of_man fman in + let child_tid_lifted = child_ask.f Queries.CurrentThreadId in + (match child_tid_lifted with + | `Top | `Bot -> () + | `Lifted child_tid -> + let _ = man.sideg tid (G.singleton child_tid) in + let child_descendants = man.global child_tid in + man.sideg tid child_descendants) + ;; +end + +let _ = MCP.register_analysis ~dep:[ "threadid" ] (module TransitiveDescendants : MCPSpec) From f212c4568f8f0c055ea2f45bc86e6fded59ec91a Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 7 Nov 2025 16:29:51 +0100 Subject: [PATCH 11/95] some comments in transitiveDescendats analysis --- src/analyses/transitiveDescendants.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/analyses/transitiveDescendants.ml b/src/analyses/transitiveDescendants.ml index 19e288d116..a22b503fbb 100644 --- a/src/analyses/transitiveDescendants.ml +++ b/src/analyses/transitiveDescendants.ml @@ -28,7 +28,9 @@ module TransitiveDescendants = struct (match child_tid_lifted with | `Top | `Bot -> () | `Lifted child_tid -> + (* contribute new child *) let _ = man.sideg tid (G.singleton child_tid) in + (* transitive hull *) let child_descendants = man.global child_tid in man.sideg tid child_descendants) ;; From 4633ec740b13897e3ade5fd92e59ba551237925c Mon Sep 17 00:00:00 2001 From: dabund24 Date: Tue, 11 Nov 2025 12:29:21 +0100 Subject: [PATCH 12/95] query for descendant analysis --- src/analyses/transitiveDescendants.ml | 8 +++++++- src/domains/queries.ml | 5 +++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/analyses/transitiveDescendants.ml b/src/analyses/transitiveDescendants.ml index a22b503fbb..4b9c1300af 100644 --- a/src/analyses/transitiveDescendants.ml +++ b/src/analyses/transitiveDescendants.ml @@ -11,12 +11,18 @@ module TransitiveDescendants = struct include StdV end - module G = SetDomain.Make (TID) + module G = ConcDomain.ThreadSet let name () = "transitiveDescendants" let startstate _ = D.bot () let exitstate _ = D.bot () + let query man (type a) (x : a Queries.t) : a Queries.result = + match x with + | Queries.DescendantThreads t -> (man.global : TID.t -> ConcDomain.ThreadSet.t) + | _ -> Queries.Result.top x + ;; + let threadspawn man ~multiple lval f args fman = let ask = Analyses.ask_of_man man in let tid_lifted = ask.f Queries.CurrentThreadId in diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 31e93dd0b2..6f75fb579d 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -146,6 +146,7 @@ type _ t = | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t (** YAML witness entries for a global unknown ([Obj.t] represents [Spec.V.t]) and YAML witness task. *) | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *) + | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t (* TODO consider returning descendants of ego threads only? *) type 'a result = 'a @@ -221,6 +222,7 @@ struct | YamlEntryGlobal _ -> (module YS) | GhostVarAvailable _ -> (module MayBool) | InvariantGlobalNodes -> (module NS) + | DescendantThreads _ -> (module ConcDomain.ThreadSet) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -295,6 +297,7 @@ struct | YamlEntryGlobal _ -> YS.top () | GhostVarAvailable _ -> MayBool.top () | InvariantGlobalNodes -> NS.top () + | DescendantThreads _ -> ConcDomain.ThreadSet.top () end (* The type any_query can't be directly defined in Any as t, @@ -366,6 +369,7 @@ struct | Any (MustProtectingLocks _) -> 61 | Any (GhostVarAvailable _) -> 62 | Any InvariantGlobalNodes -> 63 + | Any (DescendantThreads _) -> 64 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -540,6 +544,7 @@ struct | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" + | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads" end let to_value_domain_ask (ask: ask) = From 3f3e2f30463b63678c9aa433e4c141d48b08c6d4 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Sat, 15 Nov 2025 17:43:28 +0100 Subject: [PATCH 13/95] get rid of unnecessary match expression --- src/analyses/creationLockset.ml | 24 +++++++++--------------- 1 file changed, 9 insertions(+), 15 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index f58744b49c..5aebf597da 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -39,21 +39,15 @@ module CreationLocksetSpec = struct let threadspawn man ~multiple lval f args fman = let ask = Analyses.ask_of_man man in let tid_lifted = ask.f Queries.CurrentThreadId in - match tid_lifted with - | `Top | `Bot -> () - | `Lifted tid -> - let child_ask = Analyses.ask_of_man fman in - let child_tid_lifted = child_ask.f Queries.CurrentThreadId in - (match child_tid_lifted with - | `Top | `Bot -> () - | `Lifted child_tid -> - let lockset = ask.f Queries.MustLockset in - (* contribution (t_1, l) to global of t_0 for all l in L: *) - (* TODO also register for transitive descendants of t_1! *) - (* let contribute_lock lock = man.sideg child_tid (G.singleton (tid, lock)) in *) - LockDomain.MustLockset.iter - (fun l -> contribute_lock man tid l child_tid) - lockset) + let child_ask = Analyses.ask_of_man fman in + let child_tid_lifted = child_ask.f Queries.CurrentThreadId in + match tid_lifted, child_tid_lifted with + | `Lifted tid, `Lifted child_tid -> + let lockset = ask.f Queries.MustLockset in + (* contribution (t_1, l) to global of t_0 for all l in L: *) + (* TODO also register for transitive descendants of t_1! *) + LockDomain.MustLockset.iter (fun l -> contribute_lock man tid l child_tid) lockset + | _ -> (* deal with top or bottom? *) () ;; (* TODO: consider edge cases (most likely in creation lockset analysis)! - `ana.threads.include-node` is false. Two threads created with different locksets may have the same id that way! From 691cdfd5e8056bcdc7a0d527545190fc9da9fce4 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Sun, 16 Nov 2025 21:34:08 +0100 Subject: [PATCH 14/95] MayCreationLockset query --- src/analyses/creationLockset.ml | 12 ++++++++++++ src/domains/queries.ml | 6 ++++++ 2 files changed, 18 insertions(+) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 5aebf597da..583cf63dc2 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -49,10 +49,22 @@ module CreationLocksetSpec = struct LockDomain.MustLockset.iter (fun l -> contribute_lock man tid l child_tid) lockset | _ -> (* deal with top or bottom? *) () ;; + (* TODO: consider edge cases (most likely in creation lockset analysis)! - `ana.threads.include-node` is false. Two threads created with different locksets may have the same id that way! - child thread is not unique and thus could also ancestor of ego thread. In this case, it can also be created with a different lockset! - more? *) + + let query man (type a) (x : a Queries.t) : a Queries.result = + match x with + | Queries.MayCreationLockset -> + let ask = Analyses.ask_of_man man in + let tid_lifted = ask.f Queries.CurrentThreadId in + (match tid_lifted with + | `Lifted tid -> (man.global tid : G.t) + | _ -> G.top ()) + | _ -> Queries.Result.top x + ;; end module TaintedCreationLocksetSpec = struct diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 6f75fb579d..7dd48f3a2f 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -77,6 +77,7 @@ type invariant_context = Invariant.context = { module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end) +module ALS = SetDomain.Make (Printable.Prod (ThreadIdDomain.Thread) (LockDomain.MustLock)) (** GADT for queries with specific result type. *) type _ t = @@ -147,6 +148,7 @@ type _ t = | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *) | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t (* TODO consider returning descendants of ego threads only? *) + | MayCreationLockset: ALS.t t type 'a result = 'a @@ -223,6 +225,7 @@ struct | GhostVarAvailable _ -> (module MayBool) | InvariantGlobalNodes -> (module NS) | DescendantThreads _ -> (module ConcDomain.ThreadSet) + | MayCreationLockset -> (module ALS) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -298,6 +301,7 @@ struct | GhostVarAvailable _ -> MayBool.top () | InvariantGlobalNodes -> NS.top () | DescendantThreads _ -> ConcDomain.ThreadSet.top () + | MayCreationLockset -> ALS.top () end (* The type any_query can't be directly defined in Any as t, @@ -370,6 +374,7 @@ struct | Any (GhostVarAvailable _) -> 62 | Any InvariantGlobalNodes -> 63 | Any (DescendantThreads _) -> 64 + | Any MayCreationLockset -> 65 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -545,6 +550,7 @@ struct | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads" + | Any MayCreationLockset -> Pretty.dprintf "MayCreationLockset" end let to_value_domain_ask (ask: ask) = From 61d5c3f90cf275cdde0098c813d561f2c1899582 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Sun, 16 Nov 2025 22:06:14 +0100 Subject: [PATCH 15/95] InterThreadedLockset query --- src/analyses/creationLockset.ml | 14 ++++++++++++++ src/domains/queries.ml | 5 +++++ 2 files changed, 19 insertions(+) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 583cf63dc2..ad604d7dcb 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -103,6 +103,20 @@ module TaintedCreationLocksetSpec = struct ())) | _ -> () ;; + + let query man (type a) (x : a Queries.t) : a Queries.result = + match x with + | Queries.MayCreationLockset -> + let ask = Analyses.ask_of_man man in + let creation_lockset = ask.f Queries.MayCreationLockset in + let tid_lifted = ask.f Queries.CurrentThreadId in + (match tid_lifted with + | `Lifted tid -> + let tainted_creation_lockset = man.global tid in + G.diff creation_lockset tainted_creation_lockset + | _ -> G.top ()) + | _ -> Queries.Result.top x + ;; end let _ = diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 7dd48f3a2f..24c0f7880f 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -149,6 +149,7 @@ type _ t = | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *) | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t (* TODO consider returning descendants of ego threads only? *) | MayCreationLockset: ALS.t t + | InterThreadedLockset: ALS.t t type 'a result = 'a @@ -226,6 +227,7 @@ struct | InvariantGlobalNodes -> (module NS) | DescendantThreads _ -> (module ConcDomain.ThreadSet) | MayCreationLockset -> (module ALS) + | InterThreadedLockset -> (module ALS) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -302,6 +304,7 @@ struct | InvariantGlobalNodes -> NS.top () | DescendantThreads _ -> ConcDomain.ThreadSet.top () | MayCreationLockset -> ALS.top () + | InterThreadedLockset -> ALS.top () end (* The type any_query can't be directly defined in Any as t, @@ -375,6 +378,7 @@ struct | Any InvariantGlobalNodes -> 63 | Any (DescendantThreads _) -> 64 | Any MayCreationLockset -> 65 + | Any InterThreadedLockset -> 66 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -551,6 +555,7 @@ struct | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads" | Any MayCreationLockset -> Pretty.dprintf "MayCreationLockset" + | Any InterThreadedLockset -> Pretty.dprintf "InterThreadedLockset" end let to_value_domain_ask (ask: ask) = From e1719b2e55392d4eb83e03cb1780f513b29c71f2 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Sun, 16 Nov 2025 22:08:35 +0100 Subject: [PATCH 16/95] fix incorrect query answer type in transitive descendants analysis --- src/analyses/transitiveDescendants.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/transitiveDescendants.ml b/src/analyses/transitiveDescendants.ml index 4b9c1300af..eaabedc190 100644 --- a/src/analyses/transitiveDescendants.ml +++ b/src/analyses/transitiveDescendants.ml @@ -19,7 +19,7 @@ module TransitiveDescendants = struct let query man (type a) (x : a Queries.t) : a Queries.result = match x with - | Queries.DescendantThreads t -> (man.global : TID.t -> ConcDomain.ThreadSet.t) + | Queries.DescendantThreads t -> (man.global t : G.t) | _ -> Queries.Result.top x ;; From 8720b2383dd83964027c3a9d5b93afcf16c42b6d Mon Sep 17 00:00:00 2001 From: dabund24 Date: Tue, 18 Nov 2025 19:45:22 +0100 Subject: [PATCH 17/95] cartesian product helper functions --- src/analyses/creationLockset.ml | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index ad604d7dcb..e9dc78a609 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -3,7 +3,9 @@ module LF = LibraryFunctions (* TODO use ThreadLifted instead? Are Top or Bot relevant *) module TID = ThreadIdDomain.Thread +module TIDs = ConcDomain.ThreadSet module LID = LockDomain.MustLock +module LIDs = LockDomain.MustLockset module AncestorLocksetSpec = struct include IdentityUnitContextsSpec (* no context necessary(?) *) @@ -23,6 +25,21 @@ module AncestorLocksetSpec = struct let contribute_lock man tid lock child_tid = man.sideg child_tid (G.singleton (tid, lock)) ;; + + (** compute [tids] \times \{[lock]\} *) + let singleton_cartesian_prod tids lock = + TIDs.fold (fun tid acc -> G.add (tid, lock) acc) tids (G.empty ()) + ;; + + (** compute the cartesian product [tids] \times [locks] *) + let cartesian_prod tids locks = + LIDs.fold + (fun lock acc -> + let tids_times_lock = singleton_cartesian_prod tids lock in + G.union tids_times_lock acc) + locks + (G.empty ()) + ;; end (** @@ -44,9 +61,9 @@ module CreationLocksetSpec = struct match tid_lifted, child_tid_lifted with | `Lifted tid, `Lifted child_tid -> let lockset = ask.f Queries.MustLockset in - (* contribution (t_1, l) to global of t_0 for all l in L: *) + let to_contribute = cartesian_prod (TIDs.singleton tid) lockset in + man.sideg child_tid to_contribute (* TODO also register for transitive descendants of t_1! *) - LockDomain.MustLockset.iter (fun l -> contribute_lock man tid l child_tid) lockset | _ -> (* deal with top or bottom? *) () ;; From 7c6e5d9f97aaeb6a505ad4621f841afba1ee9a35 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Tue, 18 Nov 2025 19:46:16 +0100 Subject: [PATCH 18/95] remove unused function from TaintedCreationLocksetSpec --- src/analyses/creationLockset.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index e9dc78a609..359f528d6d 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -88,7 +88,6 @@ module TaintedCreationLocksetSpec = struct include AncestorLocksetSpec let name () = "taintedCreationLockset" - let eval_exp_addr (a : Queries.ask) exp = a.f (Queries.MayPointTo exp) (** stolen from mutexGhost.ml. TODO Maybe add to library? *) let mustlock_of_addr (addr : LockDomain.Addr.t) : LockDomain.MustLock.t option = From 61a48dc84d6d899075de79ea5bd307c887942c3d Mon Sep 17 00:00:00 2001 From: dabund24 Date: Tue, 18 Nov 2025 19:49:10 +0100 Subject: [PATCH 19/95] correct comment in tainted lockset analysis --- src/analyses/creationLockset.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 359f528d6d..723c762df2 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -112,7 +112,7 @@ module TaintedCreationLocksetSpec = struct let lock_opt = mustlock_of_addr addr in (match lock_opt with | Some lock -> - (* contribute possibly_running_tids \times \{lock\} *) + (* contribute for all possibly_running_tids: (tid, lock) *) ConcDomain.ThreadSet.iter (contribute_lock man tid lock) possibly_running_tids | None -> (* TODO any lock could have been unlocked. Contribute for all possibly_running_tids their full CreationLocksets to invalidate them!! *) From 31ceff8c24da34928811f580b4c0a2b8fc951fef Mon Sep 17 00:00:00 2001 From: dabund24 Date: Tue, 18 Nov 2025 19:59:46 +0100 Subject: [PATCH 20/95] replace threadset and lockset module references with shorthand --- src/analyses/creationLockset.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 723c762df2..8d96d64205 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -90,9 +90,9 @@ module TaintedCreationLocksetSpec = struct let name () = "taintedCreationLockset" (** stolen from mutexGhost.ml. TODO Maybe add to library? *) - let mustlock_of_addr (addr : LockDomain.Addr.t) : LockDomain.MustLock.t option = + let mustlock_of_addr (addr : LockDomain.Addr.t) : LID.t option = match addr with - | Addr mv when LockDomain.Mval.is_definite mv -> Some (LockDomain.MustLock.of_mval mv) + | Addr mv when LockDomain.Mval.is_definite mv -> Some (LID.of_mval mv) | _ -> None ;; @@ -106,14 +106,12 @@ module TaintedCreationLocksetSpec = struct | `Lifted tid -> let may_created_tids = ask.f Queries.CreatedThreads in let must_joined_tids = ask.f Queries.MustJoinedThreads in - let possibly_running_tids = - ConcDomain.ThreadSet.diff may_created_tids must_joined_tids - in + let possibly_running_tids = TIDs.diff may_created_tids must_joined_tids in let lock_opt = mustlock_of_addr addr in (match lock_opt with | Some lock -> (* contribute for all possibly_running_tids: (tid, lock) *) - ConcDomain.ThreadSet.iter (contribute_lock man tid lock) possibly_running_tids + TIDs.iter (contribute_lock man tid lock) possibly_running_tids | None -> (* TODO any lock could have been unlocked. Contribute for all possibly_running_tids their full CreationLocksets to invalidate them!! *) ())) From 450d349f7b5335f763ef5b648a8bb91e2f55f96c Mon Sep 17 00:00:00 2001 From: dabund24 Date: Tue, 18 Nov 2025 20:25:22 +0100 Subject: [PATCH 21/95] function for getting currently running tids --- src/analyses/creationLockset.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 8d96d64205..9096935c89 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -89,6 +89,16 @@ module TaintedCreationLocksetSpec = struct let name () = "taintedCreationLockset" + (** compute all threads that may run along with the ego thread at a program point + @param ask ask of ego thread at the program point + *) + let get_possibly_running_tids (ask : Queries.ask) = + let may_created_tids = ask.f Queries.CreatedThreads in + (* TODO also consider transitive descendants of may_created_tids *) + let must_joined_tids = ask.f Queries.MustJoinedThreads in + TIDs.diff may_created_tids must_joined_tids + ;; + (** stolen from mutexGhost.ml. TODO Maybe add to library? *) let mustlock_of_addr (addr : LockDomain.Addr.t) : LID.t option = match addr with @@ -104,9 +114,7 @@ module TaintedCreationLocksetSpec = struct (match tid_lifted with | `Top | `Bot -> () | `Lifted tid -> - let may_created_tids = ask.f Queries.CreatedThreads in - let must_joined_tids = ask.f Queries.MustJoinedThreads in - let possibly_running_tids = TIDs.diff may_created_tids must_joined_tids in + let possibly_running_tids = get_possibly_running_tids ask in let lock_opt = mustlock_of_addr addr in (match lock_opt with | Some lock -> From 7d1fa1aa079d7829117a2a928db27ba60f6a4a8f Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 19 Nov 2025 14:04:54 +0100 Subject: [PATCH 22/95] inter-threaded lockset A module --- src/analyses/creationLockset.ml | 52 +++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 9096935c89..81d2629e14 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -139,6 +139,58 @@ module TaintedCreationLocksetSpec = struct | _ -> G.top ()) | _ -> Queries.Result.top x ;; + + module A = struct + (** ego tid * lockset * inter-threaded lockset *) + include Printable.Prod3 (TID) (LIDs) (G) + + let name () = "InterThreadedLockset" + + (** checks if [itls1] has a member ([tp1], [l]) such that [itls2] has a member ([tp2], [l]) with [tp1] != [tp2] + @param itls1 inter-threaded lockset of first thread [t1] + @param itls2 inter-threaded lockset of second thread [t2] + @returns whether [t1] and [t2] must be running mutually exclusive + *) + let both_protected_inter_threaded itls1 itls2 = + let itls2_has_same_lock_other_tid (tp1, l1) = + G.exists (fun (tp2, l2) -> l1 = l2 && tp1 <> tp2) itls2 + in + G.exists itls2_has_same_lock_other_tid itls1 + ;; + + (** checks if [itls1] has a member ([tp1], [l1]) such that [l1] is in [ls2] and [tp1] != [t2] + @param itls1 inter-threaded lockset of thread [t1] at first program point + @param t2 thread id at second program point + @param ls2 lockset at second program point + @returns whether [t1] must be running mutually exclusive with second program point + *) + let one_protected_inter_threaded_other_intra_threaded itls1 t2 ls2 = + G.exists (fun (tp1, l1) -> LIDs.mem l1 ls2 && tp1 <> t2) itls1 + ;; + + let may_race (t1, ls1, itls1) (t2, ls2, itls2) = + not + (both_protected_inter_threaded itls1 itls2 + || one_protected_inter_threaded_other_intra_threaded itls1 t2 ls2 + || one_protected_inter_threaded_other_intra_threaded itls2 t1 ls1) + ;; + + let should_print _ = true + end + + let access man _ = + let ask = Analyses.ask_of_man man in + let tid_lifted = ask.f Queries.CurrentThreadId in + match tid_lifted with + | `Lifted tid -> + let lockset = ask.f Queries.MustLockset in + let creation_lockset = ask.f Queries.MayCreationLockset in + let tainted_creation_lockset = man.global tid in + (* all values in creation lockset, but not in tainted creation lockset *) + let inter_threaded_lockset = G.diff creation_lockset tainted_creation_lockset in + tid, lockset, inter_threaded_lockset + | _ -> ThreadIdDomain.UnknownThread, LIDs.empty (), G.empty () + ;; end let _ = From 3c52c76e13b2560c49e0d97425f334080b0166a7 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 19 Nov 2025 14:48:02 +0100 Subject: [PATCH 23/95] use topped set for global domain in AncestorLocksetSpec --- src/analyses/creationLockset.ml | 4 ++-- src/domains/queries.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 81d2629e14..762ea0385a 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -16,8 +16,8 @@ module AncestorLocksetSpec = struct include StdV end - module G = SetDomain.Make (Printable.Prod (TID) (LID)) - (* 2^{T\times L}. TODO: Prod or ProdSimple? *) + (** 2 ^ { [TID] \times [LID] } *) + module G = Queries.ALS let startstate _ = D.bot () let exitstate _ = D.bot () diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 24c0f7880f..a9b90c75eb 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -77,7 +77,7 @@ type invariant_context = Invariant.context = { module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end) -module ALS = SetDomain.Make (Printable.Prod (ThreadIdDomain.Thread) (LockDomain.MustLock)) +module ALS = SetDomain.ToppedSet (Printable.Prod (ThreadIdDomain.Thread) (LockDomain.MustLock)) (struct let topname = "all pairs of threads and locks" end) (** GADT for queries with specific result type. *) type _ t = From 8b1727f20d0f883130dc4e3961f2ee9ae34f5346 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 19 Nov 2025 23:13:26 +0100 Subject: [PATCH 24/95] replace comparison operators with equals function of domains --- src/analyses/creationLockset.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 762ea0385a..436e2cb9b2 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -153,7 +153,7 @@ module TaintedCreationLocksetSpec = struct *) let both_protected_inter_threaded itls1 itls2 = let itls2_has_same_lock_other_tid (tp1, l1) = - G.exists (fun (tp2, l2) -> l1 = l2 && tp1 <> tp2) itls2 + G.exists (fun (tp2, l2) -> LID.equal l1 l2 && (not @@ TID.equal tp1 tp2)) itls2 in G.exists itls2_has_same_lock_other_tid itls1 ;; @@ -165,7 +165,7 @@ module TaintedCreationLocksetSpec = struct @returns whether [t1] must be running mutually exclusive with second program point *) let one_protected_inter_threaded_other_intra_threaded itls1 t2 ls2 = - G.exists (fun (tp1, l1) -> LIDs.mem l1 ls2 && tp1 <> t2) itls1 + G.exists (fun (tp1, l1) -> LIDs.mem l1 ls2 && (not @@ TID.equal tp1 t2)) itls1 ;; let may_race (t1, ls1, itls1) (t2, ls2, itls2) = From b0751dcfcf8cc28c502203c7f5c5887ef1d0ed97 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 19 Nov 2025 23:14:56 +0100 Subject: [PATCH 25/95] add creationLockset analysis to dependencies of taintedCreationLockset analysis --- src/analyses/creationLockset.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 436e2cb9b2..2e15414465 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -201,6 +201,6 @@ let _ = let _ = MCP.register_analysis - ~dep:[ "threadid"; "mutex"; "threadJoins" ] + ~dep:[ "threadid"; "mutex"; "threadJoins"; "creationLockset" ] (module TaintedCreationLocksetSpec : MCPSpec) ;; From 09f28ba74aa5d929cc376148736a8bf2f00e4b80 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 19 Nov 2025 23:21:22 +0100 Subject: [PATCH 26/95] fix regression test files --- .../65-inter-proc-lock1_racefree.c | 6 ++--- .../66-inter-proc-lock_racefree.c | 22 +++++++++---------- .../28-race_reach/67-lock-fork_racefree.c | 9 ++++---- 3 files changed, 16 insertions(+), 21 deletions(-) diff --git a/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c b/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c index a3eff997b8..3802d10219 100644 --- a/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c +++ b/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c @@ -1,6 +1,4 @@ -//PARAM: --set lib.activated[+] sv-comp --set ana.activated[+] creationLockset #include -#include "racemacros.h" int global = 0; pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; @@ -8,13 +6,13 @@ pthread_t id1, id2; void *t1(void *arg) { pthread_mutex_lock(&mutex); - assert_racefree(global); + global++; // NORACE pthread_mutex_unlock(&mutex); return NULL; } void *t2(void *arg) { // t2 is protected by mutex locked in main thread - access(global); + global++; // NORACE return NULL; } diff --git a/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c b/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c index ece2bda785..05d960f4da 100644 --- a/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c +++ b/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c @@ -1,34 +1,32 @@ -//PARAM: --set lib.activated[+] sv-comp --set ana.activated[+] creationLockset #include -#include "racemacros.h" int global = 0; pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; -pthread_t tmain_child, t1, t1_child; +pthread_t id_main_child, id_1, id_1_child; -void *t1_child(void* arg) { // t1child is protected by mutex locked in t1 - access(global); +void *t1_child_fun(void* arg) { // t1child is protected by mutex locked in t1 + global++; // NORACE return NULL; } -void *tmain_child(void *arg) { // tmainchild is protected by mutex locked in main thread - assert_racefree(global); // NORACE +void *tmain_child_fun(void *arg) { // tmainchild is protected by mutex locked in main thread + global++; // NORACE return NULL; } void *t1_fun(void *arg) { pthread_mutex_lock(&mutex); - pthread_create(&t1_child, NULL, t1_child, NULL); - pthread_join(t1_child, NULL); + pthread_create(&id_1_child, NULL, t1_child_fun, NULL); + pthread_join(id_1_child, NULL); pthread_mutex_unlock(&mutex); return NULL; } int main(void) { - pthread_create(&t1, NULL, t1, NULL); + pthread_create(&id_1, NULL, t1_fun, NULL); pthread_mutex_lock(&mutex); - pthread_create(&tmain_child, NULL, tmain_child, NULL); - pthread_join(tmain_child, NULL); + pthread_create(&id_main_child, NULL, tmain_child_fun, NULL); + pthread_join(id_main_child, NULL); pthread_mutex_unlock(&mutex); return 0; } diff --git a/tests/regression/28-race_reach/67-lock-fork_racefree.c b/tests/regression/28-race_reach/67-lock-fork_racefree.c index 7a77b91c2c..82a92f41cc 100644 --- a/tests/regression/28-race_reach/67-lock-fork_racefree.c +++ b/tests/regression/28-race_reach/67-lock-fork_racefree.c @@ -1,21 +1,20 @@ -//PARAM: --set lib.activated[+] sv-comp #include -#include "racemacros.h" int global = 0; pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1; void *t_fun(void *arg) { pthread_mutex_lock(&mutex); // must happen after unlock in main pthread_mutex_unlock(&mutex); - assert_racefree(global); // no race + global++; // NORACE return NULL; } int main(void) { pthread_mutex_lock(&mutex); - create_threads(t); - access(global); + pthread_create(&id1, NULL, t_fun, NULL); + global++; // NORACE pthread_mutex_unlock(&mutex); return 0; } From ea5a72a694d7a70a0144aef737a96839849eb268 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 19 Nov 2025 23:30:10 +0100 Subject: [PATCH 27/95] move test files to better locations --- .../01-lockset_inter_threaded_lock_racefree.c} | 0 .../02-both_inter_threaded_lock_racefree.c} | 0 .../03-lock_fork_racefree.c} | 0 3 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/{28-race_reach/65-inter-proc-lock1_racefree.c => 89-races_ancestor_locksets/01-lockset_inter_threaded_lock_racefree.c} (100%) rename tests/regression/{28-race_reach/66-inter-proc-lock_racefree.c => 89-races_ancestor_locksets/02-both_inter_threaded_lock_racefree.c} (100%) rename tests/regression/{28-race_reach/67-lock-fork_racefree.c => 89-races_ancestor_locksets/03-lock_fork_racefree.c} (100%) diff --git a/tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c b/tests/regression/89-races_ancestor_locksets/01-lockset_inter_threaded_lock_racefree.c similarity index 100% rename from tests/regression/28-race_reach/65-inter-proc-lock1_racefree.c rename to tests/regression/89-races_ancestor_locksets/01-lockset_inter_threaded_lock_racefree.c diff --git a/tests/regression/28-race_reach/66-inter-proc-lock_racefree.c b/tests/regression/89-races_ancestor_locksets/02-both_inter_threaded_lock_racefree.c similarity index 100% rename from tests/regression/28-race_reach/66-inter-proc-lock_racefree.c rename to tests/regression/89-races_ancestor_locksets/02-both_inter_threaded_lock_racefree.c diff --git a/tests/regression/28-race_reach/67-lock-fork_racefree.c b/tests/regression/89-races_ancestor_locksets/03-lock_fork_racefree.c similarity index 100% rename from tests/regression/28-race_reach/67-lock-fork_racefree.c rename to tests/regression/89-races_ancestor_locksets/03-lock_fork_racefree.c From 0b0fae8e91d4362c383260aca46f33bfd24157bb Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 20 Nov 2025 10:07:34 +0100 Subject: [PATCH 28/95] remove unused inter threaded lockset query --- src/analyses/creationLockset.ml | 14 -------------- src/domains/queries.ml | 5 ----- 2 files changed, 19 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 2e15414465..cf858301e4 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -126,20 +126,6 @@ module TaintedCreationLocksetSpec = struct | _ -> () ;; - let query man (type a) (x : a Queries.t) : a Queries.result = - match x with - | Queries.MayCreationLockset -> - let ask = Analyses.ask_of_man man in - let creation_lockset = ask.f Queries.MayCreationLockset in - let tid_lifted = ask.f Queries.CurrentThreadId in - (match tid_lifted with - | `Lifted tid -> - let tainted_creation_lockset = man.global tid in - G.diff creation_lockset tainted_creation_lockset - | _ -> G.top ()) - | _ -> Queries.Result.top x - ;; - module A = struct (** ego tid * lockset * inter-threaded lockset *) include Printable.Prod3 (TID) (LIDs) (G) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index a9b90c75eb..846840cdbe 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -149,7 +149,6 @@ type _ t = | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *) | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t (* TODO consider returning descendants of ego threads only? *) | MayCreationLockset: ALS.t t - | InterThreadedLockset: ALS.t t type 'a result = 'a @@ -227,7 +226,6 @@ struct | InvariantGlobalNodes -> (module NS) | DescendantThreads _ -> (module ConcDomain.ThreadSet) | MayCreationLockset -> (module ALS) - | InterThreadedLockset -> (module ALS) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -304,7 +302,6 @@ struct | InvariantGlobalNodes -> NS.top () | DescendantThreads _ -> ConcDomain.ThreadSet.top () | MayCreationLockset -> ALS.top () - | InterThreadedLockset -> ALS.top () end (* The type any_query can't be directly defined in Any as t, @@ -378,7 +375,6 @@ struct | Any InvariantGlobalNodes -> 63 | Any (DescendantThreads _) -> 64 | Any MayCreationLockset -> 65 - | Any InterThreadedLockset -> 66 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -555,7 +551,6 @@ struct | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads" | Any MayCreationLockset -> Pretty.dprintf "MayCreationLockset" - | Any InterThreadedLockset -> Pretty.dprintf "InterThreadedLockset" end let to_value_domain_ask (ask: ask) = From 3a5513d5ee3d14c4e3d8812d849f83fc833d00c0 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 20 Nov 2025 12:10:30 +0100 Subject: [PATCH 29/95] hash descendant thread query param --- src/domains/queries.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 846840cdbe..de13ca303b 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -481,6 +481,7 @@ struct | Any (MaySignedOverflow e) -> CilType.Exp.hash e | Any (GasExhausted f) -> CilType.Fundec.hash f | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v + | Any (DescendantThreads t) -> ThreadIdDomain.hash_thread t (* TODO is this fine? *) (* IterSysVars: *) (* - argument is a function and functions cannot be compared in any meaningful way. *) (* - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *) From cecf2440f503dd339164cc20af68514e583d8338 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 20 Nov 2025 12:12:52 +0100 Subject: [PATCH 30/95] transitive version of (tainted) creation locksets --- src/analyses/creationLockset.ml | 35 +++++++++++++++++++++++++-------- 1 file changed, 27 insertions(+), 8 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index cf858301e4..4fe989ee48 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -22,9 +22,12 @@ module AncestorLocksetSpec = struct let startstate _ = D.bot () let exitstate _ = D.bot () - let contribute_lock man tid lock child_tid = - man.sideg child_tid (G.singleton (tid, lock)) - ;; + (** register a contribution to a global: global.[child_tid] \supseteq [to_contribute] + @param man man at program point + @param to_contribute new edges from [child_tid] to register + @param child_tid + *) + let contribute_lock man to_contribute child_tid = man.sideg child_tid to_contribute (** compute [tids] \times \{[lock]\} *) let singleton_cartesian_prod tids lock = @@ -40,6 +43,16 @@ module AncestorLocksetSpec = struct locks (G.empty ()) ;; + + (** reflexive-transitive closure of child relation applied to [tid] + @param ask any ask + @param tid + @returns [{ tid }] \cup DES([tid]) + *) + let descendants_closure (ask : Queries.ask) tid = + let transitive_descendants = ask.f @@ Queries.DescendantThreads tid in + TIDs.add tid transitive_descendants + ;; end (** @@ -60,10 +73,10 @@ module CreationLocksetSpec = struct let child_tid_lifted = child_ask.f Queries.CurrentThreadId in match tid_lifted, child_tid_lifted with | `Lifted tid, `Lifted child_tid -> + let descendants = descendants_closure child_ask child_tid in let lockset = ask.f Queries.MustLockset in let to_contribute = cartesian_prod (TIDs.singleton tid) lockset in - man.sideg child_tid to_contribute - (* TODO also register for transitive descendants of t_1! *) + TIDs.iter (contribute_lock man to_contribute) descendants | _ -> (* deal with top or bottom? *) () ;; @@ -94,9 +107,14 @@ module TaintedCreationLocksetSpec = struct *) let get_possibly_running_tids (ask : Queries.ask) = let may_created_tids = ask.f Queries.CreatedThreads in - (* TODO also consider transitive descendants of may_created_tids *) + let may_transitively_created_tids = + TIDs.fold + (fun child_tid acc -> TIDs.union acc (descendants_closure ask child_tid)) + may_created_tids + (TIDs.empty ()) + in let must_joined_tids = ask.f Queries.MustJoinedThreads in - TIDs.diff may_created_tids must_joined_tids + TIDs.diff may_transitively_created_tids must_joined_tids ;; (** stolen from mutexGhost.ml. TODO Maybe add to library? *) @@ -119,7 +137,8 @@ module TaintedCreationLocksetSpec = struct (match lock_opt with | Some lock -> (* contribute for all possibly_running_tids: (tid, lock) *) - TIDs.iter (contribute_lock man tid lock) possibly_running_tids + let to_contribute = G.singleton (tid, lock) in + TIDs.iter (contribute_lock man to_contribute) possibly_running_tids | None -> (* TODO any lock could have been unlocked. Contribute for all possibly_running_tids their full CreationLocksets to invalidate them!! *) ())) From 55184fe9cf75a47da4b70981af747ce036176504 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 20 Nov 2025 12:14:27 +0100 Subject: [PATCH 31/95] add race and transitive descendants analyses as dependencies to creation lockset analyses --- src/analyses/creationLockset.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 4fe989ee48..ded0c9f5c1 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -200,12 +200,19 @@ end let _ = MCP.register_analysis - ~dep:[ "threadid"; "mutex" ] + ~dep:[ "threadid"; "mutex"; "race"; "transitiveDescendants" ] (module CreationLocksetSpec : MCPSpec) ;; let _ = MCP.register_analysis - ~dep:[ "threadid"; "mutex"; "threadJoins"; "creationLockset" ] + ~dep: + [ "threadid" + ; "mutex" + ; "threadJoins" + ; "race" + ; "transitiveDescendants" + ; "creationLockset" + ] (module TaintedCreationLocksetSpec : MCPSpec) ;; From 611a91eb52950daf8726287c0cd69c21aaf0d371 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 20 Nov 2025 12:32:59 +0100 Subject: [PATCH 32/95] regression tests for transitive creation locksets --- ..._inter_threaded_lock_transitive_racefree.c | 31 +++++++++++++ ...ter_threaded_lockset_transitive_racefree.c | 44 +++++++++++++++++++ 2 files changed, 75 insertions(+) create mode 100644 tests/regression/89-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c create mode 100644 tests/regression/89-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c diff --git a/tests/regression/89-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c b/tests/regression/89-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c new file mode 100644 index 0000000000..2260355812 --- /dev/null +++ b/tests/regression/89-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c @@ -0,0 +1,31 @@ +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2, id3; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void* t3(void* arg) { + global++; // NORACE +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + pthread_create(&id3, NULL, t3, NULL); + pthread_join(id3, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_join(id2, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/89-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c b/tests/regression/89-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c new file mode 100644 index 0000000000..fde7d93daf --- /dev/null +++ b/tests/regression/89-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c @@ -0,0 +1,44 @@ +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id_main_child, id_main_grand_child, id_1, id_1_child, id_1_grand_child; + +void *t1_grand_child_fun(void* arg) { // t1_grand_child is protected by mutex locked in t1 + global++; // NORACE + return NULL; +} + +void *t1_child_fun(void *arg) { + pthread_create(&id_1_grand_child, NULL, t1_grand_child_fun, NULL); + pthread_join(id_1_grand_child, NULL); + return NULL; +} + +void *t1_fun(void *arg) { + pthread_mutex_lock(&mutex); + pthread_create(&id_1_child, NULL, t1_child_fun, NULL); + pthread_join(id_1_child, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *tmain_grand_child_fun(void* arg) { // tmain_grand_child is protected by mutex locked in main + global++; // NORACE + return NULL; +} + +void *tmain_child_fun(void *arg) { + pthread_create(&id_main_grand_child, NULL, tmain_grand_child_fun, NULL); + pthread_join(id_main_grand_child, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id_1, NULL, t1_fun, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id_main_child, NULL, tmain_child_fun, NULL); + pthread_join(id_main_child, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} From c1ad680cf5bb2ee87f25a48662a459762339ba20 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 20 Nov 2025 12:33:44 +0100 Subject: [PATCH 33/95] rename regression test for second case --- .../{03-lock_fork_racefree.c => 20-lock_fork_racefree.c} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename tests/regression/89-races_ancestor_locksets/{03-lock_fork_racefree.c => 20-lock_fork_racefree.c} (100%) diff --git a/tests/regression/89-races_ancestor_locksets/03-lock_fork_racefree.c b/tests/regression/89-races_ancestor_locksets/20-lock_fork_racefree.c similarity index 100% rename from tests/regression/89-races_ancestor_locksets/03-lock_fork_racefree.c rename to tests/regression/89-races_ancestor_locksets/20-lock_fork_racefree.c From 70dabb732a8d047be508c4f6eaeb4957942f4b0c Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 20 Nov 2025 13:52:07 +0100 Subject: [PATCH 34/95] add thread param to MayCreationLockset query --- src/domains/queries.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index de13ca303b..2fbebb832c 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -148,7 +148,7 @@ type _ t = | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *) | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t (* TODO consider returning descendants of ego threads only? *) - | MayCreationLockset: ALS.t t + | MayCreationLockset: ThreadIdDomain.Thread.t -> ALS.t t type 'a result = 'a @@ -225,7 +225,7 @@ struct | GhostVarAvailable _ -> (module MayBool) | InvariantGlobalNodes -> (module NS) | DescendantThreads _ -> (module ConcDomain.ThreadSet) - | MayCreationLockset -> (module ALS) + | MayCreationLockset _ -> (module ALS) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -301,7 +301,7 @@ struct | GhostVarAvailable _ -> MayBool.top () | InvariantGlobalNodes -> NS.top () | DescendantThreads _ -> ConcDomain.ThreadSet.top () - | MayCreationLockset -> ALS.top () + | MayCreationLockset _ -> ALS.top () end (* The type any_query can't be directly defined in Any as t, @@ -374,7 +374,7 @@ struct | Any (GhostVarAvailable _) -> 62 | Any InvariantGlobalNodes -> 63 | Any (DescendantThreads _) -> 64 - | Any MayCreationLockset -> 65 + | Any (MayCreationLockset _) -> 65 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -482,6 +482,7 @@ struct | Any (GasExhausted f) -> CilType.Fundec.hash f | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v | Any (DescendantThreads t) -> ThreadIdDomain.hash_thread t (* TODO is this fine? *) + | Any (MayCreationLockset t) -> ThreadIdDomain.hash_thread t (* IterSysVars: *) (* - argument is a function and functions cannot be compared in any meaningful way. *) (* - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *) @@ -551,7 +552,7 @@ struct | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads" - | Any MayCreationLockset -> Pretty.dprintf "MayCreationLockset" + | Any (MayCreationLockset t) -> Pretty.dprintf "MayCreationLockset" end let to_value_domain_ask (ask: ask) = From 0e6373136ad550278c32bd7b067e2a2d90ba0d56 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 20 Nov 2025 13:54:31 +0100 Subject: [PATCH 35/95] handle unlock of unknown mutex --- src/analyses/creationLockset.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index ded0c9f5c1..c84afcfc5d 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -87,12 +87,7 @@ module CreationLocksetSpec = struct let query man (type a) (x : a Queries.t) : a Queries.result = match x with - | Queries.MayCreationLockset -> - let ask = Analyses.ask_of_man man in - let tid_lifted = ask.f Queries.CurrentThreadId in - (match tid_lifted with - | `Lifted tid -> (man.global tid : G.t) - | _ -> G.top ()) + | Queries.MayCreationLockset tid -> (man.global tid : G.t) | _ -> Queries.Result.top x ;; end @@ -140,8 +135,12 @@ module TaintedCreationLocksetSpec = struct let to_contribute = G.singleton (tid, lock) in TIDs.iter (contribute_lock man to_contribute) possibly_running_tids | None -> - (* TODO any lock could have been unlocked. Contribute for all possibly_running_tids their full CreationLocksets to invalidate them!! *) - ())) + (* any lock could have been unlocked. Contribute for all possibly_running_tids their full CreationLocksets to invalidate them!! *) + let contribute_creation_lockset des_tid = + let creation_lockset = ask.f @@ Queries.MayCreationLockset des_tid in + man.sideg des_tid creation_lockset + in + TIDs.iter contribute_creation_lockset possibly_running_tids)) | _ -> () ;; @@ -189,7 +188,7 @@ module TaintedCreationLocksetSpec = struct match tid_lifted with | `Lifted tid -> let lockset = ask.f Queries.MustLockset in - let creation_lockset = ask.f Queries.MayCreationLockset in + let creation_lockset = ask.f @@ Queries.MayCreationLockset tid in let tainted_creation_lockset = man.global tid in (* all values in creation lockset, but not in tainted creation lockset *) let inter_threaded_lockset = G.diff creation_lockset tainted_creation_lockset in From 3514a37ba849fede36a21c187fb0f575c4306faa Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 20 Nov 2025 14:08:14 +0100 Subject: [PATCH 36/95] edit some comments --- src/analyses/creationLockset.ml | 19 +++++++------------ src/analyses/transitiveDescendants.ml | 2 +- src/domains/queries.ml | 2 +- 3 files changed, 9 insertions(+), 14 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index c84afcfc5d..729e3c216c 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -1,7 +1,6 @@ open Analyses module LF = LibraryFunctions -(* TODO use ThreadLifted instead? Are Top or Bot relevant *) module TID = ThreadIdDomain.Thread module TIDs = ConcDomain.ThreadSet module LID = LockDomain.MustLock @@ -55,10 +54,8 @@ module AncestorLocksetSpec = struct ;; end -(** - collects for each thread t_n pairs of must-ancestors and locks (t_0,l): +(** collects for each thread t_n pairs of must-ancestors and locks (t_0,l): when t_n or a must-ancestor t_1 of t_n was created, the parent t_0 must have held l. - TODO: check if this requirement can be loosened *) module CreationLocksetSpec = struct include AncestorLocksetSpec @@ -72,19 +69,14 @@ module CreationLocksetSpec = struct let child_ask = Analyses.ask_of_man fman in let child_tid_lifted = child_ask.f Queries.CurrentThreadId in match tid_lifted, child_tid_lifted with - | `Lifted tid, `Lifted child_tid -> + | `Lifted tid, `Lifted child_tid when TID.must_be_ancestor tid child_tid -> let descendants = descendants_closure child_ask child_tid in let lockset = ask.f Queries.MustLockset in let to_contribute = cartesian_prod (TIDs.singleton tid) lockset in TIDs.iter (contribute_lock man to_contribute) descendants - | _ -> (* deal with top or bottom? *) () + | _ -> (* TODO deal with top or bottom? *) () ;; - (* TODO: consider edge cases (most likely in creation lockset analysis)! - - `ana.threads.include-node` is false. Two threads created with different locksets may have the same id that way! - - child thread is not unique and thus could also ancestor of ego thread. In this case, it can also be created with a different lockset! - - more? *) - let query man (type a) (x : a Queries.t) : a Queries.result = match x with | Queries.MayCreationLockset tid -> (man.global tid : G.t) @@ -92,6 +84,9 @@ module CreationLocksetSpec = struct ;; end +(** collects for each thread t_n pairs of ancestors and locks (t_0,l): + when l is unlocked in t_0, t_n could be running. +*) module TaintedCreationLocksetSpec = struct include AncestorLocksetSpec @@ -112,7 +107,7 @@ module TaintedCreationLocksetSpec = struct TIDs.diff may_transitively_created_tids must_joined_tids ;; - (** stolen from mutexGhost.ml. TODO Maybe add to library? *) + (** stolen from mutexGhost.ml. TODO Maybe add to utils? *) let mustlock_of_addr (addr : LockDomain.Addr.t) : LID.t option = match addr with | Addr mv when LockDomain.Mval.is_definite mv -> Some (LID.of_mval mv) diff --git a/src/analyses/transitiveDescendants.ml b/src/analyses/transitiveDescendants.ml index eaabedc190..378ee875e6 100644 --- a/src/analyses/transitiveDescendants.ml +++ b/src/analyses/transitiveDescendants.ml @@ -36,7 +36,7 @@ module TransitiveDescendants = struct | `Lifted child_tid -> (* contribute new child *) let _ = man.sideg tid (G.singleton child_tid) in - (* transitive hull *) + (* transitive closure *) let child_descendants = man.global child_tid in man.sideg tid child_descendants) ;; diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 2fbebb832c..bd5b64be8e 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -147,7 +147,7 @@ type _ t = | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t (** YAML witness entries for a global unknown ([Obj.t] represents [Spec.V.t]) and YAML witness task. *) | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *) - | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t (* TODO consider returning descendants of ego threads only? *) + | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t | MayCreationLockset: ThreadIdDomain.Thread.t -> ALS.t t type 'a result = 'a From 61b96094a7cff27b25ae15ee14c231890d28fb9b Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 4 Dec 2025 12:31:21 +0100 Subject: [PATCH 37/95] remove redundant must-ancestor check --- src/analyses/creationLockset.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 729e3c216c..83881fedf6 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -1,3 +1,5 @@ +(** Ancestor-lock analysis. See https://github.com/goblint/analyzer/pull/1865 *) + open Analyses module LF = LibraryFunctions @@ -69,7 +71,7 @@ module CreationLocksetSpec = struct let child_ask = Analyses.ask_of_man fman in let child_tid_lifted = child_ask.f Queries.CurrentThreadId in match tid_lifted, child_tid_lifted with - | `Lifted tid, `Lifted child_tid when TID.must_be_ancestor tid child_tid -> + | `Lifted tid, `Lifted child_tid -> let descendants = descendants_closure child_ask child_tid in let lockset = ask.f Queries.MustLockset in let to_contribute = cartesian_prod (TIDs.singleton tid) lockset in From 52ce9f0d992d25a53774a8235b1ec0200d41e87c Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 4 Dec 2025 13:55:05 +0100 Subject: [PATCH 38/95] fix and update some comments --- src/analyses/creationLockset.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 83881fedf6..9bfa4518b1 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -2,12 +2,12 @@ open Analyses module LF = LibraryFunctions - module TID = ThreadIdDomain.Thread module TIDs = ConcDomain.ThreadSet module LID = LockDomain.MustLock module LIDs = LockDomain.MustLockset +(** common base for [CreationLocksetSpec] and [TaintedCreationLocksetSpec] *) module AncestorLocksetSpec = struct include IdentityUnitContextsSpec (* no context necessary(?) *) module D = Lattice.Unit @@ -56,8 +56,8 @@ module AncestorLocksetSpec = struct ;; end -(** collects for each thread t_n pairs of must-ancestors and locks (t_0,l): - when t_n or a must-ancestor t_1 of t_n was created, the parent t_0 must have held l. +(** collects for each thread t_n pairs of ancestors and locks (t_0,l): + when t_n or an ancestor t_1 of t_n was created, the creating thread t_0 must have held l. *) module CreationLocksetSpec = struct include AncestorLocksetSpec @@ -87,7 +87,7 @@ module CreationLocksetSpec = struct end (** collects for each thread t_n pairs of ancestors and locks (t_0,l): - when l is unlocked in t_0, t_n could be running. + l may be unlocked in t_0 while t_n could be running. *) module TaintedCreationLocksetSpec = struct include AncestorLocksetSpec From 7f4e531a6d19d65a8d19e9096ec7be0e89edd48a Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 4 Dec 2025 14:00:36 +0100 Subject: [PATCH 39/95] minimize contributions to tcl when unlock of unknown thread is encountered --- src/analyses/creationLockset.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 9bfa4518b1..0892c3223d 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -132,10 +132,13 @@ module TaintedCreationLocksetSpec = struct let to_contribute = G.singleton (tid, lock) in TIDs.iter (contribute_lock man to_contribute) possibly_running_tids | None -> - (* any lock could have been unlocked. Contribute for all possibly_running_tids their full CreationLocksets to invalidate them!! *) + (* any lock could have been unlocked. Contribute for all possibly_running_tids all members of their CreationLocksets with the ego thread to invalidate them!! *) let contribute_creation_lockset des_tid = - let creation_lockset = ask.f @@ Queries.MayCreationLockset des_tid in - man.sideg des_tid creation_lockset + let full_creation_lockset = ask.f @@ Queries.MayCreationLockset des_tid in + let filtered_creation_lockset = + G.filter (fun (t, _l) -> t = tid) full_creation_lockset + in + man.sideg des_tid filtered_creation_lockset in TIDs.iter contribute_creation_lockset possibly_running_tids)) | _ -> () From 2158f239eef7b6161d1d9af5ff0e15f8b5aa21e0 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 4 Dec 2025 14:03:09 +0100 Subject: [PATCH 40/95] align naming style of A module with other modules --- src/analyses/creationLockset.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 0892c3223d..aa085d4718 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -148,7 +148,7 @@ module TaintedCreationLocksetSpec = struct (** ego tid * lockset * inter-threaded lockset *) include Printable.Prod3 (TID) (LIDs) (G) - let name () = "InterThreadedLockset" + let name () = "interThreadedLockset" (** checks if [itls1] has a member ([tp1], [l]) such that [itls2] has a member ([tp2], [l]) with [tp1] != [tp2] @param itls1 inter-threaded lockset of first thread [t1] From 85aad486f1f7ec07f12a49cc9faae731b66f02e9 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 4 Dec 2025 14:52:39 +0100 Subject: [PATCH 41/95] remove irrelevant test case --- .../20-lock_fork_racefree.c | 20 ------------------- 1 file changed, 20 deletions(-) delete mode 100644 tests/regression/89-races_ancestor_locksets/20-lock_fork_racefree.c diff --git a/tests/regression/89-races_ancestor_locksets/20-lock_fork_racefree.c b/tests/regression/89-races_ancestor_locksets/20-lock_fork_racefree.c deleted file mode 100644 index 82a92f41cc..0000000000 --- a/tests/regression/89-races_ancestor_locksets/20-lock_fork_racefree.c +++ /dev/null @@ -1,20 +0,0 @@ -#include - -int global = 0; -pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; -pthread_t id1; - -void *t_fun(void *arg) { - pthread_mutex_lock(&mutex); // must happen after unlock in main - pthread_mutex_unlock(&mutex); - global++; // NORACE - return NULL; -} - -int main(void) { - pthread_mutex_lock(&mutex); - pthread_create(&id1, NULL, t_fun, NULL); - global++; // NORACE - pthread_mutex_unlock(&mutex); - return 0; -} From 4b9c2c7b2f0cd3c5e91f3417133fbdaf038cb932 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 4 Dec 2025 14:57:12 +0100 Subject: [PATCH 42/95] add new modules to goblint_lib --- src/goblint_lib.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index d69eb8101e..fabc344ab8 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -120,6 +120,7 @@ module ThreadAnalysis = ThreadAnalysis module ThreadJoins = ThreadJoins module MHPAnalysis = MHPAnalysis module ThreadReturn = ThreadReturn +module TransitiveDescendants = TransitiveDescendants (** {3 Other} *) @@ -131,6 +132,7 @@ module PthreadSignals = PthreadSignals module PthreadBarriers = PthreadBarriers module ExtractPthread = ExtractPthread module PthreadOnce = PthreadOnce +module CreationLockset = CreationLockset (** {2 Longjmp} From 2b62168d0f96ba54111242179e5cbc443c71ce5f Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 4 Dec 2025 15:33:07 +0100 Subject: [PATCH 43/95] add params to tests --- .../00-lockset_inter_threaded_lock_racefree.c} | 1 + .../01-both_inter_threaded_lock_racefree.c} | 1 + .../10-lockset_inter_threaded_lock_transitive_racefree.c | 1 + .../11-both_inter_threaded_lockset_transitive_racefree.c | 1 + 4 files changed, 4 insertions(+) rename tests/regression/{89-races_ancestor_locksets/01-lockset_inter_threaded_lock_racefree.c => 90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c} (75%) rename tests/regression/{89-races_ancestor_locksets/02-both_inter_threaded_lock_racefree.c => 90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c} (82%) rename tests/regression/{89-races_ancestor_locksets => 90-races_ancestor_locksets}/10-lockset_inter_threaded_lock_transitive_racefree.c (78%) rename tests/regression/{89-races_ancestor_locksets => 90-races_ancestor_locksets}/11-both_inter_threaded_lockset_transitive_racefree.c (87%) diff --git a/tests/regression/89-races_ancestor_locksets/01-lockset_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c similarity index 75% rename from tests/regression/89-races_ancestor_locksets/01-lockset_inter_threaded_lock_racefree.c rename to tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c index 3802d10219..ff36af007b 100644 --- a/tests/regression/89-races_ancestor_locksets/01-lockset_inter_threaded_lock_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/89-races_ancestor_locksets/02-both_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c similarity index 82% rename from tests/regression/89-races_ancestor_locksets/02-both_inter_threaded_lock_racefree.c rename to tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c index 05d960f4da..c161bf8c58 100644 --- a/tests/regression/89-races_ancestor_locksets/02-both_inter_threaded_lock_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/89-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c similarity index 78% rename from tests/regression/89-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c rename to tests/regression/90-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c index 2260355812..ecee96163a 100644 --- a/tests/regression/89-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/89-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c similarity index 87% rename from tests/regression/89-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c rename to tests/regression/90-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c index fde7d93daf..78474057ab 100644 --- a/tests/regression/89-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; From dbf73f10374987c11e73b75ceffab150d442200f Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 5 Dec 2025 11:05:52 +0100 Subject: [PATCH 44/95] remove comment/question concerning contexts --- src/analyses/creationLockset.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index aa085d4718..aa4b6d7af1 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -9,7 +9,7 @@ module LIDs = LockDomain.MustLockset (** common base for [CreationLocksetSpec] and [TaintedCreationLocksetSpec] *) module AncestorLocksetSpec = struct - include IdentityUnitContextsSpec (* no context necessary(?) *) + include IdentityUnitContextsSpec module D = Lattice.Unit module V = struct From e1299eabe7bdc62918dc7e6fcc535134d9ad8b92 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 5 Dec 2025 11:10:09 +0100 Subject: [PATCH 45/95] align hash calls for threads in queries with other hash calls --- src/domains/queries.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index bd5b64be8e..3cf2d9f9af 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -481,8 +481,8 @@ struct | Any (MaySignedOverflow e) -> CilType.Exp.hash e | Any (GasExhausted f) -> CilType.Fundec.hash f | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v - | Any (DescendantThreads t) -> ThreadIdDomain.hash_thread t (* TODO is this fine? *) - | Any (MayCreationLockset t) -> ThreadIdDomain.hash_thread t + | Any (DescendantThreads t) -> ThreadIdDomain.Thread.hash t + | Any (MayCreationLockset t) -> ThreadIdDomain.Thread.hash t (* IterSysVars: *) (* - argument is a function and functions cannot be compared in any meaningful way. *) (* - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *) From 87dde0543230507166bcd47ac1514a0d1090f022 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 5 Dec 2025 11:22:07 +0100 Subject: [PATCH 46/95] move address to must lock conversion from mutex ghosts/creation lockset analyses to must lock domain --- src/analyses/creationLockset.ml | 9 +-------- src/analyses/mutexGhosts.ml | 15 +++++---------- src/cdomains/lockDomain.ml | 5 +++++ 3 files changed, 11 insertions(+), 18 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index aa4b6d7af1..4c453a43c1 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -109,13 +109,6 @@ module TaintedCreationLocksetSpec = struct TIDs.diff may_transitively_created_tids must_joined_tids ;; - (** stolen from mutexGhost.ml. TODO Maybe add to utils? *) - let mustlock_of_addr (addr : LockDomain.Addr.t) : LID.t option = - match addr with - | Addr mv when LockDomain.Mval.is_definite mv -> Some (LID.of_mval mv) - | _ -> None - ;; - let event man e _ = match e with | Events.Unlock addr -> @@ -125,7 +118,7 @@ module TaintedCreationLocksetSpec = struct | `Top | `Bot -> () | `Lifted tid -> let possibly_running_tids = get_possibly_running_tids ask in - let lock_opt = mustlock_of_addr addr in + let lock_opt = LockDomain.MustLock.of_addr addr in (match lock_opt with | Some lock -> (* contribute for all possibly_running_tids: (tid, lock) *) diff --git a/src/analyses/mutexGhosts.ml b/src/analyses/mutexGhosts.ml index 98fd33d621..0007a6221b 100644 --- a/src/analyses/mutexGhosts.ml +++ b/src/analyses/mutexGhosts.ml @@ -61,11 +61,6 @@ struct let create_update = create_threadcreate end - let mustlock_of_addr (addr: LockDomain.Addr.t): LockDomain.MustLock.t option = - match addr with - | Addr mv when LockDomain.Mval.is_definite mv -> Some (LockDomain.MustLock.of_mval mv) - | _ -> None - let event man e oman = let verifier_atomic_addr = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var in begin match e with @@ -78,7 +73,7 @@ struct Locked.iter (fun lock -> Option.iter (fun lock -> man.sideg (V.lock lock) (G.create_lock true) - ) (mustlock_of_addr lock) + ) (LockDomain.MustLock.of_addr lock) ) locked ); ) @@ -91,7 +86,7 @@ struct Locked.iter (fun lock -> Option.iter (fun lock -> man.sideg (V.lock lock) (G.create_lock true) - ) (mustlock_of_addr lock) + ) (LockDomain.MustLock.of_addr lock) ) unlocked ); ) @@ -128,7 +123,7 @@ struct let (locked, unlocked, multithread) = G.node (man.global (V.node node)) in let variables' = Locked.fold (fun l acc -> - match mustlock_of_addr l with + match LockDomain.MustLock.of_addr l with | Some l when ghost_var_available man (Locked l) -> let variable = WitnessGhost.variable' (Locked l) in VariableSet.add variable acc @@ -138,7 +133,7 @@ struct in let updates = Locked.fold (fun l acc -> - match mustlock_of_addr l with + match LockDomain.MustLock.of_addr l with | Some l when ghost_var_available man (Locked l) -> let update = WitnessGhost.update' (Locked l) GoblintCil.one in update :: acc @@ -148,7 +143,7 @@ struct in let updates = Unlocked.fold (fun l acc -> - match mustlock_of_addr l with + match LockDomain.MustLock.of_addr l with | Some l when ghost_var_available man (Locked l) -> let update = WitnessGhost.update' (Locked l) GoblintCil.zero in update :: acc diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index e7295f0b56..84978bb125 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -29,6 +29,11 @@ struct let of_mval ((v, o): Mval.t): t = (v, Offset.Poly.map_indices (fun i -> IndexDomain.to_int i |> Option.get) o) + let of_addr (addr : Addr.t) : t option = + match addr with + | Addr mv when Mval.is_definite mv -> Some (of_mval mv) + | _ -> None + let to_mval ((v, o): t): Mval.t = (v, Offset.Poly.map_indices (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) o) end From b8416efeeffa72a5312b789652cbff17168dc28a Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 5 Dec 2025 11:30:26 +0100 Subject: [PATCH 47/95] should_print in A module --- src/analyses/creationLockset.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 4c453a43c1..4cb1d7a4de 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -172,7 +172,7 @@ module TaintedCreationLocksetSpec = struct || one_protected_inter_threaded_other_intra_threaded itls2 t1 ls1) ;; - let should_print _ = true + let should_print (_t, _ls, itls) = not @@ G.is_empty itls end let access man _ = From 13443f99e6f64da28def8331a5a0e4779d52bc00 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 5 Dec 2025 11:49:13 +0100 Subject: [PATCH 48/95] impose conditions on config before running creation lockset analyses --- src/maingoblint.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 7d3bf782c5..10891adb23 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -167,7 +167,9 @@ let check_arguments () = if get_bool "dbg.print_wpoints" && not (Logs.Level.should_log Debug) then warn "dbg.print_wpoints requires dbg.level debug"; if get_bool "dbg.print_tids" && not (Logs.Level.should_log Debug) then - warn "dbg.print_tids requires dbg.level debug" + warn "dbg.print_tids requires dbg.level debug"; + if List.mem "creationLockset" @@ get_string_list "ana.activated" && not (get_string "ana.thread.domain" = "history" && get_bool "ana.thread.include-node" && get_bool "ana.thread.context.create-edges") then + fail "creation lockset analysis requires ana.thread.domain to be set to \"history\" and both ana.thread.include-node and ana.thread.context.create-edges to be enabled"; (** Initialize some globals in other modules. *) let handle_flags () = From f1efd326c95b6157a8b15edbfec0b062ba55797f Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 5 Dec 2025 12:52:52 +0100 Subject: [PATCH 49/95] remove bad semicolon --- src/maingoblint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 10891adb23..ba2f6440f2 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -169,7 +169,7 @@ let check_arguments () = if get_bool "dbg.print_tids" && not (Logs.Level.should_log Debug) then warn "dbg.print_tids requires dbg.level debug"; if List.mem "creationLockset" @@ get_string_list "ana.activated" && not (get_string "ana.thread.domain" = "history" && get_bool "ana.thread.include-node" && get_bool "ana.thread.context.create-edges") then - fail "creation lockset analysis requires ana.thread.domain to be set to \"history\" and both ana.thread.include-node and ana.thread.context.create-edges to be enabled"; + fail "creation lockset analysis requires ana.thread.domain to be set to \"history\" and both ana.thread.include-node and ana.thread.context.create-edges to be enabled" (** Initialize some globals in other modules. *) let handle_flags () = From 6ec28cab130f3d9036a4c48a41b11ef7225f127f Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 8 Dec 2025 12:40:48 +0100 Subject: [PATCH 50/95] ambiguous thread creation test cases --- .../20-multiple_create_statements_racing.c | 29 ++++++++++++++ .../21-diamond_racing.c | 39 +++++++++++++++++++ .../22-circle_racing.c | 39 +++++++++++++++++++ 3 files changed, 107 insertions(+) create mode 100644 tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/21-diamond_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/22-circle_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c b/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c new file mode 100644 index 0000000000..e08873b37d --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c @@ -0,0 +1,29 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since it is created/joined twice. The lock is released before the second join happens + global++; // RACE + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_join(id2, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_unlock(&mutex); + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c b/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c new file mode 100644 index 0000000000..729dadd5ab --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c @@ -0,0 +1,39 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2, id3, id4_1, id4_2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void* t4(void* arg) { // t4 is not protected by mutex, since it is created twice and the creation in t2 does not happen with mutex locked + global++; // RACE + return NULL; +} + +void* t3(void* arg) { + pthread_mutex_lock(&mutex); + pthread_create(&id4_2, NULL, t4, NULL); + pthread_join(id4_2, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { + pthread_create(&id4_1, NULL, t4, NULL); + pthread_join(id4_1, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_create(&id3, NULL, t3, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/22-circle_racing.c b/tests/regression/90-races_ancestor_locksets/22-circle_racing.c new file mode 100644 index 0000000000..dea6ba57aa --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/22-circle_racing.c @@ -0,0 +1,39 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +#include + +// This program does not make any sense in practice (it produces a deadlock and if it did not, it wouldn't halt) +// We solely want to assert that the accesses to global race + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, idc1; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void* tc1(void* arg); + +void *tc2(void *arg) { + pthread_t idc1; + pthread_mutex_lock(&mutex); + pthread_create(&idc1, NULL, tc1, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *tc1(void *arg) { // tc1 is protected by tc2, but not by the main thread. + global++; // RACE + pthread_t idc2; + pthread_create(&idc2, NULL, tc2, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&idc1, NULL, tc1, NULL); + return 0; +} \ No newline at end of file From 1879e7e793dec3e08003c5512c126a9c03691e4e Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 8 Dec 2025 21:04:30 +0100 Subject: [PATCH 51/95] more racefree test cases --- ...inter_threaded_lock_transitive_racefree.c} | 0 ...er_threaded_lockset_transitive_racefree.c} | 0 .../04-never_unlock_never_join_racefree.c | 25 +++++++++++++++++ .../05-maybe_create_racefree.c | 28 +++++++++++++++++++ 4 files changed, 53 insertions(+) rename tests/regression/90-races_ancestor_locksets/{10-lockset_inter_threaded_lock_transitive_racefree.c => 02-lockset_inter_threaded_lock_transitive_racefree.c} (100%) rename tests/regression/90-races_ancestor_locksets/{11-both_inter_threaded_lockset_transitive_racefree.c => 03-both_inter_threaded_lockset_transitive_racefree.c} (100%) create mode 100644 tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c create mode 100644 tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c diff --git a/tests/regression/90-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/10-lockset_inter_threaded_lock_transitive_racefree.c rename to tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c diff --git a/tests/regression/90-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/03-both_inter_threaded_lockset_transitive_racefree.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/11-both_inter_threaded_lockset_transitive_racefree.c rename to tests/regression/90-races_ancestor_locksets/03-both_inter_threaded_lockset_transitive_racefree.c diff --git a/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c b/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c new file mode 100644 index 0000000000..9c524b4873 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c @@ -0,0 +1,25 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + global++; // NORACE + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c b/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c new file mode 100644 index 0000000000..55e0569189 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + global++; // NORACE + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + int maybe; + if (maybe) { + pthread_create(&id2, NULL, t2, NULL); + } + return 0; +} \ No newline at end of file From 5b97ec49c4d58b6078ccbba37be31f2259faf4e6 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 8 Dec 2025 21:05:11 +0100 Subject: [PATCH 52/95] more racing test cases --- .../10-maybe_lock_racing.c | 29 ++++++++++++++++ .../11-maybe_unlock_racing.c | 31 +++++++++++++++++ .../12-random_mutex_unlock_racing.c | 34 +++++++++++++++++++ .../13-unknown_mutex_unlock_racing.c | 28 +++++++++++++++ .../14-maybe_join_racing.c | 30 ++++++++++++++++ ...ead_one_lockset_one_interthreaded_racing.c | 22 ++++++++++++ ...om_same_thread_both_interthreaded_racing.c | 23 +++++++++++++ 7 files changed, 197 insertions(+) create mode 100644 tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c b/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c new file mode 100644 index 0000000000..ee7e0e0f1a --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c @@ -0,0 +1,29 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// TODO broken, since locksets have more granular path sensitivity than creation locksets +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since the mutex does not have to be locked during creation + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + int maybe; + if (maybe) { + pthread_mutex_lock(&mutex); + } + pthread_create(&id2, NULL, t2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c new file mode 100644 index 0000000000..bc09c8df65 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c @@ -0,0 +1,31 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// TODO broken, since locksets have more granular path sensitivity than creation locksets +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock may happen before joining + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + int maybe; + if (maybe) { + pthread_mutex_unlock(&mutex); + } + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c new file mode 100644 index 0000000000..c7e0bf3d72 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c @@ -0,0 +1,34 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// TODO broken, since locksets have more granular path sensitivity than creation locksets +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER, mutex_alt = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock may happen before joining + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_lock(&mutex_alt); + pthread_mutex_t *mutex_ref = &mutex_alt; + int maybe; + if (maybe) { + mutex_ref = &mutex; + } + pthread_mutex_unlock(mutex_ref); + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c new file mode 100644 index 0000000000..325ff4d05a --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock could happen before joining + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_t *mutex_ref; + pthread_mutex_unlock(mutex_ref); // unlock of unknown mutex + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c b/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c new file mode 100644 index 0000000000..4050f74640 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c @@ -0,0 +1,30 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, joining may happen before unlocking + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + int maybe; + if (maybe) { + pthread_join(id2, NULL); + } + pthread_mutex_unlock(&mutex); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c b/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c new file mode 100644 index 0000000000..6e1f246d3c --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c @@ -0,0 +1,22 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1; + +// both accesses are protected by same mutex **locked in same thread** + +void *t1(void *arg) { + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_mutex_lock(&mutex); + pthread_create(&id1, NULL, t1, NULL); + global++; // RACE! + pthread_join(id1, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c b/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c new file mode 100644 index 0000000000..622bf8aa07 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c @@ -0,0 +1,23 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +// both accesses are protected by same mutex **locked in same thread** + +void *tc(void *arg) { + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_mutex_lock(&mutex); + pthread_create(&id1, NULL, tc, NULL); + pthread_create(&id2, NULL, tc, NULL); + pthread_join(id1, NULL); + pthread_join(id2, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} From fc22ec0387091b1fee09f03e6587387e494b5c60 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 8 Dec 2025 21:06:16 +0100 Subject: [PATCH 53/95] use "RACE!" instead of "RACE" --- .../20-multiple_create_statements_racing.c | 4 ++-- .../regression/90-races_ancestor_locksets/21-diamond_racing.c | 4 ++-- .../regression/90-races_ancestor_locksets/22-circle_racing.c | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c b/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c index e08873b37d..b97c6b17f6 100644 --- a/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c +++ b/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c @@ -7,13 +7,13 @@ pthread_t id1, id2; void *t1(void *arg) { pthread_mutex_lock(&mutex); - global++; // RACE + global++; // RACE! pthread_mutex_unlock(&mutex); return NULL; } void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since it is created/joined twice. The lock is released before the second join happens - global++; // RACE + global++; // RACE! return NULL; } diff --git a/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c b/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c index 729dadd5ab..c867d795e4 100644 --- a/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c +++ b/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c @@ -7,13 +7,13 @@ pthread_t id1, id2, id3, id4_1, id4_2; void *t1(void *arg) { pthread_mutex_lock(&mutex); - global++; // RACE + global++; // RACE! pthread_mutex_unlock(&mutex); return NULL; } void* t4(void* arg) { // t4 is not protected by mutex, since it is created twice and the creation in t2 does not happen with mutex locked - global++; // RACE + global++; // RACE! return NULL; } diff --git a/tests/regression/90-races_ancestor_locksets/22-circle_racing.c b/tests/regression/90-races_ancestor_locksets/22-circle_racing.c index dea6ba57aa..95da00e969 100644 --- a/tests/regression/90-races_ancestor_locksets/22-circle_racing.c +++ b/tests/regression/90-races_ancestor_locksets/22-circle_racing.c @@ -10,7 +10,7 @@ pthread_t id1, idc1; void *t1(void *arg) { pthread_mutex_lock(&mutex); - global++; // RACE + global++; // RACE! pthread_mutex_unlock(&mutex); return NULL; } @@ -26,7 +26,7 @@ void *tc2(void *arg) { } void *tc1(void *arg) { // tc1 is protected by tc2, but not by the main thread. - global++; // RACE + global++; // RACE! pthread_t idc2; pthread_create(&idc2, NULL, tc2, NULL); return NULL; From 695081c8299f3d87b03eb5051597befdac649713 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 00:27:31 +0100 Subject: [PATCH 54/95] remove unused LibraryFunctions import --- src/analyses/creationLockset.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 4cb1d7a4de..22a616879a 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -1,7 +1,6 @@ (** Ancestor-lock analysis. See https://github.com/goblint/analyzer/pull/1865 *) open Analyses -module LF = LibraryFunctions module TID = ThreadIdDomain.Thread module TIDs = ConcDomain.ThreadSet module LID = LockDomain.MustLock @@ -121,12 +120,15 @@ module TaintedCreationLocksetSpec = struct let lock_opt = LockDomain.MustLock.of_addr addr in (match lock_opt with | Some lock -> + let _ = M.tracel "lol" "%a" LID.pretty lock in (* contribute for all possibly_running_tids: (tid, lock) *) let to_contribute = G.singleton (tid, lock) in TIDs.iter (contribute_lock man to_contribute) possibly_running_tids | None -> + let _ = M.tracel "lol" "idk" in (* any lock could have been unlocked. Contribute for all possibly_running_tids all members of their CreationLocksets with the ego thread to invalidate them!! *) let contribute_creation_lockset des_tid = + let _ = M.tracel "lol" "des tid %a" TID.pretty des_tid in let full_creation_lockset = ask.f @@ Queries.MayCreationLockset des_tid in let filtered_creation_lockset = G.filter (fun (t, _l) -> t = tid) full_creation_lockset From 5bf35caae0996d42cd187593f1b32f0b7b4f3633 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 00:31:03 +0100 Subject: [PATCH 55/95] add query parameters to result of pretty function --- src/domains/queries.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 3cf2d9f9af..025d005701 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -551,8 +551,8 @@ struct | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" - | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads" - | Any (MayCreationLockset t) -> Pretty.dprintf "MayCreationLockset" + | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads %a" ThreadIdDomain.Thread.pretty t + | Any (MayCreationLockset t) -> Pretty.dprintf "MayCreationLockset %a" ThreadIdDomain.Thread.pretty t end let to_value_domain_ask (ask: ask) = From 8d5928e993e320de26669487b9780b45ec3cdf88 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 00:33:54 +0100 Subject: [PATCH 56/95] add missing `return NULL;` --- .../02-lockset_inter_threaded_lock_transitive_racefree.c | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c index ecee96163a..e9e3c3b699 100644 --- a/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c @@ -14,6 +14,7 @@ void *t1(void *arg) { void* t3(void* arg) { global++; // NORACE + return NULL; } void *t2(void *arg) { // t2 is protected by mutex locked in main thread From 873ff0c7692cc1f23fb84efd02e4bf189c7e4208 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 00:37:13 +0100 Subject: [PATCH 57/95] remove redundant `;;` --- src/analyses/raceAnalysis.ml | 8 ++++---- src/analyses/transitiveDescendants.ml | 2 -- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index f9aed59f2c..2d0193d748 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -16,9 +16,9 @@ open Analyses Race checking is performed per-memo, except must additionally account for accesses to other memos (see diagram below): + access to [s.f] can race with access to a prefix like [s], which writes an entire struct at once; - + access to [s.f] can race with type-based access like [(struct S).f]; - + access to [(struct S).f] can race with type-based access to a suffix like [(int)]. - + access to [(struct T).s.f] can race with type-based access like [(struct S)], which is a combination of the above. + + access to [s.f] can race with type-based access like [(st ruct S).f]; + + access to [(st ruct S).f] can race with type-based access to a suffix like [(int)]. + + access to [(str uct T).s.f] can race with type-based access like [(str uct S)], which is a combination of the above. These are accounted for lazily (unlike in the past). @@ -66,7 +66,7 @@ open Analyses v} where: - [(int)] is a type-based memo root for the primitive [int] type; - - [(S)] and [(T)] are short for [(struct S)] and [(struct T)], which are type-based memo roots; + - [(S)] and [(T)] are short for [(stru ct S)] and [(stru ct T)], which are type-based memo roots; - prefix relations are indicated by [/], so access paths run diagonally from top-right to bottom-left; - type suffix relations are indicated by [\ ]. diff --git a/src/analyses/transitiveDescendants.ml b/src/analyses/transitiveDescendants.ml index 378ee875e6..87362ccf01 100644 --- a/src/analyses/transitiveDescendants.ml +++ b/src/analyses/transitiveDescendants.ml @@ -21,7 +21,6 @@ module TransitiveDescendants = struct match x with | Queries.DescendantThreads t -> (man.global t : G.t) | _ -> Queries.Result.top x - ;; let threadspawn man ~multiple lval f args fman = let ask = Analyses.ask_of_man man in @@ -39,7 +38,6 @@ module TransitiveDescendants = struct (* transitive closure *) let child_descendants = man.global child_tid in man.sideg tid child_descendants) - ;; end let _ = MCP.register_analysis ~dep:[ "threadid" ] (module TransitiveDescendants : MCPSpec) From b495fa98aa74c4dc79936c0698139f93621dcc5e Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 00:46:15 +0100 Subject: [PATCH 58/95] undo accidental changes to `raceAnalysis.ml` --- src/analyses/raceAnalysis.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 2d0193d748..f9aed59f2c 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -16,9 +16,9 @@ open Analyses Race checking is performed per-memo, except must additionally account for accesses to other memos (see diagram below): + access to [s.f] can race with access to a prefix like [s], which writes an entire struct at once; - + access to [s.f] can race with type-based access like [(st ruct S).f]; - + access to [(st ruct S).f] can race with type-based access to a suffix like [(int)]. - + access to [(str uct T).s.f] can race with type-based access like [(str uct S)], which is a combination of the above. + + access to [s.f] can race with type-based access like [(struct S).f]; + + access to [(struct S).f] can race with type-based access to a suffix like [(int)]. + + access to [(struct T).s.f] can race with type-based access like [(struct S)], which is a combination of the above. These are accounted for lazily (unlike in the past). @@ -66,7 +66,7 @@ open Analyses v} where: - [(int)] is a type-based memo root for the primitive [int] type; - - [(S)] and [(T)] are short for [(stru ct S)] and [(stru ct T)], which are type-based memo roots; + - [(S)] and [(T)] are short for [(struct S)] and [(struct T)], which are type-based memo roots; - prefix relations are indicated by [/], so access paths run diagonally from top-right to bottom-left; - type suffix relations are indicated by [\ ]. From 3c45dff510193de6e9e0d00c6cfe3a1df83ee9a3 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 00:47:12 +0100 Subject: [PATCH 59/95] remove redundant `;;` in `creationLockset.ml` --- src/analyses/creationLockset.ml | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 22a616879a..825afc8727 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -32,7 +32,6 @@ module AncestorLocksetSpec = struct (** compute [tids] \times \{[lock]\} *) let singleton_cartesian_prod tids lock = TIDs.fold (fun tid acc -> G.add (tid, lock) acc) tids (G.empty ()) - ;; (** compute the cartesian product [tids] \times [locks] *) let cartesian_prod tids locks = @@ -42,7 +41,6 @@ module AncestorLocksetSpec = struct G.union tids_times_lock acc) locks (G.empty ()) - ;; (** reflexive-transitive closure of child relation applied to [tid] @param ask any ask @@ -52,7 +50,6 @@ module AncestorLocksetSpec = struct let descendants_closure (ask : Queries.ask) tid = let transitive_descendants = ask.f @@ Queries.DescendantThreads tid in TIDs.add tid transitive_descendants - ;; end (** collects for each thread t_n pairs of ancestors and locks (t_0,l): @@ -76,13 +73,11 @@ module CreationLocksetSpec = struct let to_contribute = cartesian_prod (TIDs.singleton tid) lockset in TIDs.iter (contribute_lock man to_contribute) descendants | _ -> (* TODO deal with top or bottom? *) () - ;; let query man (type a) (x : a Queries.t) : a Queries.result = match x with | Queries.MayCreationLockset tid -> (man.global tid : G.t) | _ -> Queries.Result.top x - ;; end (** collects for each thread t_n pairs of ancestors and locks (t_0,l): @@ -106,7 +101,6 @@ module TaintedCreationLocksetSpec = struct in let must_joined_tids = ask.f Queries.MustJoinedThreads in TIDs.diff may_transitively_created_tids must_joined_tids - ;; let event man e _ = match e with @@ -137,7 +131,6 @@ module TaintedCreationLocksetSpec = struct in TIDs.iter contribute_creation_lockset possibly_running_tids)) | _ -> () - ;; module A = struct (** ego tid * lockset * inter-threaded lockset *) @@ -155,7 +148,6 @@ module TaintedCreationLocksetSpec = struct G.exists (fun (tp2, l2) -> LID.equal l1 l2 && (not @@ TID.equal tp1 tp2)) itls2 in G.exists itls2_has_same_lock_other_tid itls1 - ;; (** checks if [itls1] has a member ([tp1], [l1]) such that [l1] is in [ls2] and [tp1] != [t2] @param itls1 inter-threaded lockset of thread [t1] at first program point @@ -165,14 +157,12 @@ module TaintedCreationLocksetSpec = struct *) let one_protected_inter_threaded_other_intra_threaded itls1 t2 ls2 = G.exists (fun (tp1, l1) -> LIDs.mem l1 ls2 && (not @@ TID.equal tp1 t2)) itls1 - ;; let may_race (t1, ls1, itls1) (t2, ls2, itls2) = not (both_protected_inter_threaded itls1 itls2 || one_protected_inter_threaded_other_intra_threaded itls1 t2 ls2 || one_protected_inter_threaded_other_intra_threaded itls2 t1 ls1) - ;; let should_print (_t, _ls, itls) = not @@ G.is_empty itls end @@ -189,14 +179,12 @@ module TaintedCreationLocksetSpec = struct let inter_threaded_lockset = G.diff creation_lockset tainted_creation_lockset in tid, lockset, inter_threaded_lockset | _ -> ThreadIdDomain.UnknownThread, LIDs.empty (), G.empty () - ;; end let _ = MCP.register_analysis ~dep:[ "threadid"; "mutex"; "race"; "transitiveDescendants" ] (module CreationLocksetSpec : MCPSpec) -;; let _ = MCP.register_analysis @@ -209,4 +197,3 @@ let _ = ; "creationLockset" ] (module TaintedCreationLocksetSpec : MCPSpec) -;; From 6c2c849eca494b3b0d3a1d818693794846169de7 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 00:47:50 +0100 Subject: [PATCH 60/95] remove debug statements accidentally committed --- src/analyses/creationLockset.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 825afc8727..1eb15a3b8d 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -114,15 +114,12 @@ module TaintedCreationLocksetSpec = struct let lock_opt = LockDomain.MustLock.of_addr addr in (match lock_opt with | Some lock -> - let _ = M.tracel "lol" "%a" LID.pretty lock in (* contribute for all possibly_running_tids: (tid, lock) *) let to_contribute = G.singleton (tid, lock) in TIDs.iter (contribute_lock man to_contribute) possibly_running_tids | None -> - let _ = M.tracel "lol" "idk" in (* any lock could have been unlocked. Contribute for all possibly_running_tids all members of their CreationLocksets with the ego thread to invalidate them!! *) let contribute_creation_lockset des_tid = - let _ = M.tracel "lol" "des tid %a" TID.pretty des_tid in let full_creation_lockset = ask.f @@ Queries.MayCreationLockset des_tid in let filtered_creation_lockset = G.filter (fun (t, _l) -> t = tid) full_creation_lockset From 1db14cb7b21e2d3817ff57de032b75354e53e004 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 11:27:01 +0100 Subject: [PATCH 61/95] add ambiguous context regression test --- .../17-ambiguous_context_racing.c | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c b/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c new file mode 100644 index 0000000000..ba5b204b28 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c @@ -0,0 +1,38 @@ +// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +// both accesses are protected by same mutex **locked in same thread** + +void* t1(void* arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { + global++; // RACE! + return NULL; +} + +void evil(int x) { + if (x) { + pthread_mutex_lock(&mutex); + } + pthread_create(&id2, NULL, t2, NULL); +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + int maybe; + if (maybe) { + evil(0); + } else { + evil(1); + } + return 0; +} From 099f7427725a137556f90645df5325020e3b4149 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 23:47:42 +0100 Subject: [PATCH 62/95] change global domain for creation lockset analysis --- src/analyses/creationLockset.ml | 206 ++++++++++++++------------------ 1 file changed, 91 insertions(+), 115 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 1eb15a3b8d..e1f23665fc 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -1,4 +1,4 @@ -(** Ancestor-lock analysis. See https://github.com/goblint/analyzer/pull/1865 *) +(** creation-lockset analysis. See https://github.com/goblint/analyzer/pull/1865 *) open Analyses module TID = ThreadIdDomain.Thread @@ -6,8 +6,10 @@ module TIDs = ConcDomain.ThreadSet module LID = LockDomain.MustLock module LIDs = LockDomain.MustLockset -(** common base for [CreationLocksetSpec] and [TaintedCreationLocksetSpec] *) -module AncestorLocksetSpec = struct +(** constructs edges on the graph over all threads, where the edges are labelled with must-locksets: + t_1 --ls-> t_0 means that t_1 is protected by all members of ls from t_0 +*) +module Spec = struct include IdentityUnitContextsSpec module D = Lattice.Unit @@ -16,181 +18,155 @@ module AncestorLocksetSpec = struct include StdV end - (** 2 ^ { [TID] \times [LID] } *) + (** [TID] -> [LIDs] *) module G = Queries.ALS + let name () = "creationLockset" let startstate _ = D.bot () let exitstate _ = D.bot () - (** register a contribution to a global: global.[child_tid] \supseteq [to_contribute] + (** register a global contribution: global.[child_tid] \supseteq [to_contribute] @param man man at program point - @param to_contribute new edges from [child_tid] to register + @param to_contribute new edges from [child_tid] to ego thread to register @param child_tid *) - let contribute_lock man to_contribute child_tid = man.sideg child_tid to_contribute - - (** compute [tids] \times \{[lock]\} *) - let singleton_cartesian_prod tids lock = - TIDs.fold (fun tid acc -> G.add (tid, lock) acc) tids (G.empty ()) - - (** compute the cartesian product [tids] \times [locks] *) - let cartesian_prod tids locks = - LIDs.fold - (fun lock acc -> - let tids_times_lock = singleton_cartesian_prod tids lock in - G.union tids_times_lock acc) - locks - (G.empty ()) + let contribute_locks man to_contribute child_tid = man.sideg child_tid to_contribute (** reflexive-transitive closure of child relation applied to [tid] + and filtered to only include threads, where [tid] is a must-ancestor @param ask any ask @param tid @returns [{ tid }] \cup DES([tid]) *) - let descendants_closure (ask : Queries.ask) tid = - let transitive_descendants = ask.f @@ Queries.DescendantThreads tid in - TIDs.add tid transitive_descendants -end - -(** collects for each thread t_n pairs of ancestors and locks (t_0,l): - when t_n or an ancestor t_1 of t_n was created, the creating thread t_0 must have held l. -*) -module CreationLocksetSpec = struct - include AncestorLocksetSpec + let unique_descendants_closure (ask : Queries.ask) tid = + let descendants = ask.f @@ Queries.DescendantThreads tid in + let unique_descendants = TIDs.filter (TID.must_be_ancestor tid) descendants in + TIDs.add tid unique_descendants + ;; - let name () = "creationLockset" - - (** create(t_1) in t_0 with lockset L *) let threadspawn man ~multiple lval f args fman = - let ask = Analyses.ask_of_man man in + let ask = ask_of_man man in let tid_lifted = ask.f Queries.CurrentThreadId in - let child_ask = Analyses.ask_of_man fman in + let child_ask = ask_of_man fman in let child_tid_lifted = child_ask.f Queries.CurrentThreadId in match tid_lifted, child_tid_lifted with - | `Lifted tid, `Lifted child_tid -> - let descendants = descendants_closure child_ask child_tid in + | `Lifted tid, `Lifted child_tid when TID.must_be_ancestor tid child_tid -> + let unique_descendants = unique_descendants_closure child_ask child_tid in let lockset = ask.f Queries.MustLockset in - let to_contribute = cartesian_prod (TIDs.singleton tid) lockset in - TIDs.iter (contribute_lock man to_contribute) descendants - | _ -> (* TODO deal with top or bottom? *) () - - let query man (type a) (x : a Queries.t) : a Queries.result = - match x with - | Queries.MayCreationLockset tid -> (man.global tid : G.t) - | _ -> Queries.Result.top x -end - -(** collects for each thread t_n pairs of ancestors and locks (t_0,l): - l may be unlocked in t_0 while t_n could be running. -*) -module TaintedCreationLocksetSpec = struct - include AncestorLocksetSpec - - let name () = "taintedCreationLockset" + let to_contribute = G.singleton tid lockset in + TIDs.iter (contribute_locks man to_contribute) unique_descendants + | _ -> () + ;; - (** compute all threads that may run along with the ego thread at a program point + (** compute all descendant threads that may run along with the ego thread at a program point @param ask ask of ego thread at the program point *) let get_possibly_running_tids (ask : Queries.ask) = let may_created_tids = ask.f Queries.CreatedThreads in let may_transitively_created_tids = TIDs.fold - (fun child_tid acc -> TIDs.union acc (descendants_closure ask child_tid)) + (fun child_tid acc -> TIDs.union acc (unique_descendants_closure ask child_tid)) may_created_tids (TIDs.empty ()) in let must_joined_tids = ask.f Queries.MustJoinedThreads in TIDs.diff may_transitively_created_tids must_joined_tids + ;; + + (** handle unlock of mutex [lock] *) + let unlock man tid possibly_running_tids lock = + let shrink_locksets des_tid = + let old_creation_lockset = G.find tid (man.global des_tid) in + let updated_creation_lockset = LIDs.remove lock old_creation_lockset in + let to_contribute = G.singleton tid updated_creation_lockset in + man.sideg des_tid to_contribute + in + TIDs.iter shrink_locksets possibly_running_tids + ;; + + (** handle unlock of an unknown mutex. Assumes that any mutex could have been unlocked *) + let unknown_unlock man tid possibly_running_tids = + let evaporate_locksets des_tid = + let to_contribute = G.singleton tid (LIDs.empty ()) in + man.sideg des_tid to_contribute + in + TIDs.iter evaporate_locksets possibly_running_tids + ;; let event man e _ = match e with | Events.Unlock addr -> - let ask = Analyses.ask_of_man man in + let ask = ask_of_man man in let tid_lifted = ask.f Queries.CurrentThreadId in - (match tid_lifted with - | `Top | `Bot -> () - | `Lifted tid -> - let possibly_running_tids = get_possibly_running_tids ask in - let lock_opt = LockDomain.MustLock.of_addr addr in - (match lock_opt with - | Some lock -> - (* contribute for all possibly_running_tids: (tid, lock) *) - let to_contribute = G.singleton (tid, lock) in - TIDs.iter (contribute_lock man to_contribute) possibly_running_tids - | None -> - (* any lock could have been unlocked. Contribute for all possibly_running_tids all members of their CreationLocksets with the ego thread to invalidate them!! *) - let contribute_creation_lockset des_tid = - let full_creation_lockset = ask.f @@ Queries.MayCreationLockset des_tid in - let filtered_creation_lockset = - G.filter (fun (t, _l) -> t = tid) full_creation_lockset - in - man.sideg des_tid filtered_creation_lockset - in - TIDs.iter contribute_creation_lockset possibly_running_tids)) + let lock_opt = LockDomain.MustLock.of_addr addr in + let possibly_running_tids = get_possibly_running_tids ask in + (match tid_lifted, lock_opt with + | `Lifted tid, Some lock -> unlock man tid possibly_running_tids lock + | `Lifted tid, None -> unknown_unlock man tid possibly_running_tids + | _ -> ()) | _ -> () + ;; + + let query man (type a) (x : a Queries.t) : a Queries.result = + match x with + | Queries.MayCreationLockset tid -> (man.global tid : G.t) + | _ -> Queries.Result.top x + ;; module A = struct - (** ego tid * lockset * inter-threaded lockset *) + (** ego tid * must-lockset * creation-lockset *) include Printable.Prod3 (TID) (LIDs) (G) - let name () = "interThreadedLockset" + let name () = "creationLockset" - (** checks if [itls1] has a member ([tp1], [l]) such that [itls2] has a member ([tp2], [l]) with [tp1] != [tp2] - @param itls1 inter-threaded lockset of first thread [t1] - @param itls2 inter-threaded lockset of second thread [t2] + (** checks if [itls1] has a member ([tp1] |-> [ls1]) and [itls2] has a member ([tp2] |-> [ls2]) + such that [ls1] and [ls2] are not disjoint and [tp1] != [tp2] + @param cl1 creation-lockset of first thread [t1] + @param cl2 creation-lockset of second thread [t2] @returns whether [t1] and [t2] must be running mutually exclusive *) - let both_protected_inter_threaded itls1 itls2 = - let itls2_has_same_lock_other_tid (tp1, l1) = - G.exists (fun (tp2, l2) -> LID.equal l1 l2 && (not @@ TID.equal tp1 tp2)) itls2 + let both_protected_inter_threaded cl1 cl2 = + let cl2_has_same_lock_other_tid tp1 ls1 = + G.exists (fun tp2 ls2 -> not (LIDs.disjoint ls1 ls2 || TID.equal tp1 tp2)) cl2 in - G.exists itls2_has_same_lock_other_tid itls1 + G.exists cl2_has_same_lock_other_tid cl1 + ;; - (** checks if [itls1] has a member ([tp1], [l1]) such that [l1] is in [ls2] and [tp1] != [t2] - @param itls1 inter-threaded lockset of thread [t1] at first program point + (** checks if [cl1] has a mapping ([tp1] |-> [ls1]) + such that [ls1] and [ls2] are not disjoint and [tp1] != [t2] + @param cl1 creation-lockset of thread [t1] at first program point @param t2 thread id at second program point @param ls2 lockset at second program point @returns whether [t1] must be running mutually exclusive with second program point *) - let one_protected_inter_threaded_other_intra_threaded itls1 t2 ls2 = - G.exists (fun (tp1, l1) -> LIDs.mem l1 ls2 && (not @@ TID.equal tp1 t2)) itls1 + let one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 = + G.exists (fun tp1 ls1 -> not (LIDs.disjoint ls1 ls2 || TID.equal tp1 t2)) cl1 + ;; - let may_race (t1, ls1, itls1) (t2, ls2, itls2) = + let may_race (t1, ls1, cl1) (t2, ls2, cl2) = not - (both_protected_inter_threaded itls1 itls2 - || one_protected_inter_threaded_other_intra_threaded itls1 t2 ls2 - || one_protected_inter_threaded_other_intra_threaded itls2 t1 ls1) + (both_protected_inter_threaded cl1 cl2 + || one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 + || one_protected_inter_threaded_other_intra_threaded cl2 t1 ls1) + ;; - let should_print (_t, _ls, itls) = not @@ G.is_empty itls + let should_print (_t, _ls, cl) = not @@ G.is_empty cl end let access man _ = - let ask = Analyses.ask_of_man man in + let ask = ask_of_man man in let tid_lifted = ask.f Queries.CurrentThreadId in match tid_lifted with | `Lifted tid -> let lockset = ask.f Queries.MustLockset in - let creation_lockset = ask.f @@ Queries.MayCreationLockset tid in - let tainted_creation_lockset = man.global tid in - (* all values in creation lockset, but not in tainted creation lockset *) - let inter_threaded_lockset = G.diff creation_lockset tainted_creation_lockset in - tid, lockset, inter_threaded_lockset + let creation_lockset = man.global tid in + tid, lockset, creation_lockset | _ -> ThreadIdDomain.UnknownThread, LIDs.empty (), G.empty () + ;; end let _ = MCP.register_analysis - ~dep:[ "threadid"; "mutex"; "race"; "transitiveDescendants" ] - (module CreationLocksetSpec : MCPSpec) - -let _ = - MCP.register_analysis - ~dep: - [ "threadid" - ; "mutex" - ; "threadJoins" - ; "race" - ; "transitiveDescendants" - ; "creationLockset" - ] - (module TaintedCreationLocksetSpec : MCPSpec) + ~dep:[ "threadid"; "mutex"; "race"; "threadJoins"; "transitiveDescendants" ] + (module Spec : MCPSpec) +;; From 850e1cb4241ee0010e1d5f734018c7d923c79bf9 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 23:50:50 +0100 Subject: [PATCH 63/95] remove creation lockset query --- src/domains/queries.ml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 025d005701..3ec0b07ea4 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -77,7 +77,7 @@ type invariant_context = Invariant.context = { module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end) -module ALS = SetDomain.ToppedSet (Printable.Prod (ThreadIdDomain.Thread) (LockDomain.MustLock)) (struct let topname = "all pairs of threads and locks" end) +module ALS = MapDomain.MapBot (ThreadIdDomain.Thread) (LockDomain.MustLockset) (** GADT for queries with specific result type. *) type _ t = @@ -148,7 +148,6 @@ type _ t = | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *) | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t - | MayCreationLockset: ThreadIdDomain.Thread.t -> ALS.t t type 'a result = 'a @@ -225,7 +224,6 @@ struct | GhostVarAvailable _ -> (module MayBool) | InvariantGlobalNodes -> (module NS) | DescendantThreads _ -> (module ConcDomain.ThreadSet) - | MayCreationLockset _ -> (module ALS) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -301,7 +299,6 @@ struct | GhostVarAvailable _ -> MayBool.top () | InvariantGlobalNodes -> NS.top () | DescendantThreads _ -> ConcDomain.ThreadSet.top () - | MayCreationLockset _ -> ALS.top () end (* The type any_query can't be directly defined in Any as t, @@ -374,7 +371,6 @@ struct | Any (GhostVarAvailable _) -> 62 | Any InvariantGlobalNodes -> 63 | Any (DescendantThreads _) -> 64 - | Any (MayCreationLockset _) -> 65 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -482,7 +478,6 @@ struct | Any (GasExhausted f) -> CilType.Fundec.hash f | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v | Any (DescendantThreads t) -> ThreadIdDomain.Thread.hash t - | Any (MayCreationLockset t) -> ThreadIdDomain.Thread.hash t (* IterSysVars: *) (* - argument is a function and functions cannot be compared in any meaningful way. *) (* - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *) @@ -552,7 +547,6 @@ struct | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads %a" ThreadIdDomain.Thread.pretty t - | Any (MayCreationLockset t) -> Pretty.dprintf "MayCreationLockset %a" ThreadIdDomain.Thread.pretty t end let to_value_domain_ask (ask: ask) = From 76c14ddf8240b5161203076dd24925c6654efd41 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Wed, 10 Dec 2025 23:52:15 +0100 Subject: [PATCH 64/95] remove config constraints for creation lockset analysis --- src/maingoblint.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index ba2f6440f2..7d3bf782c5 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -167,9 +167,7 @@ let check_arguments () = if get_bool "dbg.print_wpoints" && not (Logs.Level.should_log Debug) then warn "dbg.print_wpoints requires dbg.level debug"; if get_bool "dbg.print_tids" && not (Logs.Level.should_log Debug) then - warn "dbg.print_tids requires dbg.level debug"; - if List.mem "creationLockset" @@ get_string_list "ana.activated" && not (get_string "ana.thread.domain" = "history" && get_bool "ana.thread.include-node" && get_bool "ana.thread.context.create-edges") then - fail "creation lockset analysis requires ana.thread.domain to be set to \"history\" and both ana.thread.include-node and ana.thread.context.create-edges to be enabled" + warn "dbg.print_tids requires dbg.level debug" (** Initialize some globals in other modules. *) let handle_flags () = From 1f3cdefc6f57bca590e0ffe8651a92b566996b00 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 00:00:33 +0100 Subject: [PATCH 65/95] remove query function from creation lockset analysis --- src/analyses/creationLockset.ml | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index e1f23665fc..0c544a2d56 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -107,12 +107,6 @@ module Spec = struct | _ -> () ;; - let query man (type a) (x : a Queries.t) : a Queries.result = - match x with - | Queries.MayCreationLockset tid -> (man.global tid : G.t) - | _ -> Queries.Result.top x - ;; - module A = struct (** ego tid * must-lockset * creation-lockset *) include Printable.Prod3 (TID) (LIDs) (G) From 72afe4a8ce8b7188a1b4961e065dd13bfdb5f06a Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 00:10:43 +0100 Subject: [PATCH 66/95] enforce must-ancestor property in unlock transfer function --- src/analyses/creationLockset.ml | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 0c544a2d56..4ced523697 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -58,15 +58,20 @@ module Spec = struct | _ -> () ;; - (** compute all descendant threads that may run along with the ego thread at a program point + (** compute all descendant threads that may run along with the ego thread at a program point. + for all of them, tid must be an ancestor + @param tid ego thread id @param ask ask of ego thread at the program point *) - let get_possibly_running_tids (ask : Queries.ask) = + let get_unique_running_descendants tid (ask : Queries.ask) = let may_created_tids = ask.f Queries.CreatedThreads in + let may_unique_created_tids = + TIDs.filter (TID.must_be_ancestor tid) may_created_tids + in let may_transitively_created_tids = TIDs.fold (fun child_tid acc -> TIDs.union acc (unique_descendants_closure ask child_tid)) - may_created_tids + may_unique_created_tids (TIDs.empty ()) in let must_joined_tids = ask.f Queries.MustJoinedThreads in @@ -99,10 +104,12 @@ module Spec = struct let ask = ask_of_man man in let tid_lifted = ask.f Queries.CurrentThreadId in let lock_opt = LockDomain.MustLock.of_addr addr in - let possibly_running_tids = get_possibly_running_tids ask in - (match tid_lifted, lock_opt with - | `Lifted tid, Some lock -> unlock man tid possibly_running_tids lock - | `Lifted tid, None -> unknown_unlock man tid possibly_running_tids + (match tid_lifted with + | `Lifted tid -> + let possibly_running_tids = get_unique_running_descendants tid ask in + (match lock_opt with + | Some lock -> unlock man tid possibly_running_tids lock + | None -> unknown_unlock man tid possibly_running_tids) | _ -> ()) | _ -> () ;; From 3b494d9372c2116e101537c2b6ac4dd76e632ecf Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 00:13:04 +0100 Subject: [PATCH 67/95] remove some semi-colons --- src/analyses/creationLockset.ml | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 4ced523697..f4479fbc96 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -42,7 +42,6 @@ module Spec = struct let descendants = ask.f @@ Queries.DescendantThreads tid in let unique_descendants = TIDs.filter (TID.must_be_ancestor tid) descendants in TIDs.add tid unique_descendants - ;; let threadspawn man ~multiple lval f args fman = let ask = ask_of_man man in @@ -56,7 +55,6 @@ module Spec = struct let to_contribute = G.singleton tid lockset in TIDs.iter (contribute_locks man to_contribute) unique_descendants | _ -> () - ;; (** compute all descendant threads that may run along with the ego thread at a program point. for all of them, tid must be an ancestor @@ -76,7 +74,6 @@ module Spec = struct in let must_joined_tids = ask.f Queries.MustJoinedThreads in TIDs.diff may_transitively_created_tids must_joined_tids - ;; (** handle unlock of mutex [lock] *) let unlock man tid possibly_running_tids lock = @@ -87,7 +84,6 @@ module Spec = struct man.sideg des_tid to_contribute in TIDs.iter shrink_locksets possibly_running_tids - ;; (** handle unlock of an unknown mutex. Assumes that any mutex could have been unlocked *) let unknown_unlock man tid possibly_running_tids = @@ -96,7 +92,6 @@ module Spec = struct man.sideg des_tid to_contribute in TIDs.iter evaporate_locksets possibly_running_tids - ;; let event man e _ = match e with @@ -112,7 +107,6 @@ module Spec = struct | None -> unknown_unlock man tid possibly_running_tids) | _ -> ()) | _ -> () - ;; module A = struct (** ego tid * must-lockset * creation-lockset *) @@ -131,7 +125,6 @@ module Spec = struct G.exists (fun tp2 ls2 -> not (LIDs.disjoint ls1 ls2 || TID.equal tp1 tp2)) cl2 in G.exists cl2_has_same_lock_other_tid cl1 - ;; (** checks if [cl1] has a mapping ([tp1] |-> [ls1]) such that [ls1] and [ls2] are not disjoint and [tp1] != [t2] @@ -142,14 +135,12 @@ module Spec = struct *) let one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 = G.exists (fun tp1 ls1 -> not (LIDs.disjoint ls1 ls2 || TID.equal tp1 t2)) cl1 - ;; let may_race (t1, ls1, cl1) (t2, ls2, cl2) = not (both_protected_inter_threaded cl1 cl2 || one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 || one_protected_inter_threaded_other_intra_threaded cl2 t1 ls1) - ;; let should_print (_t, _ls, cl) = not @@ G.is_empty cl end @@ -163,11 +154,9 @@ module Spec = struct let creation_lockset = man.global tid in tid, lockset, creation_lockset | _ -> ThreadIdDomain.UnknownThread, LIDs.empty (), G.empty () - ;; end let _ = MCP.register_analysis ~dep:[ "threadid"; "mutex"; "race"; "threadJoins"; "transitiveDescendants" ] (module Spec : MCPSpec) -;; From 583a41f0c6cd28b44dccf028d123c6bd4e37cc4f Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 00:18:53 +0100 Subject: [PATCH 68/95] fix comments for test files --- .../00-lockset_inter_threaded_lock_racefree.c | 2 +- .../01-both_inter_threaded_lock_racefree.c | 2 +- .../02-lockset_inter_threaded_lock_transitive_racefree.c | 2 +- .../03-both_inter_threaded_lockset_transitive_racefree.c | 2 +- .../04-never_unlock_never_join_racefree.c | 2 +- .../90-races_ancestor_locksets/05-maybe_create_racefree.c | 2 +- .../90-races_ancestor_locksets/10-maybe_lock_racing.c | 3 +-- .../90-races_ancestor_locksets/11-maybe_unlock_racing.c | 3 +-- .../90-races_ancestor_locksets/12-random_mutex_unlock_racing.c | 3 +-- .../13-unknown_mutex_unlock_racing.c | 2 +- .../90-races_ancestor_locksets/14-maybe_join_racing.c | 2 +- ...ock_from_same_thread_one_lockset_one_interthreaded_racing.c | 2 +- .../16-lock_from_same_thread_both_interthreaded_racing.c | 2 +- .../90-races_ancestor_locksets/17-ambiguous_context_racing.c | 2 +- .../20-multiple_create_statements_racing.c | 2 +- .../regression/90-races_ancestor_locksets/21-diamond_racing.c | 2 +- tests/regression/90-races_ancestor_locksets/22-circle_racing.c | 2 +- 17 files changed, 17 insertions(+), 20 deletions(-) diff --git a/tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c index ff36af007b..9154078560 100644 --- a/tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c index c161bf8c58..4365f821f0 100644 --- a/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c index e9e3c3b699..ca4db065ae 100644 --- a/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/03-both_inter_threaded_lockset_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/03-both_inter_threaded_lockset_transitive_racefree.c index 78474057ab..b35915f6e6 100644 --- a/tests/regression/90-races_ancestor_locksets/03-both_inter_threaded_lockset_transitive_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/03-both_inter_threaded_lockset_transitive_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c b/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c index 9c524b4873..dde1a03627 100644 --- a/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c b/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c index 55e0569189..05bf7f690c 100644 --- a/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c b/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c index ee7e0e0f1a..cf8b6c395e 100644 --- a/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c +++ b/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c @@ -1,5 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset -// TODO broken, since locksets have more granular path sensitivity than creation locksets +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c index bc09c8df65..a35cb5f2b4 100644 --- a/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c +++ b/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c @@ -1,5 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset -// TODO broken, since locksets have more granular path sensitivity than creation locksets +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c index c7e0bf3d72..7948c6b0fd 100644 --- a/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c +++ b/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c @@ -1,5 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset -// TODO broken, since locksets have more granular path sensitivity than creation locksets +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c index 325ff4d05a..5bd75bef2e 100644 --- a/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c +++ b/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c b/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c index 4050f74640..e7c57198f5 100644 --- a/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c +++ b/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c b/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c index 6e1f246d3c..0c61a6cf95 100644 --- a/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c +++ b/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c b/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c index 622bf8aa07..833896cd93 100644 --- a/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c +++ b/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c b/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c index ba5b204b28..4393cb59fe 100644 --- a/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c +++ b/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c b/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c index b97c6b17f6..73fb239823 100644 --- a/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c +++ b/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c b/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c index c867d795e4..c476c575c0 100644 --- a/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c +++ b/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/22-circle_racing.c b/tests/regression/90-races_ancestor_locksets/22-circle_racing.c index 95da00e969..f6bb9bed51 100644 --- a/tests/regression/90-races_ancestor_locksets/22-circle_racing.c +++ b/tests/regression/90-races_ancestor_locksets/22-circle_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset #include // This program does not make any sense in practice (it produces a deadlock and if it did not, it wouldn't halt) From 744f5846452da7500f4d06635fa16c57346e00bf Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 14:11:01 +0100 Subject: [PATCH 69/95] reorder some statements in event transition function --- src/analyses/creationLockset.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index f4479fbc96..b1a9bb0d3a 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -98,10 +98,10 @@ module Spec = struct | Events.Unlock addr -> let ask = ask_of_man man in let tid_lifted = ask.f Queries.CurrentThreadId in - let lock_opt = LockDomain.MustLock.of_addr addr in (match tid_lifted with | `Lifted tid -> let possibly_running_tids = get_unique_running_descendants tid ask in + let lock_opt = LockDomain.MustLock.of_addr addr in (match lock_opt with | Some lock -> unlock man tid possibly_running_tids lock | None -> unknown_unlock man tid possibly_running_tids) From 648de9a484d6180166c6c72f1ce69fb518fa3b19 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 14:33:18 +0100 Subject: [PATCH 70/95] comment on applying setminus to bottom --- src/analyses/creationLockset.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index b1a9bb0d3a..f588205d71 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -79,6 +79,7 @@ module Spec = struct let unlock man tid possibly_running_tids lock = let shrink_locksets des_tid = let old_creation_lockset = G.find tid (man.global des_tid) in + (* Bot - {something} = Bot. This is exactly what we want in this case! *) let updated_creation_lockset = LIDs.remove lock old_creation_lockset in let to_contribute = G.singleton tid updated_creation_lockset in man.sideg des_tid to_contribute From 772cf03d9a80bc1e36d08da870b82ab42b097df1 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 14:37:23 +0100 Subject: [PATCH 71/95] move domain type dafinition back from queries to analysis --- src/analyses/creationLockset.ml | 3 +-- src/domains/queries.ml | 2 -- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index f588205d71..aeb9574ef5 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -18,8 +18,7 @@ module Spec = struct include StdV end - (** [TID] -> [LIDs] *) - module G = Queries.ALS + module G = MapDomain.MapBot (TID) (LIDs) let name () = "creationLockset" let startstate _ = D.bot () diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 3ec0b07ea4..1235143540 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -77,8 +77,6 @@ type invariant_context = Invariant.context = { module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end) -module ALS = MapDomain.MapBot (ThreadIdDomain.Thread) (LockDomain.MustLockset) - (** GADT for queries with specific result type. *) type _ t = | EqualSet: exp -> ES.t t From a8479fe9eb9480f8b2d843d7e27f9ecf051f383b Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 14:41:35 +0100 Subject: [PATCH 72/95] move comment explaining the analysis to top of file --- src/analyses/creationLockset.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index aeb9574ef5..814a0b0fe5 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -1,4 +1,9 @@ -(** creation-lockset analysis. See https://github.com/goblint/analyzer/pull/1865 *) +(** creation lockset analysis [creationLockset] + constructs edges on the graph over all threads, where the edges are labelled with must-locksets: + (t_1) ---L--> (t_0) means that t_1 is protected by all members of L from t_0 + + @see https://github.com/goblint/analyzer/pull/1865 +*) open Analyses module TID = ThreadIdDomain.Thread @@ -6,9 +11,6 @@ module TIDs = ConcDomain.ThreadSet module LID = LockDomain.MustLock module LIDs = LockDomain.MustLockset -(** constructs edges on the graph over all threads, where the edges are labelled with must-locksets: - t_1 --ls-> t_0 means that t_1 is protected by all members of ls from t_0 -*) module Spec = struct include IdentityUnitContextsSpec module D = Lattice.Unit From 14d195f7edff492a310809f74f8fd263b2df17d1 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 14:43:50 +0100 Subject: [PATCH 73/95] fix an outdated comment --- src/analyses/creationLockset.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 814a0b0fe5..e54a78233f 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -116,7 +116,7 @@ module Spec = struct let name () = "creationLockset" - (** checks if [itls1] has a member ([tp1] |-> [ls1]) and [itls2] has a member ([tp2] |-> [ls2]) + (** checks if [cl1] has a member ([tp1] |-> [ls1]) and [cl2] has a member ([tp2] |-> [ls2]) such that [ls1] and [ls2] are not disjoint and [tp1] != [tp2] @param cl1 creation-lockset of first thread [t1] @param cl2 creation-lockset of second thread [t2] From a0c24469eb6723794759e0dfa8c418795632fc98 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 14:52:37 +0100 Subject: [PATCH 74/95] rename descendants analysis --- src/analyses/creationLockset.ml | 2 +- .../{transitiveDescendants.ml => threadDescendants.ml} | 6 +++--- src/goblint_lib.ml | 2 +- .../00-lockset_inter_threaded_lock_racefree.c | 2 +- .../01-both_inter_threaded_lock_racefree.c | 2 +- .../02-lockset_inter_threaded_lock_transitive_racefree.c | 2 +- .../03-both_inter_threaded_lockset_transitive_racefree.c | 2 +- .../04-never_unlock_never_join_racefree.c | 2 +- .../90-races_ancestor_locksets/05-maybe_create_racefree.c | 2 +- .../90-races_ancestor_locksets/10-maybe_lock_racing.c | 2 +- .../90-races_ancestor_locksets/11-maybe_unlock_racing.c | 2 +- .../12-random_mutex_unlock_racing.c | 2 +- .../13-unknown_mutex_unlock_racing.c | 2 +- .../90-races_ancestor_locksets/14-maybe_join_racing.c | 2 +- ..._from_same_thread_one_lockset_one_interthreaded_racing.c | 2 +- .../16-lock_from_same_thread_both_interthreaded_racing.c | 2 +- .../17-ambiguous_context_racing.c | 2 +- .../20-multiple_create_statements_racing.c | 2 +- .../90-races_ancestor_locksets/21-diamond_racing.c | 2 +- .../90-races_ancestor_locksets/22-circle_racing.c | 2 +- 20 files changed, 22 insertions(+), 22 deletions(-) rename src/analyses/{transitiveDescendants.ml => threadDescendants.ml} (87%) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index e54a78233f..674f40b63c 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -160,5 +160,5 @@ end let _ = MCP.register_analysis - ~dep:[ "threadid"; "mutex"; "race"; "threadJoins"; "transitiveDescendants" ] + ~dep:[ "threadid"; "mutex"; "race"; "threadJoins"; "threadDescendants" ] (module Spec : MCPSpec) diff --git a/src/analyses/transitiveDescendants.ml b/src/analyses/threadDescendants.ml similarity index 87% rename from src/analyses/transitiveDescendants.ml rename to src/analyses/threadDescendants.ml index 87362ccf01..41c30e8d36 100644 --- a/src/analyses/transitiveDescendants.ml +++ b/src/analyses/threadDescendants.ml @@ -2,7 +2,7 @@ open Analyses module TID = ThreadIdDomain.Thread (** flow-insensitive analysis mapping threads to may-sets of descendants *) -module TransitiveDescendants = struct +module Spec = struct include IdentityUnitContextsSpec module D = Lattice.Unit @@ -13,7 +13,7 @@ module TransitiveDescendants = struct module G = ConcDomain.ThreadSet - let name () = "transitiveDescendants" + let name () = "threadDescendants" let startstate _ = D.bot () let exitstate _ = D.bot () @@ -40,4 +40,4 @@ module TransitiveDescendants = struct man.sideg tid child_descendants) end -let _ = MCP.register_analysis ~dep:[ "threadid" ] (module TransitiveDescendants : MCPSpec) +let _ = MCP.register_analysis ~dep:[ "threadid" ] (module Spec : MCPSpec) diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index fabc344ab8..c154a37269 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -120,7 +120,7 @@ module ThreadAnalysis = ThreadAnalysis module ThreadJoins = ThreadJoins module MHPAnalysis = MHPAnalysis module ThreadReturn = ThreadReturn -module TransitiveDescendants = TransitiveDescendants +module ThreadDescendants = ThreadDescendants (** {3 Other} *) diff --git a/tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c index 9154078560..ef9de824dd 100644 --- a/tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/00-lockset_inter_threaded_lock_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c index 4365f821f0..81624ab563 100644 --- a/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c index ca4db065ae..730dfe6f9a 100644 --- a/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/03-both_inter_threaded_lockset_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/03-both_inter_threaded_lockset_transitive_racefree.c index b35915f6e6..9a69e6675b 100644 --- a/tests/regression/90-races_ancestor_locksets/03-both_inter_threaded_lockset_transitive_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/03-both_inter_threaded_lockset_transitive_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c b/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c index dde1a03627..1b40568852 100644 --- a/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/04-never_unlock_never_join_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c b/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c index 05bf7f690c..d230a21902 100644 --- a/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/05-maybe_create_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c b/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c index cf8b6c395e..2d4aed06e3 100644 --- a/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c +++ b/tests/regression/90-races_ancestor_locksets/10-maybe_lock_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c index a35cb5f2b4..4845e2fbfb 100644 --- a/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c +++ b/tests/regression/90-races_ancestor_locksets/11-maybe_unlock_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c index 7948c6b0fd..93c1d49657 100644 --- a/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c +++ b/tests/regression/90-races_ancestor_locksets/12-random_mutex_unlock_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c index 5bd75bef2e..0560e5bfe0 100644 --- a/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c +++ b/tests/regression/90-races_ancestor_locksets/13-unknown_mutex_unlock_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c b/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c index e7c57198f5..0f34d5c7c4 100644 --- a/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c +++ b/tests/regression/90-races_ancestor_locksets/14-maybe_join_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c b/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c index 0c61a6cf95..1d2b39cea9 100644 --- a/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c +++ b/tests/regression/90-races_ancestor_locksets/15-lock_from_same_thread_one_lockset_one_interthreaded_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c b/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c index 833896cd93..8b9409c80c 100644 --- a/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c +++ b/tests/regression/90-races_ancestor_locksets/16-lock_from_same_thread_both_interthreaded_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c b/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c index 4393cb59fe..4d7708e5de 100644 --- a/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c +++ b/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c b/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c index 73fb239823..2182060661 100644 --- a/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c +++ b/tests/regression/90-races_ancestor_locksets/20-multiple_create_statements_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c b/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c index c476c575c0..2f86abf974 100644 --- a/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c +++ b/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include int global = 0; diff --git a/tests/regression/90-races_ancestor_locksets/22-circle_racing.c b/tests/regression/90-races_ancestor_locksets/22-circle_racing.c index f6bb9bed51..7a76bffba1 100644 --- a/tests/regression/90-races_ancestor_locksets/22-circle_racing.c +++ b/tests/regression/90-races_ancestor_locksets/22-circle_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset #include // This program does not make any sense in practice (it produces a deadlock and if it did not, it wouldn't halt) From 048ca71994e929cc825bab96e7d0db714dae2e5a Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 14:56:43 +0100 Subject: [PATCH 75/95] make threadspawn transfer function in descendants analysis a little leaner --- src/analyses/threadDescendants.ml | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/src/analyses/threadDescendants.ml b/src/analyses/threadDescendants.ml index 41c30e8d36..9367e2da62 100644 --- a/src/analyses/threadDescendants.ml +++ b/src/analyses/threadDescendants.ml @@ -23,21 +23,15 @@ module Spec = struct | _ -> Queries.Result.top x let threadspawn man ~multiple lval f args fman = - let ask = Analyses.ask_of_man man in + let ask = ask_of_man man in let tid_lifted = ask.f Queries.CurrentThreadId in - match tid_lifted with - | `Top | `Bot -> () - | `Lifted tid -> - let child_ask = Analyses.ask_of_man fman in - let child_tid_lifted = child_ask.f Queries.CurrentThreadId in - (match child_tid_lifted with - | `Top | `Bot -> () - | `Lifted child_tid -> - (* contribute new child *) - let _ = man.sideg tid (G.singleton child_tid) in - (* transitive closure *) - let child_descendants = man.global child_tid in - man.sideg tid child_descendants) + let child_ask = ask_of_man fman in + let child_tid_lifted = child_ask.f Queries.CurrentThreadId in + match tid_lifted, child_tid_lifted with + | `Lifted tid, `Lifted child_tid -> + let to_contribute = G.add child_tid (man.global child_tid) in + man.sideg tid to_contribute + | _ -> () end let _ = MCP.register_analysis ~dep:[ "threadid" ] (module Spec : MCPSpec) From a6773146546e5e35dee84cdd30e03a2aba9c2987 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 15:01:08 +0100 Subject: [PATCH 76/95] top comment for thread descendants analysis --- src/analyses/threadDescendants.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/analyses/threadDescendants.ml b/src/analyses/threadDescendants.ml index 9367e2da62..c50bd9125e 100644 --- a/src/analyses/threadDescendants.ml +++ b/src/analyses/threadDescendants.ml @@ -1,7 +1,10 @@ +(** thread descendants analysis [threadDescendants] + flow-insensitive construction of descendants may-set for every thread +*) + open Analyses module TID = ThreadIdDomain.Thread -(** flow-insensitive analysis mapping threads to may-sets of descendants *) module Spec = struct include IdentityUnitContextsSpec module D = Lattice.Unit From 97a69679af6ee6742c1be960bdd147a601bfb5fa Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 15:15:06 +0100 Subject: [PATCH 77/95] re-add an empty line, which was removed in a previous commit --- src/domains/queries.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 1235143540..9b64be4d78 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -77,6 +77,7 @@ type invariant_context = Invariant.context = { module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end) + (** GADT for queries with specific result type. *) type _ t = | EqualSet: exp -> ES.t t From 2c9c39dcf350eff3ad403e662385271b7ef9f944 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Thu, 11 Dec 2025 22:03:12 +0100 Subject: [PATCH 78/95] remove redundant and inaccurate comment --- src/analyses/creationLockset.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 674f40b63c..073eb86744 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -37,7 +37,6 @@ module Spec = struct and filtered to only include threads, where [tid] is a must-ancestor @param ask any ask @param tid - @returns [{ tid }] \cup DES([tid]) *) let unique_descendants_closure (ask : Queries.ask) tid = let descendants = ask.f @@ Queries.DescendantThreads tid in From c36d6d1bdac1ffa0820fac13bbeebce4a96465e7 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 12 Dec 2025 22:17:13 +0100 Subject: [PATCH 79/95] must_ancestors function for thread ids --- src/cdomain/value/cdomains/threadIdDomain.ml | 26 ++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index 5ac8f02d9c..7ec5d500ee 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -17,6 +17,9 @@ sig (** Is the first TID a must ancestor of the second thread. Always false if the first TID is not unique *) val must_be_ancestor: t -> t -> bool + + (** Every TID of the returned list must be an ancestor of the passed TID. Return None if the result cannot be determined *) + val must_ancestors: t -> t list option end module type Stateless = @@ -89,6 +92,7 @@ struct let is_unique = is_main let may_be_ancestor _ _ = true let must_be_ancestor _ _ = false + let must_ancestors _ = None end @@ -169,6 +173,16 @@ struct false (* composing cannot fix incompatibility there *) ) + let must_ancestors (p, s) = + let rec build_ancestors acc p = + match p with + | [] -> acc + | h :: t -> build_ancestors ((h :: t, S.empty ()) :: acc) t + in + (* for unique threads, the first element of p is the current TID *) + let ancestor_edges = if S.is_empty s then List.tl p else p in + Some (build_ancestors [] ancestor_edges) + let compose ((p, s) as current) ni = if BatList.mem_cmp Base.compare ni p then ( let shared, unique = BatList.span (not % Base.equal ni) p in @@ -261,6 +275,12 @@ struct let may_be_ancestor = binop H.may_be_ancestor P.may_be_ancestor let must_be_ancestor = binop H.must_be_ancestor P.must_be_ancestor + let must_ancestors (t: H.t option * P.t option) = + match t with + | Some ht, None -> + Option.map (List.map (fun tid -> Some tid, None)) (H.must_ancestors ht) + | _ -> None + let created x d = let lifth x' d' = let hres = H.created x' d' in @@ -365,6 +385,12 @@ struct | Thread tid1, Thread tid2 -> FlagConfiguredTID.must_be_ancestor tid1 tid2 | _, _ -> false + let must_ancestors t = + match t with + | Thread tid -> + Option.map (List.map (fun t -> Thread t)) (FlagConfiguredTID.must_ancestors tid) + | _ -> None + module D = FlagConfiguredTID.D let threadenter ~multiple (t, d) node i v = From 3c1a51f4e3102ead5177be6154398af4d715a355 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Fri, 12 Dec 2025 22:38:24 +0100 Subject: [PATCH 80/95] must_ancestors test --- tests/unit/cdomains/threadIdDomainTest.ml | 32 +++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/tests/unit/cdomains/threadIdDomainTest.ml b/tests/unit/cdomains/threadIdDomainTest.ml index 7f829c52d1..0b9cfa466a 100644 --- a/tests/unit/cdomains/threadIdDomainTest.ml +++ b/tests/unit/cdomains/threadIdDomainTest.ml @@ -98,10 +98,42 @@ let test_history_may_be_ancestor _ = Might be related to untestability with this unit test harness: https://github.com/goblint/analyzer/pull/1561#discussion_r1888149978. *) () +let test_history_must_ancestors _ = + let open History in + let compare_ancestors a1 a2 = Option.equal (List.equal equal) a1 a2 in + let print_ancestors a = + let string_of_thread t = + GoblintCil.Pretty.sprint ~width:max_int (History.pretty () t) + in + match a with + | Some l -> "Some [" ^ String.concat ", " (List.map string_of_thread l) ^ "]" + | None -> "None" + in + + let assert_equal = + assert_equal ?printer:(Some print_ancestors) ?cmp:(Some compare_ancestors) + in + + (* unique tids *) + assert_equal (Some []) (must_ancestors main); + assert_equal (Some [ main ]) (must_ancestors (main >> a)); + assert_equal (Some [ main; main >> a; main >> a >> b; main >> a >> b >> c ]) (must_ancestors (main >> a >> b >> c >> d)); + + (* non-unique tids *) + assert_equal (Some [ main ]) (must_ancestors (main >> a >> a)); + assert_equal (Some [ main ]) (must_ancestors (main >> a >> a >> b)); + assert_equal (Some [ main ]) (must_ancestors (main >> a >> b >> c >> a)); + assert_equal (Some [ main; main >> a ]) (must_ancestors (main >> a >> b >> c >> b >> d)); + assert_equal (Some [ main; main >> a; main >> a >> b ]) (must_ancestors (main >> a >> b >> c >> c)); + + () + + let tests = "threadIdDomainTest" >::: [ "history" >::: [ "must_be_ancestor" >:: test_history_must_be_ancestor; "may_be_ancestor" >:: test_history_may_be_ancestor; + "must_ancestors" >:: test_history_must_ancestors; ] ] From 34f4e9f3fbba10a2f74e3de6b5b4f7b7cbe4590f Mon Sep 17 00:00:00 2001 From: dabund24 Date: Sun, 14 Dec 2025 20:58:50 +0100 Subject: [PATCH 81/95] change return type of must_ancestors to not be an option --- src/cdomain/value/cdomains/threadIdDomain.ml | 15 ++++++------ tests/unit/cdomains/threadIdDomainTest.ml | 24 +++++++++----------- 2 files changed, 18 insertions(+), 21 deletions(-) diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index 7ec5d500ee..a8073e96ba 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -19,7 +19,7 @@ sig val must_be_ancestor: t -> t -> bool (** Every TID of the returned list must be an ancestor of the passed TID. Return None if the result cannot be determined *) - val must_ancestors: t -> t list option + val must_ancestors: t -> t list end module type Stateless = @@ -92,7 +92,7 @@ struct let is_unique = is_main let may_be_ancestor _ _ = true let must_be_ancestor _ _ = false - let must_ancestors _ = None + let must_ancestors _ = [] end @@ -181,7 +181,7 @@ struct in (* for unique threads, the first element of p is the current TID *) let ancestor_edges = if S.is_empty s then List.tl p else p in - Some (build_ancestors [] ancestor_edges) + build_ancestors [] ancestor_edges let compose ((p, s) as current) ni = if BatList.mem_cmp Base.compare ni p then ( @@ -278,8 +278,8 @@ struct let must_ancestors (t: H.t option * P.t option) = match t with | Some ht, None -> - Option.map (List.map (fun tid -> Some tid, None)) (H.must_ancestors ht) - | _ -> None + List.map (fun tid -> Some tid, None) (H.must_ancestors ht) + | _ -> [] let created x d = let lifth x' d' = @@ -387,9 +387,8 @@ struct let must_ancestors t = match t with - | Thread tid -> - Option.map (List.map (fun t -> Thread t)) (FlagConfiguredTID.must_ancestors tid) - | _ -> None + | Thread tid -> List.map (fun t -> Thread t) (FlagConfiguredTID.must_ancestors tid) + | _ -> [] module D = FlagConfiguredTID.D diff --git a/tests/unit/cdomains/threadIdDomainTest.ml b/tests/unit/cdomains/threadIdDomainTest.ml index 0b9cfa466a..d21610efc9 100644 --- a/tests/unit/cdomains/threadIdDomainTest.ml +++ b/tests/unit/cdomains/threadIdDomainTest.ml @@ -100,14 +100,12 @@ let test_history_may_be_ancestor _ = let test_history_must_ancestors _ = let open History in - let compare_ancestors a1 a2 = Option.equal (List.equal equal) a1 a2 in - let print_ancestors a = + let compare_ancestors a1 a2 = (List.equal equal) a1 a2 in + let print_ancestors l = let string_of_thread t = GoblintCil.Pretty.sprint ~width:max_int (History.pretty () t) in - match a with - | Some l -> "Some [" ^ String.concat ", " (List.map string_of_thread l) ^ "]" - | None -> "None" + "[" ^ String.concat ", " (List.map string_of_thread l) ^ "]" in let assert_equal = @@ -115,16 +113,16 @@ let test_history_must_ancestors _ = in (* unique tids *) - assert_equal (Some []) (must_ancestors main); - assert_equal (Some [ main ]) (must_ancestors (main >> a)); - assert_equal (Some [ main; main >> a; main >> a >> b; main >> a >> b >> c ]) (must_ancestors (main >> a >> b >> c >> d)); + assert_equal ([]) (must_ancestors main); + assert_equal ([ main ]) (must_ancestors (main >> a)); + assert_equal ([ main; main >> a; main >> a >> b; main >> a >> b >> c ]) (must_ancestors (main >> a >> b >> c >> d)); (* non-unique tids *) - assert_equal (Some [ main ]) (must_ancestors (main >> a >> a)); - assert_equal (Some [ main ]) (must_ancestors (main >> a >> a >> b)); - assert_equal (Some [ main ]) (must_ancestors (main >> a >> b >> c >> a)); - assert_equal (Some [ main; main >> a ]) (must_ancestors (main >> a >> b >> c >> b >> d)); - assert_equal (Some [ main; main >> a; main >> a >> b ]) (must_ancestors (main >> a >> b >> c >> c)); + assert_equal ([ main ]) (must_ancestors (main >> a >> a)); + assert_equal ([ main ]) (must_ancestors (main >> a >> a >> b)); + assert_equal ([ main ]) (must_ancestors (main >> a >> b >> c >> a)); + assert_equal ([ main; main >> a ]) (must_ancestors (main >> a >> b >> c >> b >> d)); + assert_equal ([ main; main >> a; main >> a >> b ]) (must_ancestors (main >> a >> b >> c >> c)); () From 5403dfdc9043e1ce7ae41e1cbbdcf074766c343b Mon Sep 17 00:00:00 2001 From: dabund24 Date: Sun, 14 Dec 2025 22:17:45 +0100 Subject: [PATCH 82/95] initial version of alternative analysis --- src/analyses/creationLocksetAlternative.ml | 221 +++++++++++++++++++++ src/domains/queries.ml | 8 + src/goblint_lib.ml | 1 + 3 files changed, 230 insertions(+) create mode 100644 src/analyses/creationLocksetAlternative.ml diff --git a/src/analyses/creationLocksetAlternative.ml b/src/analyses/creationLocksetAlternative.ml new file mode 100644 index 0000000000..70b6cd4c65 --- /dev/null +++ b/src/analyses/creationLocksetAlternative.ml @@ -0,0 +1,221 @@ +(** creation lockset analysis [creationLocksetAlternative] + constructs edges on the graph over all threads, where the edges are labelled with must-locksets: + (t_1) ---L--> (t_0) means that t_1 is protected by all members of L from t_0 + + @see https://github.com/goblint/analyzer/pull/1865 +*) + +open Analyses +module TID = ThreadIdDomain.Thread +module TIDs = ConcDomain.MustThreadSet +module LID = LockDomain.MustLock +module LIDs = LockDomain.MustLockset + +module CreationLocksetAlternative = struct + include IdentityUnitContextsSpec + module D = Lattice.Unit + + module V = struct + include TID + include StdV + end + + module G = Queries.CLS + + let name () = "creationLocksetAlternative" + let startstate _ = D.bot () + let exitstate _ = D.bot () + + let threadspawn man ~multiple lval f args fman = + let ask = ask_of_man man in + let tid_lifted = ask.f Queries.CurrentThreadId in + let child_ask = ask_of_man fman in + let child_tid_lifted = child_ask.f Queries.CurrentThreadId in + match tid_lifted, child_tid_lifted with + | `Lifted tid, `Lifted child_tid when TID.must_be_ancestor tid child_tid -> + let lockset = ask.f Queries.MustLockset in + let to_contribute = G.singleton tid lockset in + man.sideg child_tid to_contribute + | _ -> () + ;; + + let query man (type a) (x : a Queries.t) : a Queries.result = + match x with + | Queries.CreationLocksetAlternative tid -> + Logs.result "query"; + Logs.result "query %a" G.pretty (man.global tid); + (man.global tid : G.t) + | _ -> Queries.Result.top x + ;; +end + +module TaintedCreationLocksetAlternative = struct + include IdentityUnitContextsSpec + module D = Lattice.Unit + + module V = struct + include TID + include StdV + end + + module Range = MapDomain.MapBot (LID) (TIDs) + module G = MapDomain.MapBot (TID) (Range) + + let name () = "taintedCreationLocksetAlternative" + let startstate _ = D.bot () + let exitstate _ = D.bot () + + let get_unique_created_children tid (ask : Queries.ask) = + let created_threads = ask.f Queries.CreatedThreads in + TIDs.filter (TID.must_be_ancestor tid) created_threads + ;; + + (** handle unlock of mutex [lock] *) + let unlock man tid created_tids lock = + Logs.result "u"; + let ask = ask_of_man man in + let joinedThreads = ask.f Queries.MustJoinedThreads in + let contribute_lock child_tid = + let to_contribute = G.singleton tid (Range.singleton lock joinedThreads) in + man.sideg child_tid to_contribute + in + TIDs.iter contribute_lock created_tids + ;; + + (** handle unlock of an unknown mutex. Assumes that any mutex could have been unlocked *) + let unknown_unlock man tid created_tids = + Logs.result "uu"; + let ask = ask_of_man man in + let evaporate_locksets child_tid = + let allCreationLocksets = ask.f @@ Queries.CreationLocksetAlternative child_tid in + let creationLockset = CreationLocksetAlternative.G.find tid allCreationLocksets in + let to_contribute_value = + LIDs.fold + (fun lock acc -> Range.join acc (Range.singleton lock (TIDs.empty ()))) + creationLockset + (Range.empty ()) + in + let to_contribute = G.singleton tid to_contribute_value in + man.sideg child_tid to_contribute + in + TIDs.iter evaporate_locksets created_tids + ;; + + let event man e _ = + Logs.result "e"; + match e with + | Events.Unlock addr -> + let ask = ask_of_man man in + let tid_lifted = ask.f Queries.CurrentThreadId in + (match tid_lifted with + | `Lifted tid -> + let created_tids = get_unique_created_children tid ask in + let lock_opt = LockDomain.MustLock.of_addr addr in + (match lock_opt with + | Some lock -> unlock man tid created_tids lock + | None -> unknown_unlock man tid created_tids) + | _ -> ()) + | _ -> () + ;; + + module A = struct + (** ego tid * must-lockset * creation-lockset *) + include Printable.Prod3 (TID) (LIDs) (Queries.CLS) + + let name () = "creationLockset" + + (** checks if [cl1] has a member ([tp1] |-> [ls1]) and [cl2] has a member ([tp2] |-> [ls2]) + such that [ls1] and [ls2] are not disjoint and [tp1] != [tp2] + @param cl1 creation-lockset of first thread [t1] + @param cl2 creation-lockset of second thread [t2] + @returns whether [t1] and [t2] must be running mutually exclusive + *) + let both_protected_inter_threaded cl1 cl2 = + let cl2_has_same_lock_other_tid tp1 ls1 = + Queries.CLS.exists + (fun tp2 ls2 -> not (LIDs.disjoint ls1 ls2 || TID.equal tp1 tp2)) + cl2 + in + Queries.CLS.exists cl2_has_same_lock_other_tid cl1 + ;; + + (** checks if [cl1] has a mapping ([tp1] |-> [ls1]) + such that [ls1] and [ls2] are not disjoint and [tp1] != [t2] + @param cl1 creation-lockset of thread [t1] at first program point + @param t2 thread id at second program point + @param ls2 lockset at second program point + @returns whether [t1] must be running mutually exclusive with second program point + *) + let one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 = + Queries.CLS.exists + (fun tp1 ls1 -> not (LIDs.disjoint ls1 ls2 || TID.equal tp1 t2)) + cl1 + ;; + + let may_race (t1, ls1, cl1) (t2, ls2, cl2) = + not + (both_protected_inter_threaded cl1 cl2 + || one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 + || one_protected_inter_threaded_other_intra_threaded cl2 t1 ls1) + ;; + + let should_print (_t, _ls, cl) = not @@ Queries.CLS.is_empty cl + end + + let access man _ = + Logs.result "a"; + let ask = Analyses.ask_of_man man in + let tid_lifted = ask.f Queries.CurrentThreadId in + match tid_lifted with + | `Lifted td -> + let must_ancestors = TID.must_ancestors td in + let compute_cl_transitive () = + Logs.result "clt1 %a" TID.pretty td; + let cl_td = ask.f @@ Queries.CreationLocksetAlternative td in + Logs.result "clt2"; + List.fold_left + (fun acc t1 -> + Queries.CLS.join acc (ask.f @@ Queries.CreationLocksetAlternative t1)) + cl_td + must_ancestors + in + let compute_tcl_transitive () = + let tcl_td = man.global td in + List.fold_left (fun acc t1 -> G.join acc (man.global t1)) tcl_td must_ancestors + in + let compute_tcl_lockset tcl_transitive t0 = + let tcl_transitive_t0 = G.find t0 tcl_transitive in + Range.fold + (fun l j acc -> if TIDs.mem td j then acc else LIDs.add l acc) + tcl_transitive_t0 + (LIDs.empty ()) + in + let compute_il cl_transitive tcl_transitive = + Queries.CLS.fold + (fun t0 l_cl acc -> + let l_tcl = compute_tcl_lockset tcl_transitive t0 in + let l_il = LIDs.diff l_cl l_tcl in + Queries.CLS.add t0 l_il acc) + cl_transitive + (Queries.CLS.empty ()) + in + let lockset = ask.f Queries.MustLockset in + let cl_transitive = compute_cl_transitive () in + let tcl_transitive = compute_tcl_transitive () in + let il = compute_il cl_transitive tcl_transitive in + td, lockset, il + | _ -> ThreadIdDomain.UnknownThread, LIDs.empty (), Queries.CLS.empty () + ;; +end + +let _ = + MCP.register_analysis + ~dep:[ "threadid"; "mutex"; "race" ] + (module CreationLocksetAlternative : MCPSpec) +;; + +let _ = + MCP.register_analysis + ~dep:[ "threadid"; "mutex"; "race"; "creationLocksetAlternative" ] + (module TaintedCreationLocksetAlternative : MCPSpec) +;; diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 9b64be4d78..9397ff2483 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -77,6 +77,8 @@ type invariant_context = Invariant.context = { module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end) +module CLS = MapDomain.MapBot_LiftTop (ThreadIdDomain.Thread) (LockDomain.MustLockset) + (** GADT for queries with specific result type. *) type _ t = @@ -147,6 +149,7 @@ type _ t = | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *) | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t + | CreationLocksetAlternative: ThreadIdDomain.Thread.t -> CLS.t t type 'a result = 'a @@ -223,6 +226,7 @@ struct | GhostVarAvailable _ -> (module MayBool) | InvariantGlobalNodes -> (module NS) | DescendantThreads _ -> (module ConcDomain.ThreadSet) + | CreationLocksetAlternative _ -> (module CLS) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -298,6 +302,7 @@ struct | GhostVarAvailable _ -> MayBool.top () | InvariantGlobalNodes -> NS.top () | DescendantThreads _ -> ConcDomain.ThreadSet.top () + | CreationLocksetAlternative _ -> CLS.top () end (* The type any_query can't be directly defined in Any as t, @@ -370,6 +375,7 @@ struct | Any (GhostVarAvailable _) -> 62 | Any InvariantGlobalNodes -> 63 | Any (DescendantThreads _) -> 64 + | Any (CreationLocksetAlternative _) -> 65 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -477,6 +483,7 @@ struct | Any (GasExhausted f) -> CilType.Fundec.hash f | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v | Any (DescendantThreads t) -> ThreadIdDomain.Thread.hash t + | Any (CreationLocksetAlternative t) -> ThreadIdDomain.Thread.hash t (* IterSysVars: *) (* - argument is a function and functions cannot be compared in any meaningful way. *) (* - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *) @@ -546,6 +553,7 @@ struct | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads %a" ThreadIdDomain.Thread.pretty t + | Any (CreationLocksetAlternative t) -> Pretty.dprintf "CreationLocksetAlternative %a" ThreadIdDomain.Thread.pretty t end let to_value_domain_ask (ask: ask) = diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 92fa69c3b4..6b727c2e0b 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -133,6 +133,7 @@ module PthreadBarriers = PthreadBarriers module ExtractPthread = ExtractPthread module PthreadOnce = PthreadOnce module CreationLockset = CreationLockset +module CreationLocksetAlternative = CreationLocksetAlternative (** {2 Longjmp} From 7770141fd90bf2cabbe1a16916c64753250704b3 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Sun, 14 Dec 2025 22:19:22 +0100 Subject: [PATCH 83/95] tests for alternative analysis --- .../50-lockset_inter_threaded_lock_racefree.c | 27 +++++++++++ .../51-both_inter_threaded_lock_racefree.c | 33 ++++++++++++++ ..._inter_threaded_lock_transitive_racefree.c | 33 ++++++++++++++ ...ter_threaded_lockset_transitive_racefree.c | 45 +++++++++++++++++++ .../54-never_unlock_never_join_racefree.c | 25 +++++++++++ .../55-maybe_create_racefree.c | 28 ++++++++++++ .../60-maybe_lock_racing.c | 28 ++++++++++++ .../61-maybe_unlock_racing.c | 30 +++++++++++++ .../62-random_mutex_unlock_racing.c | 33 ++++++++++++++ .../63-unknown_mutex_unlock_racing.c | 28 ++++++++++++ .../64-maybe_join_racing.c | 30 +++++++++++++ ...ead_one_lockset_one_interthreaded_racing.c | 22 +++++++++ ...om_same_thread_both_interthreaded_racing.c | 23 ++++++++++ .../67-ambiguous_context_racing.c | 38 ++++++++++++++++ .../70-multiple_create_statements_racing.c | 29 ++++++++++++ .../71-diamond_racing.c | 39 ++++++++++++++++ .../72-circle_racing.c | 39 ++++++++++++++++ 17 files changed, 530 insertions(+) create mode 100644 tests/regression/90-races_ancestor_locksets/50-lockset_inter_threaded_lock_racefree.c create mode 100644 tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_racefree.c create mode 100644 tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_racefree.c create mode 100644 tests/regression/90-races_ancestor_locksets/53-both_inter_threaded_lockset_transitive_racefree.c create mode 100644 tests/regression/90-races_ancestor_locksets/54-never_unlock_never_join_racefree.c create mode 100644 tests/regression/90-races_ancestor_locksets/55-maybe_create_racefree.c create mode 100644 tests/regression/90-races_ancestor_locksets/60-maybe_lock_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/61-maybe_unlock_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/62-random_mutex_unlock_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/63-unknown_mutex_unlock_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/64-maybe_join_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/65-lock_from_same_thread_one_lockset_one_interthreaded_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/66-lock_from_same_thread_both_interthreaded_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/67-ambiguous_context_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/70-multiple_create_statements_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/71-diamond_racing.c create mode 100644 tests/regression/90-races_ancestor_locksets/72-circle_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/50-lockset_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/50-lockset_inter_threaded_lock_racefree.c new file mode 100644 index 0000000000..d09ccc1fb1 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/50-lockset_inter_threaded_lock_racefree.c @@ -0,0 +1,27 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + global++; // NORACE + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_join(id2, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_racefree.c new file mode 100644 index 0000000000..dc7142e882 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_racefree.c @@ -0,0 +1,33 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id_main_child, id_1, id_1_child; + +void *t1_child_fun(void* arg) { // t1child is protected by mutex locked in t1 + global++; // NORACE + return NULL; +} + +void *tmain_child_fun(void *arg) { // tmainchild is protected by mutex locked in main thread + global++; // NORACE + return NULL; +} + +void *t1_fun(void *arg) { + pthread_mutex_lock(&mutex); + pthread_create(&id_1_child, NULL, t1_child_fun, NULL); + pthread_join(id_1_child, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(void) { + pthread_create(&id_1, NULL, t1_fun, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id_main_child, NULL, tmain_child_fun, NULL); + pthread_join(id_main_child, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_racefree.c new file mode 100644 index 0000000000..3c1812f1f9 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_racefree.c @@ -0,0 +1,33 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2, id3; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void* t3(void* arg) { + global++; // NORACE + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + pthread_create(&id3, NULL, t3, NULL); + pthread_join(id3, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_join(id2, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/90-races_ancestor_locksets/53-both_inter_threaded_lockset_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/53-both_inter_threaded_lockset_transitive_racefree.c new file mode 100644 index 0000000000..e948387224 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/53-both_inter_threaded_lockset_transitive_racefree.c @@ -0,0 +1,45 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id_main_child, id_main_grand_child, id_1, id_1_child, id_1_grand_child; + +void *t1_grand_child_fun(void* arg) { // t1_grand_child is protected by mutex locked in t1 + global++; // NORACE + return NULL; +} + +void *t1_child_fun(void *arg) { + pthread_create(&id_1_grand_child, NULL, t1_grand_child_fun, NULL); + pthread_join(id_1_grand_child, NULL); + return NULL; +} + +void *t1_fun(void *arg) { + pthread_mutex_lock(&mutex); + pthread_create(&id_1_child, NULL, t1_child_fun, NULL); + pthread_join(id_1_child, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *tmain_grand_child_fun(void* arg) { // tmain_grand_child is protected by mutex locked in main + global++; // NORACE + return NULL; +} + +void *tmain_child_fun(void *arg) { + pthread_create(&id_main_grand_child, NULL, tmain_grand_child_fun, NULL); + pthread_join(id_main_grand_child, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id_1, NULL, t1_fun, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id_main_child, NULL, tmain_child_fun, NULL); + pthread_join(id_main_child, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/90-races_ancestor_locksets/54-never_unlock_never_join_racefree.c b/tests/regression/90-races_ancestor_locksets/54-never_unlock_never_join_racefree.c new file mode 100644 index 0000000000..10b7042b71 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/54-never_unlock_never_join_racefree.c @@ -0,0 +1,25 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + global++; // NORACE + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/55-maybe_create_racefree.c b/tests/regression/90-races_ancestor_locksets/55-maybe_create_racefree.c new file mode 100644 index 0000000000..e7bbe54f69 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/55-maybe_create_racefree.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + global++; // NORACE + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + int maybe; + if (maybe) { + pthread_create(&id2, NULL, t2, NULL); + } + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/60-maybe_lock_racing.c b/tests/regression/90-races_ancestor_locksets/60-maybe_lock_racing.c new file mode 100644 index 0000000000..88b7e838a2 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/60-maybe_lock_racing.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since the mutex does not have to be locked during creation + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + int maybe; + if (maybe) { + pthread_mutex_lock(&mutex); + } + pthread_create(&id2, NULL, t2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/61-maybe_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/61-maybe_unlock_racing.c new file mode 100644 index 0000000000..f59fca940f --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/61-maybe_unlock_racing.c @@ -0,0 +1,30 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock may happen before joining + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + int maybe; + if (maybe) { + pthread_mutex_unlock(&mutex); + } + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/62-random_mutex_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/62-random_mutex_unlock_racing.c new file mode 100644 index 0000000000..964b00c72c --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/62-random_mutex_unlock_racing.c @@ -0,0 +1,33 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER, mutex_alt = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock may happen before joining + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_lock(&mutex_alt); + pthread_mutex_t *mutex_ref = &mutex_alt; + int maybe; + if (maybe) { + mutex_ref = &mutex; + } + pthread_mutex_unlock(mutex_ref); + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/63-unknown_mutex_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/63-unknown_mutex_unlock_racing.c new file mode 100644 index 0000000000..46e11e0ff0 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/63-unknown_mutex_unlock_racing.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock could happen before joining + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_t *mutex_ref; + pthread_mutex_unlock(mutex_ref); // unlock of unknown mutex + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/64-maybe_join_racing.c b/tests/regression/90-races_ancestor_locksets/64-maybe_join_racing.c new file mode 100644 index 0000000000..d89863ded6 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/64-maybe_join_racing.c @@ -0,0 +1,30 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, joining may happen before unlocking + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + int maybe; + if (maybe) { + pthread_join(id2, NULL); + } + pthread_mutex_unlock(&mutex); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/65-lock_from_same_thread_one_lockset_one_interthreaded_racing.c b/tests/regression/90-races_ancestor_locksets/65-lock_from_same_thread_one_lockset_one_interthreaded_racing.c new file mode 100644 index 0000000000..adbb7a2475 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/65-lock_from_same_thread_one_lockset_one_interthreaded_racing.c @@ -0,0 +1,22 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1; + +// both accesses are protected by same mutex **locked in same thread** + +void *t1(void *arg) { + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_mutex_lock(&mutex); + pthread_create(&id1, NULL, t1, NULL); + global++; // RACE! + pthread_join(id1, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/90-races_ancestor_locksets/66-lock_from_same_thread_both_interthreaded_racing.c b/tests/regression/90-races_ancestor_locksets/66-lock_from_same_thread_both_interthreaded_racing.c new file mode 100644 index 0000000000..7a64c4e471 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/66-lock_from_same_thread_both_interthreaded_racing.c @@ -0,0 +1,23 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +// both accesses are protected by same mutex **locked in same thread** + +void *tc(void *arg) { + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_mutex_lock(&mutex); + pthread_create(&id1, NULL, tc, NULL); + pthread_create(&id2, NULL, tc, NULL); + pthread_join(id1, NULL); + pthread_join(id2, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/90-races_ancestor_locksets/67-ambiguous_context_racing.c b/tests/regression/90-races_ancestor_locksets/67-ambiguous_context_racing.c new file mode 100644 index 0000000000..f3fd45a417 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/67-ambiguous_context_racing.c @@ -0,0 +1,38 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +// both accesses are protected by same mutex **locked in same thread** + +void* t1(void* arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { + global++; // RACE! + return NULL; +} + +void evil(int x) { + if (x) { + pthread_mutex_lock(&mutex); + } + pthread_create(&id2, NULL, t2, NULL); +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + int maybe; + if (maybe) { + evil(0); + } else { + evil(1); + } + return 0; +} diff --git a/tests/regression/90-races_ancestor_locksets/70-multiple_create_statements_racing.c b/tests/regression/90-races_ancestor_locksets/70-multiple_create_statements_racing.c new file mode 100644 index 0000000000..6a0138e637 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/70-multiple_create_statements_racing.c @@ -0,0 +1,29 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since it is created/joined twice. The lock is released before the second join happens + global++; // RACE! + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); + pthread_create(&id2, NULL, t2, NULL); + pthread_join(id2, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_unlock(&mutex); + pthread_join(id2, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/71-diamond_racing.c b/tests/regression/90-races_ancestor_locksets/71-diamond_racing.c new file mode 100644 index 0000000000..0cfa6a8442 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/71-diamond_racing.c @@ -0,0 +1,39 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2, id3, id4_1, id4_2; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void* t4(void* arg) { // t4 is not protected by mutex, since it is created twice and the creation in t2 does not happen with mutex locked + global++; // RACE! + return NULL; +} + +void* t3(void* arg) { + pthread_mutex_lock(&mutex); + pthread_create(&id4_2, NULL, t4, NULL); + pthread_join(id4_2, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *t2(void *arg) { + pthread_create(&id4_1, NULL, t4, NULL); + pthread_join(id4_1, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_create(&id3, NULL, t3, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/90-races_ancestor_locksets/72-circle_racing.c b/tests/regression/90-races_ancestor_locksets/72-circle_racing.c new file mode 100644 index 0000000000..50fcc1b9f2 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/72-circle_racing.c @@ -0,0 +1,39 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +// This program does not make any sense in practice (it produces a deadlock and if it did not, it wouldn't halt) +// We solely want to assert that the accesses to global race + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, idc1; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // RACE! + pthread_mutex_unlock(&mutex); + return NULL; +} + +void* tc1(void* arg); + +void *tc2(void *arg) { + pthread_t idc1; + pthread_mutex_lock(&mutex); + pthread_create(&idc1, NULL, tc1, NULL); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void *tc1(void *arg) { // tc1 is protected by tc2, but not by the main thread. + global++; // RACE! + pthread_t idc2; + pthread_create(&idc2, NULL, tc2, NULL); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&idc1, NULL, tc1, NULL); + return 0; +} \ No newline at end of file From 169b60f04d4405f2aa01b36bb07ca4d659332278 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 13:59:40 +0100 Subject: [PATCH 84/95] compare functions for queries --- src/domains/queries.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 9397ff2483..11c7df5f4d 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -435,6 +435,8 @@ struct | Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2 | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2 | Any (GhostVarAvailable v1), Any (GhostVarAvailable v2) -> WitnessGhostVar.compare v1 v2 + | Any (DescendantThreads t1), Any (DescendantThreads t2) -> ThreadIdDomain.Thread.compare t1 t2 + | Any (CreationLocksetAlternative t1), Any (CreationLocksetAlternative t2) -> ThreadIdDomain.Thread.compare t1 t2 (* only argumentless queries should remain *) | _, _ -> Stdlib.compare (order a) (order b) From fe3c133e8a1417464fa961d9255b542be649828d Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 16:14:22 +0100 Subject: [PATCH 85/95] give tests for alternative implementation non-unique names --- ...ee.c => 50-lockset_inter_threaded_lock_alternative_racefree.c} | 0 ...1-both_inter_threaded_lock_alternative_alternative_racefree.c} | 0 ...lockset_inter_threaded_lock_transitive_alternative_racefree.c} | 0 ...both_inter_threaded_lockset_transitive_alternative_racefree.c} | 0 ...cefree.c => 54-never_unlock_never_join_alternative_racefree.c} | 0 ...e_create_racefree.c => 55-maybe_create_alternative_racefree.c} | 0 ...{60-maybe_lock_racing.c => 60-maybe_lock_alternative_racing.c} | 0 ...maybe_unlock_racing.c => 61-maybe_unlock_alternative_racing.c} | 0 ...nlock_racing.c => 62-random_mutex_unlock_alternative_racing.c} | 0 ...lock_racing.c => 63-unknown_mutex_unlock_alternative_racing.c} | 0 ...{64-maybe_join_racing.c => 64-maybe_join_alternative_racing.c} | 0 ...ame_thread_one_lockset_one_interthreaded_alternative_racing.c} | 0 ...lock_from_same_thread_both_interthreaded_alternative_racing.c} | 0 ...context_racing.c => 67-ambiguous_context_alternative_racing.c} | 0 ...acing.c => 70-multiple_create_statements_alternative_racing.c} | 0 .../{71-diamond_racing.c => 71-diamond_alternative_racing.c} | 0 .../{72-circle_racing.c => 72-circle_alternative_racing.c} | 0 17 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/90-races_ancestor_locksets/{50-lockset_inter_threaded_lock_racefree.c => 50-lockset_inter_threaded_lock_alternative_racefree.c} (100%) rename tests/regression/90-races_ancestor_locksets/{51-both_inter_threaded_lock_racefree.c => 51-both_inter_threaded_lock_alternative_alternative_racefree.c} (100%) rename tests/regression/90-races_ancestor_locksets/{52-lockset_inter_threaded_lock_transitive_racefree.c => 52-lockset_inter_threaded_lock_transitive_alternative_racefree.c} (100%) rename tests/regression/90-races_ancestor_locksets/{53-both_inter_threaded_lockset_transitive_racefree.c => 53-both_inter_threaded_lockset_transitive_alternative_racefree.c} (100%) rename tests/regression/90-races_ancestor_locksets/{54-never_unlock_never_join_racefree.c => 54-never_unlock_never_join_alternative_racefree.c} (100%) rename tests/regression/90-races_ancestor_locksets/{55-maybe_create_racefree.c => 55-maybe_create_alternative_racefree.c} (100%) rename tests/regression/90-races_ancestor_locksets/{60-maybe_lock_racing.c => 60-maybe_lock_alternative_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{61-maybe_unlock_racing.c => 61-maybe_unlock_alternative_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{62-random_mutex_unlock_racing.c => 62-random_mutex_unlock_alternative_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{63-unknown_mutex_unlock_racing.c => 63-unknown_mutex_unlock_alternative_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{64-maybe_join_racing.c => 64-maybe_join_alternative_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{65-lock_from_same_thread_one_lockset_one_interthreaded_racing.c => 65-lock_from_same_thread_one_lockset_one_interthreaded_alternative_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{66-lock_from_same_thread_both_interthreaded_racing.c => 66-lock_from_same_thread_both_interthreaded_alternative_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{67-ambiguous_context_racing.c => 67-ambiguous_context_alternative_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{70-multiple_create_statements_racing.c => 70-multiple_create_statements_alternative_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{71-diamond_racing.c => 71-diamond_alternative_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{72-circle_racing.c => 72-circle_alternative_racing.c} (100%) diff --git a/tests/regression/90-races_ancestor_locksets/50-lockset_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/50-lockset_inter_threaded_lock_alternative_racefree.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/50-lockset_inter_threaded_lock_racefree.c rename to tests/regression/90-races_ancestor_locksets/50-lockset_inter_threaded_lock_alternative_racefree.c diff --git a/tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_alternative_alternative_racefree.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_racefree.c rename to tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_alternative_alternative_racefree.c diff --git a/tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_alternative_racefree.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_racefree.c rename to tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_alternative_racefree.c diff --git a/tests/regression/90-races_ancestor_locksets/53-both_inter_threaded_lockset_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/53-both_inter_threaded_lockset_transitive_alternative_racefree.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/53-both_inter_threaded_lockset_transitive_racefree.c rename to tests/regression/90-races_ancestor_locksets/53-both_inter_threaded_lockset_transitive_alternative_racefree.c diff --git a/tests/regression/90-races_ancestor_locksets/54-never_unlock_never_join_racefree.c b/tests/regression/90-races_ancestor_locksets/54-never_unlock_never_join_alternative_racefree.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/54-never_unlock_never_join_racefree.c rename to tests/regression/90-races_ancestor_locksets/54-never_unlock_never_join_alternative_racefree.c diff --git a/tests/regression/90-races_ancestor_locksets/55-maybe_create_racefree.c b/tests/regression/90-races_ancestor_locksets/55-maybe_create_alternative_racefree.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/55-maybe_create_racefree.c rename to tests/regression/90-races_ancestor_locksets/55-maybe_create_alternative_racefree.c diff --git a/tests/regression/90-races_ancestor_locksets/60-maybe_lock_racing.c b/tests/regression/90-races_ancestor_locksets/60-maybe_lock_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/60-maybe_lock_racing.c rename to tests/regression/90-races_ancestor_locksets/60-maybe_lock_alternative_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/61-maybe_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/61-maybe_unlock_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/61-maybe_unlock_racing.c rename to tests/regression/90-races_ancestor_locksets/61-maybe_unlock_alternative_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/62-random_mutex_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/62-random_mutex_unlock_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/62-random_mutex_unlock_racing.c rename to tests/regression/90-races_ancestor_locksets/62-random_mutex_unlock_alternative_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/63-unknown_mutex_unlock_racing.c b/tests/regression/90-races_ancestor_locksets/63-unknown_mutex_unlock_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/63-unknown_mutex_unlock_racing.c rename to tests/regression/90-races_ancestor_locksets/63-unknown_mutex_unlock_alternative_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/64-maybe_join_racing.c b/tests/regression/90-races_ancestor_locksets/64-maybe_join_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/64-maybe_join_racing.c rename to tests/regression/90-races_ancestor_locksets/64-maybe_join_alternative_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/65-lock_from_same_thread_one_lockset_one_interthreaded_racing.c b/tests/regression/90-races_ancestor_locksets/65-lock_from_same_thread_one_lockset_one_interthreaded_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/65-lock_from_same_thread_one_lockset_one_interthreaded_racing.c rename to tests/regression/90-races_ancestor_locksets/65-lock_from_same_thread_one_lockset_one_interthreaded_alternative_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/66-lock_from_same_thread_both_interthreaded_racing.c b/tests/regression/90-races_ancestor_locksets/66-lock_from_same_thread_both_interthreaded_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/66-lock_from_same_thread_both_interthreaded_racing.c rename to tests/regression/90-races_ancestor_locksets/66-lock_from_same_thread_both_interthreaded_alternative_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/67-ambiguous_context_racing.c b/tests/regression/90-races_ancestor_locksets/67-ambiguous_context_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/67-ambiguous_context_racing.c rename to tests/regression/90-races_ancestor_locksets/67-ambiguous_context_alternative_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/70-multiple_create_statements_racing.c b/tests/regression/90-races_ancestor_locksets/70-multiple_create_statements_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/70-multiple_create_statements_racing.c rename to tests/regression/90-races_ancestor_locksets/70-multiple_create_statements_alternative_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/71-diamond_racing.c b/tests/regression/90-races_ancestor_locksets/71-diamond_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/71-diamond_racing.c rename to tests/regression/90-races_ancestor_locksets/71-diamond_alternative_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/72-circle_racing.c b/tests/regression/90-races_ancestor_locksets/72-circle_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/72-circle_racing.c rename to tests/regression/90-races_ancestor_locksets/72-circle_alternative_racing.c From edda5d866c3f2e05fd917c6f43e1e1164a1fae9c Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 20:09:15 +0100 Subject: [PATCH 86/95] one more norace test case --- .../06-convoluted_norace.c | 38 +++++++++++++++++++ .../56-convoluted_alternative_norace.c | 38 +++++++++++++++++++ 2 files changed, 76 insertions(+) create mode 100644 tests/regression/90-races_ancestor_locksets/06-convoluted_norace.c create mode 100644 tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_norace.c diff --git a/tests/regression/90-races_ancestor_locksets/06-convoluted_norace.c b/tests/regression/90-races_ancestor_locksets/06-convoluted_norace.c new file mode 100644 index 0000000000..317390ad1c --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/06-convoluted_norace.c @@ -0,0 +1,38 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER, mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2, id3; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void* t3(void* arg) { + global++; // NORACE + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + pthread_create(&id3, NULL, t3, NULL); + pthread_mutex_lock(&mutex); // irrelevant lock/unlock + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); // lock and unlock mutex before creation + pthread_mutex_unlock(&mutex); + pthread_mutex_lock(&mutex); + pthread_mutex_lock(&mutex1); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_unlock(&mutex1); // unlock unrelated mutex before joining + pthread_join(id3, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_norace.c b/tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_norace.c new file mode 100644 index 0000000000..e8db3cd798 --- /dev/null +++ b/tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_norace.c @@ -0,0 +1,38 @@ +// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] creationLocksetAlternative --set ana.activated[+] taintedCreationLocksetAlternative +#include + +int global = 0; +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER, mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_t id1, id2, id3; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex); + global++; // NORACE + pthread_mutex_unlock(&mutex); + return NULL; +} + +void* t3(void* arg) { + global++; // NORACE + return NULL; +} + +void *t2(void *arg) { // t2 is protected by mutex locked in main thread + pthread_create(&id3, NULL, t3, NULL); + pthread_mutex_lock(&mutex); // irrelevant lock/unlock + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(void) { + pthread_create(&id1, NULL, t1, NULL); + pthread_mutex_lock(&mutex); // lock and unlock mutex before creation + pthread_mutex_unlock(&mutex); + pthread_mutex_lock(&mutex); + pthread_mutex_lock(&mutex1); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_unlock(&mutex1); // unlock unrelated mutex before joining + pthread_join(id3, NULL); + pthread_mutex_unlock(&mutex); + return 0; +} From b011914672c14476aa86613d809539fe96d9117b Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 20:13:13 +0100 Subject: [PATCH 87/95] consistant * style in tests --- .../01-both_inter_threaded_lock_racefree.c | 2 +- .../02-lockset_inter_threaded_lock_transitive_racefree.c | 2 +- .../90-races_ancestor_locksets/06-convoluted_norace.c | 2 +- .../90-races_ancestor_locksets/17-ambiguous_context_racing.c | 2 +- .../regression/90-races_ancestor_locksets/21-diamond_racing.c | 4 ++-- .../regression/90-races_ancestor_locksets/22-circle_racing.c | 2 +- ...oth_inter_threaded_lock_alternative_alternative_racefree.c | 2 +- ...kset_inter_threaded_lock_transitive_alternative_racefree.c | 2 +- .../56-convoluted_alternative_norace.c | 2 +- .../67-ambiguous_context_alternative_racing.c | 2 +- .../71-diamond_alternative_racing.c | 4 ++-- .../90-races_ancestor_locksets/72-circle_alternative_racing.c | 2 +- 12 files changed, 14 insertions(+), 14 deletions(-) diff --git a/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c b/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c index 81624ab563..f60144bfe2 100644 --- a/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/01-both_inter_threaded_lock_racefree.c @@ -5,7 +5,7 @@ int global = 0; pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; pthread_t id_main_child, id_1, id_1_child; -void *t1_child_fun(void* arg) { // t1child is protected by mutex locked in t1 +void *t1_child_fun(void *arg) { // t1child is protected by mutex locked in t1 global++; // NORACE return NULL; } diff --git a/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c b/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c index 730dfe6f9a..bc44ac8aa9 100644 --- a/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/02-lockset_inter_threaded_lock_transitive_racefree.c @@ -12,7 +12,7 @@ void *t1(void *arg) { return NULL; } -void* t3(void* arg) { +void *t3(void* arg) { global++; // NORACE return NULL; } diff --git a/tests/regression/90-races_ancestor_locksets/06-convoluted_norace.c b/tests/regression/90-races_ancestor_locksets/06-convoluted_norace.c index 317390ad1c..d89f94fb44 100644 --- a/tests/regression/90-races_ancestor_locksets/06-convoluted_norace.c +++ b/tests/regression/90-races_ancestor_locksets/06-convoluted_norace.c @@ -12,7 +12,7 @@ void *t1(void *arg) { return NULL; } -void* t3(void* arg) { +void *t3(void* arg) { global++; // NORACE return NULL; } diff --git a/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c b/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c index 4d7708e5de..8eb9fe5fbe 100644 --- a/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c +++ b/tests/regression/90-races_ancestor_locksets/17-ambiguous_context_racing.c @@ -7,7 +7,7 @@ pthread_t id1, id2; // both accesses are protected by same mutex **locked in same thread** -void* t1(void* arg) { +void *t1(void* arg) { pthread_mutex_lock(&mutex); global++; // RACE! pthread_mutex_unlock(&mutex); diff --git a/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c b/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c index 2f86abf974..824cb38859 100644 --- a/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c +++ b/tests/regression/90-races_ancestor_locksets/21-diamond_racing.c @@ -12,12 +12,12 @@ void *t1(void *arg) { return NULL; } -void* t4(void* arg) { // t4 is not protected by mutex, since it is created twice and the creation in t2 does not happen with mutex locked +void *t4(void* arg) { // t4 is not protected by mutex, since it is created twice and the creation in t2 does not happen with mutex locked global++; // RACE! return NULL; } -void* t3(void* arg) { +void *t3(void* arg) { pthread_mutex_lock(&mutex); pthread_create(&id4_2, NULL, t4, NULL); pthread_join(id4_2, NULL); diff --git a/tests/regression/90-races_ancestor_locksets/22-circle_racing.c b/tests/regression/90-races_ancestor_locksets/22-circle_racing.c index 7a76bffba1..7c73611db4 100644 --- a/tests/regression/90-races_ancestor_locksets/22-circle_racing.c +++ b/tests/regression/90-races_ancestor_locksets/22-circle_racing.c @@ -15,7 +15,7 @@ void *t1(void *arg) { return NULL; } -void* tc1(void* arg); +void *tc1(void* arg); void *tc2(void *arg) { pthread_t idc1; diff --git a/tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_alternative_alternative_racefree.c b/tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_alternative_alternative_racefree.c index dc7142e882..724d63afc6 100644 --- a/tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_alternative_alternative_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/51-both_inter_threaded_lock_alternative_alternative_racefree.c @@ -5,7 +5,7 @@ int global = 0; pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; pthread_t id_main_child, id_1, id_1_child; -void *t1_child_fun(void* arg) { // t1child is protected by mutex locked in t1 +void *t1_child_fun(void *arg) { // t1child is protected by mutex locked in t1 global++; // NORACE return NULL; } diff --git a/tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_alternative_racefree.c b/tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_alternative_racefree.c index 3c1812f1f9..8913d336e2 100644 --- a/tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_alternative_racefree.c +++ b/tests/regression/90-races_ancestor_locksets/52-lockset_inter_threaded_lock_transitive_alternative_racefree.c @@ -12,7 +12,7 @@ void *t1(void *arg) { return NULL; } -void* t3(void* arg) { +void *t3(void* arg) { global++; // NORACE return NULL; } diff --git a/tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_norace.c b/tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_norace.c index e8db3cd798..ddfe925214 100644 --- a/tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_norace.c +++ b/tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_norace.c @@ -12,7 +12,7 @@ void *t1(void *arg) { return NULL; } -void* t3(void* arg) { +void *t3(void* arg) { global++; // NORACE return NULL; } diff --git a/tests/regression/90-races_ancestor_locksets/67-ambiguous_context_alternative_racing.c b/tests/regression/90-races_ancestor_locksets/67-ambiguous_context_alternative_racing.c index f3fd45a417..a80622f5c7 100644 --- a/tests/regression/90-races_ancestor_locksets/67-ambiguous_context_alternative_racing.c +++ b/tests/regression/90-races_ancestor_locksets/67-ambiguous_context_alternative_racing.c @@ -7,7 +7,7 @@ pthread_t id1, id2; // both accesses are protected by same mutex **locked in same thread** -void* t1(void* arg) { +void *t1(void* arg) { pthread_mutex_lock(&mutex); global++; // RACE! pthread_mutex_unlock(&mutex); diff --git a/tests/regression/90-races_ancestor_locksets/71-diamond_alternative_racing.c b/tests/regression/90-races_ancestor_locksets/71-diamond_alternative_racing.c index 0cfa6a8442..0cd74dca39 100644 --- a/tests/regression/90-races_ancestor_locksets/71-diamond_alternative_racing.c +++ b/tests/regression/90-races_ancestor_locksets/71-diamond_alternative_racing.c @@ -12,12 +12,12 @@ void *t1(void *arg) { return NULL; } -void* t4(void* arg) { // t4 is not protected by mutex, since it is created twice and the creation in t2 does not happen with mutex locked +void *t4(void* arg) { // t4 is not protected by mutex, since it is created twice and the creation in t2 does not happen with mutex locked global++; // RACE! return NULL; } -void* t3(void* arg) { +void *t3(void* arg) { pthread_mutex_lock(&mutex); pthread_create(&id4_2, NULL, t4, NULL); pthread_join(id4_2, NULL); diff --git a/tests/regression/90-races_ancestor_locksets/72-circle_alternative_racing.c b/tests/regression/90-races_ancestor_locksets/72-circle_alternative_racing.c index 50fcc1b9f2..eb89648144 100644 --- a/tests/regression/90-races_ancestor_locksets/72-circle_alternative_racing.c +++ b/tests/regression/90-races_ancestor_locksets/72-circle_alternative_racing.c @@ -15,7 +15,7 @@ void *t1(void *arg) { return NULL; } -void* tc1(void* arg); +void *tc1(void* arg); void *tc2(void *arg) { pthread_t idc1; From 8aa1490834533e9226de73bfb327ed9c7abe578f Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 20:14:14 +0100 Subject: [PATCH 88/95] circle -> cycle --- .../{22-circle_racing.c => 22-cycle_racing.c} | 0 ...-circle_alternative_racing.c => 72-cycle_alternative_racing.c} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/90-races_ancestor_locksets/{22-circle_racing.c => 22-cycle_racing.c} (100%) rename tests/regression/90-races_ancestor_locksets/{72-circle_alternative_racing.c => 72-cycle_alternative_racing.c} (100%) diff --git a/tests/regression/90-races_ancestor_locksets/22-circle_racing.c b/tests/regression/90-races_ancestor_locksets/22-cycle_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/22-circle_racing.c rename to tests/regression/90-races_ancestor_locksets/22-cycle_racing.c diff --git a/tests/regression/90-races_ancestor_locksets/72-circle_alternative_racing.c b/tests/regression/90-races_ancestor_locksets/72-cycle_alternative_racing.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/72-circle_alternative_racing.c rename to tests/regression/90-races_ancestor_locksets/72-cycle_alternative_racing.c From 57cf4a8ca5e8f53577c0d0715daf029265d5816e Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 20:44:26 +0100 Subject: [PATCH 89/95] clean up creation lockset alternative file --- src/analyses/creationLocksetAlternative.ml | 41 +++++++--------------- 1 file changed, 13 insertions(+), 28 deletions(-) diff --git a/src/analyses/creationLocksetAlternative.ml b/src/analyses/creationLocksetAlternative.ml index 70b6cd4c65..c147bc6bc5 100644 --- a/src/analyses/creationLocksetAlternative.ml +++ b/src/analyses/creationLocksetAlternative.ml @@ -37,16 +37,11 @@ module CreationLocksetAlternative = struct let to_contribute = G.singleton tid lockset in man.sideg child_tid to_contribute | _ -> () - ;; let query man (type a) (x : a Queries.t) : a Queries.result = match x with - | Queries.CreationLocksetAlternative tid -> - Logs.result "query"; - Logs.result "query %a" G.pretty (man.global tid); - (man.global tid : G.t) + | Queries.CreationLocksetAlternative tid -> (man.global tid : G.t) | _ -> Queries.Result.top x - ;; end module TaintedCreationLocksetAlternative = struct @@ -58,8 +53,8 @@ module TaintedCreationLocksetAlternative = struct include StdV end - module Range = MapDomain.MapBot (LID) (TIDs) - module G = MapDomain.MapBot (TID) (Range) + module LockToThreads = MapDomain.MapBot (LID) (TIDs) + module G = MapDomain.MapBot (TID) (LockToThreads) let name () = "taintedCreationLocksetAlternative" let startstate _ = D.bot () @@ -68,41 +63,36 @@ module TaintedCreationLocksetAlternative = struct let get_unique_created_children tid (ask : Queries.ask) = let created_threads = ask.f Queries.CreatedThreads in TIDs.filter (TID.must_be_ancestor tid) created_threads - ;; (** handle unlock of mutex [lock] *) let unlock man tid created_tids lock = - Logs.result "u"; let ask = ask_of_man man in let joinedThreads = ask.f Queries.MustJoinedThreads in let contribute_lock child_tid = - let to_contribute = G.singleton tid (Range.singleton lock joinedThreads) in + let to_contribute = G.singleton tid (LockToThreads.singleton lock joinedThreads) in man.sideg child_tid to_contribute in TIDs.iter contribute_lock created_tids - ;; (** handle unlock of an unknown mutex. Assumes that any mutex could have been unlocked *) let unknown_unlock man tid created_tids = - Logs.result "uu"; let ask = ask_of_man man in let evaporate_locksets child_tid = let allCreationLocksets = ask.f @@ Queries.CreationLocksetAlternative child_tid in let creationLockset = CreationLocksetAlternative.G.find tid allCreationLocksets in let to_contribute_value = LIDs.fold - (fun lock acc -> Range.join acc (Range.singleton lock (TIDs.empty ()))) + (fun lock acc -> + LockToThreads.join acc (LockToThreads.singleton lock (TIDs.empty ()))) creationLockset - (Range.empty ()) + (LockToThreads.empty ()) in let to_contribute = G.singleton tid to_contribute_value in man.sideg child_tid to_contribute in TIDs.iter evaporate_locksets created_tids - ;; let event man e _ = - Logs.result "e"; match e with | Events.Unlock addr -> let ask = ask_of_man man in @@ -116,7 +106,6 @@ module TaintedCreationLocksetAlternative = struct | None -> unknown_unlock man tid created_tids) | _ -> ()) | _ -> () - ;; module A = struct (** ego tid * must-lockset * creation-lockset *) @@ -137,7 +126,6 @@ module TaintedCreationLocksetAlternative = struct cl2 in Queries.CLS.exists cl2_has_same_lock_other_tid cl1 - ;; (** checks if [cl1] has a mapping ([tp1] |-> [ls1]) such that [ls1] and [ls2] are not disjoint and [tp1] != [t2] @@ -150,46 +138,45 @@ module TaintedCreationLocksetAlternative = struct Queries.CLS.exists (fun tp1 ls1 -> not (LIDs.disjoint ls1 ls2 || TID.equal tp1 t2)) cl1 - ;; let may_race (t1, ls1, cl1) (t2, ls2, cl2) = not (both_protected_inter_threaded cl1 cl2 || one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 || one_protected_inter_threaded_other_intra_threaded cl2 t1 ls1) - ;; let should_print (_t, _ls, cl) = not @@ Queries.CLS.is_empty cl end let access man _ = - Logs.result "a"; let ask = Analyses.ask_of_man man in let tid_lifted = ask.f Queries.CurrentThreadId in match tid_lifted with | `Lifted td -> let must_ancestors = TID.must_ancestors td in + let compute_cl_transitive () = - Logs.result "clt1 %a" TID.pretty td; let cl_td = ask.f @@ Queries.CreationLocksetAlternative td in - Logs.result "clt2"; List.fold_left (fun acc t1 -> Queries.CLS.join acc (ask.f @@ Queries.CreationLocksetAlternative t1)) cl_td must_ancestors in + let compute_tcl_transitive () = let tcl_td = man.global td in List.fold_left (fun acc t1 -> G.join acc (man.global t1)) tcl_td must_ancestors in + let compute_tcl_lockset tcl_transitive t0 = let tcl_transitive_t0 = G.find t0 tcl_transitive in - Range.fold + LockToThreads.fold (fun l j acc -> if TIDs.mem td j then acc else LIDs.add l acc) tcl_transitive_t0 (LIDs.empty ()) in + let compute_il cl_transitive tcl_transitive = Queries.CLS.fold (fun t0 l_cl acc -> @@ -199,23 +186,21 @@ module TaintedCreationLocksetAlternative = struct cl_transitive (Queries.CLS.empty ()) in + let lockset = ask.f Queries.MustLockset in let cl_transitive = compute_cl_transitive () in let tcl_transitive = compute_tcl_transitive () in let il = compute_il cl_transitive tcl_transitive in td, lockset, il | _ -> ThreadIdDomain.UnknownThread, LIDs.empty (), Queries.CLS.empty () - ;; end let _ = MCP.register_analysis ~dep:[ "threadid"; "mutex"; "race" ] (module CreationLocksetAlternative : MCPSpec) -;; let _ = MCP.register_analysis ~dep:[ "threadid"; "mutex"; "race"; "creationLocksetAlternative" ] (module TaintedCreationLocksetAlternative : MCPSpec) -;; From 82ecd93fd699cabb6229eb5a9275bc1e431e4cb7 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 20:47:09 +0100 Subject: [PATCH 90/95] fix dependency analyses names --- src/analyses/creationLockset.ml | 2 +- src/analyses/creationLocksetAlternative.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 073eb86744..b3e4e02dc1 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -159,5 +159,5 @@ end let _ = MCP.register_analysis - ~dep:[ "threadid"; "mutex"; "race"; "threadJoins"; "threadDescendants" ] + ~dep:[ "threadid"; "mutex"; "threadJoins"; "threadDescendants" ] (module Spec : MCPSpec) diff --git a/src/analyses/creationLocksetAlternative.ml b/src/analyses/creationLocksetAlternative.ml index c147bc6bc5..3443ed21c1 100644 --- a/src/analyses/creationLocksetAlternative.ml +++ b/src/analyses/creationLocksetAlternative.ml @@ -197,10 +197,10 @@ end let _ = MCP.register_analysis - ~dep:[ "threadid"; "mutex"; "race" ] + ~dep:[ "threadid"; "mutex"; "threadJoins" ] (module CreationLocksetAlternative : MCPSpec) let _ = MCP.register_analysis - ~dep:[ "threadid"; "mutex"; "race"; "creationLocksetAlternative" ] + ~dep:[ "threadid"; "mutex"; "threadJoins"; "creationLocksetAlternative" ] (module TaintedCreationLocksetAlternative : MCPSpec) From 135ce02320787b93658d643645aa31b2848c0d8a Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 20:56:39 +0100 Subject: [PATCH 91/95] update module comments for alternative creation lockset analysis --- src/analyses/creationLocksetAlternative.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/analyses/creationLocksetAlternative.ml b/src/analyses/creationLocksetAlternative.ml index 3443ed21c1..b0c7beff48 100644 --- a/src/analyses/creationLocksetAlternative.ml +++ b/src/analyses/creationLocksetAlternative.ml @@ -1,7 +1,4 @@ -(** creation lockset analysis [creationLocksetAlternative] - constructs edges on the graph over all threads, where the edges are labelled with must-locksets: - (t_1) ---L--> (t_0) means that t_1 is protected by all members of L from t_0 - +(** alternative creation lockset analysis @see https://github.com/goblint/analyzer/pull/1865 *) @@ -11,6 +8,10 @@ module TIDs = ConcDomain.MustThreadSet module LID = LockDomain.MustLock module LIDs = LockDomain.MustLockset +(** [creationLocksetAlternative] + collects parent threads, which could protect the ego thread and its descendants, + since the creation must happen with a lock held. +*) module CreationLocksetAlternative = struct include IdentityUnitContextsSpec module D = Lattice.Unit @@ -44,6 +45,10 @@ module CreationLocksetAlternative = struct | _ -> Queries.Result.top x end +(** [taintedCreationLocksetAlternative] + collects parent threads, which cannot protect the ego thread and its descendants, + since an unlock could happen before joining +*) module TaintedCreationLocksetAlternative = struct include IdentityUnitContextsSpec module D = Lattice.Unit From 2054f591a20cab27712cca25ac1e80519eb3f95a Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 21:00:00 +0100 Subject: [PATCH 92/95] cl -> il in A module of alternative analysis --- src/analyses/creationLocksetAlternative.ml | 28 +++++++++++----------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/analyses/creationLocksetAlternative.ml b/src/analyses/creationLocksetAlternative.ml index b0c7beff48..6f75aaa648 100644 --- a/src/analyses/creationLocksetAlternative.ml +++ b/src/analyses/creationLocksetAlternative.ml @@ -118,37 +118,37 @@ module TaintedCreationLocksetAlternative = struct let name () = "creationLockset" - (** checks if [cl1] has a member ([tp1] |-> [ls1]) and [cl2] has a member ([tp2] |-> [ls2]) + (** checks if [il1] has a member ([tp1] |-> [ls1]) and [il2] has a member ([tp2] |-> [ls2]) such that [ls1] and [ls2] are not disjoint and [tp1] != [tp2] - @param cl1 creation-lockset of first thread [t1] - @param cl2 creation-lockset of second thread [t2] + @param il1 creation-lockset of first thread [t1] + @param il2 creation-lockset of second thread [t2] @returns whether [t1] and [t2] must be running mutually exclusive *) - let both_protected_inter_threaded cl1 cl2 = + let both_protected_inter_threaded il1 il2 = let cl2_has_same_lock_other_tid tp1 ls1 = Queries.CLS.exists (fun tp2 ls2 -> not (LIDs.disjoint ls1 ls2 || TID.equal tp1 tp2)) - cl2 + il2 in - Queries.CLS.exists cl2_has_same_lock_other_tid cl1 + Queries.CLS.exists cl2_has_same_lock_other_tid il1 - (** checks if [cl1] has a mapping ([tp1] |-> [ls1]) + (** checks if [il1] has a mapping ([tp1] |-> [ls1]) such that [ls1] and [ls2] are not disjoint and [tp1] != [t2] - @param cl1 creation-lockset of thread [t1] at first program point + @param il1 creation-lockset of thread [t1] at first program point @param t2 thread id at second program point @param ls2 lockset at second program point @returns whether [t1] must be running mutually exclusive with second program point *) - let one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 = + let one_protected_inter_threaded_other_intra_threaded il1 t2 ls2 = Queries.CLS.exists (fun tp1 ls1 -> not (LIDs.disjoint ls1 ls2 || TID.equal tp1 t2)) - cl1 + il1 - let may_race (t1, ls1, cl1) (t2, ls2, cl2) = + let may_race (t1, ls1, il1) (t2, ls2, il2) = not - (both_protected_inter_threaded cl1 cl2 - || one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 - || one_protected_inter_threaded_other_intra_threaded cl2 t1 ls1) + (both_protected_inter_threaded il1 il2 + || one_protected_inter_threaded_other_intra_threaded il1 t2 ls2 + || one_protected_inter_threaded_other_intra_threaded il2 t1 ls1) let should_print (_t, _ls, cl) = not @@ Queries.CLS.is_empty cl end From 6b8c3f33cc8824488fba90d9fdf9141c6fb81897 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 21:12:03 +0100 Subject: [PATCH 93/95] restructure unlock and unknown unlock of alternative creation lockset analysis --- src/analyses/creationLocksetAlternative.ml | 25 +++++++++++----------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/src/analyses/creationLocksetAlternative.ml b/src/analyses/creationLocksetAlternative.ml index 6f75aaa648..56c3d7e7ef 100644 --- a/src/analyses/creationLocksetAlternative.ml +++ b/src/analyses/creationLocksetAlternative.ml @@ -70,32 +70,30 @@ module TaintedCreationLocksetAlternative = struct TIDs.filter (TID.must_be_ancestor tid) created_threads (** handle unlock of mutex [lock] *) - let unlock man tid created_tids lock = - let ask = ask_of_man man in - let joinedThreads = ask.f Queries.MustJoinedThreads in + let unlock man tid created_tids joined_tids lock = let contribute_lock child_tid = - let to_contribute = G.singleton tid (LockToThreads.singleton lock joinedThreads) in + let to_contribute = G.singleton tid (LockToThreads.singleton lock joined_tids) in man.sideg child_tid to_contribute in TIDs.iter contribute_lock created_tids (** handle unlock of an unknown mutex. Assumes that any mutex could have been unlocked *) - let unknown_unlock man tid created_tids = + let unknown_unlock man tid created_tids joined_tids = let ask = ask_of_man man in - let evaporate_locksets child_tid = - let allCreationLocksets = ask.f @@ Queries.CreationLocksetAlternative child_tid in - let creationLockset = CreationLocksetAlternative.G.find tid allCreationLocksets in + let contribute_all_locks child_tid = + let all_creation_locksets = ask.f @@ Queries.CreationLocksetAlternative child_tid in + let creation_lockset = CreationLocksetAlternative.G.find tid all_creation_locksets in let to_contribute_value = LIDs.fold (fun lock acc -> - LockToThreads.join acc (LockToThreads.singleton lock (TIDs.empty ()))) - creationLockset + LockToThreads.join acc (LockToThreads.singleton lock joined_tids)) + creation_lockset (LockToThreads.empty ()) in let to_contribute = G.singleton tid to_contribute_value in man.sideg child_tid to_contribute in - TIDs.iter evaporate_locksets created_tids + TIDs.iter contribute_all_locks created_tids let event man e _ = match e with @@ -105,10 +103,11 @@ module TaintedCreationLocksetAlternative = struct (match tid_lifted with | `Lifted tid -> let created_tids = get_unique_created_children tid ask in + let joined_tids = ask.f Queries.MustJoinedThreads in let lock_opt = LockDomain.MustLock.of_addr addr in (match lock_opt with - | Some lock -> unlock man tid created_tids lock - | None -> unknown_unlock man tid created_tids) + | Some lock -> unlock man tid created_tids joined_tids lock + | None -> unknown_unlock man tid created_tids joined_tids) | _ -> ()) | _ -> () From 0df9c7613f3765333ca8a3b32a9ab0a1ce6cc34f Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 22:17:14 +0100 Subject: [PATCH 94/95] update outdated comment in thread id domain --- src/cdomain/value/cdomains/threadIdDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index a8073e96ba..faa248818a 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -18,7 +18,7 @@ sig (** Is the first TID a must ancestor of the second thread. Always false if the first TID is not unique *) val must_be_ancestor: t -> t -> bool - (** Every TID of the returned list must be an ancestor of the passed TID. Return None if the result cannot be determined *) + (** Every TID of the returned list must be an ancestor of the passed TID *) val must_ancestors: t -> t list end From 00ca4df1d389663a2b1ae8b625b54b1a5897a485 Mon Sep 17 00:00:00 2001 From: dabund24 Date: Mon, 15 Dec 2025 22:18:05 +0100 Subject: [PATCH 95/95] norace -> racefree aligning test names with those of other tests --- .../{06-convoluted_norace.c => 06-convoluted_racefree.c} | 0 ..._alternative_norace.c => 56-convoluted_alternative_racefree.c} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/90-races_ancestor_locksets/{06-convoluted_norace.c => 06-convoluted_racefree.c} (100%) rename tests/regression/90-races_ancestor_locksets/{56-convoluted_alternative_norace.c => 56-convoluted_alternative_racefree.c} (100%) diff --git a/tests/regression/90-races_ancestor_locksets/06-convoluted_norace.c b/tests/regression/90-races_ancestor_locksets/06-convoluted_racefree.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/06-convoluted_norace.c rename to tests/regression/90-races_ancestor_locksets/06-convoluted_racefree.c diff --git a/tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_norace.c b/tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_racefree.c similarity index 100% rename from tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_norace.c rename to tests/regression/90-races_ancestor_locksets/56-convoluted_alternative_racefree.c