diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index ccd41c7fe..3102a4f49 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -23,6 +23,10 @@ module Summary = Summary.Make (struct payload.Specs.threadsafety end) +let is_owned access_path attribute_map = + ThreadSafetyDomain.AttributeMapDomain.has_attribute + access_path ThreadSafetyDomain.Attribute.unconditionally_owned attribute_map + module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ThreadSafetyDomain @@ -68,12 +72,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Exp.Const _ -> true | _ -> false - let propagate_attributes lhs_access_path_opt rhs_access_path_opt rhs_exp attribute_map = + let add_conditional_ownership_attribute access_path formal_map attribute_map attributes = + match FormalMap.get_formal_index (fst access_path) formal_map with + | Some formal_index when not (is_owned access_path attribute_map) -> + Domain.AttributeSetDomain.add (Domain.Attribute.OwnedIf (Some formal_index)) attributes + | _ -> + attributes + + let propagate_attributes + lhs_access_path_opt rhs_access_path_opt rhs_exp attribute_map formal_map = match lhs_access_path_opt, rhs_access_path_opt with | Some lhs_access_path, Some rhs_access_path -> let rhs_attributes = - try Domain.AttributeMapDomain.find rhs_access_path attribute_map - with Not_found -> Domain.AttributeSetDomain.empty in + (try Domain.AttributeMapDomain.find rhs_access_path attribute_map + with Not_found -> Domain.AttributeSetDomain.empty) + |> add_conditional_ownership_attribute rhs_access_path formal_map attribute_map in Domain.AttributeMapDomain.add lhs_access_path rhs_attributes attribute_map | Some lhs_access_path, None -> let rhs_attributes = @@ -81,13 +94,59 @@ module TransferFunctions (CFG : ProcCfg.S) = struct then (* constants are both owned and functional *) Domain.AttributeSetDomain.of_list - [Domain.Attribute.Owned; Domain.Attribute.Functional] + [Domain.Attribute.unconditionally_owned; Domain.Attribute.Functional] else Domain.AttributeSetDomain.empty in Domain.AttributeMapDomain.add lhs_access_path rhs_attributes attribute_map | _ -> attribute_map + let propagate_return_attributes + ret_opt ret_attributes actuals attribute_map ~f_resolve_id formal_map = + match ret_opt with + | Some (ret_id, ret_typ) -> + let ownership_attributes, other_attributes = + Domain.AttributeSetDomain.partition + (function + | OwnedIf _ -> true + | _ -> false) + ret_attributes in + let caller_return_attributes = + match Domain.AttributeSetDomain.elements ownership_attributes with + | [] -> other_attributes + | [(OwnedIf None) as unconditionally_owned] -> + Domain.AttributeSetDomain.add unconditionally_owned other_attributes + | [OwnedIf (Some formal_index)] -> + begin + match List.nth actuals formal_index with + | Some (actual_exp, actual_typ) -> + begin + match + AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with + | Some actual_ap -> + if is_owned actual_ap attribute_map + then + Domain.AttributeSetDomain.add + Domain.Attribute.unconditionally_owned other_attributes + else + add_conditional_ownership_attribute + actual_ap formal_map attribute_map other_attributes + | None -> + other_attributes + end + | None -> + other_attributes + end + | _multiple_ownership_attributes -> + (* TODO: handle multiple ownership attributes *) + other_attributes in + Domain.AttributeMapDomain.add + (AccessPath.of_id ret_id ret_typ) + caller_return_attributes + attribute_map + | None -> + attribute_map + let add_path_to_state exp typ loc path_state id_map attribute_map tenv = (* remove the last field of the access path, if it has any *) let truncate = function @@ -120,9 +179,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else IList.fold_left (fun acc rawpath -> - if not (Domain.AttributeMapDomain.has_attribute - (truncate rawpath) Domain.Attribute.Owned attribute_map) && - not (is_safe_write rawpath tenv) + if not (is_owned (truncate rawpath) attribute_map) && not (is_safe_write rawpath tenv) then Domain.PathDomain.add_sink (Domain.make_access rawpath loc) acc else acc) path_state @@ -206,7 +263,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match AccessPath.of_lhs_exp (Exp.Var lhs_id) lhs_typ ~f_resolve_id with | Some lhs_access_path -> let attribute_map = - AttributeMapDomain.add_attribute lhs_access_path Owned astate.attribute_map in + AttributeMapDomain.add_attribute + lhs_access_path + Attribute.unconditionally_owned + astate.attribute_map in { astate with attribute_map; } | None -> astate @@ -235,7 +295,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct callee_reads, callee_conditional_writes, callee_unconditional_writes, - is_retval_owned) -> + return_attributes) -> let locks' = callee_locks || astate.locks in let astate' = (* TODO (14842325): report on constructors that aren't threadsafe @@ -259,8 +319,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct begin match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with | Some actual_access_path -> - if AttributeMapDomain.has_attribute - actual_access_path Owned astate.attribute_map + if is_owned actual_access_path astate.attribute_map then (* the actual passed to the current callee is owned. drop all the conditional writes for that actual, since they're all @@ -311,12 +370,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct { astate with reads; conditional_writes; unconditional_writes; } else astate in - let attribute_map = match ret_opt with - | Some (ret_id, ret_typ) when is_retval_owned -> - AttributeMapDomain.add_attribute - (AccessPath.of_id ret_id ret_typ) Owned astate'.attribute_map - | _ -> - astate'.attribute_map in + let attribute_map = + propagate_return_attributes + ret_opt + return_attributes + actuals + astate.attribute_map + ~f_resolve_id + extras in { astate' with locks = locks'; attribute_map; } | None -> if is_box callee_pname @@ -415,7 +476,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let rhs_access_path_opt = AccessPath.of_lhs_exp rhs_exp lhs_typ ~f_resolve_id in let attribute_map = propagate_attributes - lhs_access_path_opt rhs_access_path_opt rhs_exp astate.attribute_map in + lhs_access_path_opt rhs_access_path_opt rhs_exp astate.attribute_map extras in { astate with conditional_writes; unconditional_writes; attribute_map; } | Sil.Load (lhs_id, rhs_exp, rhs_typ, loc) -> @@ -431,7 +492,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let rhs_access_path_opt = AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id in let attribute_map = propagate_attributes - lhs_access_path_opt rhs_access_path_opt rhs_exp astate.attribute_map in + lhs_access_path_opt rhs_access_path_opt rhs_exp astate.attribute_map extras in { astate with Domain.reads; id_map; attribute_map; } | Sil.Remove_temps (ids, _) -> @@ -548,9 +609,9 @@ let make_results_table get_proc_desc file_env = fun (idenv, tenv, proc_name, proc_desc) -> let open ThreadSafetyDomain in let has_lock = false in - let ret_is_owned = false in + let return_attrs = AttributeSetDomain.empty in let empty = - has_lock, PathDomain.empty, ConditionalWritesDomain.empty, PathDomain.empty, ret_is_owned in + has_lock, PathDomain.empty, ConditionalWritesDomain.empty, PathDomain.empty, return_attrs in (* convert the abstract state to a summary by dropping the id map *) let compute_post ({ ProcData.pdesc; tenv; extras; } as proc_data) = if should_analyze_proc pdesc tenv @@ -566,7 +627,7 @@ let make_results_table get_proc_desc file_env = let attribute_map = AttributeMapDomain.add_attribute (base, []) - Owned + Attribute.unconditionally_owned ThreadSafetyDomain.empty.attribute_map in { ThreadSafetyDomain.empty with attribute_map; } | None -> ThreadSafetyDomain.empty @@ -578,9 +639,10 @@ let make_results_table get_proc_desc file_env = AccessPath.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc)) (Procdesc.get_ret_type pdesc) in - let return_is_owned = - AttributeMapDomain.has_attribute return_var_ap Owned attribute_map in - Some (locks, reads, conditional_writes, unconditional_writes, return_is_owned) + let return_attributes = + try AttributeMapDomain.find return_var_ap attribute_map + with Not_found -> AttributeSetDomain.empty in + Some (locks, reads, conditional_writes, unconditional_writes, return_attributes) | None -> None end diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 0436f94bb..76741c04c 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -53,14 +53,17 @@ module ConditionalWritesDomain = AbstractDomain.Map (IntMap) (PathDomain) module Attribute = struct type t = - | Owned + | OwnedIf of int option | Functional [@@deriving compare] let pp fmt = function - | Owned -> F.fprintf fmt "Owned" + | OwnedIf None -> F.fprintf fmt "Owned" + | OwnedIf (Some formal_index) -> F.fprintf fmt "Owned if formal %d is owned" formal_index | Functional -> F.fprintf fmt "Functional" + let unconditionally_owned = OwnedIf None + module Set = PrettyPrintable.MakePPSet(struct type nonrec t = t let compare = compare @@ -99,7 +102,11 @@ type astate = } type summary = - LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate * PathDomain.astate * bool + LocksDomain.astate * + PathDomain.astate * + ConditionalWritesDomain.astate * + PathDomain.astate * + AttributeSetDomain.astate let empty = let locks = false in @@ -153,15 +160,15 @@ let widen ~prev ~next ~num_iters = AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters in { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; } -let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, retval_owned) = +let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, return_attributes) = F.fprintf fmt - "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Retval owned: %b" + "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Return Attributes: %a" LocksDomain.pp locks PathDomain.pp reads ConditionalWritesDomain.pp conditional_writes PathDomain.pp unconditional_writes - retval_owned + AttributeSetDomain.pp return_attributes let pp fmt { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; } = F.fprintf diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 5429f0767..83e80f581 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -30,10 +30,15 @@ module ConditionalWritesDomain : module type of (AbstractDomain.Map (IntMap) (Pa module Attribute : sig type t = - | Owned + | OwnedIf of int option + (** owned unconditionally if OwnedIf None, owned when formal at index i is owned otherwise *) | Functional + (** holds a value returned from a callee marked @Functional *) [@@deriving compare] + (** alias for OwnedIf None *) + val unconditionally_owned : t + val pp : F.formatter -> t -> unit module Set : PrettyPrintable.PPSet with type elt = t @@ -80,10 +85,14 @@ type astate = (** map of access paths to attributes such as owned, functional, ... *) } -(** 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 *) +(** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of the + attributes associated with the return value *) type summary = - LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate * PathDomain.astate * bool + LocksDomain.astate * + PathDomain.astate * + ConditionalWritesDomain.astate * + PathDomain.astate * + AttributeSetDomain.astate include AbstractDomain.WithBottom with type astate := astate diff --git a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java index b073205bc..60a8848b4 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java @@ -241,4 +241,14 @@ class Annotations implements FunctionalInterface { return mBoxedLong; } + public boolean propagateFunctional() { + return returnBool(); + } + + // show that we can handle indirect returns of procedures marked @Functional + public void propagateFunctionalOk() { + boolean returnedFunctional = propagateFunctional(); + mBool = returnedFunctional; + } + } diff --git a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java index 5e473fc7e..adbc0b26c 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java @@ -164,10 +164,6 @@ public class Ownership { owned.g = new Obj(); } - Obj id(Obj param) { - return param; - } - Obj returnOwnedOrNull(boolean b) { if (b) { return null; @@ -196,10 +192,69 @@ public class Ownership { mutateIfNotNull(o); } - // need to be able to propagate ownership rather than just return it for this to work - public void FP_passOwnershipInIdFunctionOk() { + Obj id(Obj param) { + return param; + } + + public void passOwnershipInIdFunctionOk() { + Obj owned = new Obj(); + Obj shouldBeOwned = id(owned); + shouldBeOwned.f = new Object(); + } + + Obj id2(Obj param) { + return id(param); + } + + public void passOwnershipInMultiLevelIdFunctionOk() { + Obj owned = new Obj(); + Obj shouldBeOwned = id2(owned); + shouldBeOwned.f = new Object(); + } + + native boolean nondet(); + + public Obj returnConditionalOwnedInTwoBranches(Obj param) { + if (nondet()) { + return param; + } + return param; + } + + public void returnConditionalOwnedInTwoBranchesOk() { Obj owned = new Obj(); - Obj shouldBeOwned = id(owned); // we'll lose ownership here, but ideally we wouldn't + Obj shouldBeOwned = returnConditionalOwnedInTwoBranches(owned); + shouldBeOwned.f = new Object(); + } + + public Obj returnOwnedOrConditionalOwned(Obj param) { + if (nondet()) { + return param; + } else { + return new Obj(); + } + } + + // TODO: need to handle multiple ownership attributes in order to get this one + public void FP_ownAndConditionalOwnOk() { + Obj owned = new Obj(); + Obj shouldBeOwned = returnOwnedOrConditionalOwned(owned); + shouldBeOwned.f = new Object(); + } + + public Obj twoDifferentConditionalOwns(Obj param1, Obj param2) { + if (nondet()) { + return param1; + } else { + return param2; + } + } + + // need to handle multiple ownership attributes in order to get this one + public void FP_twoDifferentConditionalOwnsOk() { + Obj owned1 = new Obj(); + Obj owned2 = new Obj(); + Obj shouldBeOwned = twoDifferentConditionalOwns(owned1, owned2); shouldBeOwned.f = new Object(); } diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 1a10b5b04..5a240bf87 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -28,7 +28,8 @@ 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_passOwnershipInIdFunctionOk(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_ownAndConditionalOwnOk(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_twoDifferentConditionalOwnsOk(), 4, 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.notOwnedInCalleeBad(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.mutateIfNotNull(Obj),access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.ownInOneBranchBad(Obj,boolean), 5, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f]