[threadsafety] read/write races

Summary: Reports on reads that have one or more conflicting writes. When you report, say which other methods race with it.

Reviewed By: sblackshear

Differential Revision: D4538793

fbshipit-source-id: 47ce700

infer/src/checkers/ThreadSafety.ml

@@ -760,6 +760,7 @@ let calculate_addendum_message tenv pname =
       else ""
   | _ -> ""
 
+
 let combine_conditional_unconditional_writes conditional_writes unconditional_writes =
   let open ThreadSafetyDomain in
   ConditionalWritesDomain.fold
@@ -767,7 +768,51 @@ let combine_conditional_unconditional_writes conditional_writes unconditional_wr
     conditional_writes
     unconditional_writes
 
-let report_thread_safety_violations ( _, tenv, pname, pdesc) trace =
+let conflicting_accesses (sink1 : ThreadSafetyDomain.TraceElem.t)
+    (sink2 : ThreadSafetyDomain.TraceElem.t) =
+  AccessPath.equal_access_list
+    (snd (ThreadSafetyDomain.TraceElem.kind sink1))
+    (snd (ThreadSafetyDomain.TraceElem.kind sink2))
+
+(* trace is really reads or writes set. Fix terminology later *)
+let filter_conflicting_sinks sink trace =
+  let conflicts =
+    ThreadSafetyDomain.PathDomain.Sinks.filter
+      (fun sink2 -> conflicting_accesses sink sink2)
+      (ThreadSafetyDomain.PathDomain.sinks trace) in
+  ThreadSafetyDomain.PathDomain.update_sinks trace conflicts
+
+(* Given a sink representing a read access,
+   return a list of (proc_env,access-astate) pairs where
+   access-astate is a non-empty collection of conflicting
+   write accesses*)
+let collect_conflicting_writes sink tab =
+  let procs_and_writes =
+    IList.map
+      (fun (key,(_, _, conditional_writes, unconditional_writes, _)) ->
+         let conflicting_writes =
+           combine_conditional_unconditional_writes
+             conditional_writes unconditional_writes
+           |> filter_conflicting_sinks sink in
+         key, conflicting_writes
+      )
+      (ResultsTableType.bindings tab) in
+  List.filter
+    ~f:(fun (proc_env,writes) ->
+        (should_report_on_proc proc_env)
+        && not (ThreadSafetyDomain.PathDomain.Sinks.is_empty
+                  (ThreadSafetyDomain.PathDomain.sinks writes))
+      )
+    procs_and_writes
+
+(*A helper function used int he error reporting*)
+let pp_accesses_sink fmt sink =
+  let _, accesses = ThreadSafetyDomain.PathDomain.Sink.kind sink in
+  AccessPath.pp_access_list fmt accesses
+
+
+(* trace is really a set of accesses*)
+let report_thread_safety_violations ( _, tenv, pname, pdesc) make_description trace tab =
   let open ThreadSafetyDomain in
   let trace_of_pname callee_pname =
     match Summary.read_summary pdesc callee_pname with
@@ -776,9 +821,6 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) trace =
     | _ ->
         PathDomain.empty in
   let report_one_path ((_, sinks) as path) =
-    let pp_accesses fmt sink =
-      let _, accesses = PathDomain.Sink.kind sink in
-      AccessPath.pp_access_list fmt accesses in
     let initial_sink, _ = List.last_exn sinks in
     let final_sink, _ = List.hd_exn sinks in
     let initial_sink_site = PathDomain.Sink.call_site initial_sink in
@@ -786,19 +828,15 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) trace =
     let desc_of_sink sink =
       if CallSite.equal (PathDomain.Sink.call_site sink) final_sink_site
       then
-        Format.asprintf "access to %a" pp_accesses sink
+        Format.asprintf "access to %a" pp_accesses_sink sink
       else
         Format.asprintf
           "call to %a" Procname.pp (CallSite.pname (PathDomain.Sink.call_site sink)) in
     let loc = CallSite.loc (PathDomain.Sink.call_site initial_sink) in
     let ltr = PathDomain.to_sink_loc_trace ~desc_of_sink path in
     let msg = Localise.to_string Localise.thread_safety_violation in
-    let description =
-      Format.asprintf "Public method %a%s writes to field %a outside of synchronization.%s"
-        Procname.pp pname
-        (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly")
-        pp_accesses final_sink
-        (calculate_addendum_message tenv pname) in
+    let description = make_description tenv pname final_sink_site
+        initial_sink_site final_sink tab in
     let exn = Exceptions.Checkers (msg, Localise.verbatim_desc description) in
     Reporting.log_error pname ~loc ~ltr exn in
 
@@ -806,6 +844,58 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) trace =
     report_one_path
     (PathDomain.get_reportable_sink_paths trace ~trace_of_pname)
 
