[Eradicate] Add support for modeling boolean functions that check if the argument is null.

Summary:
Added two annotations @TrueOnNull and @FalseOnNull to be used for boolean functions to specify what value is returned when the argument is null.

Added model for TextUtils.isEmpty, which corresponds to the annotation
  @TrueOnNull
  static boolean isEmpty(@Nullable java.lang.CharSequence s)

infer/annotations/com/facebook/infer/annotation/FalseOnNull.java

@@ -0,0 +1,22 @@
+/*
+* Copyright (c) 2015 - present Facebook, Inc.
+* All rights reserved.
+*
+* This source code is licensed under the BSD style license found in the
+* LICENSE file in the root directory of this source tree. An additional grant
+* of patent rights can be found in the PATENTS file in the same directory.
+*/
+
+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;
+
+/**
+ * Annotation for a boolean function returning false when the argument is null.
+ */
+@Retention(RetentionPolicy.CLASS)
+@Target({ElementType.METHOD})
+public @interface FalseOnNull {}

infer/annotations/com/facebook/infer/annotation/TrueOnNull.java

@@ -0,0 +1,22 @@
+/*
+* Copyright (c) 2015 - present Facebook, Inc.
+* All rights reserved.
+*
+* This source code is licensed under the BSD style license found in the
+* LICENSE file in the root directory of this source tree. An additional grant
+* of patent rights can be found in the PATENTS file in the same directory.
+*/
+
+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;
+
+/**
+ * Annotation for a boolean function returning true when the argument is null.
+ */
+@Retention(RetentionPolicy.CLASS)
+@Target({ElementType.METHOD})
+public @interface TrueOnNull {}

infer/src/checkers/annotations.ml

@@ -99,6 +99,7 @@ let initializer_ = "Initializer"
 let inject = "Inject"
 let inject_view = "InjectView"
 let bind = "Bind"
+let false_on_null = "FalseOnNull"
 let mutable_ = "Mutable"
 let nullable = "Nullable"
 let nonnull = "Nonnull"
@@ -106,6 +107,7 @@ let camel_nonnull = "NonNull"
 let notnull = "NotNull"
 let present = "Present"
 let strict = "com.facebook.infer.annotation.Strict"
+let true_on_null = "TrueOnNull"
 let verify_annotation = "com.facebook.infer.annotation.Verify"
 
 let ia_is_nullable ia =
@@ -119,6 +121,12 @@ let ia_is_nonnull ia =
     (ia_ends_with ia)
     [nonnull; notnull; camel_nonnull]
 
+let ia_is_false_on_null ia =
+  ia_ends_with ia false_on_null
+
+let ia_is_true_on_null ia =
+  ia_ends_with ia true_on_null
+
 let ia_is_initializer ia =
   ia_ends_with ia initializer_
 

infer/src/checkers/annotations.mli

@@ -57,13 +57,15 @@ val ia_has_annotation_with : Sil.item_annotation -> (Sil.annotation -> bool) ->
 
 val ia_get_strict : Sil.item_annotation -> Sil.annotation option
 
+val ia_is_false_on_null : Sil.item_annotation -> bool
 val ia_is_initializer : Sil.item_annotation -> bool
 val ia_is_inject : Sil.item_annotation -> bool
 val ia_is_inject_view : Sil.item_annotation -> bool
 val ia_is_mutable : Sil.item_annotation -> bool
-val ia_is_nullable : Sil.item_annotation -> bool
 val ia_is_nonnull : Sil.item_annotation -> bool
+val ia_is_nullable : Sil.item_annotation -> bool
 val ia_is_present : Sil.item_annotation -> bool
+val ia_is_true_on_null : Sil.item_annotation -> bool
 val ia_is_verify : Sil.item_annotation -> bool
 
 val ia_iter : (Sil.annotation -> unit) -> Sil.item_annotation -> unit

infer/src/checkers/eradicateChecks.ml

@@ -115,6 +115,8 @@ let check_array_access
 type from_call =
   | From_condition (** Direct condition *)
   | From_instanceof (** x instanceof C *)
+  | From_is_false_on_null (** returns false on null *)
+  | From_is_true_on_null (** returns true on null *)
   | From_optional_isPresent (** x.isPresent *)
   | From_containsKey (** x.containsKey *)
 

infer/src/checkers/modelTables.ml

