diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 7700e5e65..fac009a24 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -54,28 +54,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let make_container_access ret_base callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc (astate : Domain.t) = let open Domain in - let callee_access = - if RacerDModels.is_synchronized_container callee_pname receiver_ap tenv then None - else + if RacerDModels.is_synchronized_container callee_pname receiver_ap tenv then None + else + let callee_access = let container_access = TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc in let ownership_pre = OwnershipDomain.get_precondition receiver_ap astate.ownership in AccessSnapshot.make container_access astate.locks astate.threads ownership_pre caller_pdesc - in - (* if a container c is owned in cpp, make c[i] owned for all i *) - let ownership_value = - match callee_pname with - | Typ.Procname.ObjC_Cpp _ | C _ -> - OwnershipAbstractValue.make_owned_if 0 - | _ -> - OwnershipAbstractValue.unowned - in - let ownership = - OwnershipDomain.add (AccessExpression.base ret_base) ownership_value astate.ownership - in - let accesses = AccessDomain.add_opt callee_access astate.accesses in - Some {astate with accesses; ownership} + in + let ownership_value = OwnershipDomain.get_owned receiver_ap astate.ownership in + let ownership = + OwnershipDomain.add (AccessExpression.base ret_base) ownership_value astate.ownership + in + let accesses = AccessDomain.add_opt callee_access astate.accesses in + Some {astate with accesses; ownership} let add_reads exps loc ({accesses; locks; threads; ownership} as astate : Domain.t) proc_data = diff --git a/infer/tests/codetoanalyze/java/racerd/Ownership.java b/infer/tests/codetoanalyze/java/racerd/Ownership.java index 4914a17d1..fb2f8cd25 100644 --- a/infer/tests/codetoanalyze/java/racerd/Ownership.java +++ b/infer/tests/codetoanalyze/java/racerd/Ownership.java @@ -9,6 +9,7 @@ package codetoanalyze.java.checkers; import java.lang.reflect.Constructor; import java.lang.reflect.InvocationTargetException; +import java.util.ArrayList; import javax.annotation.concurrent.ThreadSafe; import javax.inject.Inject; import javax.inject.Provider; @@ -532,3 +533,22 @@ class OtherObj { new OtherObj(new Obj()); } } + +@ThreadSafe +class ContainerOwnership { + + ContainerOwnership() { + ArrayList children = new ArrayList(); + setFirstOk(children); + } + + private void setFirstOk(ArrayList children) { + MyObj obj = children.get(0); + + if (obj == null) { + obj = new MyObj(); + } + + obj.data = 10; + } +} diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index 15eea1d8e..aa4b0d68b 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -71,22 +71,22 @@ codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.tryLockN codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.tryLockWrongBranchBad():void, 98, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.f`] codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.unownedReadBad():java.lang.Object, 362, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.mField3`,,call to void Locks.lockedWriteInCallee2(),access to `this.mField3`] codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.useLockInCalleeBad():void, 221, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.(codetoanalyze.java.checkers.Obj,java.lang.Object), 65, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `obj.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.cantOwnThisBad():void, 170, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.setField(Obj),access to `this.field`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.castThenCallBad():void, 343, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.castThenCall(Obj),call to void Subclass.doWrite(),access to `s.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.conditionalAliasBad(codetoanalyze.java.checkers.Obj):void, 510, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.conditionalAlias(Obj,Obj),access to `alias.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notOwnedInCalleeBad(codetoanalyze.java.checkers.Obj):void, 232, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.mutateIfNotNull(Obj),access to `o.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToAccessPathRootedAtFormalBad(codetoanalyze.java.checkers.Obj):void, 420, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `m.g`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad():void, 427, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,call to void Ownership.setField(Obj),access to `this.field`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad():void, 429, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `m.g`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.ownInOneBranchBad(codetoanalyze.java.checkers.Obj,boolean):void, 81, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `formal.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.readGlobalBad():int, 402, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `checkers.Ownership.global`,,access to `checkers.Ownership.global`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.reassignToFormalBad(codetoanalyze.java.checkers.Obj):void, 86, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `formal.g`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.reassignToFormalBad(codetoanalyze.java.checkers.Obj):void, 87, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `formal.g`,,access to `formal.g`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad1(codetoanalyze.java.checkers.Obj):void, 156, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.writeToFormal(Obj),access to `o.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad2():void, 161, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.writeToFormal(Obj),access to `o.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad3(codetoanalyze.java.checkers.Obj):void, 165, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to `o.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToOwnedInCalleeOk2():void, 182, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,access to `this.field`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.(codetoanalyze.java.checkers.Obj,java.lang.Object), 66, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `obj.f`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.cantOwnThisBad():void, 171, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.setField(Obj),access to `this.field`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.castThenCallBad():void, 344, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.castThenCall(Obj),call to void Subclass.doWrite(),access to `s.f`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.conditionalAliasBad(codetoanalyze.java.checkers.Obj):void, 511, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.conditionalAlias(Obj,Obj),access to `alias.f`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notOwnedInCalleeBad(codetoanalyze.java.checkers.Obj):void, 233, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.mutateIfNotNull(Obj),access to `o.f`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToAccessPathRootedAtFormalBad(codetoanalyze.java.checkers.Obj):void, 421, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `m.g`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad():void, 428, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,call to void Ownership.setField(Obj),access to `this.field`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad():void, 430, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `m.g`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.ownInOneBranchBad(codetoanalyze.java.checkers.Obj,boolean):void, 82, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `formal.f`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.readGlobalBad():int, 403, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `checkers.Ownership.global`,,access to `checkers.Ownership.global`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.reassignToFormalBad(codetoanalyze.java.checkers.Obj):void, 87, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `formal.g`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.reassignToFormalBad(codetoanalyze.java.checkers.Obj):void, 88, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `formal.g`,,access to `formal.g`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad1(codetoanalyze.java.checkers.Obj):void, 157, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.writeToFormal(Obj),access to `o.f`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad2():void, 162, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.writeToFormal(Obj),access to `o.f`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad3(codetoanalyze.java.checkers.Obj):void, 166, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to `o.f`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToOwnedInCalleeOk2():void, 183, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,access to `this.field`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional2_bad(boolean):void, 130, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditionalMainThreadWriteBad():void, 219, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void RaceWithMainThread.conditionalMainThreadWrite2(boolean),access to `this.mOnlyWrittenOnMain`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional_isMainThread_ElseBranch_Bad():void, 152, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.ff`]