[thread-safety] use ownership info to avoid false alarms

Summary:
Maintain an "ownership" set of access paths that hold locally allocated memory that has not escaped.
This memory is owned by the current procedure, so modifying it outside of synchronization is safe.
If an owned access path does escape to another procedure, we remove it from the ownership set.

Reviewed By: peterogithub

Differential Revision: D4320034

fbshipit-source-id: 64f9169

infer/src/checkers/ThreadSafety.ml

@@ -80,11 +80,22 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     try Some (IdAccessPathMapDomain.find id id_map)
     with Not_found -> None
 
-  let add_path_to_state exp typ loc path_state id_map =
+  let add_path_to_state exp typ loc path_state id_map owned =
+    (* remove the last field of the access path, if it has any *)
+    let truncate = function
+      | base, []
+      | base, _ :: [] -> base, []
+      | base, accesses -> base, IList.rev (IList.tl (IList.rev accesses)) in
     let f_resolve_id = resolve_id id_map in
+
     IList.fold_left
       (fun acc rawpath ->
-         ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc)
+         let base_path = truncate rawpath in
+         if not (ThreadSafetyDomain.OwnershipDomain.mem base_path owned)
+         then
+           ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc
+         else
+           acc)
       path_state
       (AccessPath.of_exp exp typ ~f_resolve_id)
 
@@ -95,12 +106,25 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | None -> id_map
 
   let exec_instr
-      ({ ThreadSafetyDomain.locks; reads; writes; id_map; } as astate)
+      ({ ThreadSafetyDomain.locks; reads; writes; id_map; owned; } as astate)
       { ProcData.pdesc; tenv; } _ =
 
+    let is_allocation pn =
+      Procname.equal pn BuiltinDecl.__new ||
+      Procname.equal pn BuiltinDecl.__new_array in
     let is_unprotected is_locked =
       not is_locked && not (Procdesc.is_java_synchronized pdesc) in
+    let f_resolve_id = resolve_id id_map in
     function
+    | Sil.Call (Some (lhs_id, lhs_typ), Const (Cfun pn), _, _, _) when is_allocation pn ->
+        begin
+          match AccessPath.of_lhs_exp (Exp.Var lhs_id) lhs_typ ~f_resolve_id with
+          | Some lhs_access_path ->
+              let owned' = ThreadSafetyDomain.OwnershipDomain.add lhs_access_path owned in
+              { astate with owned = owned'; }
+          | None ->
+              astate
+        end
     | Sil.Call (_, Const (Cfun pn), _, loc, _) ->
         begin
           (* assuming that modeled procedures do not have useful summaries *)
@@ -131,7 +155,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                         { astate with reads = reads'; writes = writes'; }
                       else
                         astate in
-                    { astate' with locks = locks' }
+                    { astate' with locks = locks'; }
                 | None ->
                     astate
               end
@@ -141,28 +165,43 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         let id_map' = analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ astate in
         { astate with id_map = id_map'; }
 
-    | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, loc) ->
-        if is_unprotected locks (* abstracts no lock being held *)
-        then
-          let writes' = add_path_to_state lhsfield typ loc writes id_map in
-          { astate with writes = writes'; }
-        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.Store (lhs_exp, lhs_typ, rhs_exp, loc) ->
+        let writes' =
+          match lhs_exp with
+          | Lfield ( _, _, typ) when is_unprotected locks -> (* abstracts no lock being held *)
+              add_path_to_state lhs_exp typ loc writes id_map owned
+          | _ -> writes in
+        (* if rhs is owned, propagate ownership to lhs. otherwise, remove lhs from ownerhsip set
+           (since it may have previously held an owned memory loc and is now being reassigned *)
+        let owned' =
+          match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id,
+                AccessPath.of_lhs_exp rhs_exp lhs_typ ~f_resolve_id with
+          | Some lhs_access_path, Some rhs_access_path ->
+              if ThreadSafetyDomain.OwnershipDomain.mem rhs_access_path owned
+              then ThreadSafetyDomain.OwnershipDomain.add lhs_access_path owned
+              else ThreadSafetyDomain.OwnershipDomain.remove lhs_access_path owned
+          | Some lhs_access_path, None ->
+              ThreadSafetyDomain.OwnershipDomain.remove lhs_access_path owned
+          | _ -> owned in
+        { astate with writes = writes'; owned = owned'; }
 
     | Sil.Load (lhs_id, rhs_exp, rhs_typ, loc) ->
         let id_map' = analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ astate in
         let reads' =
           match rhs_exp with
           | Lfield ( _, _, typ) when is_unprotected locks ->
-              add_path_to_state rhs_exp typ loc reads id_map
+              add_path_to_state rhs_exp typ loc reads id_map owned
           | _ ->
               reads in
-        { astate with Domain.reads = reads'; id_map = id_map'; }
+        (* if rhs is owned, propagate ownership to lhs *)
+        let owned' =
+          match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with
+          | Some rhs_access_path
+            when ThreadSafetyDomain.OwnershipDomain.mem rhs_access_path owned ->
+              ThreadSafetyDomain.OwnershipDomain.add (AccessPath.of_id lhs_id rhs_typ) owned
+          | _ ->
+              owned in
+        { astate with Domain.reads = reads'; id_map = id_map'; owned = owned'; }
     |  _  ->
         astate
 end

infer/src/checkers/ThreadSafetyDomain.ml

@@ -11,12 +11,17 @@ open! IStd
 
 module F = Format
 
+module RawAccessPath = struct
+  type t = AccessPath.raw
+  let compare = AccessPath.compare_raw
+  let pp = AccessPath.pp_raw
+  let pp_element = pp
+end
+
+module OwnershipDomain = AbstractDomain.InvertedSet(PrettyPrintable.MakePPSet(RawAccessPath))
+
 module TraceElem = struct
-  module Kind = struct
-    type t = AccessPath.raw
-    let compare = AccessPath.compare_raw
-    let pp = AccessPath.pp_raw
-  end
+  module Kind = RawAccessPath
 
   type t = {
     site : CallSite.t;
@@ -64,6 +69,8 @@ type astate =
     (** access paths written outside of synchronization *)
     id_map : IdAccessPathMapDomain.astate;
     (** map used to decompile temporary variables into access paths *)
+    owned : OwnershipDomain.astate;
+    (** access paths that must be owned by the current function *)
   }
 
 (** same as astate, but without [id_map] (since it's local) *)
@@ -74,7 +81,8 @@ let initial =
   let reads = PathDomain.initial in
   let writes = PathDomain.initial in
   let id_map = IdAccessPathMapDomain.initial in
-  { locks; reads; writes; id_map; }
+  let owned = OwnershipDomain.initial in
+  { locks; reads; writes; id_map; owned; }
 
 let (<=) ~lhs ~rhs =
   if phys_equal lhs rhs
@@ -83,7 +91,8 @@ let (<=) ~lhs ~rhs =
     LocksDomain.(<=) ~lhs:lhs.locks ~rhs:rhs.locks &&
     PathDomain.(<=) ~lhs:lhs.reads ~rhs:rhs.reads &&
     PathDomain.(<=) ~lhs:lhs.writes ~rhs:rhs.writes &&
-    IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map
+    IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map &&
+    OwnershipDomain.(<=) ~lhs:lhs.owned ~rhs:rhs.owned
 
 let join astate1 astate2 =
   if phys_equal astate1 astate2
@@ -94,7 +103,8 @@ let join astate1 astate2 =
     let reads = PathDomain.join astate1.reads astate2.reads in
     let writes = PathDomain.join astate1.writes astate2.writes in
     let id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in
-    { locks; reads; writes; id_map; }
+    let owned = OwnershipDomain.join astate1.owned astate2.owned in
+    { locks; reads; writes; id_map; owned; }
 
 let widen ~prev ~next ~num_iters =
   if phys_equal prev next
@@ -105,7 +115,8 @@ let widen ~prev ~next ~num_iters =
     let reads = PathDomain.widen ~prev:prev.reads ~next:next.reads ~num_iters in
     let writes = PathDomain.widen ~prev:prev.writes ~next:next.writes ~num_iters in
     let id_map = IdAccessPathMapDomain.widen ~prev:prev.id_map ~next:next.id_map ~num_iters in
-    { locks; reads; writes; id_map; }
+    let owned = OwnershipDomain.widen ~prev:prev.owned ~next:next.owned ~num_iters in
+    { locks; reads; writes; id_map; owned; }
 
 let pp_summary fmt (locks, reads, writes) =
   F.fprintf
@@ -115,9 +126,10 @@ let pp_summary fmt (locks, reads, writes) =
     PathDomain.pp reads
     PathDomain.pp writes
 
-let pp fmt { locks; reads; writes; id_map; } =
+let pp fmt { locks; reads; writes; id_map; owned; } =
   F.fprintf
     fmt
-    "%a Id Map: %a"
+    "%a Id Map: %a Owned: %a"
     pp_summary (locks, reads, writes)
     IdAccessPathMapDomain.pp id_map
+    OwnershipDomain.pp owned

infer/tests/codetoanalyze/java/threadsafety/Ownership.java

@@ -0,0 +1,112 @@
+/*
+ * 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;
+
+class Obj {
+  Object f;
+  Obj g;
+}
+
+@ThreadSafe
+public class Ownership {
+
+  Obj field;
+
+  public Ownership(Obj o) {
+    field = o;
+  }
+
+  native void leakToAnotherThread(Object o);
+
+  public void escapeViaConstructorBad() {
+    Obj local = new Obj();
+    Ownership constructed = new Ownership(local);
+    local.f = new Object();
+  }
+
+  public void ownInOneBranchBad(Obj formal, boolean b) {
+    if (b) {
+      formal = new Obj();
+    }
+    // we might not own formal
+    formal.f = new Object();
+  }
+
+  public void reassignToFormalBad(Obj formal) {
+    Obj local = new Obj();
+    formal.g = local; // bad, we don't own formal
+    formal.g.f = new Object(); // ok; now that formal.g is reassigned to local, which we do own
+  }
+
+  public void ownedLocalOk() {
+    Obj local = new Obj();
+    local.f = new Object();
+  }
+
+  public Obj returnOwnedLocalOk() {
+    Obj local = new Obj();
+    local.f = new Object();
+    return local;
+  }
+
+  public void writeOwnedLocalThenEscapeOk() {
+    Obj local = new Obj();
+    local.f = new Object();
+    leakToAnotherThread(local);
+  }
+
+  public void ownInBranchesOk1(boolean b) {
+    Obj local;
+    if (b) {
+      local = new Obj();
+      local.f = new Object();
+    } else {
+      local = new Obj();
+      local.f = new Integer(0);
+    }
+    local.f = new Boolean(false);
+  }
+
+  public void ownedAccessPathOk() {
+    Obj local = new Obj();
+    local.g = new Obj();
+    local.g.f = new Object();
+  }
+
+  public void aliasOwnedLocalOk() {
+    Obj local = new Obj();
+    Obj alias = local;
+    alias.f = new Object();
+    local.f = new Object();
+  }
+
+  public void aliasOwnedLocalAccessPathOk() {
+    Obj local = new Obj();
+    local.g = new Obj();
+    Obj alias = local.g;
+    alias.f = new Object();
+  }
+
+  // we don't understand that ownership has been transferred from returnOwnedLocalOk to the current
+  // procedure
+  public void FP_ownershipNotInterproceduralOk() {
+    Obj local = returnOwnedLocalOk();
+    local.f = new Object();
+  }
+
+  // we angelically assume that callees don't leak their arguments to another thread for now, so
+  // we'll miss this
+  public void FN_escapeThenWriteLocalBad() {
+    Obj local = new Obj();
+    leakToAnotherThread(local);
+    local.f = new Object();
+  }
+
+}

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

@@ -6,6 +6,9 @@ codetoanalyze/java/threadsafety/Locks.java, void Locks.afterReentrantLockUnlockB
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterWriteLockUnlockBad(), 3, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.lockInOneBranchBad(boolean), 4, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f]
+codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_ownershipNotInterproceduralOk(), 2, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Obj.f]
+codetoanalyze/java/threadsafety/Ownership.java, void Ownership.ownInOneBranchBad(Obj,boolean), 5, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Obj.f]
+codetoanalyze/java/threadsafety/Ownership.java, void Ownership.reassignToFormalBad(Obj), 2, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Obj.g]
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 1, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ExtendsThreadSafeExample.field]
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 1, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ExtendsThreadSafeExample.field]
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.callPublicMethodBad(), 1, THREAD_SAFETY_ERROR, [call to void ThreadSafeExample.assignInPrivateMethodOk(),access to codetoanalyze.java.checkers.ThreadSafeExample.f]