pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[racerd] ownership of contained objects should be that of container

Browse Source 
Summary:
When retrieving a value from a container, we previously had an arbitrary hack which would
- In java, give no ownership to the returned object (trying to be sound)
- In C++ give conditional ownership to the current method's first argument (trying to be complete, but doing it badly, as the first argument may not be the `this` object in a static method, or we might be accessing it through another parameter altogether).

Harmonise both by using the existing ownership of the container as ownership value for the returned object (leaning towards completeness).

Reviewed By: jvillard

Differential Revision: D18882800

fbshipit-source-id: f98f8d315
master
Nikos Gorogiannis 5 years ago committed by Facebook Github Bot
parent 6a8a811e69
commit b012bb9435
3 changed files with 46 additions and 33 deletions
Show Stats Download Patch File Download Diff File

27
infer/src/concurrency/RacerD.ml
Unescape View File

@ -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 =

20
infer/tests/codetoanalyze/java/racerd/Ownership.java
Unescape View File

@ -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<MyObj> children = new ArrayList<MyObj>();
setFirstOk(children);
}
private void setFirstOk(ArrayList<MyObj> children) {
MyObj obj = children.get(0);
if (obj == null) {
obj = new MyObj();
}
obj.data = 10;
}
}

32
infer/tests/codetoanalyze/java/racerd/issues.exp
Unescape View File

@ -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, [<Read trace>,access to `this.mField3`,<Write trace>,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.<init>(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, [<Read trace>,access to `this.field`,<Write trace>,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, [<Read trace>,access to `checkers.Ownership.global`,<Write trace>,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, [<Read trace>,access to `formal.g`,<Write trace>,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, [<Read trace>,access to `this.field`,<Write trace>,access to `this.field`]
codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.<init>(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, [<Read trace>,access to `this.field`,<Write trace>,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, [<Read trace>,access to `checkers.Ownership.global`,<Write trace>,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, [<Read trace>,access to `formal.g`,<Write trace>,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, [<Read trace>,access to `this.field`,<Write trace>,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`]

Write Preview
Loading…
Cancel
Save