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

[racerd] deep ownership

Browse Source 
Reviewed By: sblackshear

Differential Revision: D6424928

fbshipit-source-id: d3a1735
master
Peter O'Hearn 7 years ago committed by Facebook Github Bot
parent 735b0b2ef7
commit 700adc2d44
5 changed files with 106 additions and 52 deletions
Show Stats Download Patch File Download Diff File

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

@ -63,17 +63,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
OwnershipAbstractValue.unowned
(* 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 -> RacerDDomain.OwnershipDomain.is_owned (base, ap) attribute_map)
prefixes
let propagate_attributes lhs_access_path rhs_exp attribute_map =
let rhs_attributes = attributes_of_expr attribute_map rhs_exp in
Domain.AttributeMapDomain.add lhs_access_path rhs_attributes attribute_map
@ -95,7 +84,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| _ ->
false ->
ownership_of_expr rhs_exp ownership
| _ when all_prefixes_owned lhs_access_path ownership ->
| _ when Domain.OwnershipDomain.is_owned lhs_access_path ownership ->
ownership_of_expr rhs_exp ownership
| _ ->
Domain.OwnershipAbstractValue.unowned

32
infer/src/concurrency/RacerDDomain.ml
Unescape View File

@ -300,12 +300,38 @@ end
module OwnershipDomain = struct
include AbstractDomain.Map (AccessPath) (OwnershipAbstractValue)
let get_owned access_path astate =
(* Helper function used by both is_owned and get_owned. Not exported.*)
let get_owned_shallow access_path astate =
try find access_path astate with Not_found -> OwnershipAbstractValue.Unowned
let is_owned access_path astate =
match get_owned access_path astate with OwnershipAbstractValue.Owned -> true | _ -> false
(*deep ownership model where only a prefix needs to be owned in the astate*)
let is_owned (base, accesses) astate =
let is_owned_shallow access_path astate =
match get_owned_shallow access_path astate with
| OwnershipAbstractValue.Owned ->
true
| _ ->
false
in
let rec helper = function
| prefix, _ when is_owned_shallow (base, prefix) astate ->
true
| _, [] ->
false
| prefix, hd :: tl ->
helper (List.append prefix [hd], tl)
in
helper ([], accesses)
(*
returns Owned if any prefix is owned on any prefix, else OwnedIf if it is
OwnedIf in the astate, else UnOwned
*)
let get_owned access_path astate =
if is_owned access_path astate then OwnershipAbstractValue.Owned
else try find access_path astate with Not_found -> OwnershipAbstractValue.Unowned
let find = `Use_get_owned_instead

74
infer/tests/codetoanalyze/java/racerd/DeepOwnership.java
Unescape View File

@ -0,0 +1,74 @@
/*
* Copyright (c) 2017 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
import com.facebook.infer.annotation.ThreadSafe;
@ThreadSafe
class DeepOwnership {
DeepOwnership next;
static DeepOwnership global;
void globalNotOwnedBad() {
global.next = null;
}
void reassignBaseToGlobalBad(){
DeepOwnership x = new DeepOwnership();
x = global;
x.next = null;
}
void FN_reassignPathToGlobalBad() {
DeepOwnership x = new DeepOwnership();
x.next = global;
x.next.next = null;
}
void deepIntraOk(){
DeepOwnership x = new DeepOwnership();
x.next.next = null; // doesn't warn here
}
void deepInterOk(){
DeepOwnership x = new DeepOwnership();
deepPrivate(x.next);
}
private void deepPrivate(DeepOwnership y){
y.next = null;
}
DeepOwnership deepFromOwnedThisOk(){
return new DeepOwnership();
}
DeepOwnership arr[];
DeepOwnership(){
next.next = null;
arr[0] = null;
}
private void loseOwnershipOfNext() {
synchronized (this) {
this.next = global;
}
}
void FN_loseOwnershipInCalleeBad() {
DeepOwnership x = new DeepOwnership();
x.next = new DeepOwnership();
loseOwnershipOfNext();
x.next.next = null; // doesn't warn here
}
}

34
infer/tests/codetoanalyze/java/racerd/ShallowOwnership.java
Unescape View File

@ -1,34 +0,0 @@
/*
* Copyright (c) 2017 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
import com.facebook.infer.annotation.ThreadSafe;
@ThreadSafe
class ShallowOwnership {
ShallowOwnership next;
static ShallowOwnership global;
void globalNotOwnedBad() {
global.next = null;
}
void reassignBaseToGlobalBad(){
ShallowOwnership x = new ShallowOwnership();
x = global;
x.next = null;
}
void reassignPathToGlobalBad() {
ShallowOwnership x = new ShallowOwnership();
x.next = global;
x.next.next = null;
}
}

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

@ -48,6 +48,8 @@ codetoanalyze/java/racerd/Containers.java, void Containers.mapPutBad(String,Stri
codetoanalyze/java/racerd/Containers.java, void Containers.mapRemoveBad(String), 1, THREAD_SAFETY_VIOLATION, [Write to container `&this.codetoanalyze.java.checkers.Containers.mMap` via call to `remove`]
codetoanalyze/java/racerd/Containers.java, void Containers.mapSubclassWriteBad(HashMap,String), 1, THREAD_SAFETY_VIOLATION, [Write to container `&m` via call to `remove`]
codetoanalyze/java/racerd/Containers.java, void Containers.poolBad(), 5, THREAD_SAFETY_VIOLATION, [Write to container `&this.codetoanalyze.java.checkers.Containers.simplePool` via call to `release`]
codetoanalyze/java/racerd/DeepOwnership.java, void DeepOwnership.globalNotOwnedBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&#GB<codetoanalyze/java/racerd/DeepOwnership.java>$DeepOwnership.DeepOwnership.global.DeepOwnership.next`]
codetoanalyze/java/racerd/DeepOwnership.java, void DeepOwnership.reassignBaseToGlobalBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&x.DeepOwnership.next`]
codetoanalyze/java/racerd/Dispatch.java, void Dispatch.callUnannotatedInterfaceBad(UnannotatedInterface), 1, INTERFACE_NOT_THREAD_SAFE, [Call to un-annotated interface method void UnannotatedInterface.foo()]
codetoanalyze/java/racerd/Dispatch.java, void Dispatch.callUnannotatedInterfaceIndirectBad(NotThreadSafe,UnannotatedInterface), 1, INTERFACE_NOT_THREAD_SAFE, [call to void NotThreadSafe.notThreadSafeOk(UnannotatedInterface),Call to un-annotated interface method void UnannotatedInterface.foo()]
codetoanalyze/java/racerd/Inference.java, int Inference.read4OutsideSyncBad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField4`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField4`]
@ -97,9 +99,6 @@ codetoanalyze/java/racerd/ReadWriteRaces.java, void ReadWriteRaces.m1(), 2, THRE
codetoanalyze/java/racerd/ReadWriteRaces.java, void ReadWriteRaces.m2(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.racy`]
codetoanalyze/java/racerd/ReadWriteRaces.java, void ReadWriteRaces.m3(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.racy`]
codetoanalyze/java/racerd/ReadWriteRaces.java, void ReadWriteRaces.readInCalleeOutsideSyncBad(int), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,call to int C.get(),access to `&this.codetoanalyze.java.checkers.C.x`,<Write trace>,call to void C.set(int),access to `&this.codetoanalyze.java.checkers.C.x`]
codetoanalyze/java/racerd/ShallowOwnership.java, void ShallowOwnership.globalNotOwnedBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&#GB<codetoanalyze/java/racerd/ShallowOwnership.java>$ShallowOwnership.ShallowOwnership.global.ShallowOwnership.next`]
codetoanalyze/java/racerd/ShallowOwnership.java, void ShallowOwnership.reassignBaseToGlobalBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&x.ShallowOwnership.next`]
codetoanalyze/java/racerd/ShallowOwnership.java, void ShallowOwnership.reassignPathToGlobalBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&x.ShallowOwnership.next.ShallowOwnership.next`]
codetoanalyze/java/racerd/SubFld.java, int SubFld.getG(), 6, THREAD_SAFETY_VIOLATION, [<Read trace>,call to int SuperFld.getG(),access to `&this.SuperFld.g`,<Write trace>,access to `&this.SuperFld.g`]
codetoanalyze/java/racerd/ThreadSafeExample.java, Object ThreadSafeExample.FP_lazyInitOk(), 6, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeExample.sStaticField`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeExample.sStaticField`]
codetoanalyze/java/racerd/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ExtendsThreadSafeExample.field`]

Write Preview
Loading…
Cancel
Save