[thread-safety] track container reads and report read/write races

Summary:
Works the same way as read/write races on fields, except that are more relaxed (er, unsound) in deciding whether two containers may alias.
This is needed to avoid reporting a ton of FP's; full explanation in comments.

Reviewed By: da319

Differential Revision: D5493404

fbshipit-source-id: 0a5d8b1

infer/src/checkers/ThreadSafety.ml

@@ -144,19 +144,31 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             , ( "append" | "clear" | "delete" | "put" | "remove" | "removeAt" | "removeAtRange"
               | "setValueAt" ) )
            -> Some ContainerWrite
+          | ( ("android.util.SparseArray" | "android.support.v4.util.SparseArrayCompat")
+            , ("clone" | "get" | "indexOfKey" | "indexOfValue" | "keyAt" | "size" | "valueAt") )
+           -> Some ContainerRead
           | ( "android.support.v4.util.SimpleArrayMap"
             , ("clear" | "ensureCapacity" | "put" | "putAll" | "remove" | "removeAt" | "setValueAt")
             )
            -> Some ContainerWrite
+          | ( "android.support.v4.util.SimpleArrayMap"
+            , ( "containsKey" | "containsValue" | "get" | "hashCode" | "indexOfKey" | "isEmpty"
+              | "keyAt" | "size" | "valueAt" ) )
+           -> Some ContainerRead
           | "android.support.v4.util.Pools$SimplePool", ("acquire" | "release")
            -> Some ContainerWrite
           | "java.util.List", ("add" | "addAll" | "clear" | "remove" | "set")
            -> Some ContainerWrite
+          | ( "java.util.List"
+            , ( "contains" | "containsAll" | "equals" | "get" | "hashCode" | "indexOf" | "isEmpty"
+              | "iterator" | "lastIndexOf" | "listIterator" | "size" | "toArray" ) )
+           -> Some ContainerRead
           | "java.util.Map", ("clear" | "put" | "putAll" | "remove")
            -> Some ContainerWrite
-          | "java.util.Map", "get" when false
-           -> (* temporary measure to silence compiler warning *)
-              Some ContainerRead
+          | ( "java.util.Map"
+            , ( "containsKey" | "containsValue" | "entrySet" | "equals" | "get" | "hashCode"
+              | "isEmpty" | "keySet" | "size" | "values" ) )
+           -> Some ContainerRead
           | _
            -> None
         in
@@ -467,15 +479,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | _
        -> false
 
-  let make_container_write callee_pname actuals receiver_ap callee_loc tenv =
+  let make_container_access callee_pname ~is_write actuals receiver_ap callee_loc tenv =
     (* create a dummy write that represents mutating the contents of the container *)
     let open Domain in
     let callee_accesses =
       if is_synchronized_container callee_pname receiver_ap tenv then AccessDomain.empty
       else
-        let container_access = make_container_access receiver_ap callee_pname in
-        AccessDomain.add_access (Unprotected (Some 0)) (container_access ~is_write:true callee_loc)
-          AccessDomain.empty
+        let container_access =
+          make_container_access receiver_ap ~is_write callee_pname callee_loc
+        in
+        AccessDomain.add_access (Unprotected (Some 0)) container_access AccessDomain.empty
     in
     (* TODO: for now all formals escape *)
     (* we need a more intelligent escape analysis, that branches on whether
@@ -484,19 +497,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 =
+    let get_receiver_ap actuals =
+      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
     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
+     -> make_container_access callee_pname ~is_write:true actuals (get_receiver_ap actuals)
+          callee_loc tenv
     | Some ContainerRead
-     -> failwith "Container reads not yet supported"
+     -> make_container_access callee_pname ~is_write:false actuals (get_receiver_ap actuals)
+          callee_loc tenv
     | None
      -> Summary.read_summary caller_pdesc callee_pname
 
@@ -1208,7 +1223,7 @@ let make_read_write_race_description conflicts tenv pname final_sink_site initia
           "\n Note: some of these write conflicts are confined to the UI or another thread, but the current method is not specified to be. Consider adding synchronization or a @ThreadConfined annotation to the current method."
       else "" )
   in
