[thread-safety] refactoring to make it easier to add container reads

Summary: Adding new ContainerRead access kind + utilities for creating it.

Reviewed By: da319

Differential Revision: D5493322

fbshipit-source-id: 4ce6704

infer/src/checkers/ThreadSafety.ml

@@ -42,6 +42,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   type thread_model = Threaded | Unknown | ThreadedIfTrue
 
+  type container_access_model = ContainerRead | ContainerWrite
+
   let is_thread_utils_type java_pname =
     let pn = Typ.Procname.java_get_class_name java_pname in
     String.is_suffix ~suffix:"ThreadUtils" pn || String.is_suffix ~suffix:"ThreadUtil" pn
@@ -132,6 +134,36 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | _
      -> Unknown
 
+  let get_container_access pn tenv =
+    match pn with
+    | Typ.Procname.Java java_pname
+     -> let typename = Typ.Name.Java.from_string (Typ.Procname.java_get_class_name java_pname) in
+        let get_container_access_ typename _ =
+          match (Typ.Name.name typename, Typ.Procname.java_get_method java_pname) with
+          | ( ("android.util.SparseArray" | "android.support.v4.util.SparseArrayCompat")
+            , ( "append" | "clear" | "delete" | "put" | "remove" | "removeAt" | "removeAtRange"
+              | "setValueAt" ) )
+           -> Some ContainerWrite
+          | ( "android.support.v4.util.SimpleArrayMap"
+            , ("clear" | "ensureCapacity" | "put" | "putAll" | "remove" | "removeAt" | "setValueAt")
+            )
+           -> Some ContainerWrite
+          | "android.support.v4.util.Pools$SimplePool", ("acquire" | "release")
+           -> Some ContainerWrite
+          | "java.util.List", ("add" | "addAll" | "clear" | "remove" | "set")
+           -> Some ContainerWrite
+          | "java.util.Map", ("clear" | "put" | "putAll" | "remove")
+           -> Some ContainerWrite
+          | "java.util.Map", "get" when false
+           -> (* temporary measure to silence compiler warning *)
+              Some ContainerRead
+          | _
+           -> None
+        in
+        PatternMatch.supertype_find_map_opt tenv get_container_access_ typename
+    | _
+     -> None
+
   let add_conditional_ownership_attribute access_path formal_map attribute_map attributes =
     match FormalMap.get_formal_index (fst access_path) formal_map with
     | Some formal_index when not (is_owned access_path attribute_map)
@@ -392,33 +424,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     is_allocation pname || is_owned_in_library pname
     || PatternMatch.override_exists is_owned_in_library tenv pname
 
-  let is_container_write pn tenv =
-    match pn with
-    | Typ.Procname.Java java_pname
-     -> let typename = Typ.Name.Java.from_string (Typ.Procname.java_get_class_name java_pname) in
-        let is_container_write_ typename _ =
-          match (Typ.Name.name typename, Typ.Procname.java_get_method java_pname) with
-          | ( ("android.util.SparseArray" | "android.support.v4.util.SparseArrayCompat")
-            , ( "append" | "clear" | "delete" | "put" | "remove" | "removeAt" | "removeAtRange"
-              | "setValueAt" ) )
-           -> true
-          | ( "android.support.v4.util.SimpleArrayMap"
-            , ("clear" | "ensureCapacity" | "put" | "putAll" | "remove" | "removeAt" | "setValueAt")
-            )
-           -> true
-          | "android.support.v4.util.Pools$SimplePool", ("acquire" | "release")
-           -> true
-          | "java.util.List", ("add" | "addAll" | "clear" | "remove" | "set")
-           -> true
-          | "java.util.Map", ("clear" | "put" | "putAll" | "remove")
-           -> true
-          | _
-           -> false
-        in
-        PatternMatch.supertype_exists tenv is_container_write_ typename
-    | _
-     -> false
-
   let is_threadsafe_collection pn tenv =
     match pn with
     | Typ.Procname.Java java_pname
