[pulse] Add simplified models for Java iterators and `Object.equals`

Summary:
In order to improve the impurity analysis, this diff adds models for

- `hasNext()` and - `Object.equals()` modeled as returning a non-deterministic value (havoc_id)
- `next()` modeled as `StdVector.get` with a fresh index
- `iterator` modeled as just returning the underlying list

Reviewed By: jvillard

Differential Revision: D19177392

fbshipit-source-id: 0babb037a

infer/src/pulse/PulseModels.ml

@@ -50,6 +50,12 @@ module Misc = struct
 
   let skip : model = fun ~caller_summary:_ _ ~ret:_ astate -> Ok [astate]
 
+  let nondet ~fn_name : model =
+   fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
+    let event = ValueHistory.Call {f= Model fn_name; location; in_call= []} in
+    Ok [PulseOperations.havoc_id ret_id [event] astate]
+
+
   let id_first_arg arg_access_hist : model =
    fun ~caller_summary:_ _ ~ret astate ->
     Ok [PulseOperations.write_id (fst ret) arg_access_hist astate]
@@ -404,7 +410,16 @@ module ProcNameDispatcher = struct
       ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve
       ; +PatternMatch.implements_collection
         &:: "get" <>$ capt_arg_payload $+ capt_arg_payload
-        $--> StdVector.at ~desc:"Collection.get()" ]
+        $--> StdVector.at ~desc:"Collection.get()"
+      ; +PatternMatch.implements_iterator &:: "hasNext"
+        &--> Misc.nondet ~fn_name:"Iterator.hasNext()"
+      ; +PatternMatch.implements_lang "Object"
+        &:: "equals"
+        &--> Misc.nondet ~fn_name:"Object.equals"
+      ; +PatternMatch.implements_lang "Iterable"
+        &:: "iterator" <>$ capt_arg_payload $+...$--> Misc.id_first_arg
+      ; ( +PatternMatch.implements_iterator &:: "next" <>$ capt_arg_payload
+        $!--> fun x -> StdVector.at ~desc:"Iterator.next" x (AbstractValue.mk_fresh (), []) ) ]
 end
 
 let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args

infer/tests/codetoanalyze/java/impurity/Localities.java

@@ -9,7 +9,7 @@ import java.util.Iterator;
 
 class Localities {
   // @pure
-  boolean contains_pure_FP(Integer i, ArrayList<Integer> list) {
+  boolean contains_pure(Integer i, ArrayList<Integer> list) {
     Iterator<Integer> listIterator = list.iterator();
     while (listIterator.hasNext()) {
       Integer el = listIterator.next();
@@ -74,7 +74,7 @@ class Localities {
   }
 
   // @pure, @loc:{}
-  int length_pure_FP(ArrayList<Integer> list) {
+  int length_pure(ArrayList<Integer> list) {
     Counter c = new Counter();
     for (Integer i : list) {
       c.inc_impure();

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

@@ -5,14 +5,12 @@ codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_
 codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.incr(GlobalTest$Foo,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` of void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities$Counter.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Counter.inc_impure(),parameter `this` of void Localities$Counter.inc_impure(),parameter `this` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities$Foo.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Foo.inc_impure(),parameter `this` of void Localities$Foo.inc_impure(),parameter `this` modified here]
-codetoanalyze/java/impurity/Localities.java, Localities.contains_pure_FP(java.lang.Integer,java.util.ArrayList):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.contains_pure_FP(Integer,ArrayList),parameter `i` of boolean Localities.contains_pure_FP(Integer,ArrayList),parameter `i` modified here,parameter `list` of boolean Localities.contains_pure_FP(Integer,ArrayList),parameter `list` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_impure(int[],int),parameter `a` of boolean Localities.copy_ref_impure(int[],int),assigned,parameter `a` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.get_f_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo):Localities$Bar, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here,parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here]
-codetoanalyze/java/impurity/Localities.java, Localities.incrementAll_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.incrementAll_impure(ArrayList),parameter `list` of void Localities.incrementAll_impure(ArrayList),parameter `list` modified here]
-codetoanalyze/java/impurity/Localities.java, Localities.length_pure_FP(java.util.ArrayList):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int Localities.length_pure_FP(ArrayList),parameter `list` of int Localities.length_pure_FP(ArrayList),parameter `list` modified here]
-codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.makeAllZero_impure(ArrayList),parameter `list` of void Localities.makeAllZero_impure(ArrayList),parameter `list` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities.incrementAll_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.incrementAll_impure(ArrayList),parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here,parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here,parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here,parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here,parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here,parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.makeAllZero_impure(ArrayList),parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_first_el_impure(ArrayList),parameter `list` of void Localities.modify_first_el_impure(ArrayList),passed as argument to `Collection.get()` (modelled),return from call to `Collection.get()` (modelled),assigned,assigned,parameter `list` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_via_call_impure(ArrayList),parameter `list` of void Localities.modify_via_call_impure(ArrayList),passed as argument to `Localities$Foo Localities.get_first_pure(ArrayList)`,return from call to `Localities$Foo Localities.get_first_pure(ArrayList)`,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.arraycopy_pure_FP(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` of void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` modified here]