diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 95fa37ff9..f5c934fbe 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -354,10 +354,26 @@ module StdVector = struct reallocate_internal_array [crumb] vector PushBack location astate >>| List.return end +module JavaCollection = struct + let set coll index new_elem : model = + fun ~caller_summary:_ location ~ret astate -> + let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in + StdVector.element_of_internal_array location coll (fst index) astate + >>= fun (astate, ((old_addr, old_hist) as old_elem)) -> + PulseOperations.write_deref location ~ref:new_elem + ~obj:(old_addr, ValueHistory.Assignment location :: old_hist) + astate + >>= PulseOperations.invalidate_deref location (StdVector Assign) old_elem + >>| fun astate -> [PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate] +end + +module StringSet = Caml.Set.Make (String) + module ProcNameDispatcher = struct let dispatch : (Tenv.t, model, arg_payload) ProcnameDispatcher.Call.dispatcher = let open ProcnameDispatcher.Call in let match_builtin builtin _ s = String.equal s (Procname.get_method builtin) in + let pushback_modeled = StringSet.of_list ["add"; "put"; "addAll"; "putAll"; "remove"] in make_dispatcher [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete @@ -422,19 +438,35 @@ 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 + &::+ (fun _ str -> StringSet.mem str pushback_modeled) + <>$ capt_arg_payload $+...$--> StdVector.push_back + ; +PatternMatch.implements_iterator &:: "remove" <>$ capt_arg_payload + $+...$--> StdVector.push_back + ; +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 ; +PatternMatch.implements_collection &:: "get" <>$ capt_arg_payload $+ capt_arg_payload $--> StdVector.at ~desc:"Collection.get()" + ; +PatternMatch.implements_list &:: "set" <>$ capt_arg_payload $+ capt_arg_payload + $+ capt_arg_payload $--> JavaCollection.set ; +PatternMatch.implements_iterator &:: "hasNext" &--> Misc.nondet ~fn_name:"Iterator.hasNext()" + ; +PatternMatch.implements_enumeration + &:: "hasMoreElements" + &--> Misc.nondet ~fn_name:"Enumeration.hasMoreElements()" ; +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 (), []) ) ] + $!--> fun x -> StdVector.at ~desc:"Iterator.next" x (AbstractValue.mk_fresh (), []) ) + ; ( +PatternMatch.implements_enumeration + &:: "nextElement" <>$ capt_arg_payload + $!--> fun x -> StdVector.at ~desc:"Enumeration.nextElement" 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/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index 901e8f8ae..7e68e6327 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -5,6 +5,8 @@ * LICENSE file in the root directory of this source tree. */ import java.util.ArrayList; +import java.util.Enumeration; +import java.util.Iterator; class PurityModeled { @@ -51,4 +53,32 @@ class PurityModeled { void list_size_pure(ArrayList list) { for (int i = 0; i < list.size(); i++) {} } + + void list_add_impure(ArrayList list) { + list.add("a"); + } + + void list_addall_impure(ArrayList list1, ArrayList list2) { + list1.addAll(list2); + } + + void enum_loop_pure(Enumeration e) { + + for (; e.hasMoreElements(); ) { + Object o = e.nextElement(); + } + } + + void remove_impure(Iterator i) { + while (i.hasNext()) { + if (i.next().equals("Orange")) { + i.remove(); + break; + } + } + } + + void list_set_impure(ArrayList list) { + list.set(0, "e"); + } } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index bbb22b2ec..ee23a1731 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -16,8 +16,12 @@ codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(j 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.arraycopy_pure_FP(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.arraycopy_pure_FP(int[]),call to skipped function void System.arraycopy(Object,int,Object,int,int) occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_write_impure(),when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_add_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_add_impure(ArrayList),parameter `list` of void PurityModeled.list_add_impure(ArrayList),parameter `list` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_addall_impure(java.util.ArrayList,java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_addall_impure(ArrayList,ArrayList),parameter `list1` of void PurityModeled.list_addall_impure(ArrayList,ArrayList),parameter `list1` modified here] +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` of 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.remove_impure(java.util.Iterator):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure(Iterator),parameter `i` of void PurityModeled.remove_impure(Iterator),parameter `i` modified 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` accessed here,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` of void Test.alias_impure(int[],int,int),assigned,parameter `array` modified here]