Improve MHP precision using ancestor locksets

src/analyses/creationLockset.ml

@@ -0,0 +1,210 @@
+(** Ancestor-lock analysis. See https://github.com/goblint/analyzer/pull/1865 *)
+
+open Analyses
+module LF = LibraryFunctions
+module TID = ThreadIdDomain.Thread
+module TIDs = ConcDomain.ThreadSet
+module LID = LockDomain.MustLock
+module LIDs = LockDomain.MustLockset
+
+(** common base for [CreationLocksetSpec] and [TaintedCreationLocksetSpec] *)
+module AncestorLocksetSpec = struct
+  include IdentityUnitContextsSpec
+  module D = Lattice.Unit
+
+  module V = struct
+    include TID
+    include StdV
+  end
+
+  (** 2 ^ { [TID] \times [LID] } *)
+  module G = Queries.ALS
+
+  let startstate _ = D.bot ()
+  let exitstate _ = D.bot ()
+
+  (** register a contribution to a global: global.[child_tid] \supseteq [to_contribute]
+      @param man man at program point
+      @param to_contribute new edges from [child_tid] to register
+      @param child_tid
+  *)
+  let contribute_lock man to_contribute child_tid = man.sideg child_tid to_contribute
+
+  (** compute [tids] \times \{[lock]\} *)
+  let singleton_cartesian_prod tids lock =
+    TIDs.fold (fun tid acc -> G.add (tid, lock) acc) tids (G.empty ())
+  ;;
+
+  (** compute the cartesian product [tids] \times [locks] *)
+  let cartesian_prod tids locks =
+    LIDs.fold
+      (fun lock acc ->
+         let tids_times_lock = singleton_cartesian_prod tids lock in
+         G.union tids_times_lock acc)
+      locks
+      (G.empty ())
+  ;;
+
+  (** reflexive-transitive closure of child relation applied to [tid]
+      @param ask any ask
+      @param tid
+      @returns [{ tid }] \cup DES([tid])
+  *)
+  let descendants_closure (ask : Queries.ask) tid =
+    let transitive_descendants = ask.f @@ Queries.DescendantThreads tid in
+    TIDs.add tid transitive_descendants
+  ;;
+end
+
+(** collects for each thread t_n pairs of ancestors and locks (t_0,l):
+    when t_n or an ancestor t_1 of t_n was created, the creating thread t_0 must have held l.
+*)
+module CreationLocksetSpec = struct
+  include AncestorLocksetSpec
+
+  let name () = "creationLockset"
+
+  (** create(t_1) in t_0 with lockset L *)
+  let threadspawn man ~multiple lval f args fman =
+    let ask = Analyses.ask_of_man man in
+    let tid_lifted = ask.f Queries.CurrentThreadId in
+    let child_ask = Analyses.ask_of_man fman in
+    let child_tid_lifted = child_ask.f Queries.CurrentThreadId in
+    match tid_lifted, child_tid_lifted with
+    | `Lifted tid, `Lifted child_tid ->
+      let descendants = descendants_closure child_ask child_tid in
+      let lockset = ask.f Queries.MustLockset in
+      let to_contribute = cartesian_prod (TIDs.singleton tid) lockset in
+      TIDs.iter (contribute_lock man to_contribute) descendants
+    | _ -> (* TODO deal with top or bottom? *) ()
+  ;;
+
+  let query man (type a) (x : a Queries.t) : a Queries.result =
+    match x with
+    | Queries.MayCreationLockset tid -> (man.global tid : G.t)
+    | _ -> Queries.Result.top x
+  ;;
+end
+
+(** collects for each thread t_n pairs of ancestors and locks (t_0,l):
+    l may be unlocked in t_0 while t_n could be running.
+*)
+module TaintedCreationLocksetSpec = struct
+  include AncestorLocksetSpec
+
+  let name () = "taintedCreationLockset"
+
+  (** compute all threads that may run along with the ego thread at a program point
+      @param ask ask of ego thread at the program point
+  *)
+  let get_possibly_running_tids (ask : Queries.ask) =
+    let may_created_tids = ask.f Queries.CreatedThreads in
+    let may_transitively_created_tids =
+      TIDs.fold
+        (fun child_tid acc -> TIDs.union acc (descendants_closure ask child_tid))
+        may_created_tids
+        (TIDs.empty ())
+    in
+    let must_joined_tids = ask.f Queries.MustJoinedThreads in
+    TIDs.diff may_transitively_created_tids must_joined_tids
+  ;;
+
+  let event man e _ =
+    match e with
+    | Events.Unlock addr ->
+      let ask = Analyses.ask_of_man man in
+      let tid_lifted = ask.f Queries.CurrentThreadId in
+      (match tid_lifted with
+       | `Top | `Bot -> ()
+       | `Lifted tid ->
+         let possibly_running_tids = get_possibly_running_tids ask in
+         let lock_opt = LockDomain.MustLock.of_addr addr in
+         (match lock_opt with
+          | Some lock ->
+            (* contribute for all possibly_running_tids: (tid, lock) *)
+            let to_contribute = G.singleton (tid, lock) in
+            TIDs.iter (contribute_lock man to_contribute) possibly_running_tids
+          | None ->
+            (* any lock could have been unlocked. Contribute for all possibly_running_tids all members of their CreationLocksets with the ego thread to invalidate them!! *)
+            let contribute_creation_lockset des_tid =
+              let full_creation_lockset = ask.f @@ Queries.MayCreationLockset des_tid in
+              let filtered_creation_lockset =
+                G.filter (fun (t, _l) -> t = tid) full_creation_lockset
+              in
+              man.sideg des_tid filtered_creation_lockset
+            in
+            TIDs.iter contribute_creation_lockset possibly_running_tids))
+    | _ -> ()
+  ;;
+
+  module A = struct
+    (** ego tid * lockset * inter-threaded lockset *)
+    include Printable.Prod3 (TID) (LIDs) (G)
+
+    let name () = "interThreadedLockset"
+
+    (** checks if [itls1] has a member ([tp1], [l]) such that [itls2] has a member ([tp2], [l]) with [tp1] != [tp2]
+        @param itls1 inter-threaded lockset of first thread [t1]
+        @param itls2 inter-threaded lockset of second thread [t2]
+        @returns whether [t1] and [t2] must be running mutually exclusive
+    *)
+    let both_protected_inter_threaded itls1 itls2 =
+      let itls2_has_same_lock_other_tid (tp1, l1) =
+        G.exists (fun (tp2, l2) -> LID.equal l1 l2 && (not @@ TID.equal tp1 tp2)) itls2
+      in
+      G.exists itls2_has_same_lock_other_tid itls1
+    ;;
+
+    (** checks if [itls1] has a member ([tp1], [l1]) such that [l1] is in [ls2] and [tp1] != [t2]
+        @param itls1 inter-threaded 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 itls1 t2 ls2 =
+      G.exists (fun (tp1, l1) -> LIDs.mem l1 ls2 && (not @@ TID.equal tp1 t2)) itls1
+    ;;
+
+    let may_race (t1, ls1, itls1) (t2, ls2, itls2) =
+      not
+        (both_protected_inter_threaded itls1 itls2
+         || one_protected_inter_threaded_other_intra_threaded itls1 t2 ls2
+         || one_protected_inter_threaded_other_intra_threaded itls2 t1 ls1)
+    ;;
+
+    let should_print (_t, _ls, itls) = not @@ G.is_empty itls
+  end
+
+  let access man _ =
+    let ask = Analyses.ask_of_man man in
+    let tid_lifted = ask.f Queries.CurrentThreadId in
+    match tid_lifted with
+    | `Lifted tid ->
+      let lockset = ask.f Queries.MustLockset in
+      let creation_lockset = ask.f @@ Queries.MayCreationLockset tid in
+      let tainted_creation_lockset = man.global tid in
+      (* all values in creation lockset, but not in tainted creation lockset *)
+      let inter_threaded_lockset = G.diff creation_lockset tainted_creation_lockset in
+      tid, lockset, inter_threaded_lockset
+    | _ -> ThreadIdDomain.UnknownThread, LIDs.empty (), G.empty ()
+  ;;
+end
+
+let _ =
+  MCP.register_analysis
+    ~dep:[ "threadid"; "mutex"; "race"; "transitiveDescendants" ]
+    (module CreationLocksetSpec : MCPSpec)
+;;
+
+let _ =
+  MCP.register_analysis
+    ~dep:
+      [ "threadid"
+      ; "mutex"
+      ; "threadJoins"
+      ; "race"
+      ; "transitiveDescendants"
+      ; "creationLockset"
+      ]
+    (module TaintedCreationLocksetSpec : 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/transitiveDescendants.ml

@@ -0,0 +1,45 @@
+open Analyses
+module TID = ThreadIdDomain.Thread
+
+(** flow-insensitive analysis mapping threads to may-sets of descendants *)
+module TransitiveDescendants = struct
+  include IdentityUnitContextsSpec
+  module D = Lattice.Unit
+
+  module V = struct
+    include TID
+    include StdV
+  end
+
+  module G = ConcDomain.ThreadSet
+
+  let name () = "transitiveDescendants"
+  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 -> (man.global t : G.t)
+    | _ -> Queries.Result.top x
+  ;;
+
+  let threadspawn man ~multiple lval f args fman =
+    let ask = Analyses.ask_of_man man in
+    let tid_lifted = ask.f Queries.CurrentThreadId in
+    match tid_lifted with
+    | `Top | `Bot -> ()
+    | `Lifted tid ->
+      let child_ask = Analyses.ask_of_man fman in
+      let child_tid_lifted = child_ask.f Queries.CurrentThreadId in
+      (match child_tid_lifted with
+       | `Top | `Bot -> ()
+       | `Lifted child_tid ->
+         (* contribute new child *)
+         let _ = man.sideg tid (G.singleton child_tid) in
+         (* transitive closure *)
+         let child_descendants = man.global child_tid in
+         man.sideg tid child_descendants)
+  ;;
+end
+
+let _ = MCP.register_analysis ~dep:[ "threadid" ] (module TransitiveDescendants : 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

@@ -77,6 +77,7 @@ type invariant_context = Invariant.context = {
 
 module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end)
 
+module ALS = SetDomain.ToppedSet (Printable.Prod (ThreadIdDomain.Thread) (LockDomain.MustLock)) (struct let topname = "all pairs of threads and locks" end)
 
 (** GADT for queries with specific result type. *)
 type _ t =
@@ -146,6 +147,8 @@ 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
+  | MayCreationLockset: ThreadIdDomain.Thread.t -> ALS.t t
 
 type 'a result = 'a
 
@@ -221,6 +224,8 @@ struct
     | YamlEntryGlobal _ -> (module YS)
     | GhostVarAvailable _ -> (module MayBool)
     | InvariantGlobalNodes -> (module NS)
+    | DescendantThreads _ -> (module ConcDomain.ThreadSet)
+    | MayCreationLockset _ -> (module ALS)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -295,6 +300,8 @@ struct
     | YamlEntryGlobal _ -> YS.top ()
     | GhostVarAvailable _ -> MayBool.top ()
     | InvariantGlobalNodes -> NS.top ()
+    | DescendantThreads _ -> ConcDomain.ThreadSet.top ()
+    | MayCreationLockset _ -> ALS.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -366,6 +373,8 @@ struct
     | Any (MustProtectingLocks _) -> 61
     | Any (GhostVarAvailable _) -> 62
     | Any InvariantGlobalNodes -> 63
+    | Any (DescendantThreads _) -> 64
+    | Any (MayCreationLockset _) -> 65
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -472,6 +481,8 @@ 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
+    | Any (MayCreationLockset 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 +551,8 @@ 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"
+    | Any (MayCreationLockset t) -> Pretty.dprintf "MayCreationLockset"
 end
 
 let to_value_domain_ask (ask: ask) =