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