From 45ada8703e3628d47cbfa76aa13ad2525d6e47df Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 16 Jan 2020 06:14:42 -0800 Subject: [PATCH] [starvation] allow aliasing of parameters across threads Summary: Introduce a new notion of equality for comparing abstract addresses in distinct threads: ``` (** Abstract address for a lock. There are two notions of equality: - Equality for comparing two addresses within the same thread/process/trace. Under this, identical globals and identical class objects compare equal. Locks represented by access paths rooted at method parameters must have equal access paths to compare equal. Paths rooted at locals are ignored. - Equality for comparing two addresses in two distinct threads/traces. Globals and class objects are compared in the same way, but locks represented by access paths rooted at parameters need only have equal access lists (ie [x.f.g == y.f.g]). This allows demonically aliasing parameters in *distinct* threads. This relation is used in [may_deadlock]. *) ``` Reviewed By: skcho Differential Revision: D19347307 fbshipit-source-id: 9f338731b --- infer/src/concurrency/starvation.ml | 5 ++- infer/src/concurrency/starvationDomain.ml | 27 ++++++++++-- infer/src/concurrency/starvationDomain.mli | 15 ++++++- .../java/starvation-dedup/Interproc.java | 10 ++--- .../java/starvation-dedup/Intraproc.java | 2 +- .../java/starvation-dedup/issues.exp | 2 + .../java/starvation/Interproc.java | 2 +- .../java/starvation/Intraproc.java | 2 +- .../java/starvation/Parameters.java | 44 +++++++++++++++++++ .../codetoanalyze/java/starvation/issues.exp | 5 +++ 10 files changed, 98 insertions(+), 16 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/starvation/Parameters.java diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 9ae8bc7e8..348dc249c 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -631,7 +631,8 @@ let report_on_parallel_composition ~should_report_starvation tenv pdesc pair loc let acquisitions = other_pair.CriticalPair.elem.acquisitions in match other_pair.CriticalPair.elem.event with | MayBlock (block_descr, sev) - when should_report_starvation && Acquisitions.lock_is_held lock acquisitions -> + when should_report_starvation && Acquisitions.lock_is_held_in_other_thread lock acquisitions + -> let error_message = Format.asprintf "Method %a runs on UI thread and%a, which may be held by another thread which %s." @@ -641,7 +642,7 @@ let report_on_parallel_composition ~should_report_starvation tenv pdesc pair loc ReportMap.add_starvation sev tenv pdesc loc ltr error_message report_map | MonitorWait monitor_lock when should_report_starvation - && Acquisitions.lock_is_held lock acquisitions + && Acquisitions.lock_is_held_in_other_thread lock acquisitions && not (Lock.equal lock monitor_lock) -> let error_message = Format.asprintf diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 832ade9a2..5d38d4253 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -104,6 +104,18 @@ module Lock = struct type t = {root: root; path: path} [@@deriving compare, equal] + let equal_across_threads t1 t2 = + match (t1.root, t2.root) with + | Global _, Global _ | Class _, Class _ -> + (* globals and class objects must be identical across threads *) + equal t1 t2 + | Parameter _, Parameter _ -> + (* parameter position/names can be ignored across threads, if types and accesses are equal *) + equal_path t1.path t2.path + | _, _ -> + false + + (* using an indentifier for a class object, create an access path representing that lock; this is for synchronizing on Java class objects only *) let path_of_java_class = @@ -253,6 +265,13 @@ module Acquisitions = struct (* use the fact that location/procname are ignored in comparisons *) let lock_is_held lock acquisitions = mem (Acquisition.make_dummy lock) acquisitions + + let lock_is_held_in_other_thread lock acquisitions = + exists (fun acq -> Lock.equal_across_threads lock acq.lock) acquisitions + + + let no_locks_common_across_threads acqs1 acqs2 = + for_all (fun acq1 -> not (lock_is_held_in_other_thread acq1.lock acqs2)) acqs1 end module LockState : sig @@ -384,10 +403,10 @@ module CriticalPair = struct ThreadDomain.can_run_in_parallel pair1.thread pair2.thread && Option.both (get_final_acquire t1) (get_final_acquire t2) |> Option.exists ~f:(fun (lock1, lock2) -> - (not (Lock.equal lock1 lock2)) - && Acquisitions.lock_is_held lock2 pair1.acquisitions - && Acquisitions.lock_is_held lock1 pair2.acquisitions - && Acquisitions.inter pair1.acquisitions pair2.acquisitions |> Acquisitions.is_empty + (not (Lock.equal_across_threads lock1 lock2)) + && Acquisitions.lock_is_held_in_other_thread lock2 pair1.acquisitions + && Acquisitions.lock_is_held_in_other_thread lock1 pair2.acquisitions + && Acquisitions.no_locks_common_across_threads pair1.acquisitions pair2.acquisitions ) diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 43ede3fb6..d50a506bf 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -23,8 +23,16 @@ module ThreadDomain : sig include AbstractDomain.WithBottom with type t := t end -(** Abstraction of a path that represents a lock, special-casing comparison to work over type, base - variable modulo this and access list *) +(** Abstract address for a lock. There are two notions of equality: + + - Equality for comparing two addresses within the same thread/process/trace. Under this, + identical globals and identical class objects compare equal. Locks represented by access paths + rooted at method parameters must have equal access paths to compare equal. Paths rooted at + locals are ignored. + - Equality for comparing two addresses in two distinct threads/traces. Globals and class objects + are compared in the same way, but locks represented by access paths rooted at parameters need + only have equal access lists (ie [x.f.g == y.f.g]). This allows demonically aliasing + parameters in *distinct* threads. This relation is used in [may_deadlock]. *) module Lock : sig include PrettyPrintable.PrintableOrderedType @@ -73,6 +81,9 @@ module Acquisitions : sig val lock_is_held : Lock.t -> t -> bool (** is the given lock in the set *) + + val lock_is_held_in_other_thread : Lock.t -> t -> bool + (** is the given lock held, modulo memory abstraction across threads *) end (** An event and the currently-held locks at the time it occurred. *) diff --git a/infer/tests/codetoanalyze/java/starvation-dedup/Interproc.java b/infer/tests/codetoanalyze/java/starvation-dedup/Interproc.java index fbb81fc8e..dc2291bd3 100644 --- a/infer/tests/codetoanalyze/java/starvation-dedup/Interproc.java +++ b/infer/tests/codetoanalyze/java/starvation-dedup/Interproc.java @@ -7,10 +7,10 @@ class Interproc { synchronized void interproc1Bad(InterprocA a) { - interproc2Bad(a); + interproc2(a); } - void interproc2Bad(InterprocA b) { + void interproc2(InterprocA b) { synchronized (b) { } } @@ -36,11 +36,11 @@ class Interproc { } class InterprocA { - synchronized void FN_interproc1Bad(Interproc c) { - interproc2Bad(c); + synchronized void interproc1Bad(Interproc c) { + interproc2(c); } - void interproc2Bad(Interproc d) { + void interproc2(Interproc d) { synchronized (d) { } } diff --git a/infer/tests/codetoanalyze/java/starvation-dedup/Intraproc.java b/infer/tests/codetoanalyze/java/starvation-dedup/Intraproc.java index b09d8959a..fb7a5e9c7 100644 --- a/infer/tests/codetoanalyze/java/starvation-dedup/Intraproc.java +++ b/infer/tests/codetoanalyze/java/starvation-dedup/Intraproc.java @@ -31,7 +31,7 @@ class Intraproc { } class IntraprocA { - void FN_intraBad(Intraproc o) { + void intraBad(Intraproc o) { synchronized (this) { synchronized (o) { } diff --git a/infer/tests/codetoanalyze/java/starvation-dedup/issues.exp b/infer/tests/codetoanalyze/java/starvation-dedup/issues.exp index 1fc32e6fe..dc6cdf5cd 100644 --- a/infer/tests/codetoanalyze/java/starvation-dedup/issues.exp +++ b/infer/tests/codetoanalyze/java/starvation-dedup/issues.exp @@ -3,3 +3,5 @@ codetoanalyze/java/starvation-dedup/Dedup.java, Dedup.callMethodWithMultipleBloc codetoanalyze/java/starvation-dedup/Dedup.java, Dedup.callMethodWithMultipleBlocksBad():void, 28, STARVATION, no_bucket, ERROR, [`void Dedup.callMethodWithMultipleBlocksBad()`,calls `Object Future.get()`] codetoanalyze/java/starvation-dedup/Dedup.java, Dedup.onUiThreadBad():void, 20, STARVATION, no_bucket, ERROR, [`void Dedup.onUiThreadBad()`,Method call: `void Dedup.callMethodWithMultipleBlocksBad()`,calls `void CountDownLatch.await()`] codetoanalyze/java/starvation-dedup/Dedup.java, Dedup.oneWayBad():void, 35, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Dedup.oneWayBad()`, locks `this.lockA` in `class Dedup`, locks `this.lockB` in `class Dedup`,[Trace 2] `void Dedup.anotherWayBad()`, locks `this.lockB` in `class Dedup`, locks `this.lockA` in `class Dedup`] +codetoanalyze/java/starvation-dedup/Interproc.java, Interproc.interproc1Bad(InterprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interproc.interproc1Bad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.interproc2(InterprocA)`, locks `b` in `class InterprocA`,[Trace 2] `void InterprocA.interproc1Bad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.interproc2(Interproc)`, locks `d` in `class Interproc`] +codetoanalyze/java/starvation-dedup/Intraproc.java, Intraproc.intraBad(IntraprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Intraproc.intraBad(IntraprocA)`, locks `this` in `class Intraproc`, locks `o` in `class IntraprocA`,[Trace 2] `void IntraprocA.intraBad(Intraproc)`, locks `this` in `class IntraprocA`, locks `o` in `class Intraproc`] diff --git a/infer/tests/codetoanalyze/java/starvation/Interproc.java b/infer/tests/codetoanalyze/java/starvation/Interproc.java index fbb81fc8e..7aa2ba0a7 100644 --- a/infer/tests/codetoanalyze/java/starvation/Interproc.java +++ b/infer/tests/codetoanalyze/java/starvation/Interproc.java @@ -36,7 +36,7 @@ class Interproc { } class InterprocA { - synchronized void FN_interproc1Bad(Interproc c) { + synchronized void interproc1Bad(Interproc c) { interproc2Bad(c); } diff --git a/infer/tests/codetoanalyze/java/starvation/Intraproc.java b/infer/tests/codetoanalyze/java/starvation/Intraproc.java index b09d8959a..fb7a5e9c7 100644 --- a/infer/tests/codetoanalyze/java/starvation/Intraproc.java +++ b/infer/tests/codetoanalyze/java/starvation/Intraproc.java @@ -31,7 +31,7 @@ class Intraproc { } class IntraprocA { - void FN_intraBad(Intraproc o) { + void intraBad(Intraproc o) { synchronized (this) { synchronized (o) { } diff --git a/infer/tests/codetoanalyze/java/starvation/Parameters.java b/infer/tests/codetoanalyze/java/starvation/Parameters.java new file mode 100644 index 000000000..d964fd936 --- /dev/null +++ b/infer/tests/codetoanalyze/java/starvation/Parameters.java @@ -0,0 +1,44 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +class Parameters { + private static void syncOnParam(Object x) { + synchronized (x) { + } + } + + // Next two methods will deadlock + public synchronized void oneWaySyncOnParamBad(Object x) { + syncOnParam(x); + } + + public void otherWaySyncOnParamBad(Object x) { + synchronized (x) { + synchronized (this) { + } + } + } + + private static void emulateSynchronized(Parameters self) { + synchronized (self) { + } + } + + Parameters someObject; + + // Next two methods will deadlock + public synchronized void FN_oneWayEmulateSyncBad() { + emulateSynchronized(someObject); + } + + public void FN_anotherWayEmulateSyncBad() { + synchronized (someObject) { + synchronized (this) { + } + } + } +} diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp index aaf3b4b3f..6ee93aa6b 100644 --- a/infer/tests/codetoanalyze/java/starvation/issues.exp +++ b/infer/tests/codetoanalyze/java/starvation/issues.exp @@ -19,6 +19,10 @@ codetoanalyze/java/starvation/InnerClass.java, InnerClass.outerInnerBad(InnerCla codetoanalyze/java/starvation/InnerClass.java, InnerClass.outerInnerBad(InnerClass$InnerClassA):void, 16, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InnerClass.outerInnerBad(InnerClass$InnerClassA)`, locks `this` in `class InnerClass`,Method call: `void InnerClass$InnerClassA.baz()`, locks `this` in `class InnerClass$InnerClassA`,[Trace 2] `void InnerClass$InnerClassA.innerOuterBad()`, locks `this` in `class InnerClass$InnerClassA`,Method call: `void InnerClass.bar()`, locks `this` in `class InnerClass`] codetoanalyze/java/starvation/Interclass.java, Interclass.interclass1Bad(InterclassA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interclass.interclass1Bad(InterclassA)`, locks `this` in `class Interclass`,Method call: `void InterclassA.interclass1Bad()`, locks `this` in `class InterclassA`,[Trace 2] `void InterclassA.interclass2Bad(Interclass)`, locks `this` in `class InterclassA`,Method call: `void Interclass.interclass2Bad()`, locks `this` in `class Interclass`] codetoanalyze/java/starvation/Interclass.java, InterclassA.interclass2Bad(Interclass):void, 37, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InterclassA.interclass2Bad(Interclass)`, locks `this` in `class InterclassA`,Method call: `void Interclass.interclass2Bad()`, locks `this` in `class Interclass`,[Trace 2] `void Interclass.interclass1Bad(InterclassA)`, locks `this` in `class Interclass`,Method call: `void InterclassA.interclass1Bad()`, locks `this` in `class InterclassA`] +codetoanalyze/java/starvation/Interproc.java, Interproc.interproc1Bad(InterprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interproc.interproc1Bad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.interproc2Bad(InterprocA)`, locks `b` in `class InterprocA`,[Trace 2] `void InterprocA.interproc1Bad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.interproc2Bad(Interproc)`, locks `d` in `class Interproc`] +codetoanalyze/java/starvation/Interproc.java, InterprocA.interproc1Bad(Interproc):void, 40, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InterprocA.interproc1Bad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.interproc2Bad(Interproc)`, locks `d` in `class Interproc`,[Trace 2] `void Interproc.interproc1Bad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.interproc2Bad(InterprocA)`, locks `b` in `class InterprocA`] +codetoanalyze/java/starvation/Intraproc.java, Intraproc.intraBad(IntraprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Intraproc.intraBad(IntraprocA)`, locks `this` in `class Intraproc`, locks `o` in `class IntraprocA`,[Trace 2] `void IntraprocA.intraBad(Intraproc)`, locks `this` in `class IntraprocA`, locks `o` in `class Intraproc`] +codetoanalyze/java/starvation/Intraproc.java, IntraprocA.intraBad(Intraproc):void, 35, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void IntraprocA.intraBad(Intraproc)`, locks `this` in `class IntraprocA`, locks `o` in `class Intraproc`,[Trace 2] `void Intraproc.intraBad(IntraprocA)`, locks `this` in `class Intraproc`, locks `o` in `class IntraprocA`] codetoanalyze/java/starvation/LegacySync.java, LegacySync.onUiThreadOpBad():java.lang.Object, 25, STARVATION, no_bucket, ERROR, [[Trace 1] `Object LegacySync.onUiThreadOpBad()`, locks `this.table` in `class LegacySync`,[Trace 2] `void LegacySync.notOnUiThreadSyncedBad()`, locks `this.table` in `class LegacySync`,calls `Object Future.get()`] codetoanalyze/java/starvation/LockSensitivity.java, LockSensitivity.FP_assertHoldsLockAB_Ok():void, 41, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void LockSensitivity.FP_assertHoldsLockAB_Ok()`, locks `this.monitorA` in `class LockSensitivity`, locks `this.monitorB` in `class LockSensitivity`,[Trace 2] `void LockSensitivity.FP_assertHoldsLockBA_Ok()`, locks `this.monitorB` in `class LockSensitivity`, locks `this.monitorA` in `class LockSensitivity`] codetoanalyze/java/starvation/LockSensitivity.java, LockSensitivity.FP_assertHoldsLockBA_Ok():void, 46, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void LockSensitivity.FP_assertHoldsLockBA_Ok()`, locks `this.monitorB` in `class LockSensitivity`, locks `this.monitorA` in `class LockSensitivity`,[Trace 2] `void LockSensitivity.FP_assertHoldsLockAB_Ok()`, locks `this.monitorA` in `class LockSensitivity`, locks `this.monitorB` in `class LockSensitivity`] @@ -42,6 +46,7 @@ codetoanalyze/java/starvation/ObjWait.java, ObjWait.indirectWaitOnMainWithoutTim codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout1Bad():void, 31, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout1Bad()`,calls `wait` on `this.o` in `class ObjWait`] codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout2Bad():void, 38, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout2Bad()`,calls `wait` on `this.o` in `class ObjWait`] codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithoutTimeoutBad():void, 24, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithoutTimeoutBad()`,calls `wait` on `this.o` in `class ObjWait`] +codetoanalyze/java/starvation/Parameters.java, Parameters.otherWaySyncOnParamBad(java.lang.Object):void, 20, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Parameters.otherWaySyncOnParamBad(Object)`, locks `x` in `class java.lang.Object`, locks `this` in `class Parameters`,[Trace 2] `void Parameters.oneWaySyncOnParamBad(Object)`, locks `this` in `class Parameters`,Method call: `void Parameters.syncOnParam(Object)`, locks `x` in `class java.lang.Object`] codetoanalyze/java/starvation/PubPriv.java, PubPriv.alsoBad():void, 25, STARVATION, no_bucket, ERROR, [`void PubPriv.alsoBad()`,Method call: `void PubPriv.transactBad()`,Method call: `void PubPriv.doTransactOk()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`] codetoanalyze/java/starvation/PubPriv.java, PubPriv.callAnotherWayBad():void, 53, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void PubPriv.callAnotherWayBad()`,Method call: `void PubPriv.anotherWayOk()`, locks `this.lockB` in `class PubPriv`, locks `this.lockA` in `class PubPriv`,[Trace 2] `void PubPriv.callOneWayBad()`,Method call: `void PubPriv.oneWayOk()`, locks `this.lockA` in `class PubPriv`, locks `this.lockB` in `class PubPriv`] codetoanalyze/java/starvation/PubPriv.java, PubPriv.callOneWayBad():void, 49, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void PubPriv.callOneWayBad()`,Method call: `void PubPriv.oneWayOk()`, locks `this.lockA` in `class PubPriv`, locks `this.lockB` in `class PubPriv`,[Trace 2] `void PubPriv.callAnotherWayBad()`,Method call: `void PubPriv.anotherWayOk()`, locks `this.lockB` in `class PubPriv`, locks `this.lockA` in `class PubPriv`]