diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 4e6eb15e7..e2a610a4f 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -320,13 +320,17 @@ module ArrayList = struct {exec; check= no_check} - let increment_size_by extra_size alist_id _ ~ret:_ mem = + let change_size_by ~size_f alist_id _ ~ret:_ mem = let alist_v = Dom.Mem.find_stack (Loc.of_id alist_id) mem in let locs = Dom.Val.get_pow_loc alist_v in - Dom.Mem.transform_mem ~f:(fun a -> Dom.Val.plus_a a extra_size) locs mem + Dom.Mem.transform_mem ~f:size_f locs mem - let add alist_id = {exec= increment_size_by Dom.Val.Itv.one alist_id; check= no_check} + let incr_size = Dom.Val.plus_a Dom.Val.Itv.one + + let decr_size size = Dom.Val.minus_a size Dom.Val.Itv.one + + let add alist_id = {exec= change_size_by ~size_f:incr_size alist_id; check= no_check} let get_size alist mem = BoUtils.Exec.get_alist_size (Sem.eval alist mem) mem @@ -341,7 +345,7 @@ module ArrayList = struct let addAll alist_id alist_to_add = let exec _model_env ~ret mem = let to_add_length = get_size alist_to_add mem in - increment_size_by to_add_length alist_id _model_env ~ret mem + change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id _model_env ~ret mem in {exec; check= no_check} @@ -352,13 +356,21 @@ module ArrayList = struct 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} + {exec= change_size_by ~size_f:incr_size alist_id; check} + + + let remove_at_index alist_id index_exp = + let check {pname; location} mem cond_set = + let array_exp = Exp.Var alist_id in + BoUtils.Check.arraylist_access ~array_exp ~index_exp mem pname location cond_set + in + {exec= change_size_by ~size_f:decr_size alist_id; check} let addAll_at_index alist_id index_exp alist_to_add = let exec _model_env ~ret mem = let to_add_length = get_size alist_to_add mem in - increment_size_by to_add_length alist_id _model_env ~ret mem + change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id _model_env ~ret mem in let check {pname; location} mem cond_set = let array_exp = Exp.Var alist_id in @@ -411,6 +423,8 @@ module Call = struct $--> 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" &:: "remove" <>$ capt_var_exn $+ capt_exp + $--> ArrayList.remove_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/tests/codetoanalyze/java/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java index d5bd6edfc..26cc7e62b 100644 --- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java @@ -143,4 +143,46 @@ public class ArrayListTest { list.set(1, 10); } + + public void arraylist_remove_overrun_bad() { + ArrayList list = new ArrayList(); + list.add(0); + list.remove(1); + } + + public void arraylist_remove_ok() { + ArrayList list = new ArrayList(); + list.add(0); + list.add(1); + list.remove(0); + list.get(0); + + } + + + public void arraylist_remove_bad() { + ArrayList list = new ArrayList(); + list.add(0); + list.add(1); + list.remove(0); + list.get(1); + + } + + + // we can't set the size of the list to 10 because it depends on how + // many times the loop is executed. Should be fixed once we have + // relational domain working. + public void arraylist_remove_in_loop_Good_FP() { + ArrayList list = new ArrayList(); + for (int i = 0; i < 10; ++i) { + list.add(i); + } + for (int i = 0, size = list.size(); i < size; ++i) { + list.remove(i); + } + + } + + } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 3ba93942d..aebb841a3 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -12,6 +12,10 @@ codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_ 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_remove_bad(), 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_remove_in_loop_Good_FP(), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_remove_in_loop_Good_FP(), 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_remove_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_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]