@@ -479,17 +484,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     Some (true, false, false, callee_accesses, AttributeSetDomain.empty, escapee_formals)
 
   let get_summary caller_pdesc callee_pname actuals callee_loc tenv =
-    if is_container_write callee_pname tenv then
-      let receiver_ap =
-        match List.hd actuals with
-        | Some HilExp.AccessPath receiver_ap
-         -> receiver_ap
-        | _
-         -> failwithf "Call to %a is marked as a container write, but has no receiver"
-              Typ.Procname.pp callee_pname
-      in
-      make_container_write callee_pname actuals receiver_ap callee_loc tenv
-    else Summary.read_summary caller_pdesc callee_pname
+    match get_container_access callee_pname tenv with
+    | Some ContainerWrite
+     -> let receiver_ap =
+          match List.hd actuals with
+          | Some HilExp.AccessPath receiver_ap
+           -> receiver_ap
+          | _
+           -> failwithf "Call to %a is marked as a container write, but has no receiver"
+                Typ.Procname.pp callee_pname
+        in
+        make_container_write callee_pname actuals receiver_ap callee_loc tenv
+    | Some ContainerRead
+     -> failwith "Container reads not yet supported"
+    | None
+     -> Summary.read_summary caller_pdesc callee_pname
 
   (* return true if the given procname boxes a primitive type into a reference type *)
   let is_box = function
@@ -1064,7 +1073,7 @@ let pp_access fmt sink =
   match ThreadSafetyDomain.PathDomain.Sink.kind sink with
   | Read access_path | Write access_path
    -> F.fprintf fmt "%a" (MF.wrap_monospaced AccessPath.pp_access_list) (snd access_path)
-  | ContainerWrite (access_path, access_pname)
+  | ContainerRead (access_path, access_pname) | ContainerWrite (access_path, access_pname)
    -> pp_container_access fmt (access_path, access_pname)
   | InterfaceCall _ as access
    -> F.fprintf fmt "%a" ThreadSafetyDomain.Access.pp access
@@ -1076,6 +1085,10 @@ let desc_of_sink sink =
    -> if Typ.Procname.equal sink_pname Typ.Procname.empty_block then
         F.asprintf "access to %a" pp_access sink
       else F.asprintf "call to %a" Typ.Procname.pp sink_pname
+  | ContainerRead (access_path, access_pname)
+   -> if Typ.Procname.equal sink_pname access_pname then
+        F.asprintf "Read of %a" pp_container_access (access_path, access_pname)
+      else F.asprintf "call to %a" Typ.Procname.pp sink_pname
   | ContainerWrite (access_path, access_pname)
    -> if Typ.Procname.equal sink_pname access_pname then
         F.asprintf "Write to %a" pp_container_access (access_path, access_pname)
@@ -1255,7 +1268,7 @@ let report_unsafe_accesses aggregated_access_map =
     match TraceElem.kind access with
     | Access.Write _ | Access.ContainerWrite _
      -> Typ.Procname.Set.mem pname reported_writes
-    | Access.Read _
+    | Access.Read _ | Access.ContainerRead _
      -> Typ.Procname.Set.mem pname reported_reads
     | Access.InterfaceCall _
      -> false
@@ -1266,7 +1279,7 @@ let report_unsafe_accesses aggregated_access_map =
     | Access.Write _ | Access.ContainerWrite _
      -> let reported_writes = Typ.Procname.Set.add pname reported.reported_writes in
         {reported with reported_writes; reported_sites}
-    | Access.Read _
+    | Access.Read _ | Access.ContainerRead _
      -> let reported_reads = Typ.Procname.Set.add pname reported.reported_reads in
         {reported with reported_reads; reported_sites}
     | Access.InterfaceCall _
