[pulse] Model for TextUtils.isEmpty()

Summary:
Providing model for the android function TextUtils.isEmpty(). For now,
this always returns false assuming that the given value is not null.

Reviewed By: jvillard

Differential Revision: D26779619

fbshipit-source-id: 3d8e26813

infer/src/pulse/PulseModels.ml

@@ -1078,6 +1078,22 @@ module JavaPreconditions = struct
     PulseArithmetic.prune_positive address astate |> ok_continue
 end
 
+module Android = struct
+  let text_utils_is_empty ~desc (address, hist) : model =
+   fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+    let ret_val = AbstractValue.mk_fresh () in
+    let astate = PulseOperations.write_id ret_id (ret_val, event :: hist) astate in
+    let astate_equal_zero =
+      PulseArithmetic.and_eq_int ret_val IntLit.zero astate
+      |> PulseArithmetic.prune_positive address
+    in
+    let astate_not_zero =
+      PulseArithmetic.and_eq_int ret_val IntLit.one astate |> PulseArithmetic.prune_eq_zero address
+    in
+    [Ok (ContinueProgram astate_equal_zero); Ok (ContinueProgram astate_not_zero)]
+end
+
 module StringSet = Caml.Set.Make (String)
 
 module ProcNameDispatcher = struct
@@ -1411,6 +1427,9 @@ module ProcNameDispatcher = struct
           &:: "nextElement" <>$ capt_arg_payload
           $!--> fun x ->
           StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), []) )
+        ; +map_context_tenv (PatternMatch.Java.implements_android "text.TextUtils")
+          &:: "isEmpty" <>$ capt_arg_payload
+          $--> Android.text_utils_is_empty ~desc:"TextUtils.isEmpty"
         ; -"dispatch_sync" &++> ObjC.dispatch_sync
         ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_create_or_copy
           &--> C.malloc_no_param

infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java

@@ -0,0 +1,40 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+import android.text.TextUtils;
+
+public class TextUtilsExample {
+
+  public void FP_testTextUtilsIsEmptyOk(String s) {
+    if (TextUtils.isEmpty(s)) {
+      Object o = null;
+      o.toString();
+    }
+  }
+
+  public void testTextUtilsIsEmptyBad() {
+    String s = "#@%^&%";
+    if (!TextUtils.isEmpty(s)) {
+      Object o = null;
+      o.toString();
+    }
+  }
+
+  public void testTextUtilsIsEmptyEmptyStrBad() {
+    if (TextUtils.isEmpty("")) {
+      Object o = null;
+      o.toString();
+    }
+  }
+
+  public void testTextUtilsIsEmptyNullBad() {
+    String s = null;
+    if (TextUtils.isEmpty(s)) {
+      Object o = null;
+      o.toString();
+    }
+  }
+}

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

@@ -60,3 +60,7 @@ codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.Supp
 codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.<init>(), 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.FP_shouldNotReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.shouldReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.FP_testTextUtilsIsEmptyOk(java.lang.String):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyEmptyStrBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyNullBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]