From 4373945e7483df1fff9c89ff9d20b0a4b969fa74 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 19 Jan 2017 10:23:47 -0800 Subject: [PATCH] [thread-safety] don't warn on writes rooted in a parameter owned by the callee Summary: In code like ``` foo() { Object local = new Object(); iWriteToAField(local); } ``` , we don't want to warn because the object pointed to by `local` is owned by the caller, then ownership is transferred to the callee. This diff supports this by introducing a notion of "conditional" and "unconditional" writes. Conditional writes are writes that are rooted in a formal of the current procedure, and they are safe only if the actual bound to that formal is owned at the call site (as in the `foo` example above). Unconditional writes are rooted in a local, and they are only safe if a lock is held in the caller. Reviewed By: peterogithub Differential Revision: D4429131 fbshipit-source-id: 2c6112b --- infer/src/checkers/ThreadSafety.ml | 121 ++++++++++++++---- infer/src/checkers/ThreadSafetyDomain.ml | 16 +++ .../java/threadsafety/Ownership.java | 57 +++++++++ .../java/threadsafety/issues.exp | 6 + 4 files changed, 177 insertions(+), 23 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index db10ab37a..33f32842b 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -26,7 +26,7 @@ module Summary = Summary.Make (struct module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ThreadSafetyDomain - type extras = ProcData.no_extras + type extras = FormalMap.t type lock_model = | Lock @@ -64,6 +64,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct try Some (IdAccessPathMapDomain.find id id_map) with Not_found -> None + let is_owned access_path owned_set = + ThreadSafetyDomain.OwnershipDomain.mem access_path owned_set + let add_path_to_state exp typ loc path_state id_map owned tenv = (* remove the last field of the access path, if it has any *) let truncate = function @@ -88,8 +91,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct IList.fold_left (fun acc rawpath -> - if not (ThreadSafetyDomain.OwnershipDomain.mem (truncate rawpath) owned) && - not (is_safe_write rawpath) + if not (is_owned (truncate rawpath) owned) && not (is_safe_write rawpath) then ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc else @@ -103,7 +105,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Some rhs_access_path -> IdAccessPathMapDomain.add lhs_id rhs_access_path id_map | None -> id_map - let exec_instr (astate : Domain.astate) { ProcData.pdesc; tenv; } _ = + let exec_instr (astate : Domain.astate) { ProcData.pdesc; tenv; extras; } _ = let is_allocation pn = Procname.equal pn BuiltinDecl.__new || Procname.equal pn BuiltinDecl.__new_array in @@ -163,7 +165,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else begin match Summary.read_summary pdesc pn with - | Some (callee_locks, callee_reads, _, callee_unconditional_writes) -> + | Some (callee_locks, + callee_reads, + callee_conditional_writes, + callee_unconditional_writes) -> let locks' = callee_locks || astate.locks in let astate' = (* TODO (14842325): report on constructors that aren't threadsafe @@ -171,15 +176,52 @@ module TransferFunctions (CFG : ProcCfg.S) = struct if is_unprotected locks' then let call_site = CallSite.make pn loc in + (* add the conditional writes rooted in the callee formal at [index] to + the current state *) + let add_conditional_writes + ((cond_writes, uncond_writes) as acc) index (actual_exp, actual_typ) = + try + let callee_cond_writes_for_index' = + let callee_cond_writes_for_index = + ThreadSafetyDomain.ConditionalWritesDomain.find + index callee_conditional_writes in + ThreadSafetyDomain.PathDomain.with_callsite + callee_cond_writes_for_index + call_site in + begin + match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with + | Some actual_access_path -> + if is_owned actual_access_path astate.owned + then + (* the actual passed to the current callee is owned. drop all + the conditional writes for that actual, since they're all + safe *) + acc + else + cond_writes, + ThreadSafetyDomain.PathDomain.join + uncond_writes callee_cond_writes_for_index' + | _ -> + cond_writes, + ThreadSafetyDomain.PathDomain.join + uncond_writes callee_cond_writes_for_index' + end + with Not_found -> + acc in + let conditional_writes, unconditional_writes = + let combined_unconditional_writes = + ThreadSafetyDomain.PathDomain.with_callsite + callee_unconditional_writes + call_site + |> ThreadSafetyDomain.PathDomain.join astate.unconditional_writes in + IList.fold_lefti + add_conditional_writes + (astate.conditional_writes, combined_unconditional_writes) + actuals in let reads = ThreadSafetyDomain.PathDomain.with_callsite callee_reads call_site |> ThreadSafetyDomain.PathDomain.join astate.reads in - let unconditional_writes = - ThreadSafetyDomain.PathDomain.with_callsite - callee_unconditional_writes - call_site - |> ThreadSafetyDomain.PathDomain.join astate.unconditional_writes in - { astate with reads; unconditional_writes; } + { astate with reads; conditional_writes; unconditional_writes; } else astate in { astate' with locks = locks'; } @@ -193,15 +235,37 @@ module TransferFunctions (CFG : ProcCfg.S) = struct { astate with id_map = id_map'; } | Sil.Store (lhs_exp, lhs_typ, rhs_exp, loc) -> - let unconditional_writes = + let get_formal_index exp typ = match AccessPath.of_lhs_exp exp typ ~f_resolve_id with + | Some (base, _) -> FormalMap.get_formal_index base extras + | None -> None in + let conditional_writes, unconditional_writes = match lhs_exp with - | Lfield ( _, _, typ) + | Lfield (base_exp, _, typ) when is_unprotected astate.locks -> (* abstracts no lock being held *) - add_path_to_state - lhs_exp typ loc astate.unconditional_writes astate.id_map astate.owned tenv + begin + match get_formal_index base_exp typ with + | Some formal_index -> + let conditional_writes_for_index = + try + ThreadSafetyDomain.ConditionalWritesDomain.find + formal_index astate.conditional_writes + with Not_found -> + ThreadSafetyDomain.PathDomain.empty in + let conditional_writes_for_index' = + add_path_to_state + lhs_exp typ loc conditional_writes_for_index astate.id_map astate.owned tenv + in + ThreadSafetyDomain.ConditionalWritesDomain.add + formal_index conditional_writes_for_index' astate.conditional_writes, + astate.unconditional_writes + | None -> + astate.conditional_writes, + add_path_to_state + lhs_exp typ loc astate.unconditional_writes astate.id_map astate.owned tenv + end | _ -> - astate.unconditional_writes in - (* if rhs is owned, propagate ownership to lhs. otherwise, remove lhs from ownerhsip set + astate.conditional_writes, astate.unconditional_writes in + (* if rhs is owned, propagate ownership to lhs. otherwise, remove lhs from ownership 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, @@ -214,7 +278,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ThreadSafetyDomain.OwnershipDomain.remove lhs_access_path astate.owned | _ -> astate.owned in - { astate with unconditional_writes; owned; } + { astate with conditional_writes; unconditional_writes; 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 @@ -375,7 +439,7 @@ let make_results_table get_proc_desc file_env = match Interprocedural.compute_and_store_post ~compute_post - ~make_extras:ProcData.make_empty_extras + ~make_extras:FormalMap.make callback_arg with | Some post -> post | None -> empty @@ -404,12 +468,21 @@ let calculate_addendum_message tenv pname = else "" | _ -> "" +let combine_conditional_unconditional_writes conditional_writes unconditional_writes = + ThreadSafetyDomain.ConditionalWritesDomain.fold + (fun _ writes acc -> ThreadSafetyDomain.PathDomain.join writes acc) + conditional_writes + unconditional_writes + + 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 (_, _, _, unconditional_writes) -> unconditional_writes - | _ -> PathDomain.empty in + | Some (_, _, conditional_writes, unconditional_writes) -> + combine_conditional_unconditional_writes conditional_writes unconditional_writes + | _ -> + PathDomain.empty in let report_one_path ((_, sinks) as path) = let pp_accesses fmt sink = let _, accesses = PathDomain.Sink.kind sink in @@ -467,8 +540,10 @@ let process_results_table file_env tab = (should_report_on_all_procs || is_annotated Annotations.ia_is_thread_safe_method pdesc) && should_report_on_proc proc_env in ResultsTableType.iter (* report errors for each method *) - (fun proc_env (_, _, _, unconditional_writes) -> - if should_report proc_env then report_thread_safety_violations proc_env 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) tab (*This is a "cluster checker" *) diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index c662a5bad..ccb0bb879 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -84,6 +84,22 @@ type astate = (** access paths that must be owned by the current function *) } +(** the primary role of this domain is tracking *conditional* and *unconditional* writes. + conditional writes are writes that are rooted in a formal of the current procedure, and they + are safe only if the actual bound to that formal is owned at the call site (as in the foo + example below). Unconditional writes are rooted in a local, and they are only safe if a lock is + held in the caller. + To demonstrate what conditional writes buy us, consider the following example: + + foo() { + Object local = new Object(); + iWriteToAField(local); + } + + We don't want to warn on this example because the object pointed to by local is owned by the + caller foo, then ownership is transferred to the callee iWriteToAField. +*) + (** same as astate, but without [id_map]/[owned] (since they are local) *) type summary = LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate *PathDomain.astate diff --git a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java index 3230fe6ff..280b2e6d9 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java @@ -96,6 +96,63 @@ public class Ownership { alias.f = new Object(); } + private void writeToFormal(Obj formal) { + formal.f = new Object(); + } + + private void callWriteToFormal(Obj formal) { + writeToFormal(formal); + } + + private void setField(Obj o) { + this.field = o; + } + + native Obj getMaybeUnownedObj(); + + // warn here even though this this is safe if `o` is owned at all call sites. because it's a + // public method, it's possible to use it in an unsafe way + public void writeToNotOwnedInCalleeBad1(Obj o) { + writeToFormal(o); + } + + public void writeToNotOwnedInCalleeBad2() { + Obj o = getMaybeUnownedObj(); + writeToFormal(o); + } + + public void writeToNotOwnedInCalleeBad3(Obj o) { + callWriteToFormal(o); + } + + // assuming that we can't own the `this` object + public void cantOwnThisBad() { + setField(new Obj()); + } + + public void writeToOwnedInCalleeOk1() { + Obj o = new Obj(); + writeToFormal(o); + } + + public void writeToOwnedInCalleeOk2() { + synchronized (this) { + this.field = new Obj(); + } + writeToFormal(this.field); + } + + public void FP_writeToOwnedInCalleeIndirectOk1() { + Obj o = new Obj(); + callWriteToFormal(o); + } + + public void FP_writeToOwnedInCalleeIndirectOk2() { + Obj o = new Obj(); + o.g = new Obj(); + callWriteToFormal(o.g); + } + // we don't understand that ownership has been transferred from returnOwnedLocalOk to the current // procedure public void FP_ownershipNotInterproceduralOk() { diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 0516dfbcc..707f5763d 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -13,8 +13,14 @@ codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THRE 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_writeToOwnedInCalleeIndirectOk1(), 2, 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.FP_writeToOwnedInCalleeIndirectOk2(), 3, 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.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] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad1(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f] +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/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]