[pulse] Brush up Collection/List add and remove models

Summary: The models were too naive before since they invalidated the underlying array completely (copying C++'s push_back model), causing spurious vector invalidation issues in Java. This diff adds more reasonable models.

Reviewed By: skcho

Differential Revision: D21787543

fbshipit-source-id: a5a59ff69

infer/src/pulse/PulseModels.ml

@@ -630,6 +630,45 @@ module JavaCollection = struct
     in
     let astate = PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate in
     [ExecutionDomain.ContinueProgram astate]
+
+
+  (* writes to arr[index]-> new_elem   *)
+  let add_at coll (index, _) (new_elem, new_elem_hist) : model =
+   fun _ ~callee_procname:_ location ~ret:_ astate ->
+    let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in
+    let* astate, arr = GenericArrayBackedCollection.eval location coll astate in
+    let+ astate =
+      PulseOperations.write_arr_index location ~ref:arr ~index
+        ~obj:(new_elem, event :: new_elem_hist)
+        astate
+    in
+    [ExecutionDomain.ContinueProgram astate]
+
+
+  (* writes to arr[index]-> new_elem where index is a fresh address *)
+  let add coll new_elem : model =
+    let index = AbstractValue.mk_fresh () in
+    add_at coll (index, []) new_elem
+
+
+  (* writes to arr[index]-> fresh_elem   *)
+  let remove_at coll (index, _) : model =
+   fun _ ~callee_procname:_ location ~ret:_ astate ->
+    let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in
+    let* astate, arr = GenericArrayBackedCollection.eval location coll astate in
+    let fresh_elem = AbstractValue.mk_fresh () in
+    let+ astate =
+      PulseOperations.write_arr_index location ~ref:arr ~index
+        ~obj:(fresh_elem, event :: snd arr)
+        astate
+    in
+    [ExecutionDomain.ContinueProgram astate]
+
+
+  (* writes to arr[index]-> fresh_elem where index is fresh *)
+  let remove coll : model =
+    let index = AbstractValue.mk_fresh () in
+    remove_at coll (index, [])
 end
 
 module StringSet = Caml.Set.Make (String)
@@ -759,6 +798,14 @@ module ProcNameDispatcher = struct
         ; -"std" &:: "vector" &:: "shrink_to_fit" <>$ capt_arg_payload
           $--> StdVector.invalidate_references ShrinkToFit
         ; -"std" &:: "vector" &:: "push_back" <>$ capt_arg_payload $+...$--> StdVector.push_back
+        ; +PatternMatch.implements_collection
+          &:: "add" <>$ capt_arg_payload $+ capt_arg_payload $--> JavaCollection.add
+        ; +PatternMatch.implements_list &:: "add" <>$ capt_arg_payload $+ capt_arg_payload
+          $+ capt_arg_payload $--> JavaCollection.add_at
+        ; +PatternMatch.implements_collection
+          &:: "remove" <>$ capt_arg_payload $+ any_arg $--> JavaCollection.remove
+        ; +PatternMatch.implements_list &:: "remove" <>$ capt_arg_payload $+ capt_arg_payload
+          $+ any_arg $--> JavaCollection.remove_at
         ; +PatternMatch.implements_collection
           &::+ (fun _ str -> StringSet.mem str pushback_modeled)
           <>$ capt_arg_payload $+...$--> StdVector.push_back

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

@@ -159,6 +159,12 @@ class PurityModeled {
     }
   }
 
+  String add_impure(ArrayList<Integer> list) {
+    Integer el = list.get(0);
+    list.add(4);
+    return el.toString();
+  }
+
   void append_impure(StringBuilder strBuilder) {
     strBuilder.append("JavaGuru");
   }
@@ -210,9 +216,9 @@ class PurityModeled {
     }
   }
 
-  void vector_invalidation_impure(ArrayList<Integer> list) {
+  void remove_all_directly_impure(ArrayList<Integer> list) {
     for (Integer el : list) {
-      list.remove(el); // bad, must remove via iterator
+      list.remove(el); // bad, must remove via iterator.
     }
   }
 

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

@@ -15,6 +15,7 @@ codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java.
 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` 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),when calling `void Localities$Foo.inc_impure()` here,parameter `list` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.newHashCode_impure():int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int Localities.newHashCode_impure(),call to skipped function int Object.hashCode() occurs here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.add_impure(java.util.ArrayList):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.add_impure(ArrayList),parameter `list` modified here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.append_impure(java.lang.StringBuilder):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.append_impure(StringBuilder),parameter `strBuilder` modified here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_set_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_set_impure(ArrayList),when calling `void PurityModeled.list_set_impure(ArrayList)` here,parameter `list` modified here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_timing_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_timing_symb_impure(int),when calling `void PurityModeled.timing_call_in_loop_symb_impure(int)` here,call to skipped function long System.nanoTime() occurs here]
@@ -29,6 +30,7 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loo
 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_directly_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_all_directly_impure(ArrayList),parameter `list` 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]
@@ -37,8 +39,6 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_iterator_im
 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]