[thread-safety] Lay the groundwork for interprocedural trace-based re…

…porting

Summary: We'll eventually want fancy interprocedural traces. This diff adds the required boilerplate for this and adds the line number of each access to the error message. Real traces will come in a follow-up

Reviewed By: peterogithub

Differential Revision: D4251985

fbshipit-source-id: c9d9823

infer/src/checkers/ThreadSafety.ml

@@ -56,11 +56,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | _ ->
         None
 
-  let add_path_to_state exp typ pathdomainstate =
+  let add_path_to_state exp typ loc path_state =
     IList.fold_left
-      (fun pathdomainstate_acc rawpath -> ThreadSafetyDomain.PathDomain.add
-          rawpath pathdomainstate_acc)
-      pathdomainstate
+      (fun acc rawpath ->
+         ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc)
+      path_state
       (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None))
 
   let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; } _ =
@@ -90,19 +90,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               end
         end
 
-    | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, _) ->
+    | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, loc) ->
         if is_unprotected lockstate then (* abstracts no lock being held*)
-          (lockstate, (readstate, add_path_to_state lhsfield typ writestate))
+          (lockstate, (readstate, add_path_to_state lhsfield typ loc writestate))
         else astate
 
     (* Note: it appears that the third arg of Store is never an Lfield in the targets of,
        our translations, which is why we have not covered that case. *)
     | Sil.Store (_, _, Lfield _, _) ->
         failwith "Unexpected store instruction with rhs field"
 
-    | Sil.Load (_, (Lfield ( _, _, typ) as rhsfield) , _, _) ->
+    | Sil.Load (_, (Lfield ( _, _, typ) as rhsfield) , _, loc) ->
         if is_unprotected lockstate then (* abstracts no lock being held*)
-          (lockstate, (add_path_to_state rhsfield typ readstate, writestate))
+          (lockstate, (add_path_to_state rhsfield typ loc readstate, writestate))
         else astate
 
     |  _  ->
@@ -190,11 +190,12 @@ let calculate_addendum_message tenv pname =
   | _ -> ""
 
 let report_thread_safety_errors ( _, tenv, pname, pdesc) writestate =
-  let report_one_error access_path =
+  let report_one_error access_path loc =
     let description =
-      F.asprintf "Method %a writes to field %a outside of synchronization. %s"
+      F.asprintf "Method %a writes to field %a outside of synchronization at %a. %s"
         Procname.pp pname
         AccessPath.pp_access_list access_path
+        Location.pp loc
         (calculate_addendum_message tenv pname)
     in
     Checkers.ST.report_error tenv
@@ -204,7 +205,12 @@ let report_thread_safety_errors ( _, tenv, pname, pdesc) writestate =
       (Procdesc.get_loc pdesc)
       description
   in
-  IList.iter report_one_error (IList.map snd (ThreadSafetyDomain.PathDomain.elements writestate))
+  ThreadSafetyDomain.PathDomain.Sinks.iter
+    (fun sink ->
+       let _, accesses = ThreadSafetyDomain.PathDomain.Sink.kind sink in
+       let loc = CallSite.loc (ThreadSafetyDomain.PathDomain.Sink.call_site sink) in
+       report_one_error accesses loc)
+    (ThreadSafetyDomain.PathDomain.sinks writestate)
 
 
 (* For now, just checks if there is one active element amongst the posts of the analyzed methods.

infer/src/checkers/ThreadSafetyDomain.ml

@@ -6,11 +6,44 @@
  * 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.
  *)
-module PPrawpath = PrettyPrintable.MakePPSet(struct
+
+open! Utils
+
+module F = Format
+
+module TraceElem = struct
+  module Kind = struct
     type t = AccessPath.raw
     let compare = AccessPath.compare_raw
-    let pp_element = AccessPath.pp_raw
-  end)
+    let pp = AccessPath.pp_raw
+  end
+
+  type t = {
+    site : CallSite.t;
+    kind : Kind.t;
+  } [@@deriving compare]
+
+  let call_site { site; } = site
+
+  let kind { kind; } = kind
+
+  let make kind site = { kind; site; }
+
+  let with_callsite t site = { t with site; }
+
+  let pp fmt { site; kind; } =
+    F.fprintf fmt "Unprotected access to %a at %a" Kind.pp kind CallSite.pp site
+
+  module Set = PrettyPrintable.MakePPSet (struct
+      type nonrec t = t
+      let compare = compare
+      let pp_element = pp
+    end)
+end
+
+let make_access kind loc =
+  let site = CallSite.make Procname.empty_block loc in
+  TraceElem.make kind site
 
 (** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes
     the existence of one global lock. In the case that a lock is held on the access to a variable,
@@ -19,7 +52,7 @@ module PPrawpath = PrettyPrintable.MakePPSet(struct
     and which memory locations correspond to the same lock. *)
 module LocksDomain = AbstractDomain.BooleanAnd
 
-module PathDomain =  AbstractDomain.FiniteSet(PPrawpath)
+module PathDomain = SinkTrace.Make(TraceElem)
 
 module ReadWriteDomain = AbstractDomain.Pair (PathDomain) (PathDomain)
 

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

@@ -1,10 +1,10 @@
-codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 0, THREAD_SAFETY_ERROR, [Method void ExtendsThreadSafeExample.newmethodBad() writes to field codetoanalyze.java.checkers.ExtendsThreadSafeExample.field outside of synchronization. 
+codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 0, THREAD_SAFETY_ERROR, [Method void ExtendsThreadSafeExample.newmethodBad() writes to field codetoanalyze.java.checkers.ExtendsThreadSafeExample.field outside of synchronization at [line 181]. 
  Note: Superclass class codetoanalyze.java.checkers.ThreadSafeExample is marked @ThreadSafe.]
-codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 0, THREAD_SAFETY_ERROR, [Method void ExtendsThreadSafeExample.tsOK() writes to field codetoanalyze.java.checkers.ExtendsThreadSafeExample.field outside of synchronization. 
+codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 0, THREAD_SAFETY_ERROR, [Method void ExtendsThreadSafeExample.tsOK() writes to field codetoanalyze.java.checkers.ExtendsThreadSafeExample.field outside of synchronization at [line 186]. 
  Note: Superclass class codetoanalyze.java.checkers.ThreadSafeExample is marked @ThreadSafe.]
-codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.FP_unlockOneLock(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.FP_unlockOneLock() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
-codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterReentrantLockUnlockBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.afterReentrantLockUnlockBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
-codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterUnlockBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.afterUnlockBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
-codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.callPublicMethodBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.callPublicMethodBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
-codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.lockInOneBranchBad(boolean), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.lockInOneBranchBad(boolean) writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
-codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.tsBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.tsBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
+codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.FP_unlockOneLock(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.FP_unlockOneLock() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 154]. ]
+codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterReentrantLockUnlockBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.afterReentrantLockUnlockBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 71]. ]
+codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterUnlockBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.afterUnlockBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 65]. ]
+codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.callPublicMethodBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.callPublicMethodBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 82]. ]
+codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.lockInOneBranchBad(boolean), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.lockInOneBranchBad(boolean) writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 56]. ]
+codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.tsBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.tsBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 46]. ]