@@ -1,11 +1,11 @@
 (*
-* Copyright (c) 2013 - present Facebook, Inc.
+ * Copyright (c) 2015 - present Facebook, Inc.
-* All rights reserved.
+ * All rights reserved.
-*
+ *
-* This source code is licensed under the BSD style license found in the
+ * This source code is licensed under the BSD style license found in the
-* LICENSE file in the root directory of this source tree. An additional grant
+ * LICENSE file in the root directory of this source tree. An additional grant
-* of patent rights can be found in the PATENTS file in the same directory.
+ * of patent rights can be found in the PATENTS file in the same directory.
-*)
+ *)
 
 (*
  * This file is a big bunch of tables; they read better with really long lines.
@@ -89,6 +89,13 @@ let optional_isPresent_list : ((_ * bool list) * _) list =
     (o, []), "com.google.common.base.Optional.isPresent():boolean";
   ]
 
+(** Models for boolean functions that return true on null. *)
+let true_on_null_list : ((_ * bool list) * _) list =
+  [
+    n1, "android.text.TextUtils.isEmpty(java.lang.CharSequence):boolean";
+  ]
+
+
 (** Models for Map.containsKey *)
 let containsKey_list =
   [
@@ -226,6 +233,7 @@ let check_not_null_table, check_not_null_parameter_table =
   mk_table check_not_null_list, mk_table check_not_null_parameter_list
 let check_state_table = mk_table check_state_list
 let check_argument_table = mk_table check_argument_list
+let containsKey_table = mk_table containsKey_list
 let optional_get_table = mk_table optional_get_list
 let optional_isPresent_table = mk_table optional_isPresent_list
-let containsKey_table = mk_table containsKey_list
+let true_on_null_table = mk_table true_on_null_list

infer/src/checkers/modelTables.mli

@@ -1,6 +1,11 @@
 (*
-* Copyright (c) 2013 - Facebook. All rights reserved.
+ * Copyright (c) 2015 - present Facebook, Inc.
-*)
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
 
 type model_table_t = (string, bool * bool list) Hashtbl.t
 
@@ -11,6 +16,7 @@ val check_not_null_table : model_table_t
 val check_not_null_parameter_table : (string, int) Hashtbl.t
 val check_state_table : model_table_t
 val check_argument_table : model_table_t
+val containsKey_table : model_table_t
 val optional_get_table : model_table_t
 val optional_isPresent_table : model_table_t
-val containsKey_table : model_table_t
+val true_on_null_table : model_table_t

infer/src/checkers/models.ml

@@ -217,6 +217,11 @@ let is_optional_get proc_name =
 let is_optional_isPresent proc_name =
   table_has_procedure optional_isPresent_table proc_name
 
+(** Check if the procedure returns true on null. *)
+let is_true_on_null proc_name =
+  table_has_procedure true_on_null_table proc_name
+
+
 (** Check if the procedure is Map.containsKey(). *)
 let is_containsKey proc_name =
   table_has_procedure containsKey_table proc_name

infer/src/checkers/typeAnnotation.mli

@@ -22,5 +22,6 @@ val get_origin : t -> TypeOrigin.t
 val get_value : Annotations.annotation -> t -> bool
 val join : t -> t -> t option
 val origin_is_fun_library : t -> bool
+val set_value : Annotations.annotation -> bool -> t -> t
 val to_string : t -> string
 val with_origin : t -> TypeOrigin.t -> t

infer/src/checkers/typeCheck.ml

@@ -44,12 +44,40 @@ module ComplexExpressions = struct
 
   let procname_optional_isPresent = Models.is_optional_isPresent
   let procname_instanceof = Procname.equal SymExec.ModelBuiltins.__instanceof
+
+  let procname_is_false_on_null get_proc_desc pn =
+    match get_proc_desc pn with
+    | Some pdesc ->
+        let proc_attributes = Specs.pdesc_resolve_attributes pdesc in
+        let annotated_signature =
+          Models.get_modelled_annotated_signature proc_attributes in
+        let ret_ann, _ = annotated_signature.Annotations.ret in
+        Annotations.ia_is_false_on_null ret_ann
+    | None ->
+        false
+
+  let procname_is_true_on_null get_proc_desc pn =
+    let annotated_true_on_null () =
+      match get_proc_desc pn with
+      | Some pdesc ->
+          let proc_attributes = Specs.pdesc_resolve_attributes pdesc in
+          let annotated_signature =
+            Models.get_modelled_annotated_signature proc_attributes in
+          let ret_ann, _ = annotated_signature.Annotations.ret in
+          Annotations.ia_is_true_on_null ret_ann
+      | None ->
+          false in
+    Models.is_true_on_null pn ||
+    annotated_true_on_null ()
+
   let procname_containsKey = Models.is_containsKey
 
   (** Recognize *all* the procedures treated specially in conditionals *)
-  let procname_used_in_condition pn =
+  let procname_used_in_condition get_proc_desc pn =
     procname_optional_isPresent pn ||
     procname_instanceof pn ||
+    procname_is_false_on_null get_proc_desc pn ||
+    procname_is_true_on_null get_proc_desc pn ||
     procname_containsKey pn ||
     SymExec.function_is_builtin pn
 
@@ -283,7 +311,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
     let handle_function_call call_node id =
       match Errdesc.find_normal_variable_funcall call_node id with
       | Some (Sil.Const (Sil.Cfun pn), _, _, _)
-        when not (ComplexExpressions.procname_used_in_condition pn) ->
+        when not (ComplexExpressions.procname_used_in_condition get_proc_desc pn) ->
           begin
             match ComplexExpressions.exp_to_string node' exp with
             | None -> default
@@ -780,6 +808,14 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
         let from_optional_isPresent e : Sil.exp option =
           from_call ComplexExpressions.procname_optional_isPresent e in
 
+        (* check if the expression is coming from a procedure returning false on null *)
+        let from_is_false_on_null e : Sil.exp option =
+          from_call (ComplexExpressions.procname_is_false_on_null get_proc_desc) e in
+
+        (* check if the expression is coming from a procedure returning true on null *)
+        let from_is_true_on_null e : Sil.exp option =
+          from_call (ComplexExpressions.procname_is_true_on_null get_proc_desc) e in
+
         (* check if the expression is coming from Map.containsKey *)
         let from_containsKey e : Sil.exp option =
           from_call ComplexExpressions.procname_containsKey e in
@@ -812,23 +848,53 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
                 typestate, e, EradicateChecks.From_condition
           end in
 
+        let set_flag e' ann b typestate2 = (* add constraint on e' for annotation ann *)
+          let handle_pvar typestate' pvar =
+            match TypeState.lookup_pvar pvar typestate' with
+            | Some (t, ta1, locs) ->
+                if TypeAnnotation.get_value ann ta1 <> b then
+                  let ta2 = TypeAnnotation.set_value ann b ta1 in
+                  TypeState.add_pvar pvar (t, ta2, locs) typestate'
+                else typestate'
+            | None -> typestate' in
+          match e' with
+          | Sil.Lvar pvar ->
+              pvar_apply loc handle_pvar typestate2 pvar
+          | _ -> typestate2 in
 
         match c with
         | Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e)
         | Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i ->
             typecheck_expr_for_errors typestate e loc;
