[threadsafety] record threaded information alongside accesses and use disjunction for thread join

Summary: Using Conjunction for thread join has known false negatives. Finer grained recording of threading information fixes this.

Reviewed By: sblackshear

Differential Revision: D5111161

fbshipit-source-id: aab483c

infer/src/checkers/ThreadSafety.ml

@@ -48,6 +48,13 @@ let get_container_write_desc sink =
 let is_container_write_sink sink =
   Option.is_some (get_container_write_desc sink)
 
+(*Bit of redundancy with code in is_unprotected, might alter later *)
+let make_excluder locks threads =
+  if locks && not threads then ThreadSafetyDomain.Excluder.Lock
+  else if not locks && threads then ThreadSafetyDomain.Excluder.Thread
+  else if locks && threads then ThreadSafetyDomain.Excluder.Both
+  else failwithf "called when neither lock nor thread known"
+
 module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = ThreadSafetyDomain
@@ -161,11 +168,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               other_attributes in
         AttributeMapDomain.add (ret, []) caller_return_attributes attribute_map
 
-  let is_unprotected is_locked pdesc =
+  let is_unprotected is_locked is_threaded pdesc =
-    not is_locked && not (Procdesc.is_java_synchronized pdesc)
+    not is_locked && not is_threaded
+    && not (Procdesc.is_java_synchronized pdesc)
+
 
   let add_access
-      exp loc access_kind accesses locks attribute_map (proc_data : FormalMap.t ProcData.t) =
+      exp loc access_kind accesses locks threads
+      attribute_map (proc_data : FormalMap.t ProcData.t) =
     let open Domain in
     (* we don't want to warn on accesses to the field if it is (a) thread-confined, or
        (b) volatile *)
@@ -210,13 +220,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       then acc
       else
         let pre =
-          if is_unprotected locks proc_data.pdesc
+          if is_unprotected locks threads proc_data.pdesc
           then
             match FormalMap.get_formal_index base proc_data.extras with
             | Some formal_index -> AccessPrecondition.Unprotected (Some formal_index)
             | None -> AccessPrecondition.unprotected
           else
-            AccessPrecondition.Protected in
+            AccessPrecondition.Protected
+              (make_excluder (locks || Procdesc.is_java_synchronized proc_data.pdesc)
+                 threads) in
         add_field_accesses pre (base, []) acc accesses in
 
     List.fold ~f:add_access_ ~init:accesses (HilExp.get_access_paths exp)
@@ -387,9 +399,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | _ ->
         false
 
-  let add_reads exps loc accesses locks attribute_map proc_data =
+  let add_reads exps loc accesses locks threads attribute_map proc_data =
     List.fold
-      ~f:(fun acc exp -> add_access exp loc Read acc locks attribute_map proc_data)
+      ~f:(fun acc exp -> add_access exp loc Read acc locks threads attribute_map proc_data)
       exps
       ~init:accesses
 
@@ -403,7 +415,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Call (Some ret_base, Direct procname, actuals, _, loc)
       when acquires_ownership procname tenv ->
         let accesses =
-          add_reads actuals loc astate.accesses astate.locks astate.attribute_map proc_data in
+          add_reads actuals loc astate.accesses astate.locks
+            astate.threads astate.attribute_map proc_data in
         let attribute_map =
           AttributeMapDomain.add_attribute
             (ret_base, []) Attribute.unconditionally_owned astate.attribute_map in
@@ -411,7 +424,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
     | Call (ret_opt, Direct callee_pname, actuals, call_flags, loc) ->
         let accesses =
-          add_reads actuals loc astate.accesses astate.locks astate.attribute_map proc_data in
+          add_reads actuals loc astate.accesses astate.locks
+            astate.threads astate.attribute_map proc_data in
         let astate = { astate with accesses; } in
         let astate_callee =
           (* assuming that modeled procedures do not have useful summaries *)
@@ -449,7 +463,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                       AccessDomain.add pre combined_accesses caller_accesses in
                     let locks = callee_locks || astate.locks in
                     let threads = callee_threads || astate.threads in
-                    let unprotected = is_unprotected locks pdesc in
+                    let unprotected = is_unprotected locks threads pdesc in
                     (* add [ownership_accesses] to the [accesses_acc] with a protected pre if
                        [exp] is owned, and an appropriate unprotected pre otherwise *)
                     let add_ownership_access ownership_accesses actual_exp accesses_acc =
@@ -489,7 +503,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                                         AccessPrecondition.unprotected
                               else
                                 (* access protected by held lock *)
-                                AccessPrecondition.Protected in
+                                AccessPrecondition.Protected (make_excluder true threads) in
                             update_caller_accesses pre ownership_accesses accesses_acc
                       | _ ->
                           (* couldn't find access path, don't know if it's owned *)
@@ -497,13 +511,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                             AccessPrecondition.unprotected ownership_accesses accesses_acc in
                     let accesses =
                       let update_accesses pre callee_accesses accesses_acc = match pre with
-                        | AccessPrecondition.Protected ->
+                        | AccessPrecondition.Protected _ ->
                             update_caller_accesses pre callee_accesses accesses_acc
                         | AccessPrecondition.Unprotected None ->
                             let pre' =
                               if unprotected
                               then pre
-                              else AccessPrecondition.Protected in
+                              else AccessPrecondition.Protected (make_excluder true threads) in
                             update_caller_accesses pre' callee_accesses accesses_acc
                         | AccessPrecondition.Unprotected (Some index) ->
                             add_ownership_access
@@ -577,7 +591,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Assign (lhs_access_path, rhs_exp, loc) ->
         let rhs_accesses =
           add_access
-            rhs_exp loc Read astate.accesses astate.locks astate.attribute_map proc_data in
+            rhs_exp loc Read astate.accesses astate.locks
+            astate.threads astate.attribute_map proc_data in
         let rhs_access_paths = HilExp.get_access_paths rhs_exp in
         let is_functional =
           not (List.is_empty rhs_access_paths) &&
@@ -598,6 +613,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               Write
               rhs_accesses
               astate.locks
+              astate.threads
               astate.attribute_map
               proc_data in
         let attribute_map =
@@ -642,7 +658,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
         let accesses =
           add_access
-            assume_exp loc Read astate.accesses astate.locks astate.attribute_map proc_data in
+            assume_exp loc Read astate.accesses astate.locks
+            astate.threads astate.attribute_map proc_data in
         let astate' =
           match HilExp.get_access_paths assume_exp with
           | [access_path] ->
@@ -1065,7 +1082,7 @@ let report_unsafe_accesses ~is_file_threadsafe aggregated_access_map =
                 access;
               update_reported access pname reported_acc
             end
-      | Access.Write, AccessPrecondition.Protected ->
+      | Access.Write, AccessPrecondition.Protected _ ->
           (* protected write, do nothing *)
           reported_acc
       | Access.Read, AccessPrecondition.Unprotected _ ->
@@ -1088,18 +1105,30 @@ let report_unsafe_accesses ~is_file_threadsafe aggregated_access_map =
                 access;
               update_reported access pname reported_acc
             end
-      | Access.Read, AccessPrecondition.Protected ->
+      | Access.Read, AccessPrecondition.Protected excl ->
-          (* protected read. report unprotected, threaded writes as conflicts *)
+          (* protected read.
-          let unprotected_writes =
+             report unprotected writes and opposite protected writes as conflicts
+             Thread and Lock are opposites of one another, and
+             Both has no opposite*)
+          let is_opposite  = function
+            | Excluder.Lock , Excluder.Thread
+              -> true
+            | Excluder.Thread , Excluder.Lock
+              -> true
+            | _ , _ -> false in
+          let conflicting_writes =
             List.filter
-              ~f:(fun (access, pre, other_threaded, _, _) ->
+              ~f:(fun (access, pre, _, _, _) ->
                   match pre with
                   | AccessPrecondition.Unprotected _ ->
-                      TraceElem.is_write access && (other_threaded && not threaded)
+                      TraceElem.is_write access
+                  | AccessPrecondition.Protected other_excl
+                    when is_opposite (excl , other_excl) ->
+                      TraceElem.is_write access
                   | _ ->
                       false)
               accesses in
-          if List.is_empty unprotected_writes
+          if List.is_empty conflicting_writes
           then
             reported_acc
           else
@@ -1108,7 +1137,7 @@ let report_unsafe_accesses ~is_file_threadsafe aggregated_access_map =
               report_thread_safety_violation
                 tenv
                 pdesc
-                ~make_description:(make_read_write_race_description unprotected_writes)
+                ~make_description:(make_read_write_race_description conflicting_writes)
                 access;
               update_reported access pname reported_acc
             end in

infer/src/checkers/ThreadSafetyDomain.ml

@@ -82,7 +82,7 @@ module LocksDomain = AbstractDomain.BooleanAnd
    The use of || for join in this domain enforces that, to not know for sure you are threaded,
    it is enough to be unthreaded in one branch. (See RaceWithMainThread.java for  examples)
 *)
-module ThreadsDomain = AbstractDomain.BooleanOr
+module ThreadsDomain = AbstractDomain.BooleanAnd
 
 module PathDomain = SinkTrace.Make(TraceElem)
 
@@ -161,16 +161,29 @@ module AttributeMapDomain = struct
     add access_path attribute_set t
 end
 
+module Excluder = struct
+  type t =
+    | Thread
+    | Lock
+    | Both
+  [@@deriving compare]
+
+  let pp fmt = function
+    | Thread -> F.fprintf fmt "Thread"
+    | Lock -> F.fprintf fmt "Lock"
+    | Both -> F.fprintf fmt "both Thread and Lock"
+end
+
 module AccessPrecondition = struct
   type t =
-    | Protected
+    | Protected of Excluder.t
     | Unprotected of int option
   [@@deriving compare]
 
   let unprotected = Unprotected None
 
   let pp fmt = function
-    | Protected -> F.fprintf fmt "Protected"
+    | Protected excl -> F.fprintf fmt "ProtectedBy(%a)" Excluder.pp excl
     | Unprotected (Some index) -> F.fprintf fmt "Unprotected(%d)" index
     | Unprotected None -> F.fprintf fmt "Unprotected"
 end

infer/src/checkers/ThreadSafetyDomain.mli

@@ -87,10 +87,31 @@ module AttributeMapDomain : sig
   val add_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> astate
 end
 
+
+(** Excluders: Two things can provide for mutual exclusion: holding a lock,
+    and knowing that you are on a particular thread. Here, we
+    abstract it to "some" lock and "any particular" thread (typically, UI thread)
+    For a more precide semantics we would replace Thread by representatives of
+    thread id's and Lock by multiple differnet lock id's.
+    Both indicates that you both know the thread and hold a lock.
+    There is no need for a lattice relation between Thread, Lock and Both:
+    you don't ever join Thread and Lock, rather, they are treated pointwise.
+ **)
+module Excluder: sig
+  type t =
+    | Thread
+    | Lock
+    | Both
+  [@@deriving compare]
+
+  val pp : F.formatter -> t -> unit
+end
+
 module AccessPrecondition : sig
   type t =
-    | Protected
+    | Protected of Excluder.t
-    (** access safe due to held lock (i.e., pre is true *)
+    (** access potentially protected for mutual exclusion by
+        lock or thread or both *)
     | Unprotected of int option
     (** access rooted in formal at index i. Safe if actual passed at index is owned (i.e.,
         !owned(i) implies an unsafe access). Unprotected None means the access is unsafe unless a

infer/tests/codetoanalyze/java/threadsafety/Annotations.java

@@ -177,9 +177,7 @@ class Annotations implements Interface {
      ii = 22;
   }
 
-/*
+ void conditional_Bad(boolean b){
-fix with a more refined abstract domain (without going all the way to disjuntions) */
- void FN_conditional_Bad(boolean b){
    if (b)
    {
      write_on_main_thread_Ok();

infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java

@@ -90,26 +90,24 @@ class RaceWithMainThread{
      g = 77;
    }
 
-/* This was a source of false positives until we interpreted join of threaded
+Integer ff;
-by || instead of &&; see BooleanOr in ThreadSafetyDomain.ml */
+
  void conditional_Ok(boolean b){
    if (b)
    { /*People not literally putting this assert inside if's,
        but implicitly by method calls */
      o. assertMainThread();
-     f = 88;
+     ff = 88;
-   } /* BooleanAnd for threaded would hose you here and lead to a report */
+   }
  }
 
-/* On the other hand, BooleanOr leads to false negatives, which we should
+ void conditional_Bad(boolean b){
-fix with a more refined abstract domain (without going all the way to disjuntions) */
- void FN_conditional_Bad(boolean b){
    if (b)
    {
      o.assertMainThread();
-     f = 88;
+     ff = 88;
    } else {
-     f = 99; // Using || hoses this; no report
+     ff = 99;
    }
  }
 }

infer/tests/codetoanalyze/java/threadsafety/ThreadSafeMethods.java

@@ -62,7 +62,7 @@ class ThreadSafeMethods {
     this.field1 = new Object();
   }
 
-  public synchronized Object readSameFieldAsThreadSafeMethod1Ok() {
+  public synchronized Object readSameFieldAsThreadSafeMethodWhileSynchronized1Bad() {
     return this.field1;
   }
 
@@ -82,7 +82,7 @@ class ThreadSafeMethods {
   }
 
   @ThreadSafe
-  public synchronized Object synchronizedReadOk() {
+  public synchronized Object synchronizedReadBad() {
     return this.field5;
   }
 

infer/tests/codetoanalyze/java/threadsafety/issues.exp

@@ -4,6 +4,7 @@ codetoanalyze/java/threadsafety/Annotations.java, double Annotations.functionalD
 codetoanalyze/java/threadsafety/Annotations.java, int Annotations.FP_functionalAcrossBoxingLongOk(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mBoxedLong2`]
 codetoanalyze/java/threadsafety/Annotations.java, int Annotations.functionalAcrossUnboxingLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mLong2`]
 codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionaLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mLong`]
+codetoanalyze/java/threadsafety/Annotations.java, void Annotations.conditional_Bad(boolean), 5, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.ii`]
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.functionalAndNonfunctionalBad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mInt`]
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateOffUiThreadBad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.f`]
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateSubfieldOfConfinedBad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.encapsulatedField.codetoanalyze.java.checkers.Obj.f`]
@@ -62,6 +63,7 @@ codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedIn
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad2(), 2, THREAD_SAFETY_VIOLATION, [call to void Ownership.writeToFormal(Obj),access to `codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad3(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to `codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToOwnedInCalleeOk2(), 4, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.Ownership.field`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.Ownership.field`]
+codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.conditional_Bad(boolean), 6, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.RaceWithMainThread.ff`]
 codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.readProtectedUnthreadedBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.RaceWithMainThread.f`]
 codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded_Bad(), 2, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.RaceWithMainThread.f`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.RaceWithMainThread.f`]
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.callUnprotecteReadInCallee(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,call to Object ReadWriteRaces.unprotectedReadInCallee(),access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`]
@@ -84,6 +86,8 @@ codetoanalyze/java/threadsafety/ThreadSafeExample.java, void YesThreadSafeExtend
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethod1Bad(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.ThreadSafeMethods.field1`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.ThreadSafeMethods.field1`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethod2Bad(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.ThreadSafeMethods.field4`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.ThreadSafeMethods.field4`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethod3Bad(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.ThreadSafeMethods.field5`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.ThreadSafeMethods.field5`]
+codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethodWhileSynchronized1Bad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ThreadSafeMethods.field1`]
+codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.synchronizedReadBad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ThreadSafeMethods.field5`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.threadSafeMethodReadBad(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.ThreadSafeMethods.field2`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.ThreadSafeMethods.field2`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethodsSubclass.readThreadSafeFieldOfOverrideBad(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.ThreadSafeMethodsSubclass.subclassField`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.ThreadSafeMethodsSubclass.subclassField`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, void ThreadSafeMethods.threadSafeMethodWriteBad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ThreadSafeMethods.field1`]