Merge pull request #1643 from goblint/lmust_cluster

michael-schwarz · web-flow · commit db4413b8438a · 2025-01-14T11:39:52.000+01:00
Relational MM: Cluster LMust
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
@@ -761,11 +761,15 @@ module type ClusterArg = functor (RD: RelationDomain.RD) ->
 sig
   module LRD: Lattice.S
 
+  module Cluster: Printable.S
+
   val keep_only_protected_globals: Q.ask -> LockDomain.MustLock.t -> LRD.t -> LRD.t
   val keep_global: varinfo -> LRD.t -> LRD.t
 
   val lock: RD.t -> LRD.t -> LRD.t -> RD.t
-  val unlock: W.t -> RD.t -> LRD.t
+  val unlock: W.t -> RD.t -> LRD.t * (Cluster.t list)
+
+  val filter_clusters: (Cluster.t -> bool) -> LRD.t -> LRD.t
 
   val name: unit -> string
 end
@@ -775,6 +779,7 @@ module NoCluster:ClusterArg = functor (RD: RelationDomain.RD) ->
 struct
   open CommonPerMutex(RD)
   module LRD = RD
+  module Cluster = Printable.Unit
 
   let keep_only_protected_globals = keep_only_protected_globals
 
@@ -786,7 +791,13 @@ struct
     RD.meet oct (RD.join local_m get_m)
 
   let unlock w oct_side =
-    oct_side
+    oct_side, [()]
+
+  let filter_clusters f oct =
+    if f () then
+      oct
+    else
+      RD.bot ()
 
   let name () = "no-clusters"
 end
@@ -860,6 +871,8 @@ struct
   module VS = SetDomain.Make (CilType.Varinfo)
   module LRD = MapDomain.MapBot (VS) (RD)
 
+  module Cluster = VS
+
   let keep_only_protected_globals ask m octs =
     (* normal (strong) mapping: contains only still fully protected *)
     (* must filter by protection to avoid later meeting with non-protecting *)
@@ -909,7 +922,10 @@ struct
     let oct_side_cluster gs =
       RD.keep_vars oct_side (gs |> VS.elements |> List.map V.global)
     in
-    LRD.add_list_fun clusters oct_side_cluster (LRD.empty ())
+    (LRD.add_list_fun clusters oct_side_cluster (LRD.empty ()), clusters)
+
+  let filter_clusters f oct =
+    LRD.filter (fun gs _ -> f gs) oct
 
   let name = ClusteringArg.name
 end
@@ -925,6 +941,8 @@ struct
   module LRD1 = DCCluster.LRD
   module LRD = Lattice.Prod (LRD1) (LRD1) (* second component is only used between keep_* and lock for additional weak mapping *)
 
+  module Cluster = DCCluster.Cluster
+
   let name = ClusteringArg.name
 
   let filter_map' f m =
@@ -986,7 +1004,11 @@ struct
     r
 
   let unlock w oct_side =
-    (DCCluster.unlock w oct_side, LRD1.bot ())
+    let lad, clusters = DCCluster.unlock w oct_side in
+    ((lad, LRD1.bot ()), clusters)
+
+  let filter_clusters f (lad,lad') =
+    (LRD1.filter (fun gs _ -> f gs) lad, LRD1.filter (fun gs _ -> f gs) lad')
 end
 
 (** Per-mutex meet with TIDs. *)
@@ -1000,7 +1022,7 @@ struct
   module Cluster = NC
   module LRD = NC.LRD
 
-  include PerMutexTidCommon (Digest) (LRD)
+  include PerMutexTidCommon (Digest) (LRD) (NC.Cluster)
 
   module AV = RD.V
   module P = UnitP
@@ -1022,13 +1044,11 @@ struct
     let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in
     if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n  get=%a" LockDomain.MustLock.pretty m LRD.pretty get_m;
     let r =
-      if not inits then
-        get_m
-      else
-        let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
-        let get_mutex_inits' = Cluster.keep_only_protected_globals ask m get_mutex_inits in
-        if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
-        LRD.join get_m get_mutex_inits'
+      let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+      let get_mutex_inits' = Cluster.keep_only_protected_globals ask m get_mutex_inits in
+      let get_mutex_inits' = Cluster.filter_clusters inits get_mutex_inits' in
+      if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
+      LRD.join get_m get_mutex_inits'
     in
     if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r;
     r
@@ -1047,25 +1067,21 @@ struct
     in
     if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
     let r =
-      if not inits then
-        get_mutex_global_g
-      else
-        let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
-        let get_mutex_inits' = Cluster.keep_global g get_mutex_inits in
-        if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
-        LRD.join get_mutex_global_g get_mutex_inits'
+      let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+      let get_mutex_inits' = Cluster.keep_global g get_mutex_inits in
+      let get_mutex_inits' = Cluster.filter_clusters inits get_mutex_inits' in
+      if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
+      LRD.join get_mutex_global_g get_mutex_inits'
     in
     if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r;
     r
 
   let get_mutex_global_g_with_mutex_inits_atomic inits ask getg =
     (* Unprotected invariant is one big relation. *)
     let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
-    if not inits then
-      get_mutex_global_g
-    else
-      let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
-      LRD.join get_mutex_global_g get_mutex_inits
+    let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+    let get_mutex_inits' = Cluster.filter_clusters inits get_mutex_inits in
+    LRD.join get_mutex_global_g get_mutex_inits'
 
   let read_global (ask: Q.ask) getg (st: relation_components_t) g x: RD.t =
     let atomic = Param.handle_atomic && ask.f MustBeAtomic in
@@ -1079,9 +1095,9 @@ struct
       if atomic && RD.mem_var rel (AV.global g) then
         rel (* Read previous unpublished unprotected write in current atomic section. *)
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg) (* Read unprotected invariant as full relation. *)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg) (* Read unprotected invariant as full relation. *)
       else
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg g)
     in
     (* read *)
     let g_var = AV.global g in
