From 7ca2fcc948e99b8e457ad588ad45774d22d813d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 19 Mar 2020 07:31:23 -0700 Subject: [PATCH] [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 | 2 ++ infer/src/pulse/PulseModels.ml | 9 ++++++++- .../java/impurity/Localities.java | 18 ++++++++++++++++++ .../java/impurity/PurityModeled.java | 18 +++++++++++++++++- .../codetoanalyze/java/impurity/issues.exp | 2 +- 5 files changed, 46 insertions(+), 3 deletions(-) diff --git a/infer/src/checkers/purityModels.ml b/infer/src/checkers/purityModels.ml index 0ed87c987..9168500a3 100644 --- a/infer/src/checkers/purityModels.ml +++ b/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*) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 758cc30fe..5f13cc455 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/java/impurity/Localities.java b/infer/tests/codetoanalyze/java/impurity/Localities.java index 5212c5888..2df29bb68 100644 --- a/infer/tests/codetoanalyze/java/impurity/Localities.java +++ b/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]; + } + } } diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index 2c30e5cd0..81f733689 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/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 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(); + } } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index e3ed05e82..3065b1569 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/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]