From 78a84849a019f39533d53be94c6c83871e583635 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 15:01:12 +0200 Subject: [PATCH 1/6] Add lock-digest example from more-traces --- tests/regression/46-apron2/58-lock-digest.c | 36 +++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 tests/regression/46-apron2/58-lock-digest.c diff --git a/tests/regression/46-apron2/58-lock-digest.c b/tests/regression/46-apron2/58-lock-digest.c new file mode 100644 index 0000000000..c77c1ab821 --- /dev/null +++ b/tests/regression/46-apron2/58-lock-digest.c @@ -0,0 +1,36 @@ +// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet +// TODO: why does this work? even with earlyglobs +#include +#include + +int g, h; +pthread_mutex_t a = PTHREAD_MUTEX_INITIALIZER; + +void *t2(void *arg) { + pthread_mutex_lock(&a); + __goblint_check(h <= g); // TODO: should be h < g? + pthread_mutex_unlock(&a); + return NULL; +} + +void *t1(void *arg) { + pthread_t x; + pthread_create(&x, NULL, t2, NULL); + + pthread_mutex_lock(&a); + h = 11; g = 12; + pthread_mutex_unlock(&a); + + return NULL; +} + +int main() { + pthread_mutex_lock(&a); + h = 9; + g = 10; + pthread_mutex_unlock(&a); + + pthread_t x; + pthread_create(&x, NULL, t1, NULL); + return 0; +} From 3f8c5d3d5dbbc7c29b83700f9e21050979716967 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 15:04:11 +0200 Subject: [PATCH 2/6] Add going multithreaded to lock-digest test --- tests/regression/46-apron2/58-lock-digest.c | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tests/regression/46-apron2/58-lock-digest.c b/tests/regression/46-apron2/58-lock-digest.c index c77c1ab821..454d1b586c 100644 --- a/tests/regression/46-apron2/58-lock-digest.c +++ b/tests/regression/46-apron2/58-lock-digest.c @@ -20,11 +20,17 @@ void *t1(void *arg) { pthread_mutex_lock(&a); h = 11; g = 12; pthread_mutex_unlock(&a); + return NULL; +} +void *t0(void *arg) { return NULL; } int main() { + pthread_t x; + pthread_create(&x, NULL, t0, NULL); // go multithreaded + pthread_mutex_lock(&a); h = 9; g = 10; From 8e557cae9ba1281c868b2f85dd95f24518d01fb8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 15:06:03 +0200 Subject: [PATCH 3/6] Fix lock-digest test --- tests/regression/46-apron2/58-lock-digest.c | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/tests/regression/46-apron2/58-lock-digest.c b/tests/regression/46-apron2/58-lock-digest.c index 454d1b586c..6b1f909982 100644 --- a/tests/regression/46-apron2/58-lock-digest.c +++ b/tests/regression/46-apron2/58-lock-digest.c @@ -1,5 +1,4 @@ // PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet -// TODO: why does this work? even with earlyglobs #include #include @@ -8,7 +7,8 @@ pthread_mutex_t a = PTHREAD_MUTEX_INITIALIZER; void *t2(void *arg) { pthread_mutex_lock(&a); - __goblint_check(h <= g); // TODO: should be h < g? + // wrong in more-traces! + __goblint_check(h < g); // TODO pthread_mutex_unlock(&a); return NULL; } @@ -36,7 +36,6 @@ int main() { g = 10; pthread_mutex_unlock(&a); - pthread_t x; pthread_create(&x, NULL, t1, NULL); return 0; } From 87e86ed62ceb05c55e20d48dca43e1c3ecd7e564 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 15:13:54 +0200 Subject: [PATCH 4/6] Add maylocksdigest analysis --- src/analyses/mayLocksDigest.ml | 30 +++++++++++++++++++++ tests/regression/46-apron2/58-lock-digest.c | 2 +- 2 files changed, 31 insertions(+), 1 deletion(-) create mode 100644 src/analyses/mayLocksDigest.ml diff --git a/src/analyses/mayLocksDigest.ml b/src/analyses/mayLocksDigest.ml new file mode 100644 index 0000000000..11b9a71094 --- /dev/null +++ b/src/analyses/mayLocksDigest.ml @@ -0,0 +1,30 @@ +(** May lockset digest analysis ([maylocksdigest]). *) + +open Analyses +open GoblintCil +module LF = LibraryFunctions + +module Arg:LocksetAnalysis.MayArg = +struct + module D = LockDomain.MayLocksetNoRW + module P = IdentityP (D) + module G = DefaultSpec.G + module V = DefaultSpec.V + + let add ctx (l,r) = + D.add l ctx.local + + let remove ctx l = + ctx.local +end + +module Spec = +struct + include LocksetAnalysis.MakeMay (Arg) + let name () = "maylocksdigest" + + let threadenter ctx ~multiple lval f args = [ctx.local] +end + +let _ = + MCP.register_analysis ~dep:["mutexEvents"] (module Spec : MCPSpec) diff --git a/tests/regression/46-apron2/58-lock-digest.c b/tests/regression/46-apron2/58-lock-digest.c index 6b1f909982..d1206df93b 100644 --- a/tests/regression/46-apron2/58-lock-digest.c +++ b/tests/regression/46-apron2/58-lock-digest.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet +// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.activated[+] maylocksdigest --set ana.path_sens[+] maylocksdigest #include #include From 90f1a6204fb372476ec4f4a0a88dede8c119cf68 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 15:45:27 +0200 Subject: [PATCH 5/6] Add MayLocksDigest query --- src/analyses/apron/relationPriv.apron.ml | 1 + src/analyses/commonPriv.ml | 11 +++++++++++ src/analyses/mayLocksDigest.ml | 7 ++++++- src/common/util/options.schema.json | 2 +- src/domains/queries.ml | 5 +++++ tests/regression/46-apron2/58-lock-digest.c | 2 +- 6 files changed, 25 insertions(+), 3 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index a34e052602..6ec20e7df4 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -1209,6 +1209,7 @@ let priv_module: (module S) Lazy.t = | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (Clustering2))) | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (ClusteringMax))) | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (ClusteringPower))) + | "mutex-meet-lock" -> (module PerMutexMeetPrivTID (LockDigest) (NoCluster)) | _ -> failwith "ana.relation.privatization: illegal value" ) in diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 2e7ed570fd..ff1d32dedd 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -185,6 +185,17 @@ struct | _ -> true end +module LockDigest: Digest = +struct + include PreValueDomain.AD + + let current (ask: Q.ask) = + ask.f MayLocksDigest + + let compatible (ask: Q.ask) (current: t) (other: t) = + true (* TODO *) +end + module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) = struct include ConfCheck.RequireThreadFlagPathSensInit diff --git a/src/analyses/mayLocksDigest.ml b/src/analyses/mayLocksDigest.ml index 11b9a71094..fa5ce7a3d7 100644 --- a/src/analyses/mayLocksDigest.ml +++ b/src/analyses/mayLocksDigest.ml @@ -4,7 +4,7 @@ open Analyses open GoblintCil module LF = LibraryFunctions -module Arg:LocksetAnalysis.MayArg = +module Arg = struct module D = LockDomain.MayLocksetNoRW module P = IdentityP (D) @@ -24,6 +24,11 @@ struct let name () = "maylocksdigest" let threadenter ctx ~multiple lval f args = [ctx.local] + + let query (ctx: (D.t, _, _, _) ctx) (type a) (q: a Queries.t): a Queries.result = + match q with + | MayLocksDigest -> ctx.local + | _ -> Queries.Result.top q end let _ = diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 7c921c4f53..fe55fe4ad7 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -921,7 +921,7 @@ "description": "Which relation privatization to use? top/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power", "type": "string", - "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"], + "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power", "mutex-meet-lock"], "default": "mutex-meet" }, "priv": { diff --git a/src/domains/queries.ml b/src/domains/queries.ml index b9fa28f5be..72ea5b3358 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -81,6 +81,7 @@ type _ t = | MayBePublicWithout: maybepublicwithout -> MayBool.t t | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t | MustLockset: AD.t t + | MayLocksDigest: AD.t t | MustBeAtomic: MustBool.t t | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t | MustBeUniqueThread: MustBool.t t @@ -200,6 +201,7 @@ struct | MustTermAllLoops -> (module MustBool) | IsEverMultiThreaded -> (module MayBool) | TmpSpecial _ -> (module ML) + | MayLocksDigest -> (module AD) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -268,6 +270,7 @@ struct | MustTermAllLoops -> MustBool.top () | IsEverMultiThreaded -> MayBool.top () | TmpSpecial _ -> ML.top () + | MayLocksDigest -> AD.top () end (* The type any_query can't be directly defined in Any as t, @@ -333,6 +336,7 @@ struct | Any IsEverMultiThreaded -> 55 | Any (TmpSpecial _) -> 56 | Any (IsAllocVar _) -> 57 + | Any MayLocksDigest -> 58 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -489,6 +493,7 @@ struct | Any MustTermAllLoops -> Pretty.dprintf "MustTermAllLoops" | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded" | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv + | Any MayLocksDigest -> Pretty.dprintf "MayLocksDigest" end let to_value_domain_ask (ask: ask) = diff --git a/tests/regression/46-apron2/58-lock-digest.c b/tests/regression/46-apron2/58-lock-digest.c index d1206df93b..d5b29449be 100644 --- a/tests/regression/46-apron2/58-lock-digest.c +++ b/tests/regression/46-apron2/58-lock-digest.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.activated[+] maylocksdigest --set ana.path_sens[+] maylocksdigest +// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-lock --set ana.activated[+] maylocksdigest --set ana.path_sens[+] maylocksdigest --set ana.path_sens[+] threadflag #include #include From 21e0644d56cd69f4f578e7f1e5b649b291e3c753 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 16:27:31 +0200 Subject: [PATCH 6/6] Add global invariant to maylocksdigest --- src/analyses/mayLocksDigest.ml | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/src/analyses/mayLocksDigest.ml b/src/analyses/mayLocksDigest.ml index fa5ce7a3d7..4f3bc5308d 100644 --- a/src/analyses/mayLocksDigest.ml +++ b/src/analyses/mayLocksDigest.ml @@ -8,13 +8,27 @@ module Arg = struct module D = LockDomain.MayLocksetNoRW module P = IdentityP (D) - module G = DefaultSpec.G - module V = DefaultSpec.V - let add ctx (l,r) = - D.add l ctx.local - - let remove ctx l = + module V = + struct + include StdV + include LockDomain.Addr + end + module G = SetDomain.Make (D) + + let add (ctx: (D.t, G.t, D.t, V.t) ctx) (l,r) = + let l's = ctx.global l in + G.iter (fun l' -> + if not (D.mem l ctx.local && not (D.mem l l')) then + ctx.split (D.add l (D.union ctx.local l')) [] + ) l's; + if D.mem l ctx.local then + raise Deadcode + else + D.add l ctx.local (* for initial empty *) + + let remove (ctx: (D.t, G.t, D.t, V.t) ctx) l = + ctx.sideg l (G.singleton ctx.local); ctx.local end