-  Format.asprintf "Read/Write race. Non-private method %a%s reads from field %a. %s %s"
+  Format.asprintf "Read/Write race. Non-private method %a%s reads from %a. %s %s"
     (MF.wrap_monospaced pp_procname_short) pname
     (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly")
     pp_access final_sink conflicts_description (calculate_addendum_message tenv pname)
@@ -1462,6 +1477,32 @@ let may_alias tenv p1 p2 =
   | ArrayAccess t1, ArrayAccess t2
    -> equal_desc t1.desc t2.desc
 
+let may_alias_container tenv p1 p2 =
+  let sound = false in
+  if sound then
+    (* this is much too noisy: we'll warn that accesses to *any* Map can race with accesses to any
+       other Map, etc. Instead, do something simple and unsound: just assume that two accesses can
+       be to the same container if they are to the same access path *)
+    match (AccessPath.Raw.get_typ p1 tenv, AccessPath.Raw.get_typ p2 tenv) with
+    | Some {desc= Tptr ({desc= Tstruct tn1}, _)}, Some {desc= Tptr ({desc= Tstruct tn2}, _)}
+     -> PatternMatch.is_subtype tenv tn1 tn2 || PatternMatch.is_subtype tenv tn2 tn1
+    | _
+     -> true
+  else
+    (* unsound, but effective: report that the containers alias if their access paths are
+       syntactically identical *)
+    match (fst p1, fst p2) with
+    | (Var.ProgramVar pvar1, typ1), (Var.ProgramVar pvar2, typ2)
+      when Pvar.is_this pvar1 && Pvar.is_this pvar2
+           && ( Prover.Subtyping_check.check_subtype tenv typ1 typ2
+              || Prover.Subtyping_check.check_subtype tenv typ2 typ1 )
+     -> (* the `this` used in C.foo and C.bar will compare unequal if we're not careful `this` is
+           represented as a local pvar, and a local pvar contains its parent procedure name. Count
+           the `this`'s as equal if their types are compatible *)
+        AccessPath.equal_access_list (snd p1) (snd p2)
+    | _
+     -> AccessPath.Raw.equal p1 p2
+
 (* take a results table and quotient it by the may_alias relation *)
 let quotient_access_map acc_map =
   let rec aux acc m =
@@ -1479,6 +1520,9 @@ let quotient_access_map acc_map =
             match (k, k') with
             | (Read ap1 | Write ap1), (Read ap2 | Write ap2)
              -> may_alias tenv ap1 ap2
+            | ( (ContainerRead (ap1, _) | ContainerWrite (ap1, _))
+              , (ContainerRead (ap2, _) | ContainerWrite (ap2, _)) )
+             -> may_alias_container tenv ap1 ap2
             | _
              -> ThreadSafetyDomain.Access.equal k k')
           m

infer/src/checkers/ThreadSafetyDomain.ml

@@ -86,9 +86,13 @@ module TraceElem = struct
   end)
 end
 
-let make_container_access access_path pname ~is_write:_ loc =
+let make_container_access access_path pname ~is_write loc =
   let site = CallSite.make Typ.Procname.empty_block loc in
-  TraceElem.make (Access.ContainerWrite (access_path, pname)) site
+  let access =
+    if is_write then Access.ContainerWrite (access_path, pname)
+    else Access.ContainerRead (access_path, pname)
+  in
+  TraceElem.make access site
 
 let make_field_access access_path ~is_write loc =
   let site = CallSite.make Typ.Procname.empty_block loc in

infer/tests/codetoanalyze/java/threadsafety/Containers.java

@@ -85,11 +85,17 @@ class Containers {
     list.remove(index);
   }
 
+  List mListNobodyWrites;
+
   void listReadOk(int index, String s) {
-    mList.contains(s);
-    mList.get(index);
-    mList.isEmpty();
-    mList.size();
+    mListNobodyWrites.contains(s);
+    mListNobodyWrites.get(index);
+    mListNobodyWrites.isEmpty();
+    mListNobodyWrites.size();
+  }
+
+  boolean listReadBad(String s) {
+    return mList.contains(s);
   }
 
   void accessSafeListOk(CopyOnWriteArrayList list, int index) {
@@ -113,15 +119,17 @@ class Containers {
     mMap.putAll(otherMap);
   }
 
+  Map<String,String> mMapNobodyWrites;
+
   void mapReadsOk(String s) {
-    mMap.containsKey(s);
-    mMap.containsValue(s);
-    mMap.entrySet();
-    mMap.hashCode();
-    mMap.isEmpty();
-    mMap.keySet();
-    mMap.size();
-    mMap.values();
+    mMapNobodyWrites.containsKey(s);
+    mMapNobodyWrites.containsValue(s);
+    mMapNobodyWrites.entrySet();
+    mMapNobodyWrites.hashCode();
+    mMapNobodyWrites.isEmpty();
+    mMapNobodyWrites.keySet();
+    mMapNobodyWrites.size();
+    mMapNobodyWrites.values();
   }
 
   // make sure we still warn on subtypes of Map
@@ -270,7 +278,7 @@ class Containers {
   }
 
   // this should be a read/write race with addToSimpleArrayMapOk
-  public int FN_readSimpleArrayMap() {
+  public int readSimpleArrayMap() {
     return si_map.get(1);
   }
 
@@ -287,4 +295,15 @@ class Containers {
     simplePool.release(a);
   }
 
+  Map<String,String> mAliasedMap;
+
+  // won't report here because the read happens through an alias
+  public String FN_AliasedMapBad() {
+    synchronized (this) {
+      mAliasedMap.put("a", "b");
+    }
+    Map<String,String> alias = mAliasedMap;
+    return alias.get("a");
+  }
+
 }

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

@@ -21,6 +21,8 @@ codetoanalyze/java/threadsafety/Builders.java, void TopLevelBuilder.setG(String)
 codetoanalyze/java/threadsafety/Constructors.java, Constructors Constructors.singletonBad(), 2, THREAD_SAFETY_VIOLATION, [call to Constructors.<init>(Object),access to `Constructors.staticField`]
 codetoanalyze/java/threadsafety/Constructors.java, Constructors.<init>(), 1, THREAD_SAFETY_VIOLATION, [access to `Constructors.staticField`]
 codetoanalyze/java/threadsafety/Constructors.java, Constructors.<init>(Constructors), 1, THREAD_SAFETY_VIOLATION, [access to `Constructors.field`]
+codetoanalyze/java/threadsafety/Containers.java, boolean Containers.listReadBad(String), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,Read of container `&this.codetoanalyze.java.checkers.Containers.mList` via call to `contains`,<Beginning of write trace>,Write to container `&this.codetoanalyze.java.checkers.Containers.mList` via call to `set`]
+codetoanalyze/java/threadsafety/Containers.java, int Containers.readSimpleArrayMap(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,Read of container `&this.codetoanalyze.java.checkers.Containers.si_map` via call to `get`,<Beginning of write trace>,Write to container `&this.codetoanalyze.java.checkers.Containers.si_map` via call to `put`]
 codetoanalyze/java/threadsafety/Containers.java, void Containers.addToSimpleArrayMapBad(SimpleArrayMap), 1, THREAD_SAFETY_VIOLATION, [Write to container `&map` via call to `put`]
 codetoanalyze/java/threadsafety/Containers.java, void Containers.addToSparseArrayBad(SparseArray), 1, THREAD_SAFETY_VIOLATION, [Write to container `&sparseArray` via call to `put`]
 codetoanalyze/java/threadsafety/Containers.java, void Containers.addToSparseArrayCompatBad(SparseArrayCompat), 1, THREAD_SAFETY_VIOLATION, [Write to container `&sparseArray` via call to `put`]