+
+let make_unprotected_write_description
+    tenv pname final_sink_site initial_sink_site final_sink _ =
+  Format.asprintf
+    "Unprotected write. Public method %a%s writes to field %a outside of synchronization.%s"
+    Procname.pp pname
+    (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly")
+    pp_accesses_sink final_sink
+    (calculate_addendum_message tenv pname)
+
+let make_read_write_race_description tenv pname final_sink_site initial_sink_site final_sink tab =
+  let conflicting_proc_envs = IList.map
+      fst
+      (collect_conflicting_writes final_sink tab) in
+  let conflicting_proc_names = IList.map
+      (fun (_,_,proc_name,_) -> proc_name)
+      conflicting_proc_envs in
+  let pp_proc_name_list fmt proc_names =
+    let pp_sep _ _ = F.fprintf fmt " , " in
+    F.pp_print_list ~pp_sep Procname.pp fmt proc_names in
+  let conflicts_description =
+    Format.asprintf "Potentially races with writes in method%s %a."
+      (if IList.length conflicting_proc_names > 1 then "s" else "")
+      pp_proc_name_list conflicting_proc_names in
+  Format.asprintf "Read/Write race. Public method %a%s reads from field %a. %s %s"
+    Procname.pp pname
+    (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly")
+    pp_accesses_sink final_sink
+    conflicts_description
+    (calculate_addendum_message tenv pname)
+
+
+(* find those elements of reads which have conflicts
+        somewhere else, and report them *)
+let report_reads proc_env reads tab =
+  let racy_read_sinks =
+    ThreadSafetyDomain.PathDomain.Sinks.filter
+      (fun sink ->
+         (* there exists a postcondition whose write set conflicts with
+            sink*)
+         not (List.is_empty (collect_conflicting_writes sink tab))
+      )
+      (ThreadSafetyDomain.PathDomain.sinks reads)
+  in
+  let racy_reads =
+    ThreadSafetyDomain.PathDomain.update_sinks reads racy_read_sinks
+  in
+  report_thread_safety_violations proc_env
+    make_read_write_race_description
+    racy_reads
+    tab
+
 (* Currently we analyze if there is an @ThreadSafe annotation on at least one of
    the classes in a file. This might be tightened in future or even broadened in future
    based on other criteria *)
@@ -842,12 +932,19 @@ let process_results_table file_env tab =
     (should_report_on_all_procs || is_thread_safe_method pdesc tenv)
     && should_report_on_proc proc_env in
   ResultsTableType.iter (* report errors for each method *)
-    (fun proc_env (_, _, conditional_writes, unconditional_writes, _) ->
+    (fun proc_env (_, reads, conditional_writes, unconditional_writes, _) ->
        if should_report proc_env then
-         combine_conditional_unconditional_writes conditional_writes unconditional_writes
-         |> report_thread_safety_violations proc_env)
+         let writes = combine_conditional_unconditional_writes
+             conditional_writes unconditional_writes in
+         begin
+           report_thread_safety_violations
+             proc_env make_unprotected_write_description writes tab
+         ; report_reads proc_env reads tab
+         end
+    )
     tab
 
+
 (*This is a "cluster checker" *)
 (*Gathers results by analyzing all the methods in a file, then post-processes
   the results to check (approximation of) thread safety *)

infer/src/checkers/accessPath.ml

@@ -31,6 +31,9 @@ type access =
 
 let equal_access = [%compare.equal : access]
 
+
+let equal_access_list l1 l2 =  Int.equal (List.compare compare_access l1 l2) 0
+
 let pp_base fmt (pvar, _) =
   Var.pp fmt pvar
 

infer/src/checkers/accessPath.mli

@@ -45,6 +45,8 @@ val equal_base : base -> base -> bool
 
 val equal_access : access -> access -> bool
 
+val equal_access_list : access list -> access list -> bool
+
 val equal : t -> t -> bool
 
 (** create a base from a pvar *)

infer/tests/codetoanalyze/java/threadsafety/Annotations.java

@@ -59,6 +59,7 @@ interface Interface {
 @ThreadSafe
 class Annotations implements Interface {
   Object f;
+  boolean b;
 
   @UiThread
   public void setF(Object newF) {
@@ -178,18 +179,18 @@ class Annotations implements Interface {
 
   // writes to doubles are not atomic on all platforms, so this is not a benign race
   public double functionalDoubleBad() {
-    if (mDouble == 0.0) {
+    if (b) {
       mDouble = returnDouble();
     }
-    return mDouble;
+    return 0.0;
   }
 
   // writes to longs are not atomic on all platforms, so this is not a benign race
   public long functionaLongBad() {
-    if (mLong == 0L) {
+    if (b) {
       mLong = returnLong();
     }
-    return mLong;
+    return 2;
   }
 
   Boolean mBoxedBool;
@@ -197,46 +198,52 @@ class Annotations implements Interface {
   @Functional native boolean returnBool();
 
   public boolean functionalAcrossBoxingOk() {
-    if (mBoxedBool != null) {
+    if (b) {
       mBoxedBool = returnBool();
     }
-    return mBoxedBool;
+    return b;
   }
 
   boolean mBool;
 
   @Functional native Boolean returnBoxedBool();
 
+  boolean mBool2;
+
   public boolean FP_functionalAcrossUnboxingOk() {
-    if (!mBool) {
-      mBool = returnBoxedBool();
+    if (b) {
+      mBool2 = returnBoxedBool();
     }
-    return mBool;
+    return b;
   }
 
   Long mBoxedLong;
 
   @Functional native Long returnBoxedLong();
 
-  public Long functionalBoxedLongOk() {
-    if (mBoxedLong == null) {
+  public int functionalBoxedLongOk() {
+    if (b) {
       mBoxedLong = returnBoxedLong();
     }
-    return mBoxedLong;
+    return 22;
   }
 
-  public long functionalAcrossUnboxingLongBad() {
-    if (mLong != 0L) {
-      mLong = returnBoxedLong();
+  long mLong2;
+
+  public int functionalAcrossUnboxingLongBad() {
+    if (b) {
+      mLong2 = returnBoxedLong();
     }
-    return mLong;
+    return 2;
   }
 
-  public long FP_functionalAcrossBoxingLongOk() {
-    if (mBoxedLong != null) {
-      mBoxedLong = returnLong();
+  long mBoxedLong2;
+
+  public int FP_functionalAcrossBoxingLongOk() {
+    if (b) {
+      mBoxedLong2 = returnLong();
     }
-    return mBoxedLong;
+    return 2;
   }
 
   public boolean propagateFunctional() {

infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java

@@ -0,0 +1,43 @@
+/*
+ * Copyright (c) 2016 - 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.
+ */
+
+package codetoanalyze.java.checkers;
+
+import javax.annotation.concurrent.ThreadSafe;
+
+@ThreadSafe
+class ReadWriteRaces{
+
+Integer safe_read;
+Integer racy;
+
+  void m0_OK(){
+   Integer local;
+   local = safe_read;
+   }
+
+  void m0_OK2(){ //parallel reads are OK
+   Integer local;
+   local = safe_read;
+  }
+
+  void m1(){ // A read where there are other writes
+   Integer local;
+   local = racy;
+  }
+
+  public void m2(){
+   racy = 88;
+  }
+
+  public void m3(){
+   racy = 99;
+  }
+
+}

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

@@ -1,9 +1,9 @@
 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.mBool]
+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]
-codetoanalyze/java/threadsafety/Annotations.java, long Annotations.FP_functionalAcrossBoxingLongOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mBoxedLong]
+codetoanalyze/java/threadsafety/Annotations.java, int Annotations.FP_functionalAcrossBoxingLongOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mBoxedLong2]
+codetoanalyze/java/threadsafety/Annotations.java, int Annotations.functionalAcrossUnboxingLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mLong2]
 codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionaLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mLong]
-codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionalAcrossUnboxingLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mLong]
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.functionalAndNonfunctionalBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mInt]
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateOffUiThreadBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.f]
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateSubfieldOfConfinedBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.encapsulatedField.codetoanalyze.java.checkers.Obj.f]
@@ -37,9 +37,14 @@ codetoanalyze/java/threadsafety/Ownership.java, void Ownership.cantOwnThisBad(),
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.notOwnedInCalleeBad(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.mutateIfNotNull(Obj),access to codetoanalyze.java.checkers.Obj.f]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.ownInOneBranchBad(Obj,boolean), 5, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.reassignToFormalBad(Obj), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.g]
+codetoanalyze/java/threadsafety/Ownership.java, void Ownership.reassignToFormalBad(Obj), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.g]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad1(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad2(), 2, THREAD_SAFETY_VIOLATION, [call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad3(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f]
+codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToOwnedInCalleeOk2(), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Ownership.field]
+codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m1(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.racy]
+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/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 NonThreadSafeClass.threadSafeMethod(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.NonThreadSafeClass.field]