[thread-safety] allow ownership to be transferred via return

Summary:
Previously, we would correctly be silent on code like `x = new T(); x.f = ...`, but would wrongly warn on code like `x = makeT(); x.f = ...`.
The reason is that we only allowed ownership through direct allocation.
This diff adds a boolean that specifies whether the return value is owned as part of the summary.
This allows us to correctly handle many common cases of (transitively) returning a freshly allocated object, but still won't work for understanding that ownership is maintained in examples like
 `x = new T(); y = id(x); y.f = ...`.

Reviewed By: jvillard

Differential Revision: D4456864

fbshipit-source-id: b5eec02

infer/src/checkers/ThreadSafety.ml

@@ -166,7 +166,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           | None ->
               astate
         end
-    | Sil.Call (_, Const (Cfun pn), actuals, loc, _) ->
+    | Sil.Call (ret_opt, Const (Cfun pn), actuals, loc, _) ->
         begin
           (* assuming that modeled procedures do not have useful summaries *)
           match get_lock_model pn with
@@ -190,7 +190,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                   | Some (callee_locks,
                           callee_reads,
                           callee_conditional_writes,
-                          callee_unconditional_writes) ->
+                          callee_unconditional_writes,
+                          is_retval_owned) ->
                       let locks' = callee_locks || astate.locks in
                       let astate' =
                         (* TODO (14842325): report on constructors that aren't threadsafe
@@ -261,7 +262,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                           { astate with reads; conditional_writes; unconditional_writes; }
                         else
                           astate in
-                      { astate' with locks = locks'; }
+                      let owned = match ret_opt with
+                        | Some (ret_id, ret_typ) when is_retval_owned ->
+                            OwnershipDomain.add (AccessPath.of_id ret_id ret_typ) astate'.owned
+                        | _ ->
+                            astate'.owned in
+                      { astate' with locks = locks'; owned; }
                   | None ->
                       astate
                 end
@@ -458,7 +464,10 @@ let make_results_table get_proc_desc file_env =
   let compute_post_for_procedure = (* takes proc_env as arg *)
     fun (idenv, tenv, proc_name, proc_desc) ->
       let open ThreadSafetyDomain in
-      let empty = false, PathDomain.empty, ConditionalWritesDomain.empty, PathDomain.empty in
+      let has_lock = false in
+      let ret_is_owned = false in
+      let empty =
+        has_lock, PathDomain.empty, ConditionalWritesDomain.empty, PathDomain.empty, ret_is_owned in
       (* convert the abstract state to a summary by dropping the id map *)
       let compute_post ({ ProcData.pdesc; tenv; } as proc_data) =
         if should_analyze_proc pdesc tenv
@@ -466,8 +475,13 @@ let make_results_table get_proc_desc file_env =
           begin
             if not (Procdesc.did_preanalysis pdesc) then Preanal.do_liveness pdesc tenv;
             match Analyzer.compute_post proc_data ~initial:ThreadSafetyDomain.empty with
-            | Some { locks; reads; conditional_writes; unconditional_writes; } ->
+            | Some { locks; reads; conditional_writes; unconditional_writes; owned; } ->
-                Some (locks, reads, conditional_writes, unconditional_writes)
+                let return_var_ap =
+                  AccessPath.of_pvar
+                    (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc))
+                    (Procdesc.get_ret_type pdesc) in
+                let return_is_owned = OwnershipDomain.mem return_var_ap owned in
+                Some (locks, reads, conditional_writes, unconditional_writes, return_is_owned)
             | None ->
                 None
           end
@@ -519,7 +533,7 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) trace =
   let open ThreadSafetyDomain in
   let trace_of_pname callee_pname =
     match Summary.read_summary pdesc callee_pname with
-    | Some (_, _, conditional_writes, unconditional_writes) ->
+    | Some (_, _, conditional_writes, unconditional_writes, _) ->
         combine_conditional_unconditional_writes conditional_writes unconditional_writes
     | _ ->
         PathDomain.empty in
