[starvation] treat precondition calls as assumes

Summary: Guava uses assertions to ensure a future can be gotten without blocking (this means that if the future is not done, the app will crash).  This diff teaches the starvation analyser about a number of such assertions, by treating them as assumes (since we don't care about exceptions).

Reviewed By: jvillard

Differential Revision: D18893427

fbshipit-source-id: 4d26a202b

infer/src/concurrency/StarvationModels.ml

@@ -365,3 +365,17 @@ let is_thread_constructor =
       classname= "java.lang.Thread"
     ; search_superclasses= false
     ; methods= [Typ.Procname.Java.constructor_method_name] }
+
+
+let is_assume_true =
+  let open MethodMatcher in
+  of_records
+    [ { default with
+        classname= "com.facebook.common.internal.Preconditions"
+      ; methods= ["checkArgument"; "checkState"] }
+    ; { default with
+        classname= "com.facebook.infer.annotation.Assertions"
+      ; methods= ["assertCondition"; "assumeCondition"] }
+    ; { default with
+        classname= "com.google.common.base.Preconditions"
+      ; methods= ["checkArgument"; "checkState"] } ]

infer/src/concurrency/StarvationModels.mli

@@ -73,3 +73,6 @@ 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
+
+val is_assume_true : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool
+(** is the callee equivalent to assuming its first argument true *)

infer/src/concurrency/starvation.ml

@@ -210,6 +210,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             None
       else None
     in
+    let treat_assume () =
+      if StarvationModels.is_assume_true tenv callee actuals then
+        List.hd actuals |> Option.map ~f:(fun exp -> do_assume exp astate)
+      else None
+    in
     (* constructor calls are special-cased because they side-effect the receiver and do not
        return anything *)
     let treat_modeled_summaries () =
@@ -223,7 +228,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       |> Option.map ~f:(Domain.integrate_summary ~tenv ~lhs callsite astate)
     in
     IList.eval_until_first_some
-      [treat_handler_constructor; treat_thread_constructor; treat_modeled_summaries]
+      [treat_handler_constructor; treat_thread_constructor; treat_assume; treat_modeled_summaries]
     |> Option.value ~default:astate
 
 

infer/tests/codetoanalyze/java/starvation/FutureGet.java

@@ -6,7 +6,7 @@
  */
 
 import android.support.annotation.UiThread;
-import com.google.common.util.concurrent.Futures;
+import com.google.common.base.Preconditions;
 import java.util.concurrent.ExecutionException;
 import java.util.concurrent.Future;
 import java.util.concurrent.TimeUnit;
@@ -103,7 +103,14 @@ class FutureGet {
   }
 
   @UiThread
-  Object getFuturesDoneOk(Future<Object> future) throws ExecutionException {
-    return Futures.getDone(future);
+  Object getFuturesDoneOk(Future<Object> future) throws InterruptedException, ExecutionException {
+    Preconditions.checkState(future.isDone());
+    return future.get();
+  }
+
+  Object assertNotOnUIThreadOk(Future<Object> future)
+      throws InterruptedException, ExecutionException {
+    Preconditions.checkArgument(!OurThreadUtils.isMainThread());
+    return future.get();
   }
 }