pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[Loop-hoisting] Add more models for invariant analysis

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D9497910

fbshipit-source-id: 765c75c9b
master
Ezgi Çiçek 6 years ago committed by Facebook Github Bot
parent bfab195d08
commit b2e7a785ba
5 changed files with 121 additions and 17 deletions
Show Stats Download Patch File Download Diff File

16
infer/src/absint/PatternMatch.ml
Unescape View File

@ -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

19
infer/src/absint/PatternMatch.mli
Unescape View File

@ -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 *)

46
infer/src/checkers/invariantModels.ml
Unescape View File

@ -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

39
infer/tests/codetoanalyze/java/hoisting/Hoist.java
Unescape View File

@ -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;
}
}

18
infer/tests/codetoanalyze/java/hoisting/issues.exp
Unescape View File

@ -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]

Write Preview
Loading…
Cancel
Save