-            let e', typestate' = convert_complex_exp_to_pvar node' false e typestate loc in
+            let typestate1, e1, from_call = match from_is_true_on_null e with
+              | Some e1 ->
+                  typestate, e1, EradicateChecks.From_is_true_on_null
+              | None ->
+                  typestate, e, EradicateChecks.From_condition in
+            let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in
             let (typ, ta, _) =
-              typecheck_expr_simple typestate' e' Sil.Tvoid TypeOrigin.ONone loc in
+              typecheck_expr_simple typestate2 e' Sil.Tvoid TypeOrigin.ONone loc in
+
             if checks.eradicate then
               EradicateChecks.check_zero
                 find_canonical_duplicate get_proc_desc curr_pname
                 node' e' typ
                 ta true_branch EradicateChecks.From_condition
                 idenv linereader loc instr_ref;
-            typestate'
+            begin
+              match from_call with
+              | EradicateChecks.From_is_true_on_null ->
+                  (* if f returns true on null, then false branch implies != null *)
+                  if TypeAnnotation.get_value Annotations.Nullable ta
+                  then set_flag e' Annotations.Nullable false typestate2
+                  else typestate2
+              | _ ->
+                  typestate2
+            end
+
         | Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e)
         | Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i ->
+            typecheck_expr_for_errors typestate e loc;
             let typestate1, e1, from_call = match from_instanceof e with
               | Some e1 -> (* (e1 instanceof C) implies (e1 != null) *)
                   typestate, e1, EradicateChecks.From_instanceof
@@ -839,33 +905,23 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
                         typestate, e1, EradicateChecks.From_optional_isPresent
                     | None ->
                         begin
-                          match from_containsKey e with
+                          match from_is_false_on_null e with
-                          | Some e1 when ComplexExpressions.functions_idempotent () ->
+                          | Some e1 ->
-                              handle_containsKey e
+                              typestate, e1, EradicateChecks.From_is_false_on_null
-                          | _ ->
+                          | None ->
-                              typestate, e, EradicateChecks.From_condition
+                              begin
+                                match from_containsKey e with
+                                | Some e1 when ComplexExpressions.functions_idempotent () ->
+                                    handle_containsKey e
+                                | _ ->
+                                    typestate, e, EradicateChecks.From_condition
+                              end
                         end
                   end in
