diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index aa3178885..7ca52e64e 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -157,23 +157,70 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> attributes - let propagate_attributes lhs_access_path rhs_access_paths attribute_map formal_map = - let rhs_attributes = - if List.is_empty rhs_access_paths (* only happens when rhs is a constant *) - then - (* rhs is a constant, and constants are both owned and functional *) - Domain.AttributeSetDomain.of_list - [Domain.Attribute.unconditionally_owned; Domain.Attribute.Functional] - else - let propagate_attributes_ acc rhs_access_path = - (try Domain.AttributeMapDomain.find rhs_access_path attribute_map - with Not_found -> acc) - |> add_conditional_ownership_attribute rhs_access_path formal_map attribute_map in - List.fold - ~f:propagate_attributes_ - ~init:Domain.AttributeSetDomain.empty - rhs_access_paths in - Domain.AttributeMapDomain.add lhs_access_path rhs_attributes attribute_map + + let remove_ownership_attributes attributes = + Domain.AttributeSetDomain.filter + (function | Domain.Attribute.OwnedIf _ -> false | _ -> true) + attributes + + (* propagate attributes from the leaves to the root of an RHS Hil expression. + Special casing on ownership. *) + let rec attributes_of_expr formal_map attribute_map e = + let open HilExp in + let open Domain in + match e with + | Constant _ -> + AttributeSetDomain.of_list [Attribute.unconditionally_owned; Attribute.Functional] + | AccessPath ap -> + begin + try AttributeMapDomain.find ap attribute_map + with Not_found -> AttributeSetDomain.empty + end + |> add_conditional_ownership_attribute ap formal_map attribute_map + | Exception expr (* treat exceptions as transparent wrt attributes *) + | Cast(_, expr) -> + attributes_of_expr formal_map attribute_map expr + | UnaryOperator(_, expr, _) -> + attributes_of_expr formal_map attribute_map expr + |> remove_ownership_attributes + | BinaryOperator(_, expr1, expr2) -> + let attributes1 = attributes_of_expr formal_map attribute_map expr1 in + let attributes2 = attributes_of_expr formal_map attribute_map expr2 in + AttributeSetDomain.join attributes1 attributes2 + |> remove_ownership_attributes + | Closure _ | Sizeof _ -> + AttributeSetDomain.empty + + (* will return true on x.f.g.h when x.f and x.f.g are owned, but not requiring x.f.g.h *) + (* must not be called with an empty access list *) + let all_prefixes_owned (base, accesses) attribute_map = + let but_last_rev = List.rev accesses |> List.tl_exn in + let rec aux acc = function + | [] -> acc + | (_::tail) as all -> aux ((List.rev all)::acc) tail in + let prefixes = aux [] but_last_rev in + List.for_all ~f:(fun ap -> is_owned (base, ap) attribute_map) prefixes + + let propagate_attributes lhs_access_path rhs_exp attribute_map formal_map = + let rhs_attributes = attributes_of_expr formal_map attribute_map rhs_exp in + let lhs_root = fst lhs_access_path in + let filter_on_globals = + (* do not assign ownership to access paths rooted at globals *) + if Var.is_global (fst lhs_root) + then remove_ownership_attributes else Fn.id + in + let filter_on_lhs = + (* do not assign ownership when lhs is not a single var or + a single-field ap whose root is conditionally owned, or, + all prefixes are owned *) + match snd lhs_access_path with + | [] -> Fn.id + | [_] when FormalMap.is_formal lhs_root formal_map -> Fn.id + | _ when all_prefixes_owned lhs_access_path attribute_map -> Fn.id + | _ -> remove_ownership_attributes + in + let final_attributes = filter_on_globals rhs_attributes |> filter_on_lhs in + Domain.AttributeMapDomain.add lhs_access_path final_attributes attribute_map let propagate_return_attributes ret_opt ret_attributes actuals attribute_map formal_map = let open Domain in @@ -696,8 +743,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate.attribute_map proc_data in let attribute_map = - propagate_attributes - lhs_access_path (HilExp.get_access_paths rhs_exp) astate.attribute_map extras in + propagate_attributes lhs_access_path rhs_exp astate.attribute_map extras in { astate with accesses; attribute_map; } | Assume (assume_exp, _, _, loc) -> diff --git a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java index 8dc8e90dd..9f4653b20 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java @@ -385,8 +385,54 @@ public class Ownership { catch (CloneNotSupportedException e) {} } + static MyObj global; + + void storeInGlobalAndWriteBad() { + MyObj x = new MyObj(); + synchronized(this) { global = x; } + x.data = 5; + } + + int readGlobalBad() { + synchronized(this) { return global.data; } + } + + public void writeOwnedWithExceptionOk() { + Obj options = returnOwnedWithException(); + options.f = new Object(); + } + + private Obj returnOwnedWithException() { + Obj options = new Obj(); + if (options.f==null) { + throw new IllegalArgumentException(); + } + return options; + } + + // not propagating ownership to access path rooted in formal + public void notPropagatingOwnershipToAccessPathRootedAtFormalBad(Obj m) { + m.g = new Obj(); + } + + // not propagating ownership to unowned local access path + public void notPropagatingOwnershipToUnownedLocalAccessPathBad() { + Obj m; + synchronized(this) { m = field; } + m.g = new Obj(); + } + + // propagating ownership to owned access path + public void propagatingOwnershipToOwnedAccessPathOk() { + Obj m = new Obj(); + m.g = new Obj(); + m.g.g = new Obj(); + m.g.g.g = new Obj(); + } + } +class MyObj { int data; } class Subclass extends Obj { diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 617b2b2b8..e19373eab 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -56,12 +56,16 @@ codetoanalyze/java/threadsafety/Locks.java, void Locks.negatedReentrantLockTryLo codetoanalyze/java/threadsafety/Locks.java, void Locks.tryLockNoCheckBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/threadsafety/Locks.java, void Locks.tryLockWrongBranchBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/threadsafety/Ownership.java, Ownership.(Obj,Object), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.f`] +codetoanalyze/java/threadsafety/Ownership.java, int Ownership.readGlobalBad(), 1, THREAD_SAFETY_VIOLATION, [,access to `codetoanalyze.java.checkers.Ownership.global`,,access to `codetoanalyze.java.checkers.Ownership.global`] 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.castThenCallBad(), 2, THREAD_SAFETY_VIOLATION, [call to void Ownership.castThenCall(Obj),call to void Subclass.doWrite(),access to `codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.castThenReturnBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.f`] 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.notPropagatingOwnershipToAccessPathRootedAtFormalBad(Obj), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.g`] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad(), 2, THREAD_SAFETY_VIOLATION, [,access to `codetoanalyze.java.checkers.Ownership.field`,,call to void Ownership.setField(Obj),access to `codetoanalyze.java.checkers.Ownership.field`] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.g`] 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.reassignToFormalBad(Obj), 3, THREAD_SAFETY_VIOLATION, [,access to `codetoanalyze.java.checkers.Obj.g`,,access to `codetoanalyze.java.checkers.Obj.g`]