From b2e7a785ba3596fa72414402b6c850956e0c567a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 3 Sep 2018 06:50:27 -0700 Subject: [PATCH] [Loop-hoisting] Add more models for invariant analysis Reviewed By: mbouaziz Differential Revision: D9497910 fbshipit-source-id: 765c75c9b --- infer/src/absint/PatternMatch.ml | 16 +++++++ infer/src/absint/PatternMatch.mli | 19 ++++++++ infer/src/checkers/invariantModels.ml | 46 +++++++++++++++++-- .../codetoanalyze/java/hoisting/Hoist.java | 39 ++++++++++++++-- .../codetoanalyze/java/hoisting/issues.exp | 18 ++++---- 5 files changed, 121 insertions(+), 17 deletions(-) diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index fe0b2099f..a7ef8e527 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -58,6 +58,22 @@ let implements_iterator = implements "java.util.Iterator" let implements_collection = implements "java.util.Collection" +let implements_pseudo_collection t s = + implements "android.util.SparseArray" t s + || implements "android.util.SparseIntArray" t s + || implements "com.moblica.common.xmob.utils.IntArrayList" t s + + +let implements_enumeration = implements "java.util.Enumeration" + +let implements_io class_name = implements ("java.io." ^ class_name) + +let implements_map = implements "java.util.Map" + +let implements_queue = implements "java.util.Queue" + +let implements_lang class_name = implements ("java.lang." ^ class_name) + (** The type the method is invoked on *) let get_this_type proc_attributes = match proc_attributes.ProcAttributes.formals with (_, t) :: _ -> Some t | _ -> None diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli index f1baf2ff2..2396be05c 100644 --- a/infer/src/absint/PatternMatch.mli +++ b/infer/src/absint/PatternMatch.mli @@ -36,6 +36,25 @@ val implements_iterator : Tenv.t -> string -> bool val implements_collection : Tenv.t -> string -> bool (** Check whether class implements a Java's Collection *) +val implements_pseudo_collection : Tenv.t -> string -> bool +(** Check whether class implements a pseudo Collection with support + for get() and size() methods *) + +val implements_enumeration : Tenv.t -> string -> bool +(** Check whether class implements a Java's Enumeration *) + +val implements_io : string -> Tenv.t -> string -> bool +(** Check whether class implements a Java IO *) + +val implements_map : Tenv.t -> string -> bool +(** Check whether class implements a Java's Map *) + +val implements_queue : Tenv.t -> string -> bool +(** Check whether class implements a Java's Queue *) + +val implements_lang : string -> Tenv.t -> string -> bool +(** Check whether class implements a Java's lang *) + val supertype_exists : Tenv.t -> (Typ.Name.t -> Typ.Struct.t -> bool) -> Typ.Name.t -> bool (** Holds iff the predicate holds on a supertype of the named type, including the type itself *) diff --git a/infer/src/checkers/invariantModels.ml b/infer/src/checkers/invariantModels.ml index 6b5761960..5b0ad773e 100644 --- a/infer/src/checkers/invariantModels.ml +++ b/infer/src/checkers/invariantModels.ml @@ -7,17 +7,55 @@ open! IStd -type model = Invariant | Variant +type model = Variant | VariantForHoisting -let is_invariant = function Invariant -> true | Variant -> false +(* Even though functions marked with VariantForHoisting are pure, we + don't want to report them in hoisting. Hence, we model them as + Variant. *) +let is_invariant = function VariantForHoisting -> not Config.loop_hoisting | Variant -> false module Call = struct let dispatch : (Tenv.t, model) ProcnameDispatcher.Call.dispatcher = let open ProcnameDispatcher.Call in make_dispatcher - [ -"__cast" <>--> Invariant + [ -"__cast" <>--> VariantForHoisting ; +PatternMatch.implements_collection &:: "iterator" <>--> Variant ; +PatternMatch.implements_iterator &:: "hasNext" <>--> Variant + ; +PatternMatch.implements_enumeration &:: "hasMoreElements" <>--> Variant + ; +PatternMatch.implements_enumeration &:: "nextElement" <>--> Variant ; +PatternMatch.implements_iterator &:: "next" <>--> Variant - ; +PatternMatch.implements_collection &:: "size" <>--> Invariant ] + ; +PatternMatch.implements_collection &:: "size" <>--> VariantForHoisting + ; +PatternMatch.implements_collection &:: "add" <>--> Variant + ; +PatternMatch.implements_collection &:: "remove" <>--> Variant + ; +PatternMatch.implements_collection &:: "isEmpty" <>--> VariantForHoisting + ; +PatternMatch.implements_collection &:: "get" <>--> VariantForHoisting + ; +PatternMatch.implements_collection &:: "set" <>--> Variant + ; +PatternMatch.implements_pseudo_collection &:: "size" <>--> VariantForHoisting + ; +PatternMatch.implements_pseudo_collection &:: "get" <>--> VariantForHoisting + ; +PatternMatch.implements_map &:: "isEmpty" <>--> VariantForHoisting + ; +PatternMatch.implements_map &:: "put" <>--> Variant + ; +PatternMatch.implements_queue &:: "poll" <>--> Variant + ; +PatternMatch.implements_queue &:: "add" <>--> Variant + ; +PatternMatch.implements_queue &:: "remove" <>--> Variant + ; +PatternMatch.implements_queue &:: "peek" <>--> VariantForHoisting + ; +PatternMatch.implements_lang "Boolean" &:: "valueOf" <>--> VariantForHoisting + ; +PatternMatch.implements_lang "Number" &:: "valueOf" <>--> VariantForHoisting + ; +PatternMatch.implements_lang "Boolean" &:: "toString" <>--> VariantForHoisting + ; +PatternMatch.implements_lang "Number" &:: "toString" <>--> VariantForHoisting + ; +PatternMatch.implements_lang "String" &:: "length" <>--> VariantForHoisting + ; +PatternMatch.implements_lang "String" &:: "equals" <>--> VariantForHoisting + ; +PatternMatch.implements_lang "String" &:: "startsWith" <>--> VariantForHoisting + ; +PatternMatch.implements_lang "String" &:: "valueOf" <>--> VariantForHoisting + ; +PatternMatch.implements_lang "String" &:: "replace" <>--> Variant + ; +PatternMatch.implements_lang "StringBuilder" &:: "append" <>--> Variant + ; +PatternMatch.implements_lang "StringBuilder" &:: "length" <>--> VariantForHoisting + ; +PatternMatch.implements_io "OutputStream" &:: "write" <>--> Variant + ; +PatternMatch.implements_io "InputStream" &:: "read" <>--> Variant + ; +PatternMatch.implements_io "PrintStream" &:: "print" <>--> Variant + ; +PatternMatch.implements_io "PrintStream" &:: "println" <>--> Variant + ; +PatternMatch.implements_io "Reader" &:: "read" <>--> Variant + ; +PatternMatch.implements_io "BufferedReader" &:: "readLine" <>--> Variant + ; -"__new" <>--> Variant + ; +(fun _ name -> BuiltinDecl.is_declared (Typ.Procname.from_string_c_fun name)) + <>--> VariantForHoisting ] end diff --git a/infer/tests/codetoanalyze/java/hoisting/Hoist.java b/infer/tests/codetoanalyze/java/hoisting/Hoist.java index a7f0202ac..c5b37a445 100644 --- a/infer/tests/codetoanalyze/java/hoisting/Hoist.java +++ b/infer/tests/codetoanalyze/java/hoisting/Hoist.java @@ -4,6 +4,9 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. */ + +import java.util.ArrayList; + class Hoist { int foo(int x, int y) { @@ -33,9 +36,8 @@ class Hoist { } } - // it is ok to move fun call to a temp. var - void reassigned_temp_hoist(int size) { + void reassigned_temp_hoist(int size) { int x = 10; int y = 5; int d = 0; @@ -46,7 +48,7 @@ class Hoist { } // it is ok to just hoist function call into a temp var. - void used_in_loop_body_before_def_temp_hoist(int size, int[] M) { + void used_in_loop_body_before_def_temp_hoist(int size, int[] M) { int x = 10; int y = 5; int d = 20; @@ -116,7 +118,6 @@ class Hoist { } } - // y = ... can be taken out of the inner loop void nested_loop_hoist(int size, int x, int y) { int i = 0; @@ -140,4 +141,34 @@ class Hoist { i++; } } + + void new_dont_hoist(ArrayList list) { + + for (int i = 0; i < 10; i++) { + list = new ArrayList(); + } + } + + // Tests for built-in declarations + + void get_array_length_dont_hoist(int[] array) { + int k = 0; + for (int i = 0; i < 10; i++) { + k = k + array.length; + } + } + + interface Nothing {} + + class Foo {} + + class EmptyFoo extends Foo implements Nothing {} + + boolean instanceof_dont_hoist(EmptyFoo empty) { + boolean k = false;; + for (int i = 0; i < 10; i++) { + k = empty instanceof Nothing; + } + return k; + } } diff --git a/infer/tests/codetoanalyze/java/hoisting/issues.exp b/infer/tests/codetoanalyze/java/hoisting/issues.exp index f252a3194..1d12aae55 100644 --- a/infer/tests/codetoanalyze/java/hoisting/issues.exp +++ b/infer/tests/codetoanalyze/java/hoisting/issues.exp @@ -1,9 +1,9 @@ -codetoanalyze/java/hoisting/Hoist.java, Hoist.array_store_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 115] -codetoanalyze/java/hoisting/Hoist.java, Hoist.clash_function_calls_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 23] -codetoanalyze/java/hoisting/Hoist.java, Hoist.legit_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 71] -codetoanalyze/java/hoisting/Hoist.java, Hoist.loop_guard_hoist(int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 63] -codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 126] -codetoanalyze/java/hoisting/Hoist.java, Hoist.reassigned_temp_hoist(int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 43] -codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 32] -codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.bar(int) at line 32] -codetoanalyze/java/hoisting/Hoist.java, Hoist.used_in_loop_body_before_def_temp_hoist(int,int[]):void, 6, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 55] +codetoanalyze/java/hoisting/Hoist.java, Hoist.array_store_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 117] +codetoanalyze/java/hoisting/Hoist.java, Hoist.clash_function_calls_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 26] +codetoanalyze/java/hoisting/Hoist.java, Hoist.legit_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 73] +codetoanalyze/java/hoisting/Hoist.java, Hoist.loop_guard_hoist(int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 65] +codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 127] +codetoanalyze/java/hoisting/Hoist.java, Hoist.reassigned_temp_hoist(int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 45] +codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 35] +codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.bar(int) at line 35] +codetoanalyze/java/hoisting/Hoist.java, Hoist.used_in_loop_body_before_def_temp_hoist(int,int[]):void, 6, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 57]