[pulse] Adding temporary model for Collection.isEmpty()

Summary: Adding temporary model for Collections/Map isEmpty() as an attempt to reduce false positives before we provide a full model for Collections.

Reviewed By: ezgicicek

Differential Revision: D26724085

fbshipit-source-id: d3418c173

infer/src/pulse/PulseModels.ml

@@ -996,6 +996,16 @@ module JavaCollection = struct
   let remove coll : model =
     let index = AbstractValue.mk_fresh () in
     remove_at coll (index, [])
+
+
+  let is_empty (address, hist) : model =
+   fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+    let event = ValueHistory.Call {f= Model "Collections.isEmpty"; location; in_call= []} in
+    let fresh_elem = AbstractValue.mk_fresh () in
+    PulseArithmetic.prune_positive address astate
+    |> PulseArithmetic.and_eq_int fresh_elem IntLit.zero
+    |> PulseOperations.write_id ret_id (fresh_elem, event :: hist)
+    |> ok_continue
 end
 
 module JavaInteger = struct
@@ -1334,6 +1344,10 @@ module ProcNameDispatcher = struct
         ; +map_context_tenv PatternMatch.Java.implements_list
           &:: "remove" <>$ capt_arg_payload $+ capt_arg_payload $+ any_arg
           $--> JavaCollection.remove_at
+        ; +map_context_tenv PatternMatch.Java.implements_collection
+          &:: "isEmpty" <>$ capt_arg_payload $--> JavaCollection.is_empty
+        ; +map_context_tenv PatternMatch.Java.implements_map
+          &:: "isEmpty" <>$ capt_arg_payload $--> JavaCollection.is_empty
         ; +map_context_tenv PatternMatch.Java.implements_collection
           &::+ (fun _ str -> StringSet.mem str pushback_modeled)
           <>$ capt_arg_payload $+...$--> StdVector.push_back

infer/tests/codetoanalyze/java/pulse/Lists.java

@@ -7,11 +7,11 @@
 
 package codetoanalyze.java.infer;
 
-import java.util.List;
+import java.util.*;
 
 class Lists {
 
-  void FP_emptyRemembersOk(List l) {
+  void emptyRemembersOk(List l) {
     boolean empty = l.isEmpty();
     Object o = null;
     if (empty != l.isEmpty()) {
@@ -19,23 +19,19 @@ class Lists {
     }
   }
 
-  void removeInvalidatesNonEmptinessNPE(List l, int i) {
+  void FN_removeInvalidatesNonEmptinessNPEBad(List l) {
-    if (!l.isEmpty()) {
+    l.removeAll(l);
-      l.remove(i);
+    Object o = null;
-      Object o = null;
+    if (l.isEmpty()) {
-      if (l.isEmpty()) {
+      o.toString();
-        o.toString();
-      }
     }
   }
 
-  void clearCausesEmptinessNPE(List l, int i) {
+  void FN_clearCausesEmptinessNPEBad(List l) {
-    if (!l.isEmpty()) {
+    l.clear();
-      l.clear();
+    Object o = null;
-      Object o = null;
+    if (l.isEmpty()) {
-      if (l.isEmpty()) {
+      o.toString();
-        o.toString();
-      }
     }
   }
 
@@ -48,28 +44,34 @@ class Lists {
     return l.isEmpty() ? null : l.get(0);
   }
 
-  void FP_getElementOk(List l) {
+  void getElementOk(List l) {
     if (l.isEmpty()) {
       return;
     }
     getElement(l).toString();
   }
 
-  void getElementNPE(List l) {
+  void FN_getElementNPE() {
+    List l = new ArrayList();
     if (!l.isEmpty()) {
       return;
     }
     getElement(l).toString();
   }
 
-  // don't fully understand why we don't get this one; model should allow it
+  void FP_getElementOk() {
-  void addInvalidatesEmptinessNPE(List l) {
+    List l = new ArrayList();
-    if (l.isEmpty()) {
+    if (!l.isEmpty()) {
-      l.add(0, new Object());
       Object o = null;
-      if (!l.isEmpty()) {
+      o.toString();
-        o.toString();
+    }
-      }
+  }
+
+  void addInvalidatesEmptinessNPEBad(List l) {
+    l.add(0, new Object());
+    Object o = null;
+    if (!l.isEmpty()) {
+      o.toString();
     }
   }
 }

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

@@ -22,12 +22,8 @@ codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerEx
 codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsMethodMaxValueBad():void, 6, 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/InvokeDynamic.java, codetoanalyze.java.infer.InvokeDynamic.invokeDynamicThenNpeBad(java.util.List):void, 7, 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/InvokeDynamic.java, codetoanalyze.java.infer.InvokeDynamic.lambda$npeInLambdaBad$1(java.lang.String,java.lang.String):int, 1, 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/Lists.java, codetoanalyze.java.infer.Lists.FP_emptyRemembersOk(java.util.List):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/Lists.java, codetoanalyze.java.infer.Lists.FP_getElementOk():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/Lists.java, codetoanalyze.java.infer.Lists.FP_getElementOk(java.util.List):void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object Lists.getElement(List)` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object Lists.getElement(List)`,return from call to `Object Lists.getElement(List)`,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/Lists.java, codetoanalyze.java.infer.Lists.addInvalidatesEmptinessNPEBad(java.util.List):void, 4, 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/Lists.java, codetoanalyze.java.infer.Lists.addInvalidatesEmptinessNPE(java.util.List):void, 5, 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/Lists.java, codetoanalyze.java.infer.Lists.clearCausesEmptinessNPE(java.util.List,int):void, 5, 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/Lists.java, codetoanalyze.java.infer.Lists.getElementNPE(java.util.List):void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object Lists.getElement(List)` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object Lists.getElement(List)`,return from call to `Object Lists.getElement(List)`,assigned,invalid access occurs here]
-codetoanalyze/java/pulse/Lists.java, codetoanalyze.java.infer.Lists.removeInvalidatesNonEmptinessNPE(java.util.List,int):void, 5, 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/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars():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/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_derefBoxedGetterAfterCheckShouldNotCauseNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Boolean NullPointerExceptions.getBool()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Boolean NullPointerExceptions.getBool()`,return from call to `Boolean NullPointerExceptions.getBool()`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_derefGetterAfterCheckShouldNotCauseNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object NullPointerExceptions.getObj()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object NullPointerExceptions.getObj()`,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here]