[pulse] Brush up Java iterator models

Summary: Java's iterator models were wrong. This causes `VECTOR_INVALIDATION` errors in fbandroid projects. This diff aims to fix it by modeling Java iterators with a current pointer and an underlying collection array.

Reviewed By: skcho

Differential Revision: D21448322

fbshipit-source-id: 7d44354b5

infer/src/pulse/PulseInvalidation.ml

@@ -37,12 +37,17 @@ let pp_std_vector_function f = function
       F.fprintf f "std::vector::shrink_to_fit"
 
 
+type java_iterator_function = Remove [@@deriving compare]
+
+let pp_java_iterator_function f = function Remove -> F.pp_print_string f "Iterator.remove"
+
 type t =
   | CFree
   | ConstantDereference of IntLit.t
   | CppDelete
   | GoneOutOfScope of Pvar.t * Typ.t
   | StdVector of std_vector_function
+  | JavaIterator of java_iterator_function
 [@@deriving compare]
 
 let issue_type_of_cause = function
@@ -56,7 +61,7 @@ let issue_type_of_cause = function
       IssueType.use_after_delete
   | GoneOutOfScope _ ->
       IssueType.use_after_lifetime
-  | StdVector _ ->
+  | JavaIterator _ | StdVector _ ->
       IssueType.vector_invalidation
 
 
@@ -79,6 +84,8 @@ let describe f cause =
       F.fprintf f "%a whose lifetime has ended" pp_var pvar
   | StdVector std_vector_f ->
       F.fprintf f "was potentially invalidated by `%a()`" pp_std_vector_function std_vector_f
+  | JavaIterator java_iterator_f ->
+      F.fprintf f "was potentially invalidated by `%a()`" pp_java_iterator_function java_iterator_f
 
 
 let pp f invalidation =
@@ -93,3 +100,5 @@ let pp f invalidation =
       describe f invalidation
   | StdVector _ ->
       F.fprintf f "StdVector(%a)" describe invalidation
+  | JavaIterator _ ->
+      F.fprintf f "JavaIterator(%a)" describe invalidation

infer/src/pulse/PulseInvalidation.mli

@@ -21,12 +21,15 @@ type std_vector_function =
 
 val pp_std_vector_function : F.formatter -> std_vector_function -> unit
 
+type java_iterator_function = Remove [@@deriving compare]
+
 type t =
   | CFree
   | ConstantDereference of IntLit.t
   | CppDelete
   | GoneOutOfScope of Pvar.t * Typ.t
   | StdVector of std_vector_function
+  | JavaIterator of java_iterator_function
 [@@deriving compare]
 
 val pp : F.formatter -> t -> unit

infer/src/pulse/PulseModels.ml

@@ -381,20 +381,21 @@ module GenericArrayBackedCollectionIterator = struct
     PulseOperations.eval_access location iterator internal_pointer_access astate
 
 
-  let constructor ~desc this init : model =
-   fun _ ~callee_procname:_ location ~ret:_ astate ->
-    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+  let construct location event ~init ~ref astate =
     let* astate, (arr_addr, arr_hist) = GenericArrayBackedCollection.eval location init astate in
     let* astate =
-      PulseOperations.write_field location ~ref:this GenericArrayBackedCollection.field
+      PulseOperations.write_field location ~ref GenericArrayBackedCollection.field
         ~obj:(arr_addr, event :: arr_hist)
         astate
     in
     let* astate, (p_addr, p_hist) = to_internal_pointer location init astate in
-    PulseOperations.write_field location ~ref:this internal_pointer
-      ~obj:(p_addr, event :: p_hist)
-      astate
-    >>| ExecutionDomain.continue >>| List.return
+    PulseOperations.write_field location ~ref internal_pointer ~obj:(p_addr, event :: p_hist) astate
+
+
+  let constructor ~desc this init : model =
+   fun _ ~callee_procname:_ location ~ret:_ astate ->
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+    construct location event ~init ~ref:this astate >>| ExecutionDomain.continue >>| List.return
 
 
   let operator_star ~desc iter _ ~callee_procname:_ location ~ret astate =
@@ -424,6 +425,61 @@ module GenericArrayBackedCollectionIterator = struct
     >>| ExecutionDomain.continue >>| List.return
 end
 
