From 9e293eaa646ca9ef7cd13925b0e90504f8c3b419 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 16 Mar 2017 11:33:14 -0700 Subject: [PATCH] [thread-safety] add choice variables to support partial path-sensitivity Reviewed By: peterogithub Differential Revision: D4712228 fbshipit-source-id: 50a9188 --- infer/src/checkers/ThreadSafety.ml | 81 ++++++++++++++++++- infer/src/checkers/ThreadSafetyDomain.ml | 24 ++++++ infer/src/checkers/ThreadSafetyDomain.mli | 15 ++++ .../java/threadsafety/Locks.java | 51 ++++++++++-- .../java/threadsafety/issues.exp | 3 + 5 files changed, 164 insertions(+), 10 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 07479e3c1..5fb4c08d3 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -49,6 +49,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type lock_model = | Lock | Unlock + | LockedIfTrue | NoEffect @@ -68,7 +69,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | "java.util.concurrent.locks.ReentrantLock" | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock" | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock"), - ("lock" | "tryLock" | "lockInterruptibly") -> + ("lock" | "lockInterruptibly") -> Lock | ("java.util.concurrent.locks.Lock" |"java.util.concurrent.locks.ReentrantLock" @@ -76,6 +77,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock"), "unlock" -> Unlock + | ("java.util.concurrent.locks.Lock" + | "java.util.concurrent.locks.ReentrantLock" + | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock" + | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock"), + "tryLock" -> + LockedIfTrue | _ -> NoEffect end @@ -431,6 +438,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct { astate with locks = true; } | Unlock -> { astate with locks = false; } + | LockedIfTrue -> + begin + match ret_opt with + | Some (ret_id, ret_typ) -> + let attribute_map = + AttributeMapDomain.add_attribute + (AccessPath.of_id ret_id ret_typ) + (Choice Choice.LockHeld) + astate.attribute_map in + { astate with attribute_map; } + | None -> + failwithf + "Procedure %a specified as returning boolean, but returns nothing" + Typ.Procname.pp callee_pname + end | NoEffect -> match get_summary pdesc callee_pname actuals ~f_resolve_id loc tenv with @@ -629,6 +651,61 @@ module TransferFunctions (CFG : ProcCfg.S) = struct lhs_access_path rhs_exp rhs_typ ~f_resolve_id astate.attribute_map extras in { astate with accesses; id_map; attribute_map; } + | Sil.Prune (prune_exp, _, _, _) -> + let rec eval_binop op var e1 e2 = + match eval_bexp var e1, eval_bexp var e2 with + | Some b1, Some b2 -> Some (op b1 b2) + | _ -> None + (* return Some bool_value if the given boolean expression evaluates to bool_value when [var] + is set to true. return None if it has free variables that stop us from evaluating it *) + and eval_bexp var = function + | Exp.Var id -> + begin + match f_resolve_id (Var.of_id id) with + | Some ap when AccessPath.Raw.equal ap var -> Some true + | _ -> None + end + | (Exp.Const _) as e -> + Some (not (Exp.is_zero e)) + | Exp.UnOp (Unop.LNot, e, _) -> + let b_opt = eval_bexp var e in + Option.map ~f:not b_opt + | Exp.BinOp (Binop.LAnd, e1, e2) -> + eval_binop (&&) var e1 e2 + | Exp.BinOp (Binop.LOr, e1, e2) -> + eval_binop (||) var e1 e2 + | Exp.BinOp (Binop.Eq, e1, e2) -> + eval_binop Bool.equal var e1 e2 + | Exp.BinOp (Binop.Ne, e1, e2) -> + eval_binop (<>) var e1 e2 + | _ -> + (* non-boolean expression; can't evaluate it *) + None in + let add_choice bool_value acc = function + | Choice.LockHeld -> + let locks = bool_value in + { acc with locks; } + | Choice.OnMainThread -> + let threads = bool_value in + { acc with threads; } in + + begin + match AccessPath.of_lhs_exp prune_exp (Typ.Tint IBool) ~f_resolve_id with + | Some access_path -> + let choices = AttributeMapDomain.get_choices access_path astate.attribute_map in + begin + match eval_bexp access_path prune_exp with + | Some bool_value -> + (* prune (prune_exp) can only evaluate to true if the choice is [bool_value]. + add the constraint that the the choice must be [bool_value] to the state *) + List.fold ~f:(add_choice bool_value) ~init:astate choices + | None -> + astate + end + | _ -> + astate + end + | Sil.Remove_temps (ids, _) -> let id_map = List.fold @@ -637,7 +714,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ids in { astate with id_map; } - | _ -> + | _ -> astate end diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 34894b9b9..2fbfc434a 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -74,16 +74,29 @@ module ThreadsDomain = AbstractDomain.BooleanAnd module PathDomain = SinkTrace.Make(TraceElem) +module Choice = struct + type t = + | OnMainThread + | LockHeld + [@@deriving compare] + + let pp fmt = function + | OnMainThread -> F.fprintf fmt "OnMainThread" + | LockHeld -> F.fprintf fmt "LockHeld" +end + module Attribute = struct type t = | OwnedIf of int option | Functional + | Choice of Choice.t [@@deriving compare] let pp fmt = function | OwnedIf None -> F.fprintf fmt "Owned" | OwnedIf (Some formal_index) -> F.fprintf fmt "Owned if formal %d is owned" formal_index | Functional -> F.fprintf fmt "Functional" + | Choice choice -> Choice.pp fmt choice let unconditionally_owned = OwnedIf None @@ -117,6 +130,17 @@ module AttributeMapDomain = struct with Not_found -> None + let get_choices access_path t = + try + let attributes = find access_path t in + (List.filter_map + ~f:(function + | Attribute.Choice c -> Some c + | _ -> None) + (AttributeSetDomain.elements attributes)) + with Not_found -> + [] + let add_attribute access_path attribute t = let attribute_set = (try find access_path t diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index c3652f79e..7f56082be 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -43,12 +43,24 @@ module ThreadsDomain : AbstractDomain.S with type astate = bool module PathDomain : module type of SinkTrace.Make(TraceElem) +(** attribute attached to a boolean variable specifying what it means when the boolean is true *) +module Choice : sig + type t = + | OnMainThread (** the current procedure is running on the main thread *) + | LockHeld (** a lock is currently held *) + [@@deriving compare] + + val pp : F.formatter -> t -> unit +end + module Attribute : sig type t = | OwnedIf of int option (** owned unconditionally if OwnedIf None, owned when formal at index i is owned otherwise *) | Functional (** holds a value returned from a callee marked @Functional *) + | Choice of Choice.t + (** holds a boolean choice variable *) [@@deriving compare] (** alias for OwnedIf None *) @@ -69,6 +81,9 @@ module AttributeMapDomain : sig (** get the formal index of the the formal that must own the given access path (if any) *) val get_conditional_ownership_index : AccessPath.Raw.t -> astate -> int option + (** get the choice attributes associated with the given access path *) + val get_choices : AccessPath.Raw.t -> astate -> Choice.t list + val add_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> astate end diff --git a/infer/tests/codetoanalyze/java/threadsafety/Locks.java b/infer/tests/codetoanalyze/java/threadsafety/Locks.java index 74128472c..0d1fc7940 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Locks.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Locks.java @@ -83,13 +83,55 @@ public class Locks { } } - public void rReentrantLockTryLockOk() { + public void reentrantLockTryLockOk() { if (mReentrantLock.tryLock()) { f = 42; mReentrantLock.unlock(); } } + public void tryLockNoCheckBad() { + mReentrantLock.tryLock(); // might return false + f = 42; + } + + public void tryLockWrongBranchBad() { + if (mReentrantLock.tryLock()) { + } else { + f = 42; + } + } + + public void tryLockPropagateOk() { + boolean result = mReentrantLock.tryLock(); + boolean copy = result; + if (copy) { + f = 42; + } + } + + public void negatedReentrantLockTryLockBad() { + if (!mReentrantLock.tryLock()) { + f = 42; + } + } + + public void negatedReentrantLockTryLockOk() { + if (!mReentrantLock.tryLock()) { + + } else { + f = 42; + } + } + + // we could catch this by invalidating the choice predicates whenever we update the lock domain + public void FN_tryLockStaleBad() { + boolean result = mReentrantLock.tryLock(); + mReentrantLock.unlock(); + if (result) { + f = 42; // oops, actually not safe + } + } public void reentrantLockInterruptiblyOk() throws InterruptedException { mReentrantLock.lockInterruptibly(); @@ -139,13 +181,6 @@ public class Locks { f = 42; } - // we don't model the case where `tryLock` fails - public void FN_withReentrantLockTryLockBad() { - if (!mReentrantLock.tryLock()) { - f = 42; - } - } - // we shouldn't be able to write when holding a readLock public void FN_readLockOk() { mReentrantReadWriteLock.readLock().lock(); diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 7bd98a4dc..d689cdf4f 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -41,6 +41,9 @@ codetoanalyze/java/threadsafety/Locks.java, void Locks.afterReentrantLockUnlockB codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f] codetoanalyze/java/threadsafety/Locks.java, void Locks.afterWriteLockUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f] codetoanalyze/java/threadsafety/Locks.java, void Locks.lockInOneBranchBad(boolean), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f] +codetoanalyze/java/threadsafety/Locks.java, void Locks.negatedReentrantLockTryLockBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f] +codetoanalyze/java/threadsafety/Locks.java, void Locks.tryLockNoCheckBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f] +codetoanalyze/java/threadsafety/Locks.java, void Locks.tryLockWrongBranchBad(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f] codetoanalyze/java/threadsafety/Ownership.java, Ownership.(Obj,Object), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_ownAndConditionalOwnOk(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_twoDifferentConditionalOwnsOk(), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f]