[racerd] use `ThreadsDomain.astate` instead of bool in `AccessData`

Reviewed By: ngorogiannis

Differential Revision: D7423167

fbshipit-source-id: 79daa3a

infer/src/concurrency/RacerD.ml

@@ -390,7 +390,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         (* if the access occurred on a main thread in the callee, we should remember this when
            moving it to the callee. if we don't know what thread it ran on, use the caller's
            thread *)
-        let threads' = if pre.thread then ThreadsDomain.AnyThreadButSelf else threads in
+        let threads' =
+          ThreadsDomain.integrate_summary ~callee_astate:pre.thread ~caller_astate:threads
+        in
         let pre' = AccessSnapshot.make locks' threads' ownership_precondition' pdesc in
         update_caller_accesses pre' callee_accesses accesses_acc
     in
@@ -516,15 +518,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                       LocksDomain.integrate_summary ~caller_astate:astate.locks
                         ~callee_astate:locks
                     in
-                    let threads =
-                      (* if we know the callee runs on the main thread, assume the caller does too.
-                         otherwise, keep the caller's thread context *)
-                      match threads with
-                      | ThreadsDomain.AnyThreadButSelf ->
-                          threads
-                      | _ ->
-                          astate.threads
-                    in
                     let accesses =
                       add_callee_accesses astate accesses locks threads actuals callee_pname pdesc
                         loc
@@ -539,6 +532,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                         callee_pdesc
                     in
                     let wobbly_paths = StabilityDomain.join wobbly_paths callee_wps_rebased in
+                    let threads =
+                      ThreadsDomain.integrate_summary ~caller_astate:astate.threads
+                        ~callee_astate:threads
+                    in
                     {locks; threads; accesses; ownership; attribute_map; wobbly_paths}
                 | None ->
                     let should_assume_returns_ownership (call_flags: CallFlags.t) actuals =
@@ -1301,8 +1298,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
           (* protected read. report unprotected writes and opposite protected writes as conflicts *)
           let can_conflict (pre1: AccessSnapshot.t) (pre2: AccessSnapshot.t) =
             if pre1.lock && pre2.lock then false
-            else if pre1.thread && pre2.thread then false
-            else true
+            else ThreadsDomain.can_conflict pre1.thread pre2.thread
           in
           let conflicting_writes =
             List.filter

infer/src/concurrency/RacerDDomain.ml

@@ -235,11 +235,21 @@ module ThreadsDomain = struct
           "AnyThread" )
 
 
+  (* at least one access is known to occur on a background thread *)
+  let can_conflict astate1 astate2 =
+    match join astate1 astate2 with AnyThread -> true | NoThread | AnyThreadButSelf -> false
+
+
   let is_empty = function NoThread -> true | _ -> false
 
   let is_any_but_self = function AnyThreadButSelf -> true | _ -> false
 
   let is_any = function AnyThread -> true | _ -> false
+
+  let integrate_summary ~caller_astate ~callee_astate =
+    (* if we know the callee runs on the main thread, assume the caller does too. otherwise, keep 
+       the caller's thread context *)
+    match callee_astate with AnyThreadButSelf -> callee_astate | _ -> caller_astate
 end
 
 module PathDomain = SinkTrace.Make (TraceElem)
@@ -409,23 +419,26 @@ module AccessSnapshot = struct
           F.fprintf fmt "False"
   end
 
-  type t = {thread: bool; lock: bool; ownership_precondition: Precondition.t} [@@deriving compare]
+  type t =
+    {thread: ThreadsDomain.astate; lock: bool; ownership_precondition: Precondition.t}
+    [@@deriving compare]
 
-  let make lock threads ownership_precondition pdesc =
+  let make lock thread ownership_precondition pdesc =
     (* shouldn't be creating metadata for accesses that are known to be owned; we should discard
        such accesses *)
     assert (not (Precondition.is_true ownership_precondition)) ;
-    let thread = ThreadsDomain.is_any_but_self threads in
     let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in
     {thread; lock; ownership_precondition}
 
 
   let is_unprotected {thread; lock; ownership_precondition} =
-    not thread && not lock && not (Precondition.is_true ownership_precondition)
+    not (ThreadsDomain.is_any_but_self thread) && not lock
+    && not (Precondition.is_true ownership_precondition)
 
 
   let pp fmt {thread; lock; ownership_precondition} =
-    F.fprintf fmt "Thread: %b Lock: %b Pre: %a" thread lock Precondition.pp ownership_precondition
+    F.fprintf fmt "Thread: %a Lock: %b Pre: %a" ThreadsDomain.pp thread lock Precondition.pp
+      ownership_precondition
 end
 
 module AccessDomain = struct

infer/src/concurrency/RacerDDomain.mli

@@ -86,7 +86,15 @@ module ThreadsDomain : sig
 
   include AbstractDomain.WithBottom with type astate := astate
 
+  val can_conflict : astate -> astate -> bool
+  (** return true if two accesses with these thread values can run concurrently *)
+
   val is_any : astate -> bool
+
+  val is_any_but_self : astate -> bool
+
+  val integrate_summary : caller_astate:astate -> callee_astate:astate -> astate
+  (** integrate current state with a callee summary *)
 end
 
 module PathDomain : module type of SinkTrace.Make (TraceElem)
@@ -169,8 +177,9 @@ module AccessSnapshot : sig
     val pp : F.formatter -> t -> unit  [@@warning "-32"]
   end
 
-  type t = private {thread: bool; lock: bool; ownership_precondition: Precondition.t}
-  [@@deriving compare]
+  type t = private
+    {thread: ThreadsDomain.astate; lock: bool; ownership_precondition: Precondition.t}
+    [@@deriving compare]
 
   val make : LocksDomain.astate -> ThreadsDomain.astate -> Precondition.t -> Procdesc.t -> t