diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 96b283939..4e6eb15e7 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -349,7 +349,8 @@ module ArrayList = struct let add_at_index (alist_id: Ident.t) index_exp = let check {pname; location} mem cond_set = let array_exp = Exp.Var alist_id in - BoUtils.Check.lindex ~array_exp ~index_exp ~is_arraylist_add:true mem pname location cond_set + BoUtils.Check.arraylist_access ~array_exp ~index_exp ~is_arraylist_add:true mem pname + location cond_set in {exec= increment_size_by Dom.Val.Itv.one alist_id; check} @@ -361,7 +362,17 @@ module ArrayList = struct in let check {pname; location} mem cond_set = let array_exp = Exp.Var alist_id in - BoUtils.Check.lindex ~array_exp ~is_arraylist_add:true ~index_exp mem pname location cond_set + BoUtils.Check.arraylist_access ~index_exp ~array_exp ~is_arraylist_add:true mem pname + location cond_set + in + {exec; check} + + + let get_or_set_at_index alist_id index_exp = + let exec _model_env ~ret:_ mem = mem in + let check {pname; location} mem cond_set = + let array_exp = Exp.Var alist_id in + BoUtils.Check.arraylist_access ~index_exp ~array_exp mem pname location cond_set in {exec; check} end @@ -396,6 +407,10 @@ module Call = struct ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at ; -"std" &:: "array" &::.*--> StdArray.no_model + ; -"java.util.ArrayList" &:: "get" <>$ capt_var_exn $+ capt_exp + $--> ArrayList.get_or_set_at_index + ; -"java.util.ArrayList" &:: "set" <>$ capt_var_exn $+ capt_exp $+ any_arg + $--> ArrayList.get_or_set_at_index ; -"java.util.ArrayList" &:: "add" <>$ capt_var_exn $+ any_arg $--> ArrayList.add ; -"java.util.ArrayList" &:: "add" <>$ capt_var_exn $+ capt_exp $+ any_arg $!--> ArrayList.add_at_index diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index b0140dc9b..2718bb2a4 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -203,18 +203,17 @@ module Check = struct check_access ~size ~idx:idx_in_blk ~arr ~idx_traces pname location cond_set - let add_arraylist ~array_exp ~idx mem pname location cond_set = + let arraylist_access ~array_exp ~index_exp ?(is_arraylist_add= false) mem pname location cond_set = + let idx = Sem.eval index_exp mem in let arr = Sem.eval array_exp mem in let idx_traces = Dom.Val.get_traces idx in let size = Exec.get_alist_size arr mem |> Dom.Val.get_itv in let idx = Dom.Val.get_itv idx in - check_access ~size ~idx ~arr ~idx_traces ~is_arraylist_add:true pname location cond_set + check_access ~size ~idx ~arr ~idx_traces ~is_arraylist_add pname location cond_set - let lindex ~array_exp ~index_exp ?(is_arraylist_add= false) mem pname location cond_set = + let lindex ~array_exp ~index_exp mem pname location cond_set = let idx = Sem.eval index_exp mem in - if is_arraylist_add then add_arraylist ~array_exp ~idx mem pname location cond_set - else - let arr = Sem.eval_arr array_exp mem in - array_access ~arr ~idx ~is_plus:true pname location cond_set + let arr = Sem.eval_arr array_exp mem in + array_access ~arr ~idx ~is_plus:true pname location cond_set end diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 6a54b813f..2a593e9ed 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -56,6 +56,10 @@ module Check : sig -> PO.ConditionSet.t -> PO.ConditionSet.t val lindex : + array_exp:Exp.t -> index_exp:Exp.t -> Dom.Mem.astate -> Typ.Procname.t -> Location.t + -> PO.ConditionSet.t -> PO.ConditionSet.t + + val arraylist_access : array_exp:Exp.t -> index_exp:Exp.t -> ?is_arraylist_add:bool -> Dom.Mem.astate -> Typ.Procname.t -> Location.t -> PO.ConditionSet.t -> PO.ConditionSet.t end diff --git a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java index 59a284cd3..d5bd6edfc 100644 --- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java @@ -92,4 +92,55 @@ public class ArrayListTest { } + + public void arraylist_get_underrun_bad() { + ArrayList list = new ArrayList(); + list.get(0); + } + + + public void arraylist_get_overrun_bad() { + ArrayList list = new ArrayList(); + list.add(0); + list.get(2); + } + + + public void arraylist_get_ok() { + ArrayList list = new ArrayList(); + list.add(0); + list.add(1); + list.add(2); + + for (int i = 0, size = list.size(); i < size; ++i) { + list.get(i); + } + + } + + + public void arraylist_set_ok() { + ArrayList list = new ArrayList(); + list.add(0); + list.add(1); + list.add(2); + for (int i = 0, size = list.size(); i < size; ++i) { + list.set(i, i); + } + + } + + + public void arraylist_set_underrun_bad() { + ArrayList list = new ArrayList(); + list.set(0, 10); + } + + + public void arraylist_set_overrun_bad() { + ArrayList list = new ArrayList(); + list.add(0); + list.set(1, 10); + } + } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index af133f420..3ba93942d 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -10,6 +10,10 @@ codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_ codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_add_in_loop_ok(), 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_empty_overrun_bad(), 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, 0]] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_empty_underrun_bad(), 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, -1] Size: [0, 0]] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_get_overrun_bad(), 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [2, 2] Size: [1, 1]] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_get_underrun_bad(), 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_set_overrun_bad(), 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_set_underrun_bad(), 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_arraylist(ArrayList), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * list.length.ub] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_arraylist(ArrayList), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * list.length.ub] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_local_arraylist(ArrayList), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 * list.length.ub]