[pulse] Revise semantics of TextUtils.is_empty

Summary:
There are two changes:

1/ Fix incorrect merge of two cases (empty and not-empty)

```
let<*> astate_equal_zero = ... in
let<*> astate_not_zero = ... in
[Ok (ContinueProgram astate_equal_zero); Ok (ContinueProgram astate_not_zero)]
```

This was an incorrect merge, because if there is an error in the former
case `astate_equal_zero`, it doesn't even evaluate the latter case
`astate_not_zero`.

2/ Cover all cases precisely. There are actually three cases to cover:

* `TextUtils.is_empty(null) = true`
* `TextUtils.is_empty("") = true`
* `TextUtils.is_empty("abc") = false`

However, in the previous model, it missed the second case.

Reviewed By: jvillard

Differential Revision: D29393579

fbshipit-source-id: e59d9a60d

infer/src/pulse/PulseModels.ml

@@ -614,6 +614,8 @@ module JavaObject = struct
     PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate
 end
 
+let string_length_access = HilExp.Access.FieldAccess PulseOperations.ModeledField.string_length
+
 module StdBasicString = struct
   let internal_string =
     Fieldname.make
@@ -623,8 +625,6 @@ module StdBasicString = struct
 
   let internal_string_access = HilExp.Access.FieldAccess internal_string
 
-  let string_length_access = HilExp.Access.FieldAccess PulseOperations.ModeledField.string_length
-
   let to_internal_string path location bstring astate =
     PulseOperations.eval_access path Read location bstring internal_string_access astate
 
@@ -1476,19 +1476,34 @@ module JavaPreconditions = struct
 end
 
 module Android = struct
-  let text_utils_is_empty ~desc (address, hist) : model =
+  let text_utils_is_empty ~desc ((addr, hist) as addr_hist) : model =
-   fun {location; ret= ret_id, _} astate ->
+   fun {path; 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_null =
+      let<*> astate = PulseArithmetic.prune_eq_zero addr astate in
+      let<+> astate = PulseArithmetic.and_eq_int ret_val IntLit.one astate in
+      PulseOperations.write_id ret_id (ret_val, event :: hist) astate
+    in
+    let astate_not_null =
+      let<*> astate = PulseArithmetic.prune_positive addr astate in
+      let<*> astate, (len_addr, hist) =
+        PulseOperations.eval_access path Read location addr_hist string_length_access astate
+      in
       let astate = PulseOperations.write_id ret_id (ret_val, event :: hist) astate in
-    let<*> astate_equal_zero =
+      let astate_empty =
-      PulseArithmetic.and_eq_int ret_val IntLit.zero astate
+        let<*> astate = PulseArithmetic.prune_eq_zero len_addr astate in
-      >>= PulseArithmetic.prune_positive address
+        let<+> astate = PulseArithmetic.and_eq_int ret_val IntLit.one astate in
+        astate
+      in
+      let astate_not_empty =
+        let<*> astate = PulseArithmetic.prune_positive len_addr astate in
+        let<+> astate = PulseArithmetic.and_eq_int ret_val IntLit.zero astate in
+        astate
       in
-    let<*> astate_not_zero =
+      List.rev_append astate_empty astate_not_empty
-      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)]
+    List.rev_append astate_null astate_not_null
 end
 
 module StringSet = Caml.Set.Make (String)

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

@@ -23,7 +23,7 @@ public class TextUtilsExample {
     }
   }
 
-  public void FN_testTextUtilsIsEmptyEmptyStrBad() {
+  public void testTextUtilsIsEmptyEmptyStrBad() {
     if (TextUtils.isEmpty("")) {
       Object o = null;
       o.toString();

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

@@ -67,4 +67,5 @@ codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.Supp
 codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.shouldReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.FP_testTextUtilsIsEmptyOk(java.lang.String):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyEmptyStrBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyNullBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]

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

@@ -67,4 +67,5 @@ codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.Supp
 codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.shouldReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.FP_testTextUtilsIsEmptyOk(java.lang.String):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyEmptyStrBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyNullBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]