From cb9bb2a73ceae180498cde08de2e2114907e0859 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 19 Dec 2019 07:36:04 -0800 Subject: [PATCH] [pulse] Add simplified models for Java iterators and `Object.equals` Summary: In order to improve the impurity analysis, this diff adds models for - `hasNext()` and - `Object.equals()` modeled as returning a non-deterministic value (havoc_id) - `next()` modeled as `StdVector.get` with a fresh index - `iterator` modeled as just returning the underlying list Reviewed By: jvillard Differential Revision: D19177392 fbshipit-source-id: 0babb037a --- infer/src/pulse/PulseModels.ml | 17 ++++++++++++++++- .../codetoanalyze/java/impurity/Localities.java | 4 ++-- .../codetoanalyze/java/impurity/issues.exp | 6 ++---- 3 files changed, 20 insertions(+), 7 deletions(-) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 7c76740e9..736dae915 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -50,6 +50,12 @@ module Misc = struct let skip : model = fun ~caller_summary:_ _ ~ret:_ astate -> Ok [astate] + let nondet ~fn_name : model = + fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> + let event = ValueHistory.Call {f= Model fn_name; location; in_call= []} in + Ok [PulseOperations.havoc_id ret_id [event] astate] + + let id_first_arg arg_access_hist : model = fun ~caller_summary:_ _ ~ret astate -> Ok [PulseOperations.write_id (fst ret) arg_access_hist astate] @@ -404,7 +410,16 @@ module ProcNameDispatcher = struct ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve ; +PatternMatch.implements_collection &:: "get" <>$ capt_arg_payload $+ capt_arg_payload - $--> StdVector.at ~desc:"Collection.get()" ] + $--> StdVector.at ~desc:"Collection.get()" + ; +PatternMatch.implements_iterator &:: "hasNext" + &--> Misc.nondet ~fn_name:"Iterator.hasNext()" + ; +PatternMatch.implements_lang "Object" + &:: "equals" + &--> Misc.nondet ~fn_name:"Object.equals" + ; +PatternMatch.implements_lang "Iterable" + &:: "iterator" <>$ capt_arg_payload $+...$--> Misc.id_first_arg + ; ( +PatternMatch.implements_iterator &:: "next" <>$ capt_arg_payload + $!--> fun x -> StdVector.at ~desc:"Iterator.next" x (AbstractValue.mk_fresh (), []) ) ] end let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args diff --git a/infer/tests/codetoanalyze/java/impurity/Localities.java b/infer/tests/codetoanalyze/java/impurity/Localities.java index 4aeea2947..5d62a57c4 100644 --- a/infer/tests/codetoanalyze/java/impurity/Localities.java +++ b/infer/tests/codetoanalyze/java/impurity/Localities.java @@ -9,7 +9,7 @@ import java.util.Iterator; class Localities { // @pure - boolean contains_pure_FP(Integer i, ArrayList list) { + boolean contains_pure(Integer i, ArrayList list) { Iterator listIterator = list.iterator(); while (listIterator.hasNext()) { Integer el = listIterator.next(); @@ -74,7 +74,7 @@ class Localities { } // @pure, @loc:{} - int length_pure_FP(ArrayList list) { + int length_pure(ArrayList list) { Counter c = new Counter(); for (Integer i : list) { c.inc_impure(); diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index a016ad5bf..76072d7e7 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -5,14 +5,12 @@ codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_ codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.incr(GlobalTest$Foo,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` of void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` modified here] codetoanalyze/java/impurity/Localities.java, Localities$Counter.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Counter.inc_impure(),parameter `this` of void Localities$Counter.inc_impure(),parameter `this` modified here] codetoanalyze/java/impurity/Localities.java, Localities$Foo.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Foo.inc_impure(),parameter `this` of void Localities$Foo.inc_impure(),parameter `this` modified here] -codetoanalyze/java/impurity/Localities.java, Localities.contains_pure_FP(java.lang.Integer,java.util.ArrayList):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.contains_pure_FP(Integer,ArrayList),parameter `i` of boolean Localities.contains_pure_FP(Integer,ArrayList),parameter `i` modified here,parameter `list` of boolean Localities.contains_pure_FP(Integer,ArrayList),parameter `list` modified here] codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_impure(int[],int),parameter `a` of boolean Localities.copy_ref_impure(int[],int),assigned,parameter `a` modified here] 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` of Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),assigned,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` of Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),assigned,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` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here,parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` 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),parameter `list` of void Localities.incrementAll_impure(ArrayList),parameter `list` modified here] -codetoanalyze/java/impurity/Localities.java, Localities.length_pure_FP(java.util.ArrayList):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int Localities.length_pure_FP(ArrayList),parameter `list` of int Localities.length_pure_FP(ArrayList),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` of void Localities.makeAllZero_impure(ArrayList),parameter `list` 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),parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here,parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here,parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here,parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here,parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here,parameter `list` of void Localities.incrementAll_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),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` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,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` of void Localities.modify_first_el_impure(ArrayList),passed as argument to `Collection.get()` (modelled),return from call to `Collection.get()` (modelled),assigned,assigned,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),parameter `list` of void Localities.modify_via_call_impure(ArrayList),passed as argument to `Localities$Foo Localities.get_first_pure(ArrayList)`,return from call to `Localities$Foo Localities.get_first_pure(ArrayList)`,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` 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[]),parameter `src` of void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` modified here]