@@ -1298,7 +1311,7 @@ let report_unsafe_accesses aggregated_access_map =
       | (Access.Write _ | ContainerWrite _), AccessPrecondition.Protected _
        -> (* protected write, do nothing *)
           reported_acc
-      | Access.Read _, AccessPrecondition.Unprotected _
+      | (Access.Read _ | ContainerRead _), AccessPrecondition.Unprotected _
        -> (* unprotected read. report all writes as conflicts for java *)
           (* for c++ filter out unprotected writes *)
           let is_cpp_protected_write pre =
@@ -1322,7 +1335,7 @@ let report_unsafe_accesses aggregated_access_map =
               ~conflicts:(List.map ~f:(fun (access, _, _, _, _) -> access) all_writes)
               access ;
             update_reported access pname reported_acc )
-      | Access.Read _, AccessPrecondition.Protected excl
+      | (Access.Read _ | ContainerRead _), AccessPrecondition.Protected excl
        -> (* protected read.
              report unprotected writes and opposite protected writes as conflicts
              Thread and Lock are opposites of one another, and

infer/src/checkers/ThreadSafetyDomain.ml

@@ -14,6 +14,7 @@ module Access = struct
   type t =
     | Read of AccessPath.Raw.t
     | Write of AccessPath.Raw.t
+    | ContainerRead of AccessPath.Raw.t * Typ.Procname.t
     | ContainerWrite of AccessPath.Raw.t * Typ.Procname.t
     | InterfaceCall of Typ.Procname.t
     [@@deriving compare]
@@ -22,7 +23,10 @@ module Access = struct
     if is_write then Write access_path else Read access_path
 
   let get_access_path = function
-    | Read access_path | Write access_path | ContainerWrite (access_path, _)
+    | Read access_path
+    | Write access_path
+    | ContainerWrite (access_path, _)
+    | ContainerRead (access_path, _)
      -> Some access_path
     | InterfaceCall _
      -> None
@@ -34,6 +38,9 @@ module Access = struct
      -> F.fprintf fmt "Read of %a" AccessPath.Raw.pp access_path
     | Write access_path
      -> F.fprintf fmt "Write to %a" AccessPath.Raw.pp access_path
+    | ContainerRead (access_path, pname)
+     -> F.fprintf fmt "Read of container %a via %a" AccessPath.Raw.pp access_path Typ.Procname.pp
+          pname
     | ContainerWrite (access_path, pname)
      -> F.fprintf fmt "Write to container %a via %a" AccessPath.Raw.pp access_path Typ.Procname.pp
           pname
@@ -47,10 +54,18 @@ module TraceElem = struct
   type t = {site: CallSite.t; kind: Kind.t} [@@deriving compare]
 
   let is_write {kind} =
-    match kind with InterfaceCall _ | Read _ -> false | ContainerWrite _ | Write _ -> true
+    match kind with
+    | InterfaceCall _ | Read _ | ContainerRead _
+     -> false
+    | ContainerWrite _ | Write _
+     -> true
 
   let is_container_write {kind} =
-    match kind with InterfaceCall _ | Read _ | Write _ -> false | ContainerWrite _ -> true
+    match kind with
+    | InterfaceCall _ | Read _ | Write _ | ContainerRead _
+     -> false
+    | ContainerWrite _
+     -> true
 
   let call_site {site} = site
 

infer/src/checkers/ThreadSafetyDomain.mli

@@ -14,6 +14,7 @@ module Access : sig
   type t =
     | Read of AccessPath.Raw.t  (** Field or array read *)
     | Write of AccessPath.Raw.t  (** Field or array write *)
+    | ContainerRead of AccessPath.Raw.t * Typ.Procname.t  (** Read of container object *)
     | ContainerWrite of AccessPath.Raw.t * Typ.Procname.t  (** Write to container object *)
     | InterfaceCall of Typ.Procname.t
         (** Call to method of interface not annotated with @ThreadSafe *)