+module JavaIterator = struct
+  let constructor ~desc init : model =
+   fun _ ~callee_procname:_ location ~ret astate ->
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+    let ref = (AbstractValue.mk_fresh (), [event]) in
+    let+ astate = GenericArrayBackedCollectionIterator.construct location event ~init ~ref astate in
+    let astate = PulseOperations.write_id (fst ret) ref astate in
+    [ExecutionDomain.ContinueProgram astate]
+
+
+  (* {curr -> v_c} is modified to {curr -> v_fresh} and returns array[v_c] *)
+  let next ~desc iter _ ~callee_procname:_ location ~ret astate =
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+    let new_index = AbstractValue.mk_fresh () in
+    let* astate, (curr_index, curr_index_hist) =
+      GenericArrayBackedCollectionIterator.to_internal_pointer location iter astate
+    in
+    let* astate, (curr_elem_val, curr_elem_hist) =
+      GenericArrayBackedCollection.element location iter curr_index astate
+    in
+    let+ astate =
+      PulseOperations.write_field location ~ref:iter
+        GenericArrayBackedCollectionIterator.internal_pointer
+        ~obj:(new_index, event :: curr_index_hist)
+        astate
+    in
+    let astate =
+      PulseOperations.write_id (fst ret) (curr_elem_val, event :: curr_elem_hist) astate
+    in
+    [ExecutionDomain.ContinueProgram astate]
+
+
+  (* {curr -> v_c } is modified to {curr -> v_fresh} and writes to array[v_c] *)
+  let remove ~desc iter _ ~callee_procname:_ location ~ret:_ astate =
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+    let new_index = AbstractValue.mk_fresh () in
+    let* astate, (curr_index, curr_index_hist) =
+      GenericArrayBackedCollectionIterator.to_internal_pointer location iter astate
+    in
+    let* astate =
+      PulseOperations.write_field location ~ref:iter
+        GenericArrayBackedCollectionIterator.internal_pointer
+        ~obj:(new_index, event :: curr_index_hist)
+        astate
+    in
+    let new_elem = AbstractValue.mk_fresh () in
+    let* astate, arr = GenericArrayBackedCollection.eval location iter astate in
+    let+ astate =
+      PulseOperations.write_arr_index location ~ref:arr ~index:curr_index
+        ~obj:(new_elem, event :: curr_index_hist)
+        astate
+    in
+    [ExecutionDomain.ContinueProgram astate]
+end
+
 module StdVector = struct
   let reallocate_internal_array trace vector vector_f location astate =
     let* astate, array_address = GenericArrayBackedCollection.eval location vector astate in
@@ -638,7 +694,7 @@ module ProcNameDispatcher = struct
         &::+ (fun _ str -> StringSet.mem str pushback_modeled)
         <>$ capt_arg_payload $+...$--> StdVector.push_back
       ; +PatternMatch.implements_iterator &:: "remove" <>$ capt_arg_payload
-        $+...$--> StdVector.push_back
+        $+...$--> JavaIterator.remove ~desc:"remove"
       ; +PatternMatch.implements_map &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back
       ; +PatternMatch.implements_map &:: "putAll" <>$ capt_arg_payload $+...$--> StdVector.push_back
       ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve
@@ -656,9 +712,10 @@ module ProcNameDispatcher = struct
         &:: "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 (), []) )
+        &:: "iterator" <>$ capt_arg_payload
+        $+...$--> JavaIterator.constructor ~desc:"Iterable.iterator"
+      ; +PatternMatch.implements_iterator &:: "next" <>$ capt_arg_payload
+        $!--> JavaIterator.next ~desc:"Iterator.next()"
       ; ( +PatternMatch.implements_enumeration
         &:: "nextElement" <>$ capt_arg_payload
         $!--> fun x -> StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), [])

infer/src/pulse/PulseOperations.ml

@@ -212,6 +212,10 @@ let write_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate =
   write_access location addr_trace_ref (FieldAccess field) addr_trace_obj astate
 
 
+let write_arr_index location ~ref:addr_trace_ref ~index ~obj:addr_trace_obj astate =
+  write_access location addr_trace_ref (ArrayAccess (Typ.void, index)) addr_trace_obj astate
+
+
 let havoc_field location addr_trace field trace_obj astate =
   write_field location ~ref:addr_trace field ~obj:(AbstractValue.mk_fresh (), trace_obj) astate
 

infer/src/pulse/PulseOperations.mli

@@ -64,6 +64,15 @@ val write_field :
   -> t access_result
 (** write the edge [ref --.field--> obj] *)
 
