[threadsafety] Fix some FPs added by may-alias analysis.

Reviewed By: sblackshear

Differential Revision: D5172635

fbshipit-source-id: 67ed695

infer/src/checkers/ThreadSafety.ml

@@ -1243,13 +1243,22 @@ let report_unsafe_accesses ~is_file_threadsafe aggregated_access_map =
 
 (* equivalence relation computing whether two access paths may refer to the
    same heap location. *)
-let may_alias p1 p2 =
+let may_alias tenv p1 p2 =
+  let open Typ in
   let open AccessPath in
   match List.last_exn (snd p1), List.last_exn (snd p2) with
   | FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _ -> false
-  (* fields in Infer contain class name *)
+  (* fields in Java contain the class name /declaring/ them
-  | FieldAccess f1, FieldAccess f2 -> Fieldname.equal_modulo_parent f1 f2
+     thus two fields can be aliases *iff* they are equal *)
-  | ArrayAccess _, ArrayAccess _ -> true (*FIXME*)
+  | FieldAccess f1, FieldAccess f2 -> 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
 
 (* take a results table and quotient it by the may_alias relation *)
 let quotient_access_map acc_map =
@@ -1257,8 +1266,15 @@ let quotient_access_map acc_map =
     if AccessListMap.is_empty m then
       acc
     else
-      let k, _ = AccessListMap.choose m in
+      let k, vals = AccessListMap.choose m in
-      let (k_part, non_k_part) = AccessListMap.partition (fun k' _ -> may_alias k k') m in
+      let (_, _, _, tenv, _) =
+        List.find_exn vals
+          ~f:(fun (elem, _, _, _, _) ->
+              AccessPath.Raw.equal k (ThreadSafetyDomain.TraceElem.kind elem |> fst))
+      in
+      (* assumption: the tenv for k is sufficient for k' too *)
+      let (k_part, non_k_part) =
+        AccessListMap.partition (fun k' _ -> may_alias tenv k k') m in
       let k_accesses =
         AccessListMap.fold
           (fun _ v acc' -> List.append v acc')
@@ -1270,6 +1286,16 @@ let quotient_access_map acc_map =
   in
   aux AccessListMap.empty acc_map
 
+(* decide if we should throw away a path before doing safety analysis
+   for now, just check for whether the access is within a switch-map
+   that is auto-generated by Java. *)
+let should_filter_access (_, path) =
+  let check_access_step = function
+    | AccessPath.ArrayAccess _ -> false
+    | AccessPath.FieldAccess fld ->
+        String.is_substring ~substring:"$SwitchMap" (Fieldname.to_string fld) in
+  List.exists path ~f:check_access_step
+
 (* create a map from [abstraction of a memory loc] -> accesses that may touch that memory loc. for
    now, our abstraction is an access path like x.f.g whose concretization is the set of memory cells
    that x.f.g may point to during execution *)
@@ -1281,13 +1307,14 @@ let make_results_table file_env =
          PathDomain.Sinks.fold
            (fun access acc ->
               let access_path, _ = TraceElem.kind access in
-              let grouped_accesses =
+              if should_filter_access access_path then acc else
-                try AccessListMap.find access_path acc
+                let grouped_accesses =
-                with Not_found -> [] in
+                  try AccessListMap.find access_path acc
-              AccessListMap.add
+                  with Not_found -> [] in
-                access_path
+                AccessListMap.add
-                ((access, pre, threaded, tenv, pdesc) :: grouped_accesses)
+                  access_path
-                acc)
+                  ((access, pre, threaded, tenv, pdesc) :: grouped_accesses)
+                  acc)
            (PathDomain.sinks accesses)
            acc)
       accesses

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

@@ -0,0 +1,42 @@
+/*
+ * 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/SubFld.java

@@ -0,0 +1,40 @@
+/*
+ * 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;
+
+// Fields must encapsulate the class they are declared in, not
+// the class they are potentially inherited into.
+
+@ThreadSafe
+class SuperFld {
+
+  private int f = 0;
+  public int getF() {
+    return f; // should *not* report read/write race with SubFld.setF()
+  }
+
+  protected int g = 0;
+  public int getG() {
+    return g; // must report read/write race with SubFld.setG()
+  }
+
+}
+
+@ThreadSafe
+public class SubFld extends SuperFld {
+
+  private int f = 0;
+  synchronized public void setF() {
+    f = 5; // should *not* report
+  }
+
+  synchronized public void setG() {
+    g = 5; // must report
+  }
+}

infer/tests/codetoanalyze/java/threadsafety/SwitchEnum.java

@@ -0,0 +1,29 @@
+/*
+ * 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;
+
+@ThreadSafe
+public class SwitchEnum {
+  int[] a = new int[8];
+
+  // Java generates a class for the switch, which contains an int array
+  // This leads to races where there are int arrays, here a[]
+  public String getName(EnumClass value) {
+    synchronized(this) {
+      a[0] = 0; // should not report here
+    }
+    switch (value) {
+      case VALUE1: return "value 1";
+      case VALUE3: return "value 3";
+      default:     return "other";
+    }
+  }
+}
+
+enum EnumClass { VALUE1, VALUE2, VALUE3 }

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

@@ -80,6 +80,8 @@ 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`]
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.callPublicMethodBad(), 1, THREAD_SAFETY_VIOLATION, [call to void ThreadSafeExample.assignInPrivateMethodOk(),access to `codetoanalyze.java.checkers.ThreadSafeExample.f`]