diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml index 1cff9abd8..f12360f27 100644 --- a/infer/src/pulse/PulseInvalidation.ml +++ b/infer/src/pulse/PulseInvalidation.ml @@ -37,12 +37,17 @@ let pp_std_vector_function f = function F.fprintf f "std::vector::shrink_to_fit" +type java_iterator_function = Remove [@@deriving compare] + +let pp_java_iterator_function f = function Remove -> F.pp_print_string f "Iterator.remove" + type t = | CFree | ConstantDereference of IntLit.t | CppDelete | GoneOutOfScope of Pvar.t * Typ.t | StdVector of std_vector_function + | JavaIterator of java_iterator_function [@@deriving compare] let issue_type_of_cause = function @@ -56,7 +61,7 @@ let issue_type_of_cause = function IssueType.use_after_delete | GoneOutOfScope _ -> IssueType.use_after_lifetime - | StdVector _ -> + | JavaIterator _ | StdVector _ -> IssueType.vector_invalidation @@ -79,6 +84,8 @@ let describe f cause = F.fprintf f "%a whose lifetime has ended" pp_var pvar | StdVector std_vector_f -> F.fprintf f "was potentially invalidated by `%a()`" pp_std_vector_function std_vector_f + | JavaIterator java_iterator_f -> + F.fprintf f "was potentially invalidated by `%a()`" pp_java_iterator_function java_iterator_f let pp f invalidation = @@ -93,3 +100,5 @@ let pp f invalidation = describe f invalidation | StdVector _ -> F.fprintf f "StdVector(%a)" describe invalidation + | JavaIterator _ -> + F.fprintf f "JavaIterator(%a)" describe invalidation diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli index b15e7b8ed..f7f01c094 100644 --- a/infer/src/pulse/PulseInvalidation.mli +++ b/infer/src/pulse/PulseInvalidation.mli @@ -21,12 +21,15 @@ type std_vector_function = val pp_std_vector_function : F.formatter -> std_vector_function -> unit +type java_iterator_function = Remove [@@deriving compare] + type t = | CFree | ConstantDereference of IntLit.t | CppDelete | GoneOutOfScope of Pvar.t * Typ.t | StdVector of std_vector_function + | JavaIterator of java_iterator_function [@@deriving compare] val pp : F.formatter -> t -> unit diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 87688a272..df71b7323 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -381,20 +381,21 @@ module GenericArrayBackedCollectionIterator = struct PulseOperations.eval_access location iterator internal_pointer_access astate - let constructor ~desc this init : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> - let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let construct location event ~init ~ref astate = let* astate, (arr_addr, arr_hist) = GenericArrayBackedCollection.eval location init astate in let* astate = - PulseOperations.write_field location ~ref:this GenericArrayBackedCollection.field + PulseOperations.write_field location ~ref GenericArrayBackedCollection.field ~obj:(arr_addr, event :: arr_hist) astate in let* astate, (p_addr, p_hist) = to_internal_pointer location init astate in - PulseOperations.write_field location ~ref:this internal_pointer - ~obj:(p_addr, event :: p_hist) - astate - >>| ExecutionDomain.continue >>| List.return + PulseOperations.write_field location ~ref internal_pointer ~obj:(p_addr, event :: p_hist) astate + + + let constructor ~desc this init : model = + fun _ ~callee_procname:_ location ~ret:_ astate -> + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + construct location event ~init ~ref:this astate >>| ExecutionDomain.continue >>| List.return let operator_star ~desc iter _ ~callee_procname:_ location ~ret astate = @@ -424,6 +425,61 @@ module GenericArrayBackedCollectionIterator = struct >>| ExecutionDomain.continue >>| List.return end +module JavaIterator = struct + let constructor ~desc init : model = + fun _ ~callee_procname:_ location ~ret astate -> + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let ref = (AbstractValue.mk_fresh (), [event]) in + let+ astate = GenericArrayBackedCollectionIterator.construct location event ~init ~ref astate in + let astate = PulseOperations.write_id (fst ret) ref astate in + [ExecutionDomain.ContinueProgram astate] + + + (* {curr -> v_c} is modified to {curr -> v_fresh} and returns array[v_c] *) + let next ~desc iter _ ~callee_procname:_ location ~ret astate = + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let new_index = AbstractValue.mk_fresh () in + let* astate, (curr_index, curr_index_hist) = + GenericArrayBackedCollectionIterator.to_internal_pointer location iter astate + in + let* astate, (curr_elem_val, curr_elem_hist) = + GenericArrayBackedCollection.element location iter curr_index astate + in + let+ astate = + PulseOperations.write_field location ~ref:iter + GenericArrayBackedCollectionIterator.internal_pointer + ~obj:(new_index, event :: curr_index_hist) + astate + in + let astate = + PulseOperations.write_id (fst ret) (curr_elem_val, event :: curr_elem_hist) astate + in + [ExecutionDomain.ContinueProgram astate] + + + (* {curr -> v_c } is modified to {curr -> v_fresh} and writes to array[v_c] *) + let remove ~desc iter _ ~callee_procname:_ location ~ret:_ astate = + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let new_index = AbstractValue.mk_fresh () in + let* astate, (curr_index, curr_index_hist) = + GenericArrayBackedCollectionIterator.to_internal_pointer location iter astate + in + let* astate = + PulseOperations.write_field location ~ref:iter + GenericArrayBackedCollectionIterator.internal_pointer + ~obj:(new_index, event :: curr_index_hist) + astate + in + let new_elem = AbstractValue.mk_fresh () in + let* astate, arr = GenericArrayBackedCollection.eval location iter astate in + let+ astate = + PulseOperations.write_arr_index location ~ref:arr ~index:curr_index + ~obj:(new_elem, event :: curr_index_hist) + astate + in + [ExecutionDomain.ContinueProgram astate] +end + module StdVector = struct let reallocate_internal_array trace vector vector_f location astate = let* astate, array_address = GenericArrayBackedCollection.eval location vector astate in @@ -638,7 +694,7 @@ module ProcNameDispatcher = struct &::+ (fun _ str -> StringSet.mem str pushback_modeled) <>$ capt_arg_payload $+...$--> StdVector.push_back ; +PatternMatch.implements_iterator &:: "remove" <>$ capt_arg_payload - $+...$--> StdVector.push_back + $+...$--> JavaIterator.remove ~desc:"remove" ; +PatternMatch.implements_map &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back ; +PatternMatch.implements_map &:: "putAll" <>$ capt_arg_payload $+...$--> StdVector.push_back ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve @@ -656,9 +712,10 @@ module ProcNameDispatcher = struct &:: "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 (), []) ) + &:: "iterator" <>$ capt_arg_payload + $+...$--> JavaIterator.constructor ~desc:"Iterable.iterator" + ; +PatternMatch.implements_iterator &:: "next" <>$ capt_arg_payload + $!--> JavaIterator.next ~desc:"Iterator.next()" ; ( +PatternMatch.implements_enumeration &:: "nextElement" <>$ capt_arg_payload $!--> fun x -> StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), []) diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 4ea03ff72..6aba963ae 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -212,6 +212,10 @@ let write_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate = write_access location addr_trace_ref (FieldAccess field) addr_trace_obj astate +let write_arr_index location ~ref:addr_trace_ref ~index ~obj:addr_trace_obj astate = + write_access location addr_trace_ref (ArrayAccess (Typ.void, index)) addr_trace_obj astate + + let havoc_field location addr_trace field trace_obj astate = write_field location ~ref:addr_trace field ~obj:(AbstractValue.mk_fresh (), trace_obj) astate diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index f512ee44d..67a80d77c 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -64,6 +64,15 @@ val write_field : -> t access_result (** write the edge [ref --.field--> obj] *) +val write_arr_index : + Location.t + -> ref:AbstractValue.t * ValueHistory.t + -> index:AbstractValue.t + -> obj:AbstractValue.t * ValueHistory.t + -> t + -> t access_result +(** write the edge [ref\[index\]--> obj] *) + val write_deref : Location.t -> ref:AbstractValue.t * ValueHistory.t diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index 62dbf2a1a..3c4699226 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -163,12 +163,54 @@ class PurityModeled { strBuilder.append("JavaGuru"); } - // Our model of Iterator.next is wrong. It should be modeled as - // impure. - Integer next_impure_FN(Iterator it) { + Integer next_impure(Iterator it) { return it.next(); } + String remove_iterator_impure(Iterator listIterator) { + Integer f = listIterator.next(); + listIterator.remove(); + return f.toString(); + } + + String remove_fresh_impure(ArrayList list) { + Iterator listIterator = list.iterator(); + Integer f = listIterator.next(); + listIterator.remove(); + return f.toString(); + } + + void remove_impure_mult(ArrayList list) { + String s1 = remove_fresh_impure(list); + String s2 = remove_fresh_impure(list); + } + + public static void remove_all_impure(ArrayList list) { + for (Iterator iter = list.iterator(); iter.hasNext(); ) { + Integer entry = iter.next(); + iter.remove(); + System.out.println(entry.toString()); + } + } + + void nested_remove_impure(ArrayList> list) { + Iterator> listIterator = list.iterator(); + while (listIterator.hasNext()) { + ArrayList inner_list = listIterator.next(); + Iterator innerListIterator = inner_list.iterator(); + while (innerListIterator.hasNext()) { + Integer el = innerListIterator.next(); + innerListIterator.remove(); + } + } + } + + void vector_invalidation_impure(ArrayList list) { + for (Integer el : list) { + list.remove(el); // bad, must remove via iterator + } + } + public static final String toString_delete_pure(Object args) { StringBuilder builder = new StringBuilder(32).append('{'); if (args != null) { diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 7eb9213a1..811613280 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -25,11 +25,19 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_addall_impure codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_set_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_set_impure(ArrayList),parameter `list` was potentially invalidated by `std::vector::assign()` here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_impure():double, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double PurityModeled.math_random_impure(),call to skipped function double Math.random() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loop_impure(int):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int PurityModeled.math_random_in_loop_impure(int),when calling `void PurityModeled.call_write_impure()` here,when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here,call to skipped function double Math.random() occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.nested_remove_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.nested_remove_impure(ArrayList),parameter `list` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.next_impure(java.util.Iterator):java.lang.Integer, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Integer PurityModeled.next_impure(Iterator),parameter `it` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.process_queue_impure(java.util.ArrayList,java.util.Queue):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.process_queue_impure(ArrayList,Queue),parameter `queue` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_all_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_all_impure(ArrayList),parameter `list` modified here,call to skipped function void PrintStream.println(String) occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_fresh_impure(java.util.ArrayList):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.remove_fresh_impure(ArrayList),parameter `list` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure(java.util.Iterator):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure(Iterator),parameter `i` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure_mult(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure_mult(ArrayList),when calling `String PurityModeled.remove_fresh_impure(ArrayList)` here,parameter `list` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_iterator_impure(java.util.Iterator):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.remove_iterator_impure(Iterator),parameter `listIterator` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.replace_impure(java.lang.String):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.replace_impure(String),parameter `s` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_impure() with empty pulse summary] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_symb_impure(int),call to skipped function long System.nanoTime() occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.vector_invalidation_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.vector_invalidation_impure(ArrayList),parameter `list` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.vector_invalidation_impure(java.util.ArrayList):void, 1, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `list` of void PurityModeled.vector_invalidation_impure(ArrayList),was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,parameter `list` of void PurityModeled.vector_invalidation_impure(ArrayList),passed as argument to `Iterable.iterator` (modelled),return from call to `Iterable.iterator` (modelled),invalid access occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.write_impure(),call to skipped function void PrintStream.write(byte[],int,int) occurs here] codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` modified here] codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter `array` modified here]