Improve MHP precision using ancestor locksets

src/analyses/creationLockset.ml

@@ -0,0 +1,212 @@
+open Analyses
+module LF = LibraryFunctions
+
+module TID = ThreadIdDomain.Thread
+module TIDs = ConcDomain.ThreadSet
+module LID = LockDomain.MustLock
+module LIDs = LockDomain.MustLockset
+
+module AncestorLocksetSpec = struct
+  include IdentityUnitContextsSpec (* no context necessary(?) *)
+  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 must-ancestors and locks (t_0,l):
+    when t_n or a must-ancestor t_1 of t_n was created, the parent 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 when TID.must_be_ancestor tid 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):
+    when l is unlocked in t_0, 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
+  ;;
+
+  (** stolen from mutexGhost.ml. TODO Maybe add to utils? *)
+  let mustlock_of_addr (addr : LockDomain.Addr.t) : LID.t option =
+    match addr with
+    | Addr mv when LockDomain.Mval.is_definite mv -> Some (LID.of_mval mv)
+    | _ -> None
+  ;;
+
+  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 = 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 their full CreationLocksets to invalidate them!! *)
+            let contribute_creation_lockset des_tid =
+              let creation_lockset = ask.f @@ Queries.MayCreationLockset des_tid in
+              man.sideg des_tid 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 _ = true
+  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/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/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.hash_thread t (* TODO is this fine? *)
+    | Any (MayCreationLockset t) -> ThreadIdDomain.hash_thread 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) =

tests/regression/89-races_ancestor_locksets/01-lockset_inter_threaded_lock_racefree.c

@@ -0,0 +1,26 @@
+#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;
+}

tests/regression/89-races_ancestor_locksets/02-both_inter_threaded_lock_racefree.c

@@ -0,0 +1,32 @@
+#include <pthread.h>
+
+int global = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_t id_main_child, id_1, id_1_child;
+
+void *t1_child_fun(void* arg) { // t1child is protected by mutex locked in t1
+  global++; // NORACE
+  return NULL;
+}
+
+void *tmain_child_fun(void *arg) { // tmainchild is protected by mutex locked in main thread
+  global++; // NORACE
+  return NULL;
+}
+
+void *t1_fun(void *arg) {
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id_1_child, NULL, t1_child_fun, NULL);
+  pthread_join(id_1_child, NULL);
+  pthread_mutex_unlock(&mutex);
+  return NULL;
+}
+
+int main(void) {
+  pthread_create(&id_1, NULL, t1_fun, NULL);
+  pthread_mutex_lock(&mutex);
+  pthread_create(&id_main_child, NULL, tmain_child_fun, NULL);
+  pthread_join(id_main_child, NULL);
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}