From 6edf037659e2eba72807fbd47845b61a0b27a192 Mon Sep 17 00:00:00 2001
From: Nikos Gorogiannis <nikosg@fb.com>
Date: Wed, 11 Dec 2019 03:28:19 -0800
Subject: [PATCH] [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          | 14 ++++++++++++++
 infer/src/concurrency/StarvationModels.mli         |  3 +++
 infer/src/concurrency/starvation.ml                |  7 ++++++-
 .../codetoanalyze/java/starvation/FutureGet.java   | 13 ++++++++++---
 4 files changed, 33 insertions(+), 4 deletions(-)

diff --git a/infer/src/concurrency/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml
index ce3cd4cc6..ecbc34836 100644
--- a/infer/src/concurrency/StarvationModels.ml
+++ b/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"] } ]
diff --git a/infer/src/concurrency/StarvationModels.mli b/infer/src/concurrency/StarvationModels.mli
index d0d8b3808..623398c3a 100644
--- a/infer/src/concurrency/StarvationModels.mli
+++ b/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 *)
diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml
index eae38ac85..577442c15 100644
--- a/infer/src/concurrency/starvation.ml
+++ b/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
 
 
diff --git a/infer/tests/codetoanalyze/java/starvation/FutureGet.java b/infer/tests/codetoanalyze/java/starvation/FutureGet.java
index 11c90124b..df3d39757 100644
--- a/infer/tests/codetoanalyze/java/starvation/FutureGet.java
+++ b/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();
   }
 }