-            typecheck_expr_for_errors typestate1 e1 loc;
             let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in
             let (typ, ta, _) =
               typecheck_expr_simple typestate2 e' Sil.Tvoid TypeOrigin.ONone loc in
 
-            let set_flag e' ann b = (* add constraint on e' for annotation ann *)
-              let handle_pvar typestate' pvar =
-                match TypeState.lookup_pvar pvar typestate' with
-                | Some (t, ta1, locs) ->
-                    if TypeAnnotation.get_value ann ta1 <> b then
-                      let origin = TypeAnnotation.get_origin ta1 in
-                      let ta2 = TypeAnnotation.const ann b origin in
-                      TypeState.add_pvar pvar (t, ta2, locs) typestate'
-                    else typestate'
-                | None -> typestate' in
-              match e' with
-              | Sil.Lvar pvar ->
-                  pvar_apply loc handle_pvar typestate2 pvar
-              | _ -> typestate2 in
-
             if checks.eradicate then
               EradicateChecks.check_nonzero find_canonical_duplicate get_proc_desc curr_pname
                 node e' typ ta true_branch from_call idenv linereader loc instr_ref;
@@ -873,13 +929,16 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
               match from_call with
               | EradicateChecks.From_optional_isPresent ->
                   if TypeAnnotation.get_value Annotations.Present ta = false
-                  then set_flag e' Annotations.Present true
+                  then set_flag e' Annotations.Present true typestate2
                   else typestate2
+              | EradicateChecks.From_is_true_on_null ->
+                  typestate2
               | EradicateChecks.From_condition
+              | EradicateChecks.From_containsKey
               | EradicateChecks.From_instanceof
-              | EradicateChecks.From_containsKey ->
+              | EradicateChecks.From_is_false_on_null ->
                   if TypeAnnotation.get_value Annotations.Nullable ta then
-                    set_flag e' Annotations.Nullable false
+                    set_flag e' Annotations.Nullable false typestate2
                   else typestate2
             end
 

infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java

@@ -9,11 +9,14 @@
 
 package codetoanalyze.java.eradicate;
 
+import android.text.TextUtils;
 import com.google.common.base.Preconditions;
 
 import java.lang.System;
 import javax.annotation.Nullable;
 import com.facebook.infer.annotation.Assertions;
+import com.facebook.infer.annotation.FalseOnNull;
+import com.facebook.infer.annotation.TrueOnNull;
 
 
 public class NullMethodCall {
@@ -239,5 +242,55 @@ public class NullMethodCall {
     int n = s.length();
   }
 
+
+  static class MyTextUtils {
+
+    @TrueOnNull
+    static boolean isEmpty(@Nullable java.lang.CharSequence s) {
+      return s == null || s.equals("");
+    }
+
+    @FalseOnNull
+    static boolean isNotEmpty(@Nullable java.lang.CharSequence s) {
+      return s != null && s.length() > 0;
+    }
+  }
+
+  class TestTextUtilsIsEmpty {
+    void textUtilsNotIsEmpty(@Nullable CharSequence s) {
+      if (!TextUtils.isEmpty(s)) {
+        s.toString(); // OK
+      }
+    }
+
+    void textUtilsIsEmpty(@Nullable CharSequence s) {
+      if (TextUtils.isEmpty(s)) {
+        s.toString(); // BAD
+      }
+    }
+
+    void myTextUtilsNotIsEmpty(@Nullable CharSequence s) {
+      if (!MyTextUtils.isEmpty(s)) {
+        s.toString(); // OK
+      }
+    }
+
+    void myTextUtilsIsEmpty(@Nullable CharSequence s) {
+      if (MyTextUtils.isEmpty(s)) {
+        s.toString(); // BAD
+      }
+    }
+    void myTextUtilsIsNotEmpty(@Nullable CharSequence s) {
+      if (MyTextUtils.isNotEmpty(s)) {
+        s.toString(); // OK
+      }
+    }
+
+    void myTextUtilsNotIsNotEmpty(@Nullable CharSequence s) {
+      if (!MyTextUtils.isNotEmpty(s)) {
+        s.toString(); // BAD
+      }
+    }
+  }
 }
 

infer/tests/endtoend/java/eradicate/NullMethodCallTest.java

@@ -46,6 +46,9 @@ public class NullMethodCallTest {
         "testFieldAssignmentIfThenElse",
         "testExceptionPerInstruction",
         "testSystemGetPropertyReturn",
+        "textUtilsIsEmpty",
+        "myTextUtilsIsEmpty",
+        "myTextUtilsNotIsNotEmpty",
     };
     assertThat(
         "Results should contain " + NULL_METHOD_CALL,