@@ -1113,9 +1129,9 @@ struct
       if atomic && RD.mem_var rel (AV.global g) then
         rel (* Read previous unpublished unprotected write in current atomic section. *)
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg) (* Read unprotected invariant as full relation. *)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg) (* Read unprotected invariant as full relation. *)
       else
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg g)
     in
     (* write *)
     let g_var = AV.global g in
@@ -1125,7 +1141,7 @@ struct
     (* unlock *)
     if not atomic then (
       let rel_side = RD.keep_vars rel_local [g_var] in
-      let rel_side = Cluster.unlock (W.singleton g) rel_side in
+      let rel_side, clusters = Cluster.unlock (W.singleton g) rel_side in
       let digest = Digest.current ask in
       let sidev = GMutex.singleton digest rel_side in
       if Param.handle_atomic then
@@ -1139,7 +1155,8 @@ struct
         else
           rel_local
       in
-      {rel = rel_local'; priv = (W.add g w,LMust.add lm lmust,l')}
+      let lmust' = List.fold (fun a c -> LMust.add (lm,c) a) lmust clusters in
+      {rel = rel_local'; priv = (W.add g w,lmust',l')}
     )
     else
       (* Delay publishing unprotected write in the atomic section. *)
@@ -1151,7 +1168,7 @@ struct
       let rel = st.rel in
       let _,lmust,l = st.priv in
       let lm = LLock.mutex m in
