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`]