+val write_arr_index :
+     Location.t
+  -> ref:AbstractValue.t * ValueHistory.t
+  -> index:AbstractValue.t
+  -> obj:AbstractValue.t * ValueHistory.t
+  -> t
+  -> t access_result
+(** write the edge [ref\[index\]--> obj] *)
+
 val write_deref :
      Location.t
   -> ref:AbstractValue.t * ValueHistory.t

infer/tests/codetoanalyze/java/impurity/PurityModeled.java

@@ -163,12 +163,54 @@ class PurityModeled {
     strBuilder.append("JavaGuru");
   }
 
-  // Our model of Iterator.next is wrong. It should be modeled as
-  // impure.
-  Integer next_impure_FN(Iterator<Integer> it) {
+  Integer next_impure(Iterator<Integer> it) {
     return it.next();
   }
 
+  String remove_iterator_impure(Iterator<Integer> listIterator) {
+    Integer f = listIterator.next();
+    listIterator.remove();
+    return f.toString();
+  }
+
+  String remove_fresh_impure(ArrayList<Integer> list) {
+    Iterator<Integer> listIterator = list.iterator();
+    Integer f = listIterator.next();
+    listIterator.remove();
+    return f.toString();
+  }
+
+  void remove_impure_mult(ArrayList<Integer> list) {
+    String s1 = remove_fresh_impure(list);
+    String s2 = remove_fresh_impure(list);
+  }
+
+  public static void remove_all_impure(ArrayList<Integer> list) {
+    for (Iterator<Integer> iter = list.iterator(); iter.hasNext(); ) {
+      Integer entry = iter.next();
+      iter.remove();
+      System.out.println(entry.toString());
+    }
+  }
+
+  void nested_remove_impure(ArrayList<ArrayList<Integer>> list) {
+    Iterator<ArrayList<Integer>> listIterator = list.iterator();
+    while (listIterator.hasNext()) {
+      ArrayList<Integer> inner_list = listIterator.next();
+      Iterator<Integer> innerListIterator = inner_list.iterator();
+      while (innerListIterator.hasNext()) {
+        Integer el = innerListIterator.next();
+        innerListIterator.remove();
+      }
+    }
+  }
+
+  void vector_invalidation_impure(ArrayList<Integer> list) {
+    for (Integer el : list) {
+      list.remove(el); // bad, must remove via iterator
+    }
+  }
+
   public static final String toString_delete_pure(Object args) {
     StringBuilder builder = new StringBuilder(32).append('{');
     if (args != null) {

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

@@ -25,11 +25,19 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_addall_impure
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_set_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_set_impure(ArrayList),parameter `list` was potentially invalidated by `std::vector::assign()` here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_impure():double, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double PurityModeled.math_random_impure(),call to skipped function double Math.random() occurs here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loop_impure(int):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int PurityModeled.math_random_in_loop_impure(int),when calling `void PurityModeled.call_write_impure()` here,when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here,call to skipped function double Math.random() occurs here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.nested_remove_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.nested_remove_impure(ArrayList),parameter `list` modified here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.next_impure(java.util.Iterator):java.lang.Integer, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Integer PurityModeled.next_impure(Iterator),parameter `it` modified here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.process_queue_impure(java.util.ArrayList,java.util.Queue):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.process_queue_impure(ArrayList,Queue),parameter `queue` modified here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_all_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_all_impure(ArrayList),parameter `list` modified here,call to skipped function void PrintStream.println(String) occurs here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_fresh_impure(java.util.ArrayList):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.remove_fresh_impure(ArrayList),parameter `list` modified here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure(java.util.Iterator):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure(Iterator),parameter `i` modified here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure_mult(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure_mult(ArrayList),when calling `String PurityModeled.remove_fresh_impure(ArrayList)` here,parameter `list` modified here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_iterator_impure(java.util.Iterator):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.remove_iterator_impure(Iterator),parameter `listIterator` modified here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.replace_impure(java.lang.String):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.replace_impure(String),parameter `s` modified here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_impure() with empty pulse summary]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_symb_impure(int),call to skipped function long System.nanoTime() occurs here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.vector_invalidation_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.vector_invalidation_impure(ArrayList),parameter `list` modified here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.vector_invalidation_impure(java.util.ArrayList):void, 1, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `list` of void PurityModeled.vector_invalidation_impure(ArrayList),was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,parameter `list` of void PurityModeled.vector_invalidation_impure(ArrayList),passed as argument to `Iterable.iterator` (modelled),return from call to `Iterable.iterator` (modelled),invalid access occurs here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.write_impure(),call to skipped function void PrintStream.write(byte[],int,int) occurs here]
 codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` modified here]
 codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter `array` modified here]