From 369feb4149940549ac5692c4b87bc735334ecf5c Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 26 Jan 2017 08:58:42 -0800 Subject: [PATCH] [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 | 30 ++++++++++++----- infer/src/checkers/ThreadSafetyDomain.ml | 15 ++++++--- infer/src/checkers/ThreadSafetyDomain.mli | 5 +-- .../java/threadsafety/Ownership.java | 32 +++++++++++++++++-- .../java/threadsafety/issues.exp | 2 +- 5 files changed, 65 insertions(+), 19 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 53bb81a73..e79be8f5b 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/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) + | Some { locks; reads; conditional_writes; unconditional_writes; owned; } -> + 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) diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 7d3b8012d..5f3f5cdc3 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/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" - pp_summary (locks, reads, conditional_writes, unconditional_writes) + "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Id Map: %a Owned: %a" + LocksDomain.pp locks + PathDomain.pp reads + ConditionalWritesDomain.pp conditional_writes + PathDomain.pp unconditional_writes IdAccessPathMapDomain.pp id_map OwnershipDomain.pp owned diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index a2e2b17a9..595341a29 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java index d3bcb3e44..d60aa51ef 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java +++ b/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 - // procedure - public void FP_ownershipNotInterproceduralOk() { + public Obj ownershipCanBeInterproceduralOk() { 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 + } } diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index e0d5f75be..f69441001 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/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]