[thread-safety] relax treatment of array aliasing

Reviewed By: ngorogiannis

Differential Revision: D5512595

fbshipit-source-id: b47cc08

infer/src/checkers/ThreadSafety.ml

@@ -1455,30 +1455,9 @@ let report_unsafe_accesses aggregated_access_map =
     aggregated_access_map empty_reported
   |> ignore
 
-(* equivalence relation computing whether two access paths may refer to the
-   same heap location. *)
-let may_alias tenv p1 p2 =
-  let open Typ in
-  let open AccessPath in
-  phys_equal p1 p2
-  ||
-  match (List.last_exn (snd p1), List.last_exn (snd p2)) with
-  | FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _
-   -> false
-  (* fields in Java contain the class name /declaring/ them
-     thus two fields can be aliases *iff* they are equal *)
-  | FieldAccess f1, FieldAccess f2
-   -> Typ.Fieldname.equal f1 f2
-  (* if arrays of objects that have an inheritance rel then they can alias *)
-  | ( ArrayAccess {desc= Tptr ({desc= Tstruct tn1}, _)}
-    , ArrayAccess {desc= Tptr ({desc= Tstruct tn2}, _)} )
-   -> PatternMatch.is_subtype tenv tn1 tn2 || PatternMatch.is_subtype tenv tn2 tn1
-  (* primitive type arrays can alias if the prim. type is the same *)
-  | ArrayAccess t1, ArrayAccess t2
-   -> equal_desc t1.desc t2.desc
+let sound = false
 
 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
@@ -1503,6 +1482,29 @@ let may_alias_container tenv p1 p2 =
     | _
      -> AccessPath.Raw.equal p1 p2
 
+(* equivalence relation computing whether two access paths may refer to the
+   same heap location. *)
+let may_alias tenv p1 p2 =
+  let open Typ in
+  let open AccessPath in
+  phys_equal p1 p2
+  ||
+  match (List.last_exn (snd p1), List.last_exn (snd p2)) with
+  | FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _
+   -> false
+  (* fields in Java contain the class name /declaring/ them
+     thus two fields can be aliases *iff* they are equal *)
+  | FieldAccess f1, FieldAccess f2
+   -> Typ.Fieldname.equal f1 f2
+  (* if arrays of objects that have an inheritance rel then they can alias *)
+  | ( ArrayAccess {desc= Tptr ({desc= Tstruct tn1}, _)}
+    , ArrayAccess {desc= Tptr ({desc= Tstruct tn2}, _)} )
+   -> if sound then PatternMatch.is_subtype tenv tn1 tn2 || PatternMatch.is_subtype tenv tn2 tn1
+      else may_alias_container tenv p1 p2
+  (* primitive type arrays can alias if the prim. type is the same *)
+  | ArrayAccess t1, ArrayAccess t2
+   -> if sound then equal_desc t1.desc t2.desc else may_alias_container tenv 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 =

infer/tests/codetoanalyze/java/threadsafety/Arrays.java

@@ -0,0 +1,80 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+import javax.annotation.concurrent.ThreadSafe;
+
+// Test may_alias treatment of arrays
+// two arrays of types in a subtype relation may alias, and race
+
+@ThreadSafe
+class Parent {}
+
+@ThreadSafe
+class Child extends Parent {}
+
+@ThreadSafe
+class Arrays {
+  Child[] childArr = new Child[5];
+  Parent[] parentArr = childArr; // actual aliasing not required, but for documentation
+  final String[] strArr1 = new String[5];
+  final String[] strArr2 = new String[5];
+
+  void arrayParameterWriteBad(int[] name1) {
+    name1[2] = 4;
+  }
+
+  // we'll report this because name1 and name2 may alias
+  int arrayParameterReadBad(int[] name2) {
+    return name2[2];
+  }
+
+  int arrayParameterLiteralReadOk() {
+    return (new int[] { 2, 3})[1];
+  }
+
+  public void writeWriteRaceBad(String s) {
+    strArr1[2] = s;
+  }
+
+  // same array
+  public String readWriteRaceBad(String s) {
+    synchronized (this) {
+      strArr1[2] = s;
+    }
+    return strArr1[2];
+  }
+
+  // arrays are same type, but can't alias
+  public String notReadWriteRace1Ok(String s) {
+    synchronized (this) {
+      strArr1[0] = s;
+    }
+    return strArr2[0];
+  }
+
+  // arrays are compatible types and can alias
+  public Child FN_readWriteAliasRaceBad() {
+    synchronized(this) {
+      parentArr[3] = null;
+    }
+    return childArr[3];
+  }
+
+  String[] type1Arr[];
+  Parent[] type2Arr;
+
+  // arrays are different types and thus cannot alias
+  public Parent noRaceOk() {
+    synchronized(this) {
+      type1Arr[3] = null;
+    }
+
+    return type2Arr[3];
+  }
+
+}