-      let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in
+      let get_m = get_m_with_mutex_inits (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg m in
       let local_m = BatOption.default (LRD.bot ()) (L.find_opt lm l) in
       (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
       let local_m = Cluster.keep_only_protected_globals ask m local_m in
@@ -1181,13 +1198,14 @@ struct
         {rel = rel_local; priv = (w',lmust,l)}
       else
         let rel_side = keep_only_protected_globals ask m rel in
-        let rel_side = Cluster.unlock w rel_side in
+        let rel_side, clusters = Cluster.unlock w rel_side in
         let digest = Digest.current ask in
         let sidev = GMutex.singleton digest rel_side in
         sideg (V.mutex m) (G.create_mutex sidev);
         let lm = LLock.mutex m in
         let l' = L.add lm rel_side l in
-        {rel = rel_local; priv = (w',LMust.add lm lmust,l')}
+        let lmust' = List.fold (fun a c -> LMust.add (lm,c) a) lmust clusters in
+        {rel = rel_local; priv = (w',lmust',l')}
     )
     else (
       (* Publish delayed unprotected write as if it were protected by the atomic section. *)
@@ -1198,14 +1216,15 @@ struct
         {rel = rel_local; priv = (w',lmust,l)}
       else
         let rel_side = keep_only_globals ask m rel in
-        let rel_side = Cluster.unlock w rel_side in
+        let rel_side, clusters = Cluster.unlock w rel_side in
         let digest = Digest.current ask in
         let sidev = GMutex.singleton digest rel_side in
         (* Unprotected invariant is one big relation. *)
         sideg (V.mutex atomic_mutex) (G.create_mutex sidev);
         let (lmust', l') = W.fold (fun g (lmust, l) ->
             let lm = LLock.global g in
-            (LMust.add lm lmust, L.add lm rel_side l)
+            let lmust'' = List.fold (fun a c -> LMust.add (lm,c) a) lmust clusters in
+            (lmust'', L.add lm rel_side l)
           ) w (lmust, l)
         in
         {rel = rel_local; priv = (w',lmust',l')}
@@ -1295,7 +1314,7 @@ struct
       ) (RD.vars rel)
     in
     let rel_side = RD.keep_vars rel g_vars in
-    let rel_side = Cluster.unlock (W.top ()) rel_side in (* top W to avoid any filtering *)
+    let rel_side, clusters = Cluster.unlock (W.top ()) rel_side in (* top W to avoid any filtering *)
     let digest = Digest.current ask in
     let sidev = GMutex.singleton digest rel_side in
     sideg V.mutex_inits (G.create_mutex sidev);
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
@@ -499,7 +499,7 @@ module PerMutexMeetTIDPriv (Digest: Digest): S =
 struct
   open Queries.Protection
   include PerMutexMeetPrivBase
-  include PerMutexTidCommon (Digest) (CPA)
+  include PerMutexTidCommonNC (Digest) (CPA)
 
   let iter_sys_vars getg vq vf =
     match vq with
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
@@ -237,7 +237,7 @@ struct
     | _ -> false
 end
 
-module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) =
+module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) (Cluster:Printable.S) =
 struct
   include ConfCheck.RequireThreadFlagPathSensInit
 
@@ -266,9 +266,9 @@ struct
     let global x = `Right x
   end
 
-  (** Mutexes / globals to which values have been published, i.e. for which the initializers need not be read **)
+  (** Mutexes / clusters of globals to which values have been published, i.e., for which the initializers need not be read **)
   module LMust = struct
-    include SetDomain.Reverse (SetDomain.ToppedSet (LLock) (struct let topname = "All locks" end))
+    include SetDomain.Reverse (SetDomain.ToppedSet (Printable.Prod(LLock)(Cluster)) (struct let topname = "All locks" end))
     let name () = "LMust"
   end
 
@@ -315,6 +315,14 @@ struct
   let startstate () = W.bot (), LMust.top (), L.bot ()
 end
 
+module PerMutexTidCommonNC (Digest: Digest) (LD:Lattice.S) = struct
+  include PerMutexTidCommon (Digest) (LD) (Printable.Unit)
+  module LMust = struct
+    include LMust
+    let mem lm lmust = mem (lm, ()) lmust
+    let add lm lmust = add (lm, ()) lmust
+  end
+end
 
 let lift_lock (ask: Q.ask) f st (addr: LockDomain.Addr.t) =
   (* Should be in sync with:
diff --git a/tests/regression/46-apron2/98-issue-1511b.c b/tests/regression/46-apron2/98-issue-1511b.c
@@ -0,0 +1,33 @@
+// CRAM
+#include<pthread.h>
+int d, j, k;
+
+pthread_mutex_t f;
+
+void nothing() {};
+void nothing2() {};
+
+int top() {
+  int top2;
+  return top2;
+}
+
+void main() {
+  d = top();
+  if (d) {
+    k = 1;
+    pthread_t tid;
+    pthread_create(&tid, 0, &nothing, NULL);
+    pthread_mutex_lock(&f);
+    j = 0; // To ensure something is published
+    pthread_mutex_unlock(&f);
+    pthread_mutex_lock(&f);
+
+    pthread_t tid2;
+    pthread_create(&tid2, 0, &nothing2, NULL);
+    float f = 8.0f;
+  } else {
+    pthread_t tid2;
+    pthread_create(&tid2, 0, &nothing2, NULL);
+  }
+}
diff --git a/tests/regression/46-apron2/98-issue-1511b.t b/tests/regression/46-apron2/98-issue-1511b.t
@@ -0,0 +1,44 @@
+  $ goblint --disable warn.unsound --disable warn.imprecise --disable sem.unknown_function.invalidate.globals --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 98-issue-1511b.c --set witness.yaml.path 98-issue-1511b.yml
+  [Info][Witness] witness generation summary:
+    location invariants: 52
+    loop invariants: 0
+    flow-insensitive invariants: 2
+    total generation entries: 29
+
+  $ goblint --disable warn.unsound --disable warn.imprecise --disable sem.unknown_function.invalidate.globals --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 98-issue-1511b.yml 98-issue-1511b.c
+  [Warning][Witness] cannot validate entry of type flow_insensitive_invariant
+  [Info][Witness] witness validation summary:
+    confirmed: 52
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 2
+    disabled: 0
+    total validation entries: 54
+  [Success][Witness] invariant confirmed: (1LL + (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (1LL - (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (2147483646LL + (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (2147483646LL - (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (2147483646LL - (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (2147483649LL + (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (1LL + (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (1LL - (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (2147483646LL + (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (2147483646LL - (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (2147483646LL - (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (2147483649LL + (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:27:5)
diff --git a/tests/regression/46-apron2/99-lmust-cluster-unsound.c b/tests/regression/46-apron2/99-lmust-cluster-unsound.c
