From b994fa7f70c2f174465d7fc352570f2ccaa141e0 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Wed, 11 Dec 2019 03:28:15 -0800 Subject: [PATCH] [starvation] add path sensitivity on Future.isDone Summary: A future is guaranteed not to block if `isDone()` has returned true first. Add logic for supporting that by remembering the objects that we have called `isDone` on and by making `assume` do the right thing with that knowledge. All this is achieved with the attribute domain. Reviewed By: ezgicicek Differential Revision: D18833901 fbshipit-source-id: 7f4ea0cd1 --- infer/src/concurrency/StarvationModels.ml | 18 +++++++++--- infer/src/concurrency/StarvationModels.mli | 4 +++ infer/src/concurrency/starvation.ml | 28 +++++++++++++++++-- infer/src/concurrency/starvationDomain.ml | 24 ++++++++++++++++ infer/src/concurrency/starvationDomain.mli | 7 +++++ .../java/starvation/FutureGet.java | 9 ++++++ 6 files changed, 84 insertions(+), 6 deletions(-) diff --git a/infer/src/concurrency/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml index 56c43c06e..ce3cd4cc6 100644 --- a/infer/src/concurrency/StarvationModels.ml +++ b/infer/src/concurrency/StarvationModels.ml @@ -123,10 +123,6 @@ let standard_matchers = in let low_sev = [ { default with - classname= "java.util.concurrent.Future" - ; methods= ["get"] - ; actuals_pred= no_args_or_excessive_timeout_and_timeunit } - ; { default with classname= "android.os.AsyncTask" ; methods= ["get"] ; actuals_pred= no_args_or_excessive_timeout_and_timeunit } ] @@ -136,6 +132,20 @@ let standard_matchers = [(high_sev_matcher, High); (low_sev_matcher, Low)] +let is_future_get = + let open MethodMatcher in + of_record + { default with + classname= "java.util.concurrent.Future" + ; methods= ["get"] + ; actuals_pred= no_args_or_excessive_timeout_and_timeunit } + + +let is_future_is_done = + MethodMatcher.( + of_record {default with classname= "java.util.concurrent.Future"; methods= ["isDone"]}) + + (* sort from High to Low *) let may_block tenv pn actuals = List.find_map standard_matchers ~f:(fun (matcher, sev) -> diff --git a/infer/src/concurrency/StarvationModels.mli b/infer/src/concurrency/StarvationModels.mli index fa43bf147..d0d8b3808 100644 --- a/infer/src/concurrency/StarvationModels.mli +++ b/infer/src/concurrency/StarvationModels.mli @@ -69,3 +69,7 @@ val is_getMainLooper : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool val is_handler_constructor : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool val is_thread_constructor : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool + +val is_future_get : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool + +val is_future_is_done : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index f71fd1a2d..eae38ac85 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -61,13 +61,26 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let do_assume assume_exp (astate : Domain.t) = let open Domain in - let add_choice (acc : Domain.t) bool_value = + let add_thread_choice (acc : Domain.t) bool_value = let thread = if bool_value then ThreadDomain.UIThread else ThreadDomain.BGThread in {acc with thread} in + let add_future_done_choice acc_exp (acc : Domain.t) bool_value = + AttributeDomain.find_opt acc_exp acc.attributes + |> Option.bind ~f:(function Attribute.FutureDoneGuard future -> Some future | _ -> None) + |> Option.value_map ~default:acc ~f:(fun future -> + let attributes = + AttributeDomain.add future (Attribute.FutureDoneState bool_value) acc.attributes + in + {acc with attributes} ) + in match HilExp.get_access_exprs assume_exp with | [access_expr] when AttributeDomain.is_thread_guard access_expr astate.attributes -> - HilExp.eval_boolean_exp access_expr assume_exp |> Option.fold ~init:astate ~f:add_choice + HilExp.eval_boolean_exp access_expr assume_exp + |> Option.fold ~init:astate ~f:add_thread_choice + | [access_expr] when AttributeDomain.is_future_done_guard access_expr astate.attributes -> + HilExp.eval_boolean_exp access_expr assume_exp + |> Option.fold ~init:astate ~f:(add_future_done_choice access_expr) | _ -> astate @@ -142,6 +155,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | UnknownThread -> None in + let get_future_is_done_summary () = + match actuals with + | HilExp.AccessExpression future :: _ + when StarvationModels.is_future_is_done tenv callee actuals -> + Some (make_ret_attr (FutureDoneGuard future)) + | _ -> + None + in let get_mainLooper_summary () = if StarvationModels.is_getMainLooper tenv callee actuals then Some (make_ret_attr (Looper ForUIThread)) @@ -196,6 +217,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct IList.eval_until_first_some [ get_returned_executor_summary ; get_thread_assert_summary + ; get_future_is_done_summary ; get_mainLooper_summary ; get_callee_summary ] |> Option.map ~f:(Domain.integrate_summary ~tenv ~lhs callsite astate) @@ -258,6 +280,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Domain.strict_mode_call ~callee ~loc astate | NoEffect when is_java && is_monitor_wait tenv callee actuals -> Domain.wait_on_monitor ~loc actuals astate + | NoEffect when is_java && is_future_get tenv callee actuals -> + Domain.future_get ~callee ~loc actuals astate | NoEffect when is_java -> ( let ret_exp = HilExp.AccessExpression.base ret_base in let astate = do_work_scheduling tenv callee actuals loc astate in diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 490c47c75..c6aef5dfe 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -456,6 +456,8 @@ module Attribute = struct type t = | Nothing | ThreadGuard + | FutureDoneGuard of HilExp.AccessExpression.t + | FutureDoneState of bool | Runnable of Typ.Procname.t | WorkScheduler of StarvationModels.scheduler_thread_constraint | Looper of StarvationModels.scheduler_thread_constraint @@ -476,6 +478,10 @@ module Attribute = struct F.pp_print_string fmt "Nothing" | ThreadGuard -> F.pp_print_string fmt "ThreadGuard" + | FutureDoneGuard exp -> + F.fprintf fmt "FutureDoneGuard(%a)" HilExp.AccessExpression.pp exp + | FutureDoneState state -> + F.fprintf fmt "FutureDoneState(%b)" state | Runnable runproc -> F.fprintf fmt "Runnable(%a)" Typ.Procname.pp runproc | WorkScheduler c -> @@ -502,6 +508,11 @@ module AttributeDomain = struct find_opt acc_exp t |> Option.bind ~f:(function Attribute.WorkScheduler c -> Some c | _ -> None) + let is_future_done_guard acc_exp t = + find_opt acc_exp t + |> Option.exists ~f:(function Attribute.FutureDoneGuard _ -> true | _ -> false) + + let exit_scope vars t = let pred key _value = HilExp.AccessExpression.get_base key @@ -616,6 +627,19 @@ let wait_on_monitor ~loc actuals astate = astate +let future_get ~callee ~loc actuals astate = + match actuals with + | HilExp.AccessExpression exp :: _ + when AttributeDomain.find_opt exp astate.attributes + |> Option.exists ~f:(function Attribute.FutureDoneState x -> x | _ -> false) -> + astate + | HilExp.AccessExpression _ :: _ -> + let new_event = Event.make_blocking_call callee Low in + make_call_with_event new_event ~loc astate + | _ -> + astate + + let strict_mode_call ~callee ~loc astate = let new_event = Event.make_strict_mode_call callee in make_call_with_event new_event ~loc astate diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 41be075e4..943967718 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -109,6 +109,8 @@ module Attribute : sig type t = | Nothing | ThreadGuard (** is boolean equivalent to whether on UI thread *) + | FutureDoneGuard of HilExp.AccessExpression.t (** boolean equivalent to [Future.isDone()] *) + | FutureDoneState of bool (** is a [Future] ready for non-blocking consumption *) | Runnable of Typ.Procname.t (** is a Runnable/Callable with given "run" procname *) | WorkScheduler of StarvationModels.scheduler_thread_constraint (** exp is something that schedules work on the given thread *) @@ -129,6 +131,9 @@ module AttributeDomain : sig val get_scheduler_constraint : HilExp.AccessExpression.t -> t -> StarvationModels.scheduler_thread_constraint option + val is_future_done_guard : HilExp.AccessExpression.t -> t -> bool + (** does the given expr has attribute [FutureDone x] return [Some x] else [None] *) + val exit_scope : Var.t list -> t -> t end @@ -161,6 +166,8 @@ val blocking_call : callee:Typ.Procname.t -> StarvationModels.severity -> loc:Lo val wait_on_monitor : loc:Location.t -> HilExp.t list -> t -> t +val future_get : callee:Typ.Procname.t -> loc:Location.t -> HilExp.t list -> t -> t + val strict_mode_call : callee:Typ.Procname.t -> loc:Location.t -> t -> t val add_guard : diff --git a/infer/tests/codetoanalyze/java/starvation/FutureGet.java b/infer/tests/codetoanalyze/java/starvation/FutureGet.java index e5999044a..11c90124b 100644 --- a/infer/tests/codetoanalyze/java/starvation/FutureGet.java +++ b/infer/tests/codetoanalyze/java/starvation/FutureGet.java @@ -93,6 +93,15 @@ class FutureGet { } } + @UiThread + Object sensitivityOnIsDoneOk() throws InterruptedException, ExecutionException { + if (future.isDone()) { + return future.get(); + } else { + return null; + } + } + @UiThread Object getFuturesDoneOk(Future future) throws ExecutionException { return Futures.getDone(future);