[pulse] Add more naive Java models

Summary:
This diff naively models the following as `StdVector.push_back`:
- `StringBuilder.append`
- `String.replace`
- `Queue.poll`

It also adds a FN test for `Iterator.next`.

Reviewed By: skcho

Differential Revision: D20469786

fbshipit-source-id: 2d8e8d117

infer/src/pulse/PulseModels.ml

@@ -400,7 +400,9 @@ module ProcNameDispatcher = struct
   let dispatch : (Tenv.t, model, arg_payload) ProcnameDispatcher.Call.dispatcher =
     let open ProcnameDispatcher.Call in
     let match_builtin builtin _ s = String.equal s (Procname.get_method builtin) in
-    let pushback_modeled = StringSet.of_list ["add"; "put"; "addAll"; "putAll"; "remove"] in
+    let pushback_modeled =
+      StringSet.of_list ["add"; "addAll"; "append"; "remove"; "replace"; "poll"; "put"; "putAll"]
+    in
     make_dispatcher
       [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
       ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc
@@ -470,6 +472,15 @@ module ProcNameDispatcher = struct
       ; +PatternMatch.implements_collection
         &::+ (fun _ str -> StringSet.mem str pushback_modeled)
         <>$ capt_arg_payload $+...$--> StdVector.push_back
+      ; +PatternMatch.implements_queue
+        &::+ (fun _ str -> StringSet.mem str pushback_modeled)
+        <>$ capt_arg_payload $+...$--> StdVector.push_back
+      ; +PatternMatch.implements_lang "StringBuilder"
+        &::+ (fun _ str -> StringSet.mem str pushback_modeled)
+        <>$ capt_arg_payload $+...$--> StdVector.push_back
+      ; +PatternMatch.implements_lang "String"
+        &::+ (fun _ str -> StringSet.mem str pushback_modeled)
+        <>$ capt_arg_payload $+...$--> StdVector.push_back
       ; +PatternMatch.implements_iterator &:: "remove" <>$ capt_arg_payload
         $+...$--> StdVector.push_back
       ; +PatternMatch.implements_map &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back

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

@@ -7,6 +7,7 @@
 import java.util.ArrayList;
 import java.util.Enumeration;
 import java.util.Iterator;
+import java.util.Queue;
 
 class PurityModeled {
 
@@ -133,4 +134,29 @@ class PurityModeled {
     ArrayList<String> cloned = (ArrayList<String>) list.clone();
     cloned.add(""); // no change the list
   }
+
+  String replace_impure(String s) {
+    return s.replace('a', 'f');
+  }
+
+  void process_queue_impure(ArrayList<Integer> list, Queue<Integer> queue) {
+    for (Integer el : list) {
+      queue.add(el);
+    }
+  }
+
+  void append_impure(StringBuilder strBuilder) {
+    strBuilder.append("JavaGuru");
+  }
+
+  void append_pure() {
+    StringBuilder strBuilder = new StringBuilder("Core");
+    strBuilder.append("JavaGuru");
+  }
+
+  // Our model of Iterator.next is wrong. It should be modeled as
+  // impure.
+  Integer next_impure_FN(Iterator<Integer> it) {
+    return it.next();
+  }
 }

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

@@ -14,6 +14,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.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.arraycopy_pure_FP(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.arraycopy_pure_FP(int[]),call to skipped function void System.arraycopy(Object,int,Object,int,int) occurs here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_timing_symb_unrelated_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_timing_symb_unrelated_impure(int,int),when calling `void PurityModeled.timing_call_in_loop_symb_impure(int)` here,call to skipped function long System.nanoTime() occurs here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_write_impure(),when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here]
@@ -22,7 +23,9 @@ 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.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_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.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_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.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]