[threadsafety] fix false negative on locations that may alias.

Reviewed By: sblackshear

Differential Revision: D5137332

fbshipit-source-id: 87e009c

infer/src/checkers/ThreadSafety.ml

@@ -1201,6 +1201,36 @@ let report_unsafe_accesses ~is_file_threadsafe aggregated_access_map =
     empty_reported
   |> ignore
 
+(* equivalence relation computing whether two access paths may refer to the
+   same heap location. *)
+let may_alias p1 p2 =
+  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 *)
+  | FieldAccess f1, FieldAccess f2 ->
+      String.equal (Fieldname.java_get_field f1) (Fieldname.java_get_field f2)
+  | ArrayAccess _, ArrayAccess _ -> true (*FIXME*)
+
+(* take a results table and quotient it by the may_alias relation *)
+let quotient_access_map acc_map =
+  let rec aux acc m =
+    if AccessListMap.is_empty m then
+      acc
+    else
+      let k, _ = AccessListMap.choose m in
+      let (k_part, non_k_part) = AccessListMap.partition (fun k' _ -> may_alias k k') m in
+      let k_accesses =
+        AccessListMap.fold
+          (fun _ v acc' -> List.append v acc')
+          k_part
+          []
+      in
+      let new_acc = AccessListMap.add k k_accesses acc in
+      aux new_acc non_k_part
+  in
+  aux AccessListMap.empty acc_map
+
 (* 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 *)
@@ -1227,7 +1257,7 @@ let make_results_table file_env =
     match Summary.read_summary proc_desc proc_name with
     | Some summary -> aggregate_post summary tenv proc_desc acc
     | None -> acc in
-  List.fold ~f:aggregate_posts file_env ~init:AccessListMap.empty
+  List.fold ~f:aggregate_posts file_env ~init:AccessListMap.empty |> quotient_access_map
 
 (**
    Principles for race reporting.

infer/tests/codetoanalyze/java/threadsafety/Alias.java

@@ -0,0 +1,33 @@
+/*
+ * 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
+class Alias{
+  A a,b;
+
+  public void foo() {
+    int x;
+    synchronized(this){
+      a = b;
+      a.f = 101;
+    }
+    x = b.f;  // may_alias
+  }
+
+  public void bar(A a,A b) {
+     int x;
+     synchronized(this){
+       a.f = 101;
+     }
+    x = b.f;  // no may_alias needed, argument treatment suffices
+  }
+}
+
+class A { int f = 0; }

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

@@ -1,3 +1,5 @@
+codetoanalyze/java/threadsafety/Alias.java, void Alias.bar(A,A), 5, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `A.f`,<Beginning of write trace>,access to `Alias.a.A.f`]
+codetoanalyze/java/threadsafety/Alias.java, void Alias.foo(), 6, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `Alias.b.A.f`,<Beginning of write trace>,access to `Alias.a.A.f`]
 codetoanalyze/java/threadsafety/AndroidModels.java, void AndroidModels.someResourceMethodsNotFunctionalBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.AndroidModels.mField`]
 codetoanalyze/java/threadsafety/Annotations.java, boolean Annotations.FP_functionalAcrossUnboxingOk(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mBool2`]
 codetoanalyze/java/threadsafety/Annotations.java, double Annotations.functionalDoubleBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mDouble`]