diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 9d8ccfe81..1306c4a11 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -1186,9 +1186,9 @@ module AliasMap = struct else x - let add_zero_size_alias ~size ~i ~arr x = - add_alias ~lhs:(KeyLhs.of_loc size) ~rhs:arr - (AliasTarget.Size {alias_typ= Eq; i; java_tmp= None}) + let add_size_alias ~lhs ~lhs_v ~arr ~arr_size x = + add_alias ~lhs:(KeyLhs.of_loc lhs) ~rhs:arr + (AliasTarget.Size {alias_typ= Eq; i= IntLit.sub lhs_v arr_size; java_tmp= None}) x @@ -1343,12 +1343,12 @@ module Alias = struct update_size_alias locs a ~f:(fun loc acc -> lift_map (AliasMap.incr_or_not_size_alias loc) acc) - let add_empty_size_alias : Loc.t -> IntLit.t -> PowLoc.t -> t -> t = + let add_size_alias : Loc.t -> IntLit.t -> (Loc.t * IntLit.t) list -> t -> t = fun loc i arr_locs prev -> - let accum_empty_size_alias arr_loc acc = - lift_map (AliasMap.add_zero_size_alias ~size:loc ~i ~arr:arr_loc) acc + let accum_size_alias acc (arr_loc, arr_size) = + lift_map (AliasMap.add_size_alias ~lhs:loc ~lhs_v:i ~arr:arr_loc ~arr_size) acc in - PowLoc.fold accum_empty_size_alias arr_locs (lift_map (AliasMap.forget loc) prev) + List.fold arr_locs ~init:(lift_map (AliasMap.forget loc) prev) ~f:accum_size_alias let add_iterator_offset_alias : Ident.t -> PowLoc.t -> t -> t = @@ -1888,11 +1888,14 @@ module MemReach = struct | Exp.Const (Const.Cint i) when IntLit.iszero i || IntLit.isone i -> let arr_locs = let add_arr l v acc = - if Itv.is_zero (Val.array_sizeof v) then PowLoc.add l acc else acc + let size = Val.array_sizeof v in + if Itv.is_zero size then (l, IntLit.zero) :: acc + else if Itv.is_one size then (l, IntLit.one) :: acc + else acc in - MemPure.fold add_arr m.mem_pure PowLoc.empty + MemPure.fold add_arr m.mem_pure [] in - {m with alias= Alias.add_empty_size_alias loc i arr_locs m.alias} + {m with alias= Alias.add_size_alias loc i arr_locs m.alias} | _ -> {m with alias= Alias.store_simple loc e m.alias} diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java index cea94ce55..7b058ad18 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java @@ -94,6 +94,28 @@ class ArrayListTest { } } + void add_in_loop_by_param4_ok(ArrayList b) { + ArrayList a = new ArrayList<>(); + a.add(0); + if (b.size() > 0) { + for (int i = 1; i < b.size(); i++) { + a.add(0); + } // a.size = b.size + int j = a.get(b.size() - 1); + } + } + + void add_in_loop_by_param4_bad(ArrayList b) { + ArrayList a = new ArrayList<>(); + a.add(0); + if (b.size() > 0) { + for (int i = 1; i < b.size(); i++) { + a.add(0); + } // a.size = b.size + int j = a.get(b.size() + 1); + } + } + void add_in_loop_iterator_ok(ArrayList b) { ArrayList a = new ArrayList<>(); for (Integer i : b) { diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 89fae33b9..3e588aec6 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -11,6 +11,7 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_and_remov codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 6 Size: 5] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param2_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,Assignment,,Assignment,Array declaration,Array access: Offset: [0, b.length] Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param3_bad(java.util.ArrayList):void, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Array declaration,Assignment,,Array declaration,Assignment,Array declaration,Array access: Offset: [-1+max(1, b.length), b.length - 1] Size: -1+max(1, b.length)] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param4_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Array declaration,Assignment,,Array declaration,Assignment,Array declaration,Array access: Offset: [1+max(1, b.length), b.length + 1] Size: max(1, b.length)] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Array declaration,Assignment,,Parameter `b.elements[*]`,Assignment,Array declaration,Array access: Offset: b.length + 1 Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator2_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,Assignment,,Parameter `b.elements[*]`,Array access: Offset: [0, b.length] Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `b.elements[*]`,Assignment,,Array declaration,Array access: Offset: b.length + 1 Size: b.length]