From 700adc2d4435216c3b43811d6ed5b7fabeefa74b Mon Sep 17 00:00:00 2001 From: Peter O'Hearn Date: Thu, 7 Dec 2017 01:04:05 -0800 Subject: [PATCH] [racerd] deep ownership Reviewed By: sblackshear Differential Revision: D6424928 fbshipit-source-id: d3a1735 --- infer/src/concurrency/RacerD.ml | 13 +--- infer/src/concurrency/RacerDDomain.ml | 32 +++++++- .../java/racerd/DeepOwnership.java | 74 +++++++++++++++++++ .../java/racerd/ShallowOwnership.java | 34 --------- .../codetoanalyze/java/racerd/issues.exp | 5 +- 5 files changed, 106 insertions(+), 52 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/racerd/DeepOwnership.java delete mode 100644 infer/tests/codetoanalyze/java/racerd/ShallowOwnership.java diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index e0e70543e..a54abc04c 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -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 diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 91fe07f4f..5dce692b3 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -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 diff --git a/infer/tests/codetoanalyze/java/racerd/DeepOwnership.java b/infer/tests/codetoanalyze/java/racerd/DeepOwnership.java new file mode 100644 index 000000000..5267b5c48 --- /dev/null +++ b/infer/tests/codetoanalyze/java/racerd/DeepOwnership.java @@ -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 + } + +} diff --git a/infer/tests/codetoanalyze/java/racerd/ShallowOwnership.java b/infer/tests/codetoanalyze/java/racerd/ShallowOwnership.java deleted file mode 100644 index 4d2267f62..000000000 --- a/infer/tests/codetoanalyze/java/racerd/ShallowOwnership.java +++ /dev/null @@ -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; - } - -} diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index e3a37bbe8..aacb826a6 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -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$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, [,access to `&this.codetoanalyze.java.checkers.Inference.mField4`,,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, [,call to int C.get(),access to `&this.codetoanalyze.java.checkers.C.x`,,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$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, [,call to int SuperFld.getG(),access to `&this.SuperFld.g`,,access to `&this.SuperFld.g`] codetoanalyze/java/racerd/ThreadSafeExample.java, Object ThreadSafeExample.FP_lazyInitOk(), 6, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.ThreadSafeExample.sStaticField`,,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`]