diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 5e1e1e6f3..cc1c78dfc 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 ~arr 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= IntLit.zero; java_tmp= None}) + (AliasTarget.Size {alias_typ= Eq; i; java_tmp= None}) x @@ -1343,10 +1343,10 @@ 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 -> PowLoc.t -> t -> t = - fun loc arr_locs prev -> + let add_empty_size_alias : Loc.t -> IntLit.t -> PowLoc.t -> 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 ~arr:arr_loc) acc + lift_map (AliasMap.add_zero_size_alias ~size:loc ~i ~arr:arr_loc) acc in PowLoc.fold accum_empty_size_alias arr_locs (lift_map (AliasMap.forget loc) prev) @@ -1864,11 +1864,12 @@ module MemReach = struct fun k m -> AliasTargets.fold accum_simple_alias (Alias.find_id k m.alias) [] - let find_size_alias : Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * Loc.t option) list = + let find_size_alias : + Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * IntLit.t * Loc.t option) list = let accum_size_alias l tgt acc = match tgt with - | AliasTarget.Size {alias_typ; java_tmp} -> - (alias_typ, l, java_tmp) :: acc + | AliasTarget.Size {alias_typ; i; java_tmp} -> + (alias_typ, l, i, java_tmp) :: acc | _ -> acc in @@ -1884,14 +1885,14 @@ module MemReach = struct let store_simple_alias : Loc.t -> Exp.t -> t -> t = fun loc e m -> match e with - | Exp.Const (Const.Cint zero) when IntLit.iszero zero -> + | 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 in MemPure.fold add_arr m.mem_pure PowLoc.empty in - {m with alias= Alias.add_empty_size_alias loc arr_locs m.alias} + {m with alias= Alias.add_empty_size_alias loc i arr_locs m.alias} | _ -> {m with alias= Alias.store_simple loc e m.alias} @@ -2281,7 +2282,8 @@ module Mem = struct fun k -> f_lift_default ~default:[] (MemReach.find_simple_alias k) - let find_size_alias : Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * Loc.t option) list = + let find_size_alias : + Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * IntLit.t * Loc.t option) list = fun k -> f_lift_default ~default:[] (MemReach.find_size_alias k) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index cd01880e8..e5e8c9a1c 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -650,18 +650,23 @@ module Prune = struct let prune_alias_core ~val_prune_eq ~val_prune_le ~make_pruning_exp integer_type_widths x e ({mem} as astate) = List.fold (Mem.find_size_alias x mem) ~init:astate - ~f:(fun astate (alias_typ, lv, java_tmp) -> + ~f:(fun astate (alias_typ, lv, i, java_tmp) -> let array_v = Mem.find lv mem in - let size = - Val.get_array_blk array_v |> ArrayBlk.sizeof |> Val.of_itv - |> Val.set_itv_updated_by_addition + let lhs = + Val.get_array_blk array_v |> ArrayBlk.sizeof + |> Itv.plus (Itv.of_int_lit i) + |> Val.of_itv |> Val.set_itv_updated_by_addition in let rhs = eval integer_type_widths e mem in let prune_target val_prune astate = - let size' = val_prune size rhs in - let array_v' = Val.set_array_length Location.dummy ~length:size' array_v in - let pruning_exp = make_pruning_exp ~lhs:size' ~rhs in - (update_mem_in_prune lv array_v' ~pruning_exp astate, size', pruning_exp) + let lhs' = val_prune lhs rhs in + let array_v' = + Val.set_array_length Location.dummy + ~length:(Val.minus_a lhs' (Val.of_int_lit i)) + array_v + in + let pruning_exp = make_pruning_exp ~lhs:lhs' ~rhs in + (update_mem_in_prune lv array_v' ~pruning_exp astate, lhs', pruning_exp) in match alias_typ with | AliasTarget.Eq -> diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java index c67e11184..47111dc51 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java @@ -74,6 +74,26 @@ class ArrayListTest { int j = b.get(a.size()); } + void add_in_loop_by_param3_ok(ArrayList b) { + ArrayList a = new ArrayList<>(); + if (b.size() > 0) { + for (int i = 1; i < b.size(); i++) { + a.add(0); + } + int j = a.get(b.size() - 2); + } + } + + void add_in_loop_by_param3_bad(ArrayList b) { + ArrayList a = new ArrayList<>(); + if (b.size() > 0) { + for (int i = 1; i < b.size(); i++) { + a.add(0); + } + 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 4f2cda028..1a886e554 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -10,6 +10,7 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_and_remove_bad(java.util.ArrayList):void, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] 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_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]