[thread-safety] report on write outside sync, read inside sync races

Summary:
This was the one type of races we were not yet reporting (besides ones that use the wrong synchronization :)).

Wrote new utility function to aggregate all accesses by the memory they access.
This makes it easy to say which accesses we should report and what their conflicts are.
Eventually, we can simplify the reporting of other kinds of unsafe accesses using this structure.

Reviewed By: peterogithub

Differential Revision: D4770542

fbshipit-source-id: 96d948e

infer/src/checkers/SinkTrace.ml

@@ -25,6 +25,8 @@ module type S = sig
   (** update sink with the given call site *)
   val with_callsite : t -> CallSite.t -> t
 
+  val of_sink : Sink.t -> t
+
   val to_sink_loc_trace :
     ?desc_of_sink:(Sink.t -> string) -> ?sink_should_nest:(Sink.t -> bool) ->
     sink_path -> Errlog.loc_trace_elem list
@@ -66,6 +68,10 @@ module Make (TraceElem : TraceElem.S) = struct
       ~init:empty
       (Sinks.elements (sinks t))
 
+  let of_sink sink =
+    let sinks = Sinks.add sink Sinks.empty in
+    update_sinks empty sinks
+
   let pp fmt t =
     let pp_passthroughs_if_not_empty fmt p =
       if not (Passthroughs.is_empty p) then

infer/src/checkers/SinkTrace.mli

@@ -23,6 +23,8 @@ module type S = sig
   (** update sink with the given call site *)
   val with_callsite : t -> CallSite.t -> t
 
+  val of_sink : Sink.t -> t
+
   val to_sink_loc_trace :
     ?desc_of_sink:(Sink.t -> string) -> ?sink_should_nest:(Sink.t -> bool) ->
     sink_path -> Errlog.loc_trace_elem list

infer/src/checkers/ThreadSafety.ml

@@ -945,27 +945,26 @@ let filter_by_kind access_kind trace =
     (PathDomain.sinks trace)
   |> PathDomain.update_sinks trace
 
-(* get all of the unprotected accesses of the given kind *)
-let get_possibly_unsafe_accesses access_kind accesses =
+let get_all_accesses_with_pre pre_filter access_kind accesses =
   let open ThreadSafetyDomain in
   AccessDomain.fold
-    (fun pre trace acc -> match pre with
-       | Unprotected _ -> PathDomain.join (filter_by_kind access_kind trace) acc
-       | Protected -> acc)
+    (fun pre trace acc ->
+       if pre_filter pre
+       then PathDomain.join (filter_by_kind access_kind trace) acc
+       else acc)
     accesses
     PathDomain.empty
 
-let get_possibly_unsafe_reads = get_possibly_unsafe_accesses Read
+(* get all of the unprotected accesses of the given kind *)
+let get_unprotected_accesses =
+  get_all_accesses_with_pre
+    (function ThreadSafetyDomain.AccessPrecondition.Unprotected _ -> true | Protected -> false)
 
-let get_possibly_unsafe_writes = get_possibly_unsafe_accesses Write
+let get_all_accesses = get_all_accesses_with_pre (fun _ -> true)
 
-(* get all accesses of the given kind *)
-let get_all_accesses access_kind accesses =
-  let open ThreadSafetyDomain in
-  AccessDomain.fold
-    (fun _ trace acc ->  PathDomain.join (filter_by_kind access_kind trace) acc)
-    accesses
-    PathDomain.empty
+let get_possibly_unsafe_reads = get_unprotected_accesses Read
+
+let get_possibly_unsafe_writes = get_unprotected_accesses Write
 
 let equal_locs (sink1 : ThreadSafetyDomain.TraceElem.t) (sink2 : ThreadSafetyDomain.TraceElem.t) =
   Location.equal
@@ -985,6 +984,15 @@ let conflicting_accesses (sink1 : ThreadSafetyDomain.TraceElem.t)
     (sink2 : ThreadSafetyDomain.TraceElem.t) =
   equal_accesses sink1 sink2
 
+(* we assume two access paths can alias if their access parts are equal (we ignore the base). *)
+let can_alias access_path1 access_path2 =
+  List.compare AccessPath.compare_access (snd access_path1) (snd access_path2)
+
+module AccessListMap = Caml.Map.Make(struct
+    type t = AccessPath.Raw.t [@@deriving compare]
+    let compare = can_alias
+  end)
+
 (* trace is really reads or writes set. Fix terminology later *)
 let filter_conflicting_sinks sink trace =
   let conflicts =
@@ -1078,9 +1086,9 @@ let pp_accesses_sink fmt ~is_write_access sink =
 
 (* trace is really a set of accesses*)
 let report_thread_safety_violations
-    (tenv, pdesc) ~get_unsafe_accesses make_description trace threaded tab =
-  let pname = Procdesc.get_proc_name pdesc in
+    tenv pdesc ~get_unsafe_accesses make_description trace threaded tab =
   let open ThreadSafetyDomain in
+  let pname = Procdesc.get_proc_name pdesc in
   let trace_of_pname callee_pname =
     match Summary.read_summary pdesc callee_pname with
     | Some (_, _, accesses, _) -> get_unsafe_accesses accesses
@@ -1110,7 +1118,6 @@ let report_thread_safety_violations
     ~f:report_one_path
     (PathDomain.get_reportable_sink_paths (de_dup trace) ~trace_of_pname)
 
-
 let make_unprotected_write_description
     tenv pname final_sink_site initial_sink_site final_sink _ _ =
   Format.asprintf
@@ -1152,9 +1159,88 @@ let make_read_write_race_description
     conflicts_description
     (calculate_addendum_message tenv pname)
 
+(* report accesses that may race with each other *)
+let report_unsafe_accesses tab aggregated_access_map =
+  let report_unsafe_access (access, pre, threaded, tenv, pdesc) accesses reported_sites =
+    let open ThreadSafetyDomain in
+    let call_site = TraceElem.call_site access in
+    if CallSite.Set.mem call_site reported_sites
+    then
+      (* already reported a warning originating at this call site; don't double-report *)
+      reported_sites
+    else
+      match snd (TraceElem.kind access), pre with
+      | Access.Write, AccessPrecondition.Unprotected _ ->
+          (* unprotected write. TODO: warn. *)
+          reported_sites
+      | Access.Write, AccessPrecondition.Protected ->
+          (* protected write, do nothing *)
+          reported_sites
+      | Access.Read, AccessPrecondition.Unprotected _ ->
+          (* unprotected read. TODO: report all writes as conflicts *)
+          reported_sites
+      | Access.Read, AccessPrecondition.Protected ->
+          (* protected read. report unprotected writes as conflicts *)
+          let unprotected_writes =
+            List.filter
+              ~f:(fun (access, pre, _, _, _) ->
+                  match pre with
+                  | AccessPrecondition.Unprotected _ -> TraceElem.is_write access
+                  | _ -> false)
+              accesses in
+          if List.is_empty unprotected_writes
+          then reported_sites
+          else
+            begin
+              (* protected read with conflicting unprotected write(s). warn. *)
+              report_thread_safety_violations
+                tenv
+                pdesc
+                ~get_unsafe_accesses:(get_all_accesses Read)
+                make_read_write_race_description
+                (PathDomain.of_sink access)
+                threaded
+                tab;
+              CallSite.Set.add call_site reported_sites
+            end in
+  AccessListMap.fold
+    (fun _ grouped_accesses acc ->
+       List.fold
+         ~f:(fun acc access -> report_unsafe_access access grouped_accesses acc)
+         grouped_accesses
+         ~init:acc)
+    aggregated_access_map
+    CallSite.Set.empty
+  |> ignore
+
+(* group accesses that may touch the same memory *)
+let aggregate_accesses tab =
+  let open ThreadSafetyDomain in
+  let aggregate (threaded, _, accesses, _) tenv pdesc acc =
+    AccessDomain.fold
+      (fun pre accesses acc ->
+         PathDomain.Sinks.fold
+           (fun access acc ->
+              let access_path, _ = TraceElem.kind access in
+              let grouped_accesses =
+                try AccessListMap.find access_path acc
+                with Not_found -> [] in
+              AccessListMap.add
+                access_path
+                ((access, pre, threaded, tenv, pdesc) :: grouped_accesses)
+                acc)
+           (PathDomain.sinks accesses)
+           acc)
+      accesses
+      acc in
+  ResultsTableType.fold
+    (fun (tenv, pdesc) summary acc -> aggregate summary tenv pdesc acc)
+    tab
+    AccessListMap.empty
+
 (* find those elements of reads which have conflicts
         somewhere else, and report them *)
-let report_reads proc_env reads threaded tab =
+let report_reads (tenv, pdesc) reads threaded tab =
   let racy_read_sinks =
     ThreadSafetyDomain.PathDomain.Sinks.filter
       (fun sink ->
@@ -1168,7 +1254,8 @@ let report_reads proc_env reads threaded tab =
     ThreadSafetyDomain.PathDomain.update_sinks reads racy_read_sinks
   in
   report_thread_safety_violations
-    proc_env
+    tenv
+    pdesc
     ~get_unsafe_accesses:get_possibly_unsafe_reads
     make_read_write_race_description
     racy_reads
@@ -1225,8 +1312,12 @@ let process_results_table file_env tab =
   let should_report ((tenv, pdesc) as proc_env) =
     (should_report_on_all_procs && should_report_on_proc proc_env) ||
     is_thread_safe_method pdesc tenv in
+
+  aggregate_accesses tab
+  |> report_unsafe_accesses tab;
+
   ResultsTableType.iter (* report errors for each method *)
-    (fun proc_env (threaded, _, accesses, _) ->
+    (fun ((tenv, pdesc) as proc_env) (threaded, _, accesses, _) ->
        if should_report proc_env
        then
          let open ThreadSafetyDomain in
@@ -1248,7 +1339,8 @@ let process_results_table file_env tab =
            if not threaded
            then (*don't report writes for threaded; TODO to extend this*)
              report_thread_safety_violations
-               proc_env
+               tenv
+               pdesc
                ~get_unsafe_accesses:get_possibly_unsafe_writes
                make_unprotected_write_description
                unsafe_writes

infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java

@@ -71,14 +71,12 @@ class RaceWithMainThread{
     }
   }
 
-  /*TODO: There should be a warning either here or in main_thread_OK()
-   or maybe even in both.*/
-  void read_protected_unthreaded_Bad_FN(){
+  void readProtectedUnthreadedBad(){
     Integer x;
     synchronized (this){
       x = f;
     }
-   }
+  }
 
   Integer g;
 

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

@@ -109,4 +109,17 @@ class ReadWriteRaces {
     }
   }
 
+  // write outside sync, read inside of sync races
+
+  Object field4;
+
+  public void unprotectedWrite4Bad() {
+    this.field4 = new Object();
+  }
+
+  public synchronized Object protectedRead4Bad() {
+    return this.field4;
+  }
+
+
 }

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

@@ -60,8 +60,10 @@ codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedIn
 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/RaceWithMainThread.java, void RaceWithMainThread.readProtectedUnthreadedBad(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.RaceWithMainThread.f]
 codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded_Bad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.RaceWithMainThread.f]
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.callUnprotecteReadInCallee(), 1, THREAD_SAFETY_VIOLATION, [call to Object ReadWriteRaces.unprotectedReadInCallee(),access to codetoanalyze.java.checkers.ReadWriteRaces.field1]
+codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.protectedRead4Bad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field4]
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead1(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field1]
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead2(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field2]
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead3(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field3]
@@ -69,6 +71,7 @@ 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, [call to int C.get(),access to codetoanalyze.java.checkers.C.x]
+codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.unprotectedWrite4Bad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field4]
 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]