Merge branch 'goblint:master' into master

goblint.opam

@@ -98,7 +98,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
   # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
+  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
   [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release

goblint.opam.locked

@@ -140,7 +140,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.5"
-    "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd"
+    "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f"
   ]
   [
     "camlidl.1.12"

goblint.opam.template

@@ -3,7 +3,7 @@
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
   # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
+  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
   [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release

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

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

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:

src/framework/analyses.ml

@@ -1,6 +1,5 @@
 (** {{!Spec} Analysis specification} and {{!MonSystem} constraint system} signatures. *)
 
-open Batteries
 open GoblintCil
 open Pretty
 open GobConfig

src/witness/yamlWitnessType.ml

@@ -463,7 +463,6 @@ struct
         | Int i -> GobYaml.int i
 
       let of_yaml y =
-        let open GobYaml in
         match y with
         | `String s -> Ok (String s)
         | `Float f -> Ok (Int (int_of_float f))

tests/regression/03-practical/31-zstd-cctxpool-blobs.c

@@ -21,7 +21,7 @@ int main() {
 
   ZSTDMT_CCtxPool* const cctxPool = calloc(1, sizeof(ZSTDMT_CCtxPool));
   cctxPool->cctx[0] = malloc(sizeof(ZSTD_CCtx));
-  if (!cctxPool->cctx[0]) // TODO NOWARN
+  if (!cctxPool->cctx[0]) // NOWARN (Trying to update a field, but the struct is unknown)
     __goblint_check(1); // reachable
   else
     __goblint_check(1); // reachable

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);
+  }
+}