[pulse][purity] Add more naive models for Java

Summary:
- Add more naive pulse models for:
  - `System.arraycopy`
  - `StringBuilder.setLength`
  - `StringBuilder.delete`

- Model the following as pure
  - `SparseArrayCompat.valueAt`
  - `File.get...`

- Add a nice test

Reviewed By: jvillard

Differential Revision: D20513397

fbshipit-source-id: 6d412d13a

infer/src/checkers/purityModels.ml

@@ -81,6 +81,7 @@ module ProcName = struct
       ; +PatternMatch.implements_google "common.base.Preconditions"
         &::+ startsWith "check" <>--> PurityDomain.pure
       ; +PatternMatch.implements_inject "Provider" &:: "get" <>--> PurityDomain.pure
+      ; +PatternMatch.implements_io "File" &::+ startsWith "get" <>--> PurityDomain.pure
       ; +PatternMatch.implements_io "OutputStream" &:: "write" <>--> PurityDomain.impure_global
       ; +PatternMatch.implements_io "InputStream" &:: "read" <>--> PurityDomain.impure_global
       ; +PatternMatch.implements_io "PrintStream" &:: "print" <>--> PurityDomain.impure_global
@@ -97,6 +98,7 @@ module ProcName = struct
         &::+ startsWith "get" <>--> PurityDomain.pure
       ; +PatternMatch.implements_pseudo_collection &:: "size" <>--> PurityDomain.pure
       ; +PatternMatch.implements_pseudo_collection &:: "get" <>--> PurityDomain.pure
+      ; +PatternMatch.implements_pseudo_collection &:: "valueAt" <>--> PurityDomain.pure
       ; +PatternMatch.implements_lang "Math" &:: "random" <>--> PurityDomain.impure_global
       ; +PatternMatch.implements_lang "Math" &::.*--> PurityDomain.pure
         (* for (int|short|byte...)Value*)

infer/src/pulse/PulseModels.ml

@@ -401,7 +401,8 @@ module ProcNameDispatcher = struct
     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"; "addAll"; "append"; "remove"; "replace"; "poll"; "put"; "putAll"]
+      StringSet.of_list
+        ["add"; "addAll"; "append"; "delete"; "remove"; "replace"; "poll"; "put"; "putAll"]
     in
     make_dispatcher
       [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
@@ -426,6 +427,9 @@ module ProcNameDispatcher = struct
       ; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg_payload
         $--> Misc.shallow_copy "std::function::operator="
       ; +PatternMatch.implements_lang "Object" &:: "clone" $ capt_arg_payload $--> JavaObject.clone
+      ; ( +PatternMatch.implements_lang "System"
+        &:: "arraycopy" $ capt_arg_payload $+ any_arg $+ capt_arg_payload
+        $+...$--> fun src dest -> Misc.shallow_copy "System.arraycopy" dest src )
       ; -"std" &:: "atomic" &:: "atomic" <>$ capt_arg_payload $+ capt_arg_payload
         $--> StdAtomicInteger.constructor
       ; -"std" &:: "__atomic_base" &:: "fetch_add" <>$ capt_arg_payload $+ capt_arg_payload
@@ -478,6 +482,9 @@ module ProcNameDispatcher = struct
       ; +PatternMatch.implements_lang "StringBuilder"
         &::+ (fun _ str -> StringSet.mem str pushback_modeled)
         <>$ capt_arg_payload $+...$--> StdVector.push_back
+      ; +PatternMatch.implements_lang "StringBuilder"
+        &:: "setLength" <>$ capt_arg_payload
+        $+...$--> StdVector.invalidate_references ShrinkToFit
       ; +PatternMatch.implements_lang "String"
         &::+ (fun _ str -> StringSet.mem str pushback_modeled)
         <>$ capt_arg_payload $+...$--> StdVector.push_back

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

@@ -182,4 +182,22 @@ class Localities {
   public static boolean call_is_null_pure(Byte a) {
     return is_null_pure(a);
   }
+
+  private static final int MAX_SIZE = 2;
+
+  private static final int[][][] pool = new int[3][2][];
+
+  static int[] get_impure(int size) {
+    if (size > MAX_SIZE) {
+      return new int[size];
+    }
+    int[][] arrays = pool[size];
+    if (arrays[1] != null) {
+      int[] a = arrays[1];
+      arrays[1] = null;
+      return a;
+    } else {
+      return new int[size];
+    }
+  }
 }

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

@@ -4,6 +4,7 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  */
+import java.io.*;
 import java.util.ArrayList;
 import java.util.Enumeration;
 import java.util.Iterator;
@@ -22,7 +23,7 @@ class PurityModeled {
     return 0;
   }
 
-  void arraycopy_pure_FP(int[] src) {
+  void arraycopy_pure(int[] src) {
     int[] dst = {5, 10, 20, 30, 40, 50};
     // copies an array from the specified source array
     System.arraycopy(src, 0, dst, 0, 1);
@@ -159,4 +160,19 @@ class PurityModeled {
   Integer next_impure_FN(Iterator<Integer> it) {
     return it.next();
   }
+
+  public static final String toString_delete_pure(Object args) {
+    StringBuilder builder = new StringBuilder(32).append('{');
+    if (args != null) {
+      if (builder.charAt(builder.length() - 2) == ',') {
+        builder.delete(builder.length() - 2, builder.length());
+      }
+    }
+    builder.append('}').setLength(10);
+    return builder.toString();
+  }
+
+  String getCanonicalPath_pure(File file) throws IOException {
+    return file.getCanonicalPath();
+  }
 }

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

@@ -9,13 +9,13 @@ codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],in
 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` 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` 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` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities.get_impure(int):int[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int[] Localities.get_impure(int),global variable `Localities` 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),when calling `void Localities$Foo.inc_impure()` here,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` 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` 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]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_add_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_add_impure(ArrayList),parameter `list` modified here]