From 90f1a6204fb372476ec4f4a0a88dede8c119cf68 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 15:45:27 +0200 Subject: [PATCH] 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