Add may-ever-have-been-locked digests for relational mutex-meet

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

src/analyses/commonPriv.ml

@@ -185,6 +185,17 @@ struct
     | _ -> false
 end
 
+module LockDigest: Digest =
+struct
+  include PreValueDomain.AD
+
+  let current (ask: Q.ask) =
+    ask.f MayLocksDigest
+
+  let accounted_for (ask: Q.ask) ~(current: t) ~(other: t) =
+    false (* TODO *)
+end
+
 module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) =
 struct
   include ConfCheck.RequireThreadFlagPathSensInit

src/analyses/mayLocksDigest.ml

@@ -0,0 +1,49 @@
+(** May lockset digest analysis ([maylocksdigest]). *)
+
+open Analyses
+open GoblintCil
+module LF = LibraryFunctions
+
+module Arg =
+struct
+  module D = LockDomain.MayLocksetNoRW
+  module P = IdentityP (D)
+
+  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
+
+module Spec =
+struct
+  include LocksetAnalysis.MakeMay (Arg)
+  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 _ =
+  MCP.register_analysis ~dep:["mutexEvents"] (module Spec : MCPSpec)

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": {

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) =

tests/regression/46-apron2/58-lock-digest.c

@@ -0,0 +1,41 @@
+// 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>
+
+int g, h;
+pthread_mutex_t a = PTHREAD_MUTEX_INITIALIZER;
+
+void *t2(void *arg) {
+  pthread_mutex_lock(&a);
+  // wrong in more-traces!
+  __goblint_check(h < g); // TODO
+  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;
+}
+
+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;
+  pthread_mutex_unlock(&a);
+
+  pthread_create(&x, NULL, t1, NULL);
+  return 0;
+}