infer/tests/codetoanalyze/java/threadsafety/SubArr.java

@@ -1,42 +0,0 @@
-/*
- * Copyright (c) 2017 - present Facebook, Inc.
- * All rights reserved.
- *
- * This source code is licensed under the BSD style license found in the
- * LICENSE file in the root directory of this source tree. An additional grant
- * of patent rights can be found in the PATENTS file in the same directory.
- */
-import javax.annotation.concurrent.ThreadSafe;
-
-// Test may_alias treatment of arrays
-// two arrays of types in a subtype relation may alias, and race
-
-@ThreadSafe
-class Parent {}
-
-@ThreadSafe
-class Child extends Parent {}
-
-@ThreadSafe
-class SubArr {
-  Child[] childArr = new Child[5];
-  Parent[] parentArr = childArr; // actual aliasing not required, but for documentation
-  String[] strArr = new String[5];
-
-  public Child RWrace() {
-    synchronized(this) {
-      parentArr[3] = null;
-    }
-
-    return childArr[4];
-  }
-
-  public String NOrace() {
-    synchronized(this) {
-      parentArr[3] = null;
-    }
-
-    return strArr[2];
-  }
-
-}

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

@@ -14,6 +14,10 @@ codetoanalyze/java/threadsafety/Annotations.java, void Annotations.read_from_non
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.read_off_UI_thread_Bad(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.Annotations.f`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.Annotations.f`]
 codetoanalyze/java/threadsafety/Annotations.java, void ThreadSafeAlias.threadSafeAliasBad1(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ThreadSafeAlias.field`]
 codetoanalyze/java/threadsafety/Annotations.java, void ThreadSafeAlias.threadSafeAliasBad2(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ThreadSafeAlias.field`]
+codetoanalyze/java/threadsafety/Arrays.java, String Arrays.readWriteRaceBad(String), 4, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `Arrays.strArr1.[_]`,<Beginning of write trace>,access to `Arrays.strArr1.[_]`]
+codetoanalyze/java/threadsafety/Arrays.java, int Arrays.arrayParameterReadBad(int[]), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `[_]`,<Beginning of write trace>,access to `[_]`]
+codetoanalyze/java/threadsafety/Arrays.java, void Arrays.arrayParameterWriteBad(int[]), 1, THREAD_SAFETY_VIOLATION, [access to `[_]`]
+codetoanalyze/java/threadsafety/Arrays.java, void Arrays.writeWriteRaceBad(String), 1, THREAD_SAFETY_VIOLATION, [access to `Arrays.strArr1.[_]`]
 codetoanalyze/java/threadsafety/Builders.java, Builders$Obj Builders.buildThenMutateBad(Builders$Obj), 2, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,call to Builders$Obj$Builder Builders$Obj$Builder.setFromObj(Builders$Obj),access to `codetoanalyze.java.checkers.Builders$Obj.g`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.Builders$Obj.g`]
 codetoanalyze/java/threadsafety/Builders.java, Builders$Obj Builders.buildThenMutateBad(Builders$Obj), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Builders$Obj.g`]
 codetoanalyze/java/threadsafety/Builders.java, Builders$Obj Builders.mutateBad(Builders$Obj), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Builders$Obj.g`]
@@ -90,7 +94,6 @@ codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m1(), 2
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m2(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ReadWriteRaces.racy`]
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m3(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ReadWriteRaces.racy`]
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.readInCalleeOutsideSyncBad(int), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,call to int C.get(),access to `codetoanalyze.java.checkers.C.x`,<Beginning of write trace>,call to void C.set(int),access to `codetoanalyze.java.checkers.C.x`]
-codetoanalyze/java/threadsafety/SubArr.java, Child SubArr.RWrace(), 5, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `SubArr.childArr.[_]`,<Beginning of write trace>,access to `SubArr.parentArr.[_]`]
 codetoanalyze/java/threadsafety/SubFld.java, int SubFld.getG(), 6, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,call to int SuperFld.getG(),access to `SuperFld.g`,<Beginning of write trace>,access to `SuperFld.g`]
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ExtendsThreadSafeExample.field`]
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ExtendsThreadSafeExample.field`]