[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

@@ -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) ->

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

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

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

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 :

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<Object> future) throws ExecutionException {
     return Futures.getDone(future);