Merge pull request #1865 from dabund24/master

Improve MHP precision using ancestor locksets

Author: dabund24

src/analyses/creationLockset.ml

@@ -0,0 +1,156 @@
+(** creation lockset analysis [creationLockset]
+    constructs edges on the graph over all threads, where the edges are labelled with must-locksets:
+    (t_1) ---L--> (t_0) is represented by global t_1 t_0 = L and means that t_1 is protected by all members of L from t_0
+
+    @see https://github.com/goblint/analyzer/pull/1865
+*)
+
+open Analyses
+module TID = ThreadIdDomain.Thread
+module TIDs = ConcDomain.ThreadSet
+module Lock = LockDomain.MustLock
+module Lockset = LockDomain.MustLockset
+
+module Spec = struct
+  include IdentityUnitContextsSpec
+  module D = Lattice.Unit
+
+  module V = struct
+    include TID
+    include StdV
+  end
+
+  module G = MapDomain.MapBot (TID) (Lockset)
+
+  let name () = "creationLockset"
+  let startstate _ = D.bot ()
+  let exitstate _ = D.bot ()
+
+  (** register a global contribution: global.[child_tid] \supseteq [to_contribute]
+      @param man man at program point
+      @param to_contribute new edges from [child_tid] to ego thread to register
+      @param child_tid
+  *)
+  let contribute_locks man to_contribute child_tid = man.sideg child_tid to_contribute
+
+  (** reflexive-transitive closure of child relation applied to [tid]
+      and filtered to only include threads, where [tid] is a must-ancestor
+      @param man any man
+      @param tid
+  *)
+  let must_ancestor_descendants_closure man tid =
+    let descendants = man.ask @@ Queries.DescendantThreads tid in
+    let must_ancestors_descendants = TIDs.filter (TID.must_be_ancestor tid) descendants in
+    TIDs.add tid must_ancestors_descendants
+
+  let threadspawn man ~multiple lval f args fman =
+    let tid_lifted = man.ask Queries.CurrentThreadId in
+    let child_tid_lifted = fman.ask Queries.CurrentThreadId in
+    match tid_lifted, child_tid_lifted with
+    | `Lifted tid, `Lifted child_tid when TID.must_be_ancestor tid child_tid ->
+      let must_ancestor_descendants = must_ancestor_descendants_closure fman child_tid in
+      let lockset = man.ask Queries.MustLockset in
+      let to_contribute = G.singleton tid lockset in
+      TIDs.iter (contribute_locks man to_contribute) must_ancestor_descendants
+    | _ -> ()
+
+  (** compute all descendant threads that may run along with the ego thread at a program point.
+      for all of them, tid must be an ancestor
+      @param man man of ego thread at the program point
+      @param tid ego thread id
+  *)
+  let get_must_ancestor_running_descendants man tid =
+    let may_created_tids = man.ask Queries.CreatedThreads in
+    let may_must_ancestor_created_tids =
+      TIDs.filter (TID.must_be_ancestor tid) may_created_tids
+    in
+    let may_transitively_created_tids =
+      TIDs.fold
+        (fun child_tid acc -> TIDs.union acc (must_ancestor_descendants_closure man child_tid))
+        may_must_ancestor_created_tids
+        (TIDs.empty ())
+    in
+    let must_joined_tids = man.ask Queries.MustJoinedThreads in
+    TIDs.diff may_transitively_created_tids must_joined_tids
+
+  (** handle unlock of mutex [lock] *)
+  let unlock man tid possibly_running_tids lock =
+    let shrink_locksets des_tid =
+      let old_creation_lockset = G.find tid (man.global des_tid) in
+      (* Bot - {something} = Bot. This is exactly what we want in this case! *)
+      let updated_creation_lockset = Lockset.remove lock old_creation_lockset in
+      let to_contribute = G.singleton tid updated_creation_lockset in
+      man.sideg des_tid to_contribute
+    in
+    TIDs.iter shrink_locksets possibly_running_tids
+
+  (** handle unlock of an unknown mutex. Assumes that any mutex could have been unlocked *)
+  let unknown_unlock man tid possibly_running_tids =
+    let evaporate_locksets des_tid =
+      let to_contribute = G.singleton tid (Lockset.empty ()) in
+      man.sideg des_tid to_contribute
+    in
+    TIDs.iter evaporate_locksets possibly_running_tids
+
+  let event man e _ =
+    match e with
+    | Events.Unlock addr ->
+      let tid_lifted = man.ask Queries.CurrentThreadId in
+      (match tid_lifted with
+       | `Lifted tid ->
+         let possibly_running_tids = get_must_ancestor_running_descendants man tid in
+         let lock_opt = LockDomain.MustLock.of_addr addr in
+         (match lock_opt with
+          | Some lock -> unlock man tid possibly_running_tids lock
+          | None -> unknown_unlock man tid possibly_running_tids)
+       | _ -> ())
+    | _ -> ()
+
+  module A = struct
+    (** ego tid * must-lockset * creation-lockset *)
+    include Printable.Prod3 (TID) (Lockset) (G)
+
+    let name () = "creationLockset"
+
+    (** checks if [cl1] has a mapping ([tp1] |-> [ls1])
+        such that [ls1] and [ls2] are not disjoint and [tp1] != [t2]
+        @param cl1 creation-lockset of thread [t1] at first program point
+        @param t2 thread id at second program point
+        @param ls2 lockset at second program point
+        @returns whether [t1] must be running mutually exclusive with second program point
+    *)
+    let one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2 =
+      G.exists (fun tp1 ls1 -> not (Lockset.disjoint ls1 ls2 || TID.equal tp1 t2)) cl1
+
+    (** checks if [cl1] has a member ([tp1] |-> [ls1]) and [cl2] has a member ([tp2] |-> [ls2])
+        such that [ls1] and [ls2] are not disjoint and [tp1] != [tp2]
+        @param cl1 creation-lockset of first thread [t1]
+        @param cl2 creation-lockset of second thread [t2]
+        @returns whether [t1] and [t2] must be running mutually exclusive
+    *)
+    let both_protected_inter_threaded cl1 cl2 =
+      G.exists (one_protected_inter_threaded_other_intra_threaded cl1) cl2
+
+    let may_race (t1, ls1, cl1) (t2, ls2, cl2) =
+      not
+        (both_protected_inter_threaded cl1 cl2
+         || one_protected_inter_threaded_other_intra_threaded cl1 t2 ls2
+         || one_protected_inter_threaded_other_intra_threaded cl2 t1 ls1)
+
+    let should_print (_t, _ls, cl) = not @@ G.is_empty cl
+  end
+
+  let access man _ =
+    let tid_lifted = man.ask Queries.CurrentThreadId in
+    match tid_lifted with
+    | `Lifted tid ->
+      let lockset = man.ask Queries.MustLockset in
+      let creation_lockset = man.global tid in
+      tid, lockset, creation_lockset
+    | _ -> ThreadIdDomain.UnknownThread, Lockset.empty (), G.empty ()
+end
+
+let _ =
+  MCP.register_analysis
+    ~dep:[ "threadid"; "mutex"; "threadJoins"; "threadDescendants" ]
+    (module Spec : MCPSpec)

src/analyses/mutexGhosts.ml

@@ -61,11 +61,6 @@ struct
     let create_update = create_threadcreate
   end
 
-  let mustlock_of_addr (addr: LockDomain.Addr.t): LockDomain.MustLock.t option =
-    match addr with
-    | Addr mv when LockDomain.Mval.is_definite mv -> Some (LockDomain.MustLock.of_mval mv)
-    | _ -> None
-
   let event man e oman =
     let verifier_atomic_addr = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var in
     begin match e with
@@ -78,7 +73,7 @@ struct
             Locked.iter (fun lock ->
                 Option.iter (fun lock ->
                     man.sideg (V.lock lock) (G.create_lock true)
-                  ) (mustlock_of_addr lock)
+                  ) (LockDomain.MustLock.of_addr lock)
               ) locked
           );
         )
@@ -91,7 +86,7 @@ struct
             Locked.iter (fun lock ->
                 Option.iter (fun lock ->
                     man.sideg (V.lock lock) (G.create_lock true)
-                  ) (mustlock_of_addr lock)
+                  ) (LockDomain.MustLock.of_addr lock)
               ) unlocked
           );
         )
@@ -128,7 +123,7 @@ struct
               let (locked, unlocked, multithread) = G.node (man.global (V.node node)) in
               let variables' =
                 Locked.fold (fun l acc ->
-                    match mustlock_of_addr l with
+                    match LockDomain.MustLock.of_addr l with
                     | Some l when ghost_var_available man (Locked l) ->
                       let variable = WitnessGhost.variable' (Locked l) in
                       VariableSet.add variable acc
@@ -138,7 +133,7 @@ struct
               in
               let updates =
                 Locked.fold (fun l acc ->
-                    match mustlock_of_addr l with
+                    match LockDomain.MustLock.of_addr l with
                     | Some l when ghost_var_available man (Locked l) ->
                       let update = WitnessGhost.update' (Locked l) GoblintCil.one in
                       update :: acc
@@ -148,7 +143,7 @@ struct
               in
               let updates =
                 Unlocked.fold (fun l acc ->
-                    match mustlock_of_addr l with
+                    match LockDomain.MustLock.of_addr l with
                     | Some l when ghost_var_available man (Locked l) ->
                       let update = WitnessGhost.update' (Locked l) GoblintCil.zero in
                       update :: acc

src/analyses/threadDescendants.ml

@@ -0,0 +1,42 @@
+(** thread descendants analysis [threadDescendants]
+    flow-insensitive construction of descendants may-set for every thread
+*)
+
+open Analyses
+module TID = ThreadIdDomain.Thread
+
+module Spec = struct
+  include IdentityUnitContextsSpec
+  module D = Lattice.Unit
+
+  module V = struct
+    include TID
+    include StdV
+  end
+
+  module G = ConcDomain.ThreadSet
+
+  let name () = "threadDescendants"
+  let startstate _ = D.bot ()
+  let exitstate _ = D.bot ()
+
+  let query man (type a) (x : a Queries.t) : a Queries.result =
+    match x with
+    | Queries.DescendantThreads t ->
+      let children = man.global t in
+      (G.fold
+         (fun e acc -> G.union (man.ask @@ Queries.DescendantThreads e) acc)
+         children
+         children
+       : G.t)
+    | _ -> Queries.Result.top x
+
+  let threadspawn man ~multiple lval f args fman =
+    let tid_lifted = man.ask Queries.CurrentThreadId in
+    let child_tid_lifted = fman.ask Queries.CurrentThreadId in
+    match tid_lifted, child_tid_lifted with
+    | `Lifted tid, `Lifted child_tid -> man.sideg tid (G.singleton child_tid)
+    | _ -> ()
+end
+
+let _ = MCP.register_analysis ~dep:[ "threadid" ] (module Spec : MCPSpec)

src/cdomains/lockDomain.ml

@@ -29,6 +29,11 @@ struct
   let of_mval ((v, o): Mval.t): t =
     (v, Offset.Poly.map_indices (fun i -> IndexDomain.to_int i |> Option.get) o)
 
+  let of_addr (addr : Addr.t) : t option =
+    match addr with
+    | Addr mv when Mval.is_definite mv -> Some (of_mval mv)
+    | _ -> None
+
   let to_mval ((v, o): t): Mval.t =
     (v, Offset.Poly.map_indices (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) o)
 end

src/domains/queries.ml

@@ -146,6 +146,7 @@ type _ t =
   | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t (** YAML witness entries for a global unknown ([Obj.t] represents [Spec.V.t]) and YAML witness task. *)
   | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t
   | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *)
+  | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t
 
 type 'a result = 'a
 
@@ -221,6 +222,7 @@ struct
     | YamlEntryGlobal _ -> (module YS)
     | GhostVarAvailable _ -> (module MayBool)
     | InvariantGlobalNodes -> (module NS)
+    | DescendantThreads _ -> (module ConcDomain.ThreadSet)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -295,6 +297,7 @@ struct
     | YamlEntryGlobal _ -> YS.top ()
     | GhostVarAvailable _ -> MayBool.top ()
     | InvariantGlobalNodes -> NS.top ()
+    | DescendantThreads _ -> ConcDomain.ThreadSet.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -366,6 +369,7 @@ struct
     | Any (MustProtectingLocks _) -> 61
     | Any (GhostVarAvailable _) -> 62
     | Any InvariantGlobalNodes -> 63
+    | Any (DescendantThreads _) -> 64
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -425,6 +429,7 @@ struct
       | Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2
       | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2
       | Any (GhostVarAvailable v1), Any (GhostVarAvailable v2) -> WitnessGhostVar.compare v1 v2
+      | Any (DescendantThreads t1), Any (DescendantThreads t2) -> ThreadIdDomain.Thread.compare t1 t2
       (* only argumentless queries should remain *)
       | _, _ -> Stdlib.compare (order a) (order b)
 
@@ -472,6 +477,7 @@ struct
     | Any (MaySignedOverflow e) -> CilType.Exp.hash e
     | Any (GasExhausted f) -> CilType.Fundec.hash f
     | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v
+    | Any (DescendantThreads t) -> ThreadIdDomain.Thread.hash t
     (* IterSysVars:                                                                    *)
     (*   - argument is a function and functions cannot be compared in any meaningful way. *)
     (*   - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *)
@@ -540,6 +546,7 @@ struct
     | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f
     | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v
     | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes"
+    | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads %a" ThreadIdDomain.Thread.pretty t
 end
 
 let to_value_domain_ask (ask: ask) =

src/goblint_lib.ml

@@ -120,6 +120,7 @@ module ThreadAnalysis = ThreadAnalysis
 module ThreadJoins = ThreadJoins
 module MHPAnalysis = MHPAnalysis
 module ThreadReturn = ThreadReturn
+module ThreadDescendants = ThreadDescendants
 
 (** {3 Other} *)
 
@@ -131,6 +132,7 @@ module PthreadSignals = PthreadSignals
 module PthreadBarriers = PthreadBarriers
 module ExtractPthread = ExtractPthread
 module PthreadOnce = PthreadOnce
+module CreationLockset = CreationLockset
 
 (** {2 Longjmp}
 

tests/regression/53-races-mhp/10-lockset_inter_threaded_lock_racefree.c

@@ -0,0 +1,27 @@
+// PARAM: --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] creationLockset
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id1, id2;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex);
+  global++; // NORACE
+  pthread_mutex_unlock(&mutex);
+  return NULL;
+}
+
+void *t2(void *arg) { // t2 is protected by mutex locked in main thread
+  global++; // NORACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_create(&id1, NULL, t1, NULL);
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id2, NULL, t2, NULL);
+  pthread_join(id2, NULL);
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}