From 584b10647de1b587440b74195c0556ae589e2038 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 5 Feb 2018 10:57:14 -0800 Subject: [PATCH] [racerd] new lock domain Summary: The boolean lock domain is simple and surprisingly effective. But it's starting to cause false positives in the case where locks are nested. Releasing the inner lock also releases the outer lock. This diff introduces a new locks domain: a map of locks (access paths) to a bounded count representing an underapproximation of the number of times the lock has been acquired. For now, we just use a single dummy access path to represent all locks (and thus a count actually would have been sufficiently expressive; we don't need the map yet). But I'm planning to remove this limitation in a follow-up by refactoring the lock models to give us an access path. Knowing the names of locks could be useful for error messages and suggesting fixes. Reviewed By: jberdine Differential Revision: D6182006 fbshipit-source-id: 6624971 --- infer/src/absint/AbstractDomain.ml | 31 +++++ infer/src/absint/AbstractDomain.mli | 23 ++++ infer/src/concurrency/RacerD.ml | 21 ++-- infer/src/concurrency/RacerDDomain.ml | 47 ++++++-- infer/src/concurrency/RacerDDomain.mli | 20 +++- .../tests/codetoanalyze/cpp/racerd/basics.cpp | 32 +++++ .../tests/codetoanalyze/cpp/racerd/issues.exp | 1 + .../codetoanalyze/java/racerd/Locks.java | 110 +++++++++++++++++- .../codetoanalyze/java/racerd/issues.exp | 7 +- 9 files changed, 262 insertions(+), 30 deletions(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index c899de0c3..fd8cd6b7b 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -298,3 +298,34 @@ module BooleanOr = struct let pp fmt astate = F.fprintf fmt "%b" astate end + +module type MaxCount = sig + val max : int +end + +module CountDomain (MaxCount : MaxCount) = struct + type astate = int + + let top = + assert (MaxCount.max > 0) ; + MaxCount.max + + + let empty = 0 + + let is_top = Int.equal top + + let is_empty = Int.equal empty + + let ( <= ) ~lhs ~rhs = lhs <= rhs + + let join astate1 astate2 = Int.min top (Int.max astate1 astate2) + + let widen ~prev ~next ~num_iters:_ = join prev next + + let increment astate = if is_top astate then top else astate + 1 + + let decrement astate = if is_empty astate then empty else astate - 1 + + let pp = Int.pp +end diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index dc4831ac0..782ab79bf 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -108,3 +108,26 @@ module BooleanAnd : S with type astate = bool (** Boolean domain ordered by ~p || q. Useful when you want a boolean that's true only when it's true in one conditional branch. *) module BooleanOr : WithBottom with type astate = bool + +module type MaxCount = sig + val max : int + (** must be positive *) +end + +(** Domain keeping a non-negative count with a bounded maximum value. The count can be only + incremented and decremented *) +module CountDomain (MaxCount : MaxCount) : sig + include WithBottom with type astate = private int + + val top : astate [@@warning "-32"] + (** maximum value *) + + val is_top : astate -> bool [@@warning "-32"] + (** return true if this is the maximum value *) + + val increment : astate -> astate + (** bump the count by one if it is less than the max *) + + val decrement : astate -> astate + (** descrease the count by one if it is greater than 0 *) +end diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 35984942a..1a6e97c69 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -365,7 +365,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct OwnershipAbstractValue.unowned in Some - { locks= false + { locks= LocksDomain.empty ; threads= ThreadsDomain.empty ; accesses= callee_accesses ; return_ownership @@ -531,7 +531,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in if AccessData.Precondition.is_true ownership_precondition' then accesses_acc else - let locks' = locks || pre.lock in + let locks' = if pre.lock then LocksDomain.add_lock locks else locks in (* if the access occurred on a main thread in the callee, we should remember this when moving it to the callee. if we don't know what thread it ran on, use the caller's thread *) @@ -604,9 +604,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in match Models.get_lock callee_pname actuals with | Lock -> - {astate with locks= true; threads= update_for_lock_use astate.threads} + { astate with + locks= LocksDomain.add_lock astate.locks + ; threads= update_for_lock_use astate.threads } | Unlock -> - {astate with locks= false; threads= update_for_lock_use astate.threads} + { astate with + locks= LocksDomain.remove_lock astate.locks + ; threads= update_for_lock_use astate.threads } | LockedIfTrue -> ( match ret_opt with | Some ret_access_path -> @@ -631,7 +635,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {summary with accesses= rebased_accesses} ) with | Some {threads; locks; accesses; return_ownership; return_attributes} -> - let locks = locks || astate.locks in + let locks = LocksDomain.join locks astate.locks in let threads = match (astate.threads, threads) with | _, ThreadsDomain.AnyThreadButSelf | AnyThreadButSelf, _ -> @@ -767,7 +771,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let add_choice bool_value (acc: Domain.astate) = function | Choice.LockHeld -> - let locks = bool_value in + let locks = + if bool_value then LocksDomain.add_lock acc.locks + else LocksDomain.remove_lock acc.locks + in {acc with locks} | Choice.OnMainThread -> let threads = @@ -916,7 +923,7 @@ let is_marked_thread_safe pdesc tenv = let empty_post : RacerDDomain.summary = { threads= RacerDDomain.ThreadsDomain.empty - ; locks= false + ; locks= RacerDDomain.LocksDomain.empty ; accesses= RacerDDomain.AccessDomain.empty ; return_ownership= RacerDDomain.OwnershipAbstractValue.unowned ; return_attributes= RacerDDomain.AttributeSetDomain.empty } diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 491798b3a..266078100 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -151,14 +151,37 @@ module TraceElem = struct make (Access.InterfaceCall pname) site end -(* In this domain true<=false. The intended denotations [[.]] are - [[true]] = the set of all states where we know according, to annotations - or assertions or lock instructions, that some lock is held. - [[false]] = the empty set - The use of && for join in this domain enforces that, to know a lock is held, one must hold in - all branches. -*) -module LocksDomain = AbstractDomain.BooleanAnd +module LockCount = AbstractDomain.CountDomain (struct + let max = 5 + + (* arbitrary threshold for max locks we expect to be held simultaneously *) +end) + +module LocksDomain = struct + include AbstractDomain.Map (AccessPath) (LockCount) + + (* TODO: eventually, we'll ask add_lock/remove_lock to pass the lock name. for now, this is a hack + to model having a single lock used everywhere *) + let the_only_lock = ((Var.of_id (Ident.create Ident.knormal 0), Typ.void_star), []) + + let is_locked astate = + (* we only add locks with positive count, so safe to just check emptiness *) + not (is_empty astate) + + + let add_lock astate = + let count = try find the_only_lock astate with Not_found -> LockCount.empty in + add the_only_lock (LockCount.increment count) astate + + + let remove_lock astate = + try + let count = find the_only_lock astate in + let count' = LockCount.decrement count in + if LockCount.is_empty count' then remove the_only_lock astate + else add the_only_lock count' astate + with Not_found -> astate +end module ThreadsDomain = struct type astate = NoThread | AnyThreadButSelf | AnyThread [@@deriving compare] @@ -379,12 +402,12 @@ module AccessData = struct type t = {thread: bool; lock: bool; ownership_precondition: Precondition.t} [@@deriving compare] - let make locks threads ownership_precondition pdesc = + let make lock threads ownership_precondition pdesc = (* shouldn't be creating metadata for accesses that are known to be owned; we should discard such accesses *) assert (not (Precondition.is_true ownership_precondition)) ; let thread = ThreadsDomain.is_any_but_self threads in - let lock = locks || Procdesc.is_java_synchronized pdesc in + let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in {thread; lock; ownership_precondition} @@ -417,7 +440,7 @@ type astate = let empty = let threads = ThreadsDomain.empty in - let locks = false in + let locks = LocksDomain.empty in let accesses = AccessDomain.empty in let ownership = OwnershipDomain.empty in let attribute_map = AttributeMapDomain.empty in @@ -425,7 +448,7 @@ let empty = let is_empty {threads; locks; accesses; ownership; attribute_map} = - ThreadsDomain.is_empty threads && not locks && AccessDomain.is_empty accesses + ThreadsDomain.is_empty threads && LocksDomain.is_empty locks && AccessDomain.is_empty accesses && OwnershipDomain.is_empty ownership && AttributeMapDomain.is_empty attribute_map diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 34a5792b4..e2503da03 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -51,12 +51,20 @@ module TraceElem : sig val make_unannotated_call_access : Typ.Procname.t -> Location.t -> t end -(** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes - the existence of one global lock. In the case that a lock is held on the access to a variable, - but the lock held is the wrong one, we will erroneously say that the access is thread-safe. - However, this coarse abstraction saves us from the complexity of tracking which locks are held - and which memory locations correspond to the same lock. *) -module LocksDomain : AbstractDomain.S with type astate = bool +(** Overapproximation of number of locks that are currently held *) +module LocksDomain : sig + include AbstractDomain.WithBottom + + val is_locked : astate -> bool + [@@warning "-32"] + (** returns true if the number of locks held is greater than zero or Top *) + + val add_lock : astate -> astate + (** record acquisition of a lock *) + + val remove_lock : astate -> astate + (** record release of a lock *) +end (** Abstraction of threads that may run in parallel with the current thread. NoThread < AnyThreadExceptSelf < AnyThread *) diff --git a/infer/tests/codetoanalyze/cpp/racerd/basics.cpp b/infer/tests/codetoanalyze/cpp/racerd/basics.cpp index b9a06b007..ba0ad7712 100644 --- a/infer/tests/codetoanalyze/cpp/racerd/basics.cpp +++ b/infer/tests/codetoanalyze/cpp/racerd/basics.cpp @@ -54,12 +54,44 @@ class Basic { int read_array_outside_lock_ok(char* arr2, int i) { return arr2[i]; } + void set_double(int new_value) { + mutex_.lock(); + mutex_2.lock(); + double_lock_guarded = new_value; + mutex_2.unlock(); + single_lock_guarded = new_value; + single_lock_suspiciously_read = new_value; + mutex_.unlock(); + } + + int test_double_lock_1_ok() { + int result; + mutex_2.lock(); + result = double_lock_guarded; + mutex_2.unlock(); + return result; + } + + int test_double_lock_2_ok() { + int result; + mutex_.lock(); + result = single_lock_guarded; + mutex_.unlock(); + return result; + } + + int test_double_lock_bad() { return single_lock_suspiciously_read; } + private: int well_guarded; int suspiciously_read; int suspiciously_written; int not_guarded; + int double_lock_guarded; + int single_lock_guarded; + int single_lock_suspiciously_read; std::mutex mutex_; + std::mutex mutex_2; int get_private_suspiciously_read() { return suspiciously_read; } }; diff --git a/infer/tests/codetoanalyze/cpp/racerd/issues.exp b/infer/tests/codetoanalyze/cpp/racerd/issues.exp index e100a0b49..917e160c3 100644 --- a/infer/tests/codetoanalyze/cpp/racerd/issues.exp +++ b/infer/tests/codetoanalyze/cpp/racerd/issues.exp @@ -1,6 +1,7 @@ codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get2, 3, LOCK_CONSISTENCY_VIOLATION, [,access to `&this.suspiciously_written`,,access to `&this.suspiciously_written`] codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get4, 0, LOCK_CONSISTENCY_VIOLATION, [,access to `&this.suspiciously_read`,,access to `&this.suspiciously_read`] codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get5, 0, LOCK_CONSISTENCY_VIOLATION, [,call to basics::Basic_get_private_suspiciously_read,access to `&this.suspiciously_read`,,access to `&this.suspiciously_read`] +codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_test_double_lock_bad, 0, LOCK_CONSISTENCY_VIOLATION, [,access to `&this.single_lock_suspiciously_read`,,access to `&this.single_lock_suspiciously_read`] codetoanalyze/cpp/racerd/constructor_ownership.cpp, constructors::TSL_not_locked_race, 0, LOCK_CONSISTENCY_VIOLATION, [,call to constructors::BSS_toJson_race,call to constructors::dynamic_operator=,access to `&this.type_`,,call to constructors::BSS_toJson_race,call to constructors::dynamic_operator=,access to `&this.type_`] codetoanalyze/cpp/racerd/locals_ownership.cpp, locals::Ownership_test2_bad, 5, LOCK_CONSISTENCY_VIOLATION, [,access to `&x.f`,,access to `&x.f`] codetoanalyze/cpp/racerd/locals_ownership.cpp, locals::Ownership_test3_bad, 5, LOCK_CONSISTENCY_VIOLATION, [,access to `&x.f`,,access to `&x.f`] diff --git a/infer/tests/codetoanalyze/java/racerd/Locks.java b/infer/tests/codetoanalyze/java/racerd/Locks.java index 30d480612..eebcbf717 100644 --- a/infer/tests/codetoanalyze/java/racerd/Locks.java +++ b/infer/tests/codetoanalyze/java/racerd/Locks.java @@ -25,7 +25,8 @@ public class Locks { ReentrantLock mReentrantLock; ReentrantReadWriteLock mReentrantReadWriteLock; - public void lockInOneBranchBad(boolean b) { + // we allow this for now + public void FN_lockInOneBranchBad(boolean b) { if (b) { mLock.lock(); } @@ -164,8 +165,111 @@ public class Locks { mLock.unlock(); } - // our "squish all locks into one" abstraction is not ideal here... - public void FP_unlockOneLock() { + void nested1Ok() { + synchronized (this) { + synchronized (this) { + } + // a bad abstraction of locks will treat this as unlocked... + f = 32; + } + } + + void nested2Ok() { + synchronized (this) { + synchronized (this) { + f = 32; + } + } + } + + void nested3Ok() { + synchronized (this) { + f = 32; + synchronized (this) { + } + } + } + + void nested1Bad() { + synchronized (this) { + synchronized (this) { + } + } + f = 32; + } + + void nested2Bad() { + synchronized (this) { + } + f = 32; + synchronized (this) { + } + } + + void nested3Bad() { + synchronized (this) { + } + synchronized (this) { + } + f = 32; + } + + + void useLock() { + synchronized (this) { + } + } + + void useLockInCalleeBad() { + useLock(); + f = 32; + } + + void lockInLoopOk(int i) { + while (i > 0) { + i++; + mLock.lock(); + } + f = 32; + } + + void unlockInLoopOk(int i) { + mLock.lock(); + while (i > 0) { + i++; + mLock.unlock(); + } + f = 32; + } + + void lockInLoopLexicalBad(int i) { + while (i > 0) { + i++; + synchronized(this) { + } + } + f = 32; + } + + void lockInLoopLexicalOk(int i) { + while (i > 0) { + i++; + synchronized(this) { + f = 32; + } + } + } + + void loopInLockLexicalBad(int i) { + synchronized(this) { + while (i > 0) { + i++; + } + f = 32; + } + } + + public void unlockOneLockOk() { mLock.lock(); mReentrantLock.lock(); mReentrantLock.unlock(); diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index 2eccaef79..7057ce8a6 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -56,14 +56,17 @@ codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead2Bad(), 1 codetoanalyze/java/racerd/Locks.java, Object Locks.unownedReadBad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Locks.mField3`,,call to void Locks.lockedWriteInCallee2(),access to `&this.codetoanalyze.java.checkers.Locks.mField3`] codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock1Bad(), 3, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Locks.mField`,,access to `&this.codetoanalyze.java.checkers.Locks.mField`] codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock2Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Locks.mField`,,access to `&this.codetoanalyze.java.checkers.Locks.mField`] -codetoanalyze/java/racerd/Locks.java, void Locks.FP_unlockOneLock(), 4, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/racerd/Locks.java, void Locks.afterReentrantLockUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/racerd/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/racerd/Locks.java, void Locks.afterWriteLockUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] -codetoanalyze/java/racerd/Locks.java, void Locks.lockInOneBranchBad(boolean), 4, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] +codetoanalyze/java/racerd/Locks.java, void Locks.lockInLoopLexicalBad(int), 6, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/racerd/Locks.java, void Locks.negatedReentrantLockTryLockBad(), 2, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] +codetoanalyze/java/racerd/Locks.java, void Locks.nested1Bad(), 5, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] +codetoanalyze/java/racerd/Locks.java, void Locks.nested2Bad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] +codetoanalyze/java/racerd/Locks.java, void Locks.nested3Bad(), 5, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/racerd/Locks.java, void Locks.tryLockNoCheckBad(), 2, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/racerd/Locks.java, void Locks.tryLockWrongBranchBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] +codetoanalyze/java/racerd/Locks.java, void Locks.useLockInCalleeBad(), 2, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/racerd/Ownership.java, Ownership.(Obj,Object), 1, THREAD_SAFETY_VIOLATION, [access to `&obj.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, int Ownership.readGlobalBad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&#GB<>$codetoanalyze.java.checkers.Ownership.codetoanalyze.java.checkers.Ownership.global`,,access to `&#GB<>$codetoanalyze.java.checkers.Ownership.codetoanalyze.java.checkers.Ownership.global`] codetoanalyze/java/racerd/Ownership.java, void Ownership.cantOwnThisBad(), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.setField(Obj),access to `&this.codetoanalyze.java.checkers.Ownership.field`]