Add MayLocksDigest query

goblint · Nov 30, 2023 · 90f1a62 · 90f1a62
1 parent 87e86ed
commit 90f1a62
Show file tree

Hide file tree

Showing 6 changed files with 25 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 <pthread.h>
 #include <goblint.h>