[threadsafety] Fix make-excluder uses which potentially incorrectly assume a lock is held.

Reviewed By: sblackshear

Differential Revision: D5931811

fbshipit-source-id: d51dd6b

infer/src/checkers/ThreadSafety.ml

@@ -21,14 +21,6 @@ module Summary = Summary.Make (struct
   let read_payload (summary: Specs.summary) = summary.payload.threadsafety
 end)
 
-(*Bit of redundancy with code in is_unprotected, might alter later *)
-let make_excluder locks thread =
-  let is_main_thread = ThreadSafetyDomain.ThreadsDomain.is_any_but_self thread in
-  if locks && not is_main_thread then ThreadSafetyDomain.Excluder.Lock
-  else if not locks && is_main_thread then ThreadSafetyDomain.Excluder.Thread
-  else if locks && is_main_thread then ThreadSafetyDomain.Excluder.Both
-  else L.(die InternalError) "called when neither lock nor thread known"
-
 module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = ThreadSafetyDomain
@@ -306,10 +298,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         let attribute_map' = AttributeMapDomain.add ret_access_path ret_attributes attribute_map in
         (ownership', attribute_map')
 
-  let is_unprotected is_locked thread pdesc =
-    not is_locked && not (ThreadSafetyDomain.ThreadsDomain.is_any_but_self thread)
-    && not (Procdesc.is_java_synchronized pdesc)
-
   (** return true if this function is library code from the JDK core libraries or Android *)
   let is_java_library = function
     | Typ.Procname.Java java_pname -> (
@@ -342,12 +330,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
        && not (has_return_annot Annotations.ia_is_thread_safe pname)
     then
       let open Domain in
-      let pre =
+      let pre = AccessPrecondition.make locks threads proc_data.pdesc in
-        if is_unprotected locks threads proc_data.pdesc then AccessPrecondition.TotallyUnprotected
-        else
-          AccessPrecondition.Protected
-            (make_excluder (locks || Procdesc.is_java_synchronized proc_data.pdesc) threads)
-      in
       AccessDomain.add_access pre (make_unannotated_call_access pname loc) attribute_map
     else attribute_map
 
@@ -390,7 +373,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       if List.is_empty accesses || OwnershipDomain.is_owned base_access_path ownership then acc
       else
         let pre =
-          if is_unprotected locks threads proc_data.pdesc then
+          match AccessPrecondition.make locks threads proc_data.pdesc with
+          | AccessPrecondition.Protected _ as excluder
+           -> excluder
+          | _ ->
             match OwnershipDomain.get_owned base_access_path ownership with
             | OwnershipAbstractValue.OwnedIf formal_indexes
              -> AccessPrecondition.Unprotected formal_indexes
@@ -398,9 +384,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
              -> assert false
             | OwnershipAbstractValue.Unowned
              -> AccessPrecondition.TotallyUnprotected
-          else
-            AccessPrecondition.Protected
-              (make_excluder (locks || Procdesc.is_java_synchronized proc_data.pdesc) threads)
         in
         add_field_accesses pre base_access_path acc accesses
     in
@@ -720,7 +703,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                       | _
                        -> ThreadsDomain.join threads astate.threads
                     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 =
@@ -735,14 +717,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                             accesses_acc
                           else
                             let pre =
-                              if unprotected then
+                              match AccessPrecondition.make locks threads pdesc with
-                                let base = fst actual_access_path in
+                              | AccessPrecondition.Protected _ as excluder (* access protected *)
+                               -> excluder
+                              | _
+                               -> let base = fst actual_access_path in
                                   match OwnershipDomain.get_owned (base, []) astate.ownership with
                                   | OwnershipAbstractValue.OwnedIf formal_indexes
                                    -> (* the actual passed to the current callee is rooted in a
                                      formal *)
                                       AccessPrecondition.Unprotected formal_indexes
-                                | OwnershipAbstractValue.Unowned | OwnershipAbstractValue.Owned ->
+                                  | OwnershipAbstractValue.Unowned | OwnershipAbstractValue.Owned
+                                   ->
                                     match
                                       OwnershipDomain.get_owned actual_access_path astate.ownership
                                     with
@@ -756,9 +742,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                                      -> (* access path not rooted in a formal and not conditionally
                                        owned *)
                                         AccessPrecondition.TotallyUnprotected
-                              else
-                                (* access protected by held lock *)
-                                AccessPrecondition.Protected (make_excluder true threads)
                             in
                             update_caller_accesses pre ownership_accesses accesses_acc
                       | _
@@ -772,10 +755,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                         | AccessPrecondition.Protected _
                          -> update_caller_accesses pre callee_accesses accesses_acc
                         | AccessPrecondition.TotallyUnprotected
-                         -> let pre' =
+                         -> let pre' = AccessPrecondition.make locks threads pdesc in
-                              if unprotected then pre
-                              else AccessPrecondition.Protected (make_excluder true threads)
-                            in
                             update_caller_accesses pre' callee_accesses accesses_acc
                         | AccessPrecondition.Unprotected formal_indexes
                          -> IntSet.fold

infer/src/checkers/ThreadSafetyDomain.ml

@@ -336,6 +336,14 @@ module AccessPrecondition = struct
     | Unprotected indexes
      -> F.fprintf fmt "Unprotected(%a)" (PrettyPrintable.pp_collection ~pp_item:Int.pp)
           (IntSet.elements indexes)
+
+  let make locks thread pdesc =
+    let is_main_thread = ThreadsDomain.is_any_but_self thread in
+    let locked = locks || Procdesc.is_java_synchronized pdesc in
+    if not locked && not is_main_thread then TotallyUnprotected
+    else if locked && is_main_thread then Protected Excluder.Both
+    else if locked then Protected Excluder.Lock
+    else Protected Excluder.Thread
 end
 
 module AccessDomain = struct

infer/src/checkers/ThreadSafetyDomain.mli

@@ -164,6 +164,8 @@ module AccessPrecondition : sig
     [@@deriving compare]
 
   val pp : F.formatter -> t -> unit
+
+  val make : LocksDomain.astate -> ThreadsDomain.astate -> Procdesc.t -> t
 end
 
 (** map of access precondition |-> set of accesses. the map should hold all accesses to a