diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 29d898f32..6ad572942 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -630,6 +630,45 @@ module JavaCollection = struct in let astate = PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate in [ExecutionDomain.ContinueProgram astate] + + + (* writes to arr[index]-> new_elem *) + let add_at coll (index, _) (new_elem, new_elem_hist) : model = + fun _ ~callee_procname:_ location ~ret:_ astate -> + let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in + let* astate, arr = GenericArrayBackedCollection.eval location coll astate in + let+ astate = + PulseOperations.write_arr_index location ~ref:arr ~index + ~obj:(new_elem, event :: new_elem_hist) + astate + in + [ExecutionDomain.ContinueProgram astate] + + + (* writes to arr[index]-> new_elem where index is a fresh address *) + let add coll new_elem : model = + let index = AbstractValue.mk_fresh () in + add_at coll (index, []) new_elem + + + (* writes to arr[index]-> fresh_elem *) + let remove_at coll (index, _) : model = + fun _ ~callee_procname:_ location ~ret:_ astate -> + let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in + let* astate, arr = GenericArrayBackedCollection.eval location coll astate in + let fresh_elem = AbstractValue.mk_fresh () in + let+ astate = + PulseOperations.write_arr_index location ~ref:arr ~index + ~obj:(fresh_elem, event :: snd arr) + astate + in + [ExecutionDomain.ContinueProgram astate] + + + (* writes to arr[index]-> fresh_elem where index is fresh *) + let remove coll : model = + let index = AbstractValue.mk_fresh () in + remove_at coll (index, []) end module StringSet = Caml.Set.Make (String) @@ -759,6 +798,14 @@ module ProcNameDispatcher = struct ; -"std" &:: "vector" &:: "shrink_to_fit" <>$ capt_arg_payload $--> StdVector.invalidate_references ShrinkToFit ; -"std" &:: "vector" &:: "push_back" <>$ capt_arg_payload $+...$--> StdVector.push_back + ; +PatternMatch.implements_collection + &:: "add" <>$ capt_arg_payload $+ capt_arg_payload $--> JavaCollection.add + ; +PatternMatch.implements_list &:: "add" <>$ capt_arg_payload $+ capt_arg_payload + $+ capt_arg_payload $--> JavaCollection.add_at + ; +PatternMatch.implements_collection + &:: "remove" <>$ capt_arg_payload $+ any_arg $--> JavaCollection.remove + ; +PatternMatch.implements_list &:: "remove" <>$ capt_arg_payload $+ capt_arg_payload + $+ any_arg $--> JavaCollection.remove_at ; +PatternMatch.implements_collection &::+ (fun _ str -> StringSet.mem str pushback_modeled) <>$ capt_arg_payload $+...$--> StdVector.push_back diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index 6fbffe118..6e3667f66 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -159,6 +159,12 @@ class PurityModeled { } } + String add_impure(ArrayList list) { + Integer el = list.get(0); + list.add(4); + return el.toString(); + } + void append_impure(StringBuilder strBuilder) { strBuilder.append("JavaGuru"); } @@ -210,9 +216,9 @@ class PurityModeled { } } - void vector_invalidation_impure(ArrayList list) { + void remove_all_directly_impure(ArrayList list) { for (Integer el : list) { - list.remove(el); // bad, must remove via iterator + list.remove(el); // bad, must remove via iterator. } } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 638a19892..a2a55458d 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -15,6 +15,7 @@ codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java. 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.add_impure(java.util.ArrayList):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.add_impure(ArrayList),parameter `list` modified 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.call_set_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_set_impure(ArrayList),when calling `void PurityModeled.list_set_impure(ArrayList)` here,parameter `list` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_timing_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_timing_symb_impure(int),when calling `void PurityModeled.timing_call_in_loop_symb_impure(int)` here,call to skipped function long System.nanoTime() occurs here] @@ -29,6 +30,7 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loo 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_directly_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_all_directly_impure(ArrayList),parameter `list` 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] @@ -37,8 +39,6 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_iterator_im 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]