[starvation] add NonBlocking annotation

Summary: Introduce an annotation that forces the summary of a method to be free of blocking events, without suppressing other reports.

Reviewed By: jeremydubreil

Differential Revision: D8276787

fbshipit-source-id: be9eed8

infer/annotations/src/main/java/com/facebook/infer/annotation/NonBlocking.java

@@ -0,0 +1,27 @@
+/*
+ * Copyright (c) 2004-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+package com.facebook.infer.annotation;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Retention(RetentionPolicy.CLASS)
+@Target({
+        ElementType.CONSTRUCTOR,
+        ElementType.METHOD,
+        ElementType.TYPE
+})
+
+// Signal to the starvation checker that the method (or all the methods of the class,
+// if at class level) does not perform any potentially blocking operations.  Can be used to
+// effectively filter out all method calls which Infer may consider blocking.  This means that
+// not only Infer will not warn on any starvation issues in the method, but will also not warn on
+// any of the callers of this method.
+public @interface NonBlocking {}

infer/src/backend/reporting.ml

@@ -112,22 +112,22 @@ let is_suppressed ?(field_name= None) tenv proc_desc kind =
     let normalize str = Str.global_replace (Str.regexp "[_-]") "" (String.lowercase str) in
     let drop_prefix str = Str.replace_first (Str.regexp "^[A-Za-z]+_") "" str in
     let normalized_equal s1 s2 = String.equal (normalize s1) (normalize s2) in
-    let is_parameter_suppressed =
+    let is_parameter_suppressed () =
       String.is_suffix a.class_name ~suffix:Annotations.suppress_lint
       && List.mem ~equal:normalized_equal a.parameters kind.IssueType.unique_id
     in
-    let is_annotation_suppressed =
+    let is_annotation_suppressed () =
       String.is_suffix
         ~suffix:(normalize (drop_prefix kind.IssueType.unique_id))
         (normalize a.class_name)
     in
-    is_parameter_suppressed || is_annotation_suppressed
+    is_parameter_suppressed () || is_annotation_suppressed ()
   in
-  let is_method_suppressed =
+  let is_method_suppressed () =
     Annotations.ma_has_annotation_with proc_attributes.ProcAttributes.method_annotation
       annotation_matches
   in
-  let is_field_suppressed =
+  let is_field_suppressed () =
     match (field_name, PatternMatch.get_this_type proc_attributes) with
     | Some field_name, Some t -> (
       match Typ.Struct.get_field_type_and_annotation ~lookup field_name t with
@@ -138,7 +138,7 @@ let is_suppressed ?(field_name= None) tenv proc_desc kind =
     | _ ->
         false
   in
-  let is_class_suppressed =
+  let is_class_suppressed () =
     match PatternMatch.get_this_type proc_attributes with
     | Some t -> (
       match PatternMatch.type_get_annotation tenv t with
@@ -149,4 +149,4 @@ let is_suppressed ?(field_name= None) tenv proc_desc kind =
     | None ->
         false
   in
-  is_method_suppressed || is_field_suppressed || is_class_suppressed
+  is_method_suppressed () || is_field_suppressed () || is_class_suppressed ()

infer/src/checkers/annotations.ml

@@ -67,6 +67,8 @@ let on_unbind = "OnUnbind"
 
 let on_unmount = "OnUnmount"
 
+let nonblocking = "NonBlocking"
+
 let notnull = "NotNull"
 
 let not_thread_safe = "NotThreadSafe"
@@ -184,6 +186,8 @@ let ia_is_thrift_service ia = ia_ends_with ia thrift_service
 
 let ia_is_true_on_null ia = ia_ends_with ia true_on_null
 
+let ia_is_nonblocking ia = ia_ends_with ia nonblocking
+
 let ia_is_initializer ia = ia_ends_with ia initializer_
 
 let ia_is_volatile ia = ia_contains ia volatile

infer/src/checkers/annotations.mli

@@ -104,6 +104,8 @@ val ia_is_on_unmount : Annot.Item.t -> bool
 
 val ia_is_not_thread_safe : Annot.Item.t -> bool
 
+val ia_is_nonblocking : Annot.Item.t -> bool
+
 val ia_is_returns_ownership : Annot.Item.t -> bool
 
 val ia_is_synchronized_collection : Annot.Item.t -> bool

infer/src/concurrency/starvation.ml

@@ -15,6 +15,19 @@ let is_on_ui_thread pn =
   RacerDConfig.(match Models.get_thread pn with Models.MainThread -> true | _ -> false)
 
 
+let is_nonblocking tenv proc_desc =
+  let proc_attributes = Procdesc.get_attributes proc_desc in
+  let is_method_suppressed =
+    Annotations.pdesc_has_return_annot proc_desc Annotations.ia_is_nonblocking
+  in
+  let is_class_suppressed =
+    PatternMatch.get_this_type proc_attributes
+    |> Option.bind ~f:(PatternMatch.type_get_annotation tenv)
+    |> Option.value_map ~default:false ~f:Annotations.ia_is_nonblocking
+  in
+  is_method_suppressed || is_class_suppressed
+
+
 module Payload = SummaryPayload.Make (struct
   type t = StarvationDomain.summary
 
@@ -104,6 +117,7 @@ let die_if_not_java proc_desc =
 
 
 let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
+  let open StarvationDomain in
   die_if_not_java proc_desc ;
   let pname = Procdesc.get_proc_name proc_desc in
   let formals = FormalMap.make proc_desc in
@@ -128,7 +142,17 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
     RacerDConfig.Models.runs_on_ui_thread tenv proc_desc
     |> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial)
   in
-  Analyzer.compute_post proc_data ~initial
+  let filter_blocks =
+    if is_nonblocking tenv proc_desc then fun ({events; order} as astate) ->
+      { astate with
+        events= EventDomain.filter (function {elem= MayBlock _} -> false | _ -> true) events
+      ; order=
+          OrderDomain.filter
+            (function {eventually= {elem= MayBlock _}} -> false | _ -> true)
+            order }
+    else Fn.id
+  in
+  Analyzer.compute_post proc_data ~initial |> Option.map ~f:filter_blocks
   |> Option.value_map ~default:summary ~f:(fun astate -> Payload.update_summary astate summary)
 
 

infer/tests/codetoanalyze/java/starvation/NonBlk.java

@@ -0,0 +1,44 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+import java.util.concurrent.Future;
+import java.util.concurrent.ExecutionException;
+import java.io.IOException;
+import android.support.annotation.UiThread;
+import com.facebook.infer.annotation.NonBlocking;
+
+class NonBlk {
+  Future future;
+
+  @NonBlocking
+  void doGet() throws InterruptedException, ExecutionException {
+    future.get();
+  }
+
+  @UiThread
+  void onUiThreadIndirectOk() throws InterruptedException, ExecutionException {
+    doGet();
+  }
+
+  @NonBlocking
+  @UiThread
+  void onUiThreadDirectOk() throws InterruptedException, ExecutionException {
+    future.get();
+  }
+
+  @NonBlocking
+  synchronized void deadlockABBad() {
+    synchronized(future) {}
+  }
+
+  @NonBlocking
+  void deadlockBABad() {
+    synchronized(future) {
+      synchronized(this) {}
+    }
+  }
+}

infer/tests/codetoanalyze/java/starvation/issues.exp

@@ -24,6 +24,7 @@ codetoanalyze/java/starvation/Interclass.java, void Interclass.interclass1Bad(In
 codetoanalyze/java/starvation/Interproc.java, void Interproc.interproc1Bad(InterprocA), 9, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interproc.interproc1Bad(InterprocA)`,locks `this` in class `Interproc*`,Method call: `void Interproc.interproc2Bad(InterprocA)`,locks `b` in class `InterprocA*`,[Trace 2] `void InterprocA.interproc1Bad(Interproc)`,locks `this` in class `InterprocA*`,Method call: `void InterprocA.interproc2Bad(Interproc)`,locks `d` in class `Interproc*`]
 codetoanalyze/java/starvation/Intraproc.java, void Intraproc.intraBad(IntraprocA), 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Intraproc.intraBad(IntraprocA)`,locks `this` in class `Intraproc*`,locks `o` in class `IntraprocA*`,[Trace 2] `void IntraprocA.intraBad(Intraproc)`,locks `this` in class `IntraprocA*`,locks `o` in class `Intraproc*`]
 codetoanalyze/java/starvation/LegacySync.java, Object LegacySync.onUiThreadOpBad(), 25, STARVATION, no_bucket, ERROR, [[Trace 1] `Object LegacySync.onUiThreadOpBad()`,locks `this.LegacySync.table` in class `LegacySync*`,[Trace 2] `void LegacySync.notOnUiThreadSyncedBad()`,locks `this.LegacySync.table` in class `LegacySync*`,calls `Object Future.get()` from `void LegacySync.notOnUiThreadSyncedBad()`]
+codetoanalyze/java/starvation/NonBlk.java, void NonBlk.deadlockABBad(), 34, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void NonBlk.deadlockABBad()`,locks `this` in class `NonBlk*`,locks `this.NonBlk.future` in class `NonBlk*`,[Trace 2] `void NonBlk.deadlockBABad()`,locks `this.NonBlk.future` in class `NonBlk*`,locks `this` in class `NonBlk*`]
 codetoanalyze/java/starvation/ServiceOnUIThread.java, IBinder ServiceOnUIThread.onBind(Intent), 19, STARVATION, no_bucket, ERROR, [`IBinder ServiceOnUIThread.onBind(Intent)`,Method call: `void ServiceOnUIThread.transactBad()`,calls `boolean IBinder.transact(int,Parcel,Parcel,int)` from `void ServiceOnUIThread.transactBad()`]
 codetoanalyze/java/starvation/ServiceOnUIThread.java, void ServiceOnUIThread.transactBad(), 25, STARVATION, no_bucket, ERROR, [`void ServiceOnUIThread.transactBad()`,calls `boolean IBinder.transact(int,Parcel,Parcel,int)` from `void ServiceOnUIThread.transactBad()`]
 codetoanalyze/java/starvation/StaticLock.java, void StaticLock.lockOtherClassOneWayBad(), 23, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void StaticLock.lockOtherClassOneWayBad()`,locks `StaticLock$0` in class `java.lang.Class*`,locks `this` in class `StaticLock*`,[Trace 2] `void StaticLock.lockOtherClassAnotherWayNad()`,locks `this` in class `StaticLock*`,Method call: `void StaticLock.staticSynced()`,locks `StaticLock$0` in class `java.lang.Class*`]