@@ -599,7 +613,7 @@ 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 (_, _, conditional_writes, unconditional_writes, _) ->
        if should_report proc_env then
          combine_conditional_unconditional_writes conditional_writes unconditional_writes
          |> report_thread_safety_violations proc_env)

infer/src/checkers/ThreadSafetyDomain.ml

@@ -65,8 +65,9 @@ type astate =
     owned : OwnershipDomain.astate;
   }
 
+
 type summary =
-  LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate *PathDomain.astate
+  LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate * PathDomain.astate * bool
 
 let empty =
   let locks = false in
@@ -119,19 +120,23 @@ let widen ~prev ~next ~num_iters =
     let owned = OwnershipDomain.widen ~prev:prev.owned ~next:next.owned ~num_iters in
     { locks; reads; conditional_writes; unconditional_writes; id_map; owned; }
 
-let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes) =
+let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, retval_owned) =
   F.fprintf
     fmt
-    "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a"
+    "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Retval owned: %b"
     LocksDomain.pp locks
     PathDomain.pp reads
     ConditionalWritesDomain.pp conditional_writes
     PathDomain.pp unconditional_writes
+    retval_owned
 
 let pp fmt { locks; reads; conditional_writes; unconditional_writes; id_map; owned; } =
   F.fprintf
     fmt
-    "%a Id Map: %a Owned: %a"
+    "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Id Map: %a Owned: %a"
-    pp_summary (locks, reads, conditional_writes, unconditional_writes)
+    LocksDomain.pp locks
+    PathDomain.pp reads
+    ConditionalWritesDomain.pp conditional_writes
+    PathDomain.pp unconditional_writes
     IdAccessPathMapDomain.pp id_map
     OwnershipDomain.pp owned

infer/src/checkers/ThreadSafetyDomain.mli

@@ -59,9 +59,10 @@ type astate =
     (** access paths that must be owned by the current function *)
   }
 
-(** same as astate, but without [id_map]/[owned] (since they are local) *)
+(** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of a
+    boolean that is true if the return value is owned *)
 type summary =
-  LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate * PathDomain.astate
+  LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate * PathDomain.astate * bool
 
 include AbstractDomain.WithBottom with type astate := astate
 

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

@@ -153,11 +153,26 @@ public class Ownership {
     callWriteToFormal(o.g);
   }
 
-  // we don't understand that ownership has been transferred from returnOwnedLocalOk to the current
+  public Obj ownershipCanBeInterproceduralOk() {
-  // procedure
-  public void FP_ownershipNotInterproceduralOk() {
     Obj local = returnOwnedLocalOk();
     local.f = new Object();
+    return local;
+  }
+
+  public void mutateDoubleReturnOwnedOk() {
+    Obj owned = ownershipCanBeInterproceduralOk();
+    owned.g = new Obj();
+  }
+
+  Obj id(Obj param) {
+    return param;
+  }
+
+  // need to be able to propagate ownership rather than just return it for this to work
+  public void FP_passOwnershipInIdFunctionOk() {
+    Obj owned = new Obj();
+    Obj shouldBeOwned = id(owned); // we'll lose ownership here, but ideally we wouldn't
+    shouldBeOwned.f = new Object();
   }
 
   // we angelically assume that callees don't leak their arguments to another thread for now, so
@@ -168,4 +183,15 @@ public class Ownership {
     local.f = new Object();
   }
 
+  private Obj leakThenReturn() {
+    Obj local = new Obj();
+    leakToAnotherThread(local);
+    return local;
+  }
+
+  // the summary for leakThenReturn should not say that the caller owns the return value
+  public void FN_mutateReturnedBad() {
+    Obj notOwned = leakThenReturn();
+    notOwned.f = new Object(); // should warn here
+  }
 }

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

@@ -15,7 +15,7 @@ codetoanalyze/java/threadsafety/Locks.java, void Locks.afterReentrantLockUnlockB
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterWriteLockUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.lockInOneBranchBad(boolean), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
-codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_ownershipNotInterproceduralOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f]
+codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_passOwnershipInIdFunctionOk(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.cantOwnThisBad(), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.setField(Obj),access to codetoanalyze.java.checkers.Ownership.field]
 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]