From d154415cd0c455358dda65171ebce999ed0f12fe Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 31 Oct 2019 04:39:16 -0700 Subject: [PATCH] [starvation] add path sensitivity restricted to thread status Summary: Steal a page from RacerD (and improve interface of) on using certain calls to assert execution on a particular thread. Reduces FPs and FNs too. Reviewed By: dulmarod Differential Revision: D18199843 fbshipit-source-id: 5bdff0dfe --- infer/src/IR/HilExp.ml | 28 +++++++++++ infer/src/IR/HilExp.mli | 5 ++ infer/src/concurrency/ConcurrencyModels.ml | 11 +++-- infer/src/concurrency/ConcurrencyModels.mli | 5 +- infer/src/concurrency/RacerD.ml | 36 +------------- infer/src/concurrency/StarvationModels.ml | 4 -- infer/src/concurrency/StarvationModels.mli | 3 -- infer/src/concurrency/starvation.ml | 47 +++++++++++++++---- infer/src/concurrency/starvationDomain.ml | 40 ++++++++++++++-- infer/src/concurrency/starvationDomain.mli | 18 +++++++ .../java/starvation/ThreadSensitivity.java | 4 +- .../codetoanalyze/java/starvation/issues.exp | 2 - 12 files changed, 139 insertions(+), 64 deletions(-) diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index 95f34d055..38f4caeda 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -643,6 +643,34 @@ and eval = function None +let rec eval_boolean_binop op var e1 e2 = + Option.both (eval_boolean_exp var e1) (eval_boolean_exp var e2) + |> Option.map ~f:(fun (b1, b2) -> op b1 b2) + + +(** 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_boolean_exp var = function + | AccessExpression access_expr when AccessExpression.equal access_expr var -> + Some true + | Constant c -> + Some (not (Const.iszero_int_float c)) + | UnaryOperator (Unop.LNot, e, _) -> + eval_boolean_exp var e |> Option.map ~f:not + | BinaryOperator (Binop.LAnd, e1, e2) -> + eval_boolean_binop ( && ) var e1 e2 + | BinaryOperator (Binop.LOr, e1, e2) -> + eval_boolean_binop ( || ) var e1 e2 + | BinaryOperator (Binop.Eq, e1, e2) -> + eval_boolean_binop Bool.equal var e1 e2 + | BinaryOperator (Binop.Ne, e1, e2) -> + eval_boolean_binop ( <> ) var e1 e2 + | _ -> + (* non-boolean expression; can't evaluate it *) + None + + let rec ignore_cast e = match e with Cast (_, e) -> ignore_cast e | _ -> e let access_expr_of_exp ~include_array_indexes ~f_resolve_id exp typ = diff --git a/infer/src/IR/HilExp.mli b/infer/src/IR/HilExp.mli index cbe8be4f6..fddca643e 100644 --- a/infer/src/IR/HilExp.mli +++ b/infer/src/IR/HilExp.mli @@ -123,6 +123,11 @@ val is_int_zero : t -> bool val eval : t -> Const.t option +val eval_boolean_exp : AccessExpression.t -> t -> bool option +(** [eval_boolean_exp var exp] returns [Some bool_value] if the given boolean expression [exp] + evaluates to [bool_value] when [var] is set to true. Return None if it has free variables + that stop us from evaluating it, or is not a boolean expression. *) + val ignore_cast : t -> t val access_expr_of_exp : diff --git a/infer/src/concurrency/ConcurrencyModels.ml b/infer/src/concurrency/ConcurrencyModels.ml index 021b208b0..92f71c3de 100644 --- a/infer/src/concurrency/ConcurrencyModels.ml +++ b/infer/src/concurrency/ConcurrencyModels.ml @@ -34,14 +34,17 @@ let is_thread_utils_method method_name_str = function false -let get_thread = function +let get_thread_assert_effect = function | Typ.Procname.Java java_pname when is_thread_utils_type java_pname -> ( match Typ.Procname.Java.get_method java_pname with - | "assertMainThread" | "assertOnUiThread" | "checkOnMainThread" -> + | "assertMainThread" | "assertOnUiThread" | "checkOnMainThread" | "checkIsOnMainThread" -> MainThread - | "isMainThread" | "isUiThread" -> + | "isMainThread" | "isOnMainThread" | "isUiThread" -> MainThreadIfTrue - | "assertOnBackgroundThread" | "assertOnNonUiThread" | "checkOnNonUiThread" -> + | "assertOnBackgroundThread" + | "assertOnNonUiThread" + | "checkOnNonUiThread" + | "checkOnWorkerThread" -> BackgroundThread | _ -> UnknownThread ) diff --git a/infer/src/concurrency/ConcurrencyModels.mli b/infer/src/concurrency/ConcurrencyModels.mli index 8b02fafa9..da8c96cbf 100644 --- a/infer/src/concurrency/ConcurrencyModels.mli +++ b/infer/src/concurrency/ConcurrencyModels.mli @@ -29,8 +29,9 @@ val is_thread_utils_method : string -> Typ.Procname.t -> bool val get_lock_effect : Typ.Procname.t -> HilExp.t list -> lock_effect (** describe how this procedure behaves with respect to locking *) -val get_thread : Typ.Procname.t -> thread -(** describe how this procedure behaves with respect to thread access *) +val get_thread_assert_effect : Typ.Procname.t -> thread +(** In Java, certain methods can be used to assert execution on a specific kind of thread, + or return a boolean equivalent to such a fact. *) val get_current_class_and_annotated_superclasses : (Annot.Item.t -> bool) -> Tenv.t -> Typ.Procname.t -> (Typ.name * Typ.name list) option diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index fcc082a5e..3cc99677e 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -273,7 +273,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else astate in let astate = - match get_thread callee_pname with + match get_thread_assert_effect callee_pname with | BackgroundThread -> {astate with threads= ThreadsDomain.AnyThread} | MainThread -> @@ -405,38 +405,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with accesses; ownership; attribute_map} - 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 - | HilExp.AccessExpression access_expr -> - if AccessExpression.equal access_expr var then Some true else None - | HilExp.Constant c -> - Some (not (Const.iszero_int_float c)) - | HilExp.UnaryOperator (Unop.LNot, e, _) -> - let b_opt = eval_bexp var e in - Option.map ~f:not b_opt - | HilExp.BinaryOperator (Binop.LAnd, e1, e2) -> - eval_binop ( && ) var e1 e2 - | HilExp.BinaryOperator (Binop.LOr, e1, e2) -> - eval_binop ( || ) var e1 e2 - | HilExp.BinaryOperator (Binop.Eq, e1, e2) -> - eval_binop Bool.equal var e1 e2 - | HilExp.BinaryOperator (Binop.Ne, e1, e2) -> - eval_binop ( <> ) var e1 e2 - | _ -> - (* non-boolean expression; can't evaluate it *) - None - - let do_assume assume_exp loc proc_data (astate : Domain.t) = let open Domain in let add_choice bool_value (acc : Domain.t) = function @@ -459,7 +427,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let astate' = match HilExp.get_access_exprs assume_exp with | [access_expr] -> - eval_bexp access_expr assume_exp + HilExp.eval_boolean_exp access_expr assume_exp |> Option.fold ~init:astate ~f:(fun init bool_value -> let choices = AttributeMapDomain.get_choices access_expr astate.attribute_map in (* prune (prune_exp) can only evaluate to true if the choice is [bool_value]. diff --git a/infer/src/concurrency/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml index 396aff8ab..a967f3fba 100644 --- a/infer/src/concurrency/StarvationModels.ml +++ b/infer/src/concurrency/StarvationModels.ml @@ -192,10 +192,6 @@ let is_strict_mode_violation tenv pn actuals = Config.starvation_strict_mode && strict_mode_matcher tenv pn actuals -let is_ui_thread_model pn = - ConcurrencyModels.(match get_thread pn with MainThread -> true | _ -> false) - - let is_annotated_nonblocking ~attrs_of_pname tenv pname = ConcurrencyModels.find_override_or_superclass_annotated ~attrs_of_pname Annotations.ia_is_nonblocking tenv pname diff --git a/infer/src/concurrency/StarvationModels.mli b/infer/src/concurrency/StarvationModels.mli index e92e62a0a..dc7eed7bb 100644 --- a/infer/src/concurrency/StarvationModels.mli +++ b/infer/src/concurrency/StarvationModels.mli @@ -24,9 +24,6 @@ val is_synchronized_library_call : Tenv.t -> Typ.Procname.t -> bool val should_skip_analysis : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool (** should we treat a method call as skip (eg library methods in guava) to avoid FPs? *) -val is_ui_thread_model : Typ.Procname.t -> bool -(** is procedure an assertion we are on the UI thread or equivalent *) - val is_annotated_nonblocking : attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option) -> Tenv.t -> Typ.Procname.t -> bool (** is procedure transitively annotated [@Nonblocking] *) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 9bdb8c755..3fdfc0ac6 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -70,12 +70,42 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Payload.read ~caller_summary:summary ~callee_pname:callee |> Option.fold ~init:astate ~f:(Domain.integrate_summary tenv callsite) in + let do_assume assume_exp (astate : Domain.t) = + let open Domain in + let add_choice (acc : Domain.t) bool_value = + let thread = if bool_value then ThreadDomain.UIThread else ThreadDomain.AnyThread in + {acc with thread} + in + match HilExp.get_access_exprs assume_exp with + | [access_expr] when BranchGuardDomain.is_thread_guard access_expr astate.branch_guards -> + HilExp.eval_boolean_exp access_expr assume_exp |> Option.fold ~init:astate ~f:add_choice + | _ -> + astate + in + let do_thread_assert_effect ret_base callee (astate : Domain.t) = + let open Domain in + match ConcurrencyModels.get_thread_assert_effect callee with + | BackgroundThread -> + {astate with thread= ThreadDomain.AnyThread} + | MainThread -> + {astate with thread= ThreadDomain.UIThread} + | MainThreadIfTrue -> + let ret_access_exp = HilExp.AccessExpression.base ret_base in + let branch_guards = + BranchGuardDomain.add ret_access_exp BranchGuard.Thread astate.branch_guards + in + {astate with branch_guards} + | UnknownThread -> + astate + in match instr with - | Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | Metadata _ -> + | Assign _ | Call (_, Indirect _, _, _, _) | Metadata _ -> astate | Call (_, Direct callee, actuals, _, _) when should_skip_analysis tenv callee actuals -> astate - | Call (_, Direct callee, actuals, _, loc) -> ( + | Assume (assume_exp, _, _, _) -> + do_assume assume_exp astate + | Call (ret_base, Direct callee, actuals, _, loc) -> ( match get_lock_effect callee actuals with | Lock locks -> do_lock locks loc astate @@ -100,16 +130,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* model a synchronized call without visible internal behaviour *) let locks = List.hd actuals |> Option.to_list in do_lock locks loc astate |> do_unlock locks - | NoEffect when is_java && is_ui_thread_model callee -> - Domain.set_on_ui_thread astate | NoEffect when is_java && is_strict_mode_violation tenv callee actuals -> Domain.strict_mode_call ~callee ~loc astate | NoEffect when is_java -> ( - match may_block tenv callee actuals with - | Some sev -> - Domain.blocking_call ~callee sev ~loc astate - | None -> - do_call callee loc astate ) + let astate = do_thread_assert_effect ret_base callee astate in + match may_block tenv callee actuals with + | Some sev -> + Domain.blocking_call ~callee sev ~loc astate + | None -> + do_call callee loc astate ) | NoEffect -> (* in C++/Obj C we only care about deadlocks, not starvation errors *) do_call callee loc astate ) diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index b5870b320..09876c104 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -411,34 +411,65 @@ module GuardToLockMap = struct let add_guard astate ~guard ~lock = add guard (FlatLock.v lock) astate end +module BranchGuard = struct + type t = Nothing | Thread + + let top = Nothing + + let is_top = function Nothing -> true | _ -> false + + let pp fmt t = F.fprintf fmt (match t with Nothing -> "Nothing" | Thread -> "Thread") + + let leq ~lhs ~rhs = + match (lhs, rhs) with _, Nothing -> true | Nothing, _ -> false | Thread, Thread -> true + + + let join lhs rhs = match (lhs, rhs) with Thread, Thread -> lhs | _ -> Nothing + + let widen ~prev ~next ~num_iters:_ = join prev next +end + +module BranchGuardDomain = struct + include AbstractDomain.InvertedMap (HilExp.AccessExpression) (BranchGuard) + + let is_thread_guard acc_exp t = + find_opt acc_exp t |> Option.exists ~f:(function BranchGuard.Thread -> true | _ -> false) +end + type t = { guard_map: GuardToLockMap.t ; lock_state: LockState.t ; critical_pairs: CriticalPairs.t + ; branch_guards: BranchGuardDomain.t ; thread: ThreadDomain.t } let bottom = { guard_map= GuardToLockMap.empty ; lock_state= LockState.top ; critical_pairs= CriticalPairs.empty + ; branch_guards= BranchGuardDomain.empty ; thread= ThreadDomain.top } -let is_bottom {guard_map; lock_state; critical_pairs; thread} = +let is_bottom {guard_map; lock_state; critical_pairs; branch_guards; thread} = GuardToLockMap.is_empty guard_map && LockState.is_top lock_state && CriticalPairs.is_empty critical_pairs + && BranchGuardDomain.is_top branch_guards && ThreadDomain.is_top thread -let pp fmt {guard_map; lock_state; critical_pairs; thread} = - F.fprintf fmt "{guard_map= %a; lock_state= %a; critical_pairs= %a; thread= %a}" GuardToLockMap.pp - guard_map LockState.pp lock_state CriticalPairs.pp critical_pairs ThreadDomain.pp thread +let pp fmt {guard_map; lock_state; critical_pairs; branch_guards; thread} = + F.fprintf fmt + "{guard_map= %a; lock_state= %a; critical_pairs= %a; branch_guards= %a; thread= %a}" + GuardToLockMap.pp guard_map LockState.pp lock_state CriticalPairs.pp critical_pairs + BranchGuardDomain.pp branch_guards ThreadDomain.pp thread let join lhs rhs = { guard_map= GuardToLockMap.join lhs.guard_map rhs.guard_map ; lock_state= LockState.join lhs.lock_state rhs.lock_state ; critical_pairs= CriticalPairs.join lhs.critical_pairs rhs.critical_pairs + ; branch_guards= BranchGuardDomain.join lhs.branch_guards rhs.branch_guards ; thread= ThreadDomain.join lhs.thread rhs.thread } @@ -448,6 +479,7 @@ let leq ~lhs ~rhs = GuardToLockMap.leq ~lhs:lhs.guard_map ~rhs:rhs.guard_map && LockState.leq ~lhs:lhs.lock_state ~rhs:rhs.lock_state && CriticalPairs.leq ~lhs:lhs.critical_pairs ~rhs:rhs.critical_pairs + && BranchGuardDomain.leq ~lhs:lhs.branch_guards ~rhs:rhs.branch_guards && ThreadDomain.leq ~lhs:lhs.thread ~rhs:rhs.thread diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 4a4030420..41ba937a1 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -96,10 +96,28 @@ module CriticalPairs : AbstractDomain.FiniteSetS with type elt = CriticalPair.t module GuardToLockMap : AbstractDomain.WithTop +(** tracks whether an expression has been tested for whether we execute on UI thread *) +module BranchGuard : sig + type t = Nothing | Thread + + include AbstractDomain.WithTop with type t := t +end + +(** tracks all expressions currently known to have been tested for conditions in [BranchGuard] *) +module BranchGuardDomain : sig + include + AbstractDomain.InvertedMapS + with type key = HilExp.AccessExpression.t + and type value = BranchGuard.t + + val is_thread_guard : HilExp.AccessExpression.t -> t -> bool +end + type t = { guard_map: GuardToLockMap.t ; lock_state: LockState.t ; critical_pairs: CriticalPairs.t + ; branch_guards: BranchGuardDomain.t ; thread: ThreadDomain.t } include AbstractDomain.WithBottom with type t := t diff --git a/infer/tests/codetoanalyze/java/starvation/ThreadSensitivity.java b/infer/tests/codetoanalyze/java/starvation/ThreadSensitivity.java index a77c59ba6..a72d272bf 100644 --- a/infer/tests/codetoanalyze/java/starvation/ThreadSensitivity.java +++ b/infer/tests/codetoanalyze/java/starvation/ThreadSensitivity.java @@ -30,7 +30,7 @@ class ThreadSensitivity { // the branches in the following two methods are both on main/UI thread so cannot deadlock - void FP_conditionalIsMainThread_Ok() { + void conditionalIsMainThread_Ok() { if (OurThreadUtils.isMainThread()) { synchronized (monitorC) { synchronized (monitorD) { @@ -39,7 +39,7 @@ class ThreadSensitivity { } } - void FP_conditionalIsUiThread_Ok() { + void conditionalIsUiThread_Ok() { if (OurThreadUtils.isUiThread()) { synchronized (monitorD) { synchronized (monitorC) { diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp index d2f8f1ca8..35817cf4b 100644 --- a/infer/tests/codetoanalyze/java/starvation/issues.exp +++ b/infer/tests/codetoanalyze/java/starvation/issues.exp @@ -73,8 +73,6 @@ codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.assertOnBackgr codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.assertOnUIThreadBad():void, 52, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.assertOnUIThreadBad()`, locks `this` in `class ThreadDeadlock`, locks `this.lockC` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.assertOnBackgroundThreadBad()`, locks `this.lockC` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`] codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.notAnnotatedBBad():void, 77, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.notAnnotatedBBad()`, locks `this.lockD` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.notAnnotatedBadA()`, locks `this` in `class ThreadDeadlock`, locks `this.lockD` in `class ThreadDeadlock`] codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.notAnnotatedBadA():void, 71, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.notAnnotatedBadA()`, locks `this` in `class ThreadDeadlock`, locks `this.lockD` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.notAnnotatedBBad()`, locks `this.lockD` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`] -codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.FP_conditionalIsMainThread_Ok():void, 35, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.FP_conditionalIsMainThread_Ok()`, locks `this.monitorC` in `class ThreadSensitivity`, locks `this.monitorD` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.FP_conditionalIsUiThread_Ok()`, locks `this.monitorD` in `class ThreadSensitivity`, locks `this.monitorC` in `class ThreadSensitivity`] -codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.FP_conditionalIsUiThread_Ok():void, 44, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.FP_conditionalIsUiThread_Ok()`, locks `this.monitorD` in `class ThreadSensitivity`, locks `this.monitorC` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.FP_conditionalIsMainThread_Ok()`, locks `this.monitorC` in `class ThreadSensitivity`, locks `this.monitorD` in `class ThreadSensitivity`] codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.FP_confusedAssertOk(boolean):void, 99, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.FP_confusedAssertOk(boolean)`, locks `this.monitorI` in `class ThreadSensitivity`, locks `this.monitorJ` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.FP_confusedAssertOk(boolean)`, locks `this.monitorJ` in `class ThreadSensitivity`, locks `this.monitorI` in `class ThreadSensitivity`] codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.FP_confusedAssertOk(boolean):void, 106, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.FP_confusedAssertOk(boolean)`, locks `this.monitorJ` in `class ThreadSensitivity`, locks `this.monitorI` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.FP_confusedAssertOk(boolean)`, locks `this.monitorI` in `class ThreadSensitivity`, locks `this.monitorJ` in `class ThreadSensitivity`] codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.conditionalAssertMainThread_Bad(boolean):void, 16, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.conditionalAssertMainThread_Bad(boolean)`, locks `this.monitorA` in `class ThreadSensitivity`, locks `this.monitorB` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.conditionalAssertMainThread_Bad(boolean)`, locks `this.monitorB` in `class ThreadSensitivity`, locks `this.monitorA` in `class ThreadSensitivity`]