diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 7c118354f..de4686674 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -143,10 +143,13 @@ module Loc = struct let of_allocsite a = Allocsite a let append_star_field l0 ~fn = - let rec aux = function + let rec aux l = + match l with + | Allocsite a when Allocsite.is_unknown a -> + l | Var _ | Allocsite _ -> StarField {prefix= l0; last_field= fn} - | StarField {last_field} as l when Fieldname.equal fn last_field -> + | StarField {last_field} when Fieldname.equal fn last_field -> l | StarField {prefix} -> StarField {prefix; last_field= fn} @@ -161,6 +164,8 @@ module Loc = struct if Symb.SymbolPath.is_field_depth_beyond_limit depth then append_star_field l0 ~fn else match l with + | Allocsite a when Allocsite.is_unknown a -> + l | Var _ | Allocsite _ -> Field {prefix= l0; fn; typ} | StarField {last_field} as l when Fieldname.equal fn last_field -> @@ -392,30 +397,174 @@ module Loc = struct x end +module LocSet = PrettyPrintable.MakePPSet (Loc) + module PowLoc = struct - include AbstractDomain.FiniteSet (Loc) + (* The known set of locations should not be empty and not include the unknown location. Every + constructors in this module should be defined carefully to keep that constraint. *) + type t = Bottom | Unknown | Known of LocSet.t [@@deriving compare] + + let pp f = function + | Bottom -> + F.pp_print_string f SpecialChars.up_tack + | Unknown -> + Loc.pp f Loc.unknown + | Known locs -> + LocSet.pp f locs + + + let leq ~lhs ~rhs = + match (lhs, rhs) with + | Bottom, _ -> + true + | _, Bottom -> + false + | Unknown, _ -> + true + | _, Unknown -> + false + | Known lhs, Known rhs -> + LocSet.subset lhs rhs + - let bot = empty + let join x y = + match (x, y) with + | Bottom, _ -> + y + | _, Bottom -> + x + | Unknown, _ -> + y + | _, Unknown -> + x + | Known x, Known y -> + Known (LocSet.union x y) + + + let widen ~prev ~next ~num_iters:_ = join prev next + + let bot = Bottom + + let is_bot = function Bottom -> true | Unknown | Known _ -> false - let is_bot = is_empty + let unknown = Unknown + + let singleton l = if Loc.is_unknown l then Unknown else Known (LocSet.singleton l) + + let fold f ploc init = + match ploc with + | Bottom -> + init + | Unknown -> + f Loc.unknown init + | Known ploc -> + LocSet.fold f ploc init + + + let exists f ploc = + match ploc with + | Bottom -> + false + | Unknown -> + f Loc.unknown + | Known ploc -> + LocSet.exists f ploc + + + let normalize ploc = + match ploc with + | Bottom | Unknown -> + ploc + | Known ploc' -> ( + match LocSet.is_singleton_or_more ploc' with + | Empty -> + Bottom + | Singleton loc when Loc.is_unknown loc -> + Unknown + | More when LocSet.mem Loc.unknown ploc' -> + Known (LocSet.remove Loc.unknown ploc') + | _ -> + ploc ) + + + let map f ploc = + match ploc with + | Bottom -> + Bottom + | Unknown -> + singleton (f Loc.unknown) + | Known ploc -> + Known (LocSet.map f ploc) |> normalize + + + let is_singleton_or_more = function + | Bottom -> + IContainer.Empty + | Unknown -> + IContainer.Singleton Loc.unknown + | Known ploc -> + LocSet.is_singleton_or_more ploc + + + let min_elt_opt = function + | Bottom -> + None + | Unknown -> + Some Loc.unknown + | Known ploc -> + LocSet.min_elt_opt ploc + + + let add l ploc = + match ploc with + | Bottom | Unknown -> + singleton l + | Known _ when Loc.is_unknown l -> + ploc + | Known ploc -> + Known (LocSet.add l ploc) + + + let mem l = function + | Bottom -> + false + | Unknown -> + Loc.is_unknown l + | Known ploc -> + LocSet.mem l ploc - let unknown = singleton Loc.unknown let append_field ploc ~fn = - if is_bot ploc then singleton Loc.unknown - else fold (fun l -> add (Loc.append_field l ~fn)) ploc empty + match normalize ploc with + | Bottom -> + (* Return the unknown location to avoid unintended unreachable nodes *) + Unknown + | Unknown -> + ploc + | Known ploc -> + Known (LocSet.fold (fun l -> LocSet.add (Loc.append_field l ~fn)) ploc LocSet.empty) let append_star_field ploc ~fn = - if is_bot ploc then singleton Loc.unknown - else fold (fun l -> add (Loc.append_star_field l ~fn)) ploc empty + match normalize ploc with + | Bottom -> + (* Return the unknown location to avoid unintended unreachable nodes *) + Unknown + | Unknown -> + ploc + | Known ploc -> + Known (LocSet.fold (fun l -> LocSet.add (Loc.append_star_field l ~fn)) ploc LocSet.empty) let lift_cmp cmp_loc ploc1 ploc2 = - match (is_singleton_or_more ploc1, is_singleton_or_more ploc2) with - | IContainer.Singleton loc1, IContainer.Singleton loc2 -> - Boolean.EqualOrder.of_equal cmp_loc (Loc.eq loc1 loc2) - | _ -> + match (ploc1, ploc2) with + | Known ploc1, Known ploc2 -> ( + match (LocSet.is_singleton_or_more ploc1, LocSet.is_singleton_or_more ploc2) with + | IContainer.Singleton loc1, IContainer.Singleton loc2 -> + Boolean.EqualOrder.of_equal cmp_loc (Loc.eq loc1 loc2) + | _ -> + Boolean.Top ) + | _, _ -> Boolean.Top @@ -432,7 +581,7 @@ module PowLoc = struct let subst x (eval_locpath : eval_locpath) = - fold (fun l acc -> join acc (subst_loc l eval_locpath)) x empty + fold (fun l acc -> join acc (subst_loc l eval_locpath)) x bot let exists_str ~f x = exists (fun l -> Loc.exists_str ~f l) x @@ -440,6 +589,14 @@ module PowLoc = struct let of_c_strlen x = map Loc.of_c_strlen x let cast typ x = map (Loc.cast typ) x + + let to_set = function + | Bottom -> + LocSet.empty + | Unknown -> + LocSet.singleton Loc.unknown + | Known ploc -> + ploc end let always_strong_update = false diff --git a/infer/src/bufferoverrun/absLoc.mli b/infer/src/bufferoverrun/absLoc.mli index f507e41a0..c638c50ac 100644 --- a/infer/src/bufferoverrun/absLoc.mli +++ b/infer/src/bufferoverrun/absLoc.mli @@ -108,8 +108,12 @@ module Loc : sig (** It appends field. [typ] is the type of [fn]. *) end +module LocSet : PrettyPrintable.PPSet with type elt = Loc.t + module PowLoc : sig - include AbstractDomain.FiniteSetS with type elt = Loc.t + include AbstractDomain.S + + val compare : t -> t -> int val append_field : t -> fn:Fieldname.t -> t @@ -117,6 +121,20 @@ module PowLoc : sig val bot : t + val add : Loc.t -> t -> t + + val exists : (Loc.t -> bool) -> t -> bool + + val mem : Loc.t -> t -> bool + + val is_singleton_or_more : t -> Loc.t IContainer.singleton_or_more + + val min_elt_opt : t -> Loc.t option + + val singleton : Loc.t -> t + + val fold : (Loc.t -> 'a -> 'a) -> t -> 'a -> 'a + val cast : Typ.typ -> t -> t val of_c_strlen : t -> t @@ -141,6 +159,8 @@ module PowLoc : sig val lift_cmp : Boolean.EqualOrder.t -> t -> t -> Boolean.t (** It lifts a comparison of [Loc.t] to [t]. The comparison can be [Boolean.EqualOrder.eq], [Boolean.EqualOrder.ne], etc. *) + + val to_set : t -> LocSet.t end val can_strong_update : PowLoc.t -> bool diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index a5cf834a1..b67459a29 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -357,7 +357,7 @@ let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> PowLoc.t * t = in PowLoc.fold add_allocsite locs (powloc_acc, acc) in - fold subst1 a (PowLoc.empty, empty) + fold subst1 a (PowLoc.bot, empty) let is_symbolic : t -> bool = fun a -> exists (fun _ ai -> ArrInfo.is_symbolic ai) a diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index ba9dad24d..14382a4ac 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -92,8 +92,8 @@ module TransferFunctions = struct let instantiate_mem_reachable (ret_id, ret_typ) callee_formals callee_pname params ~callee_exit_mem ({Dom.eval_locpath} as eval_sym_trace) mem location = let formal_locs = - List.fold callee_formals ~init:PowLoc.bot ~f:(fun acc (formal, _) -> - PowLoc.add (Loc.of_pvar formal) acc ) + List.fold callee_formals ~init:LocSet.empty ~f:(fun acc (formal, _) -> + LocSet.add (Loc.of_pvar formal) acc ) in let copy_reachable_locs_from locs mem = let copy loc acc = @@ -103,7 +103,7 @@ module TransferFunctions = struct PowLoc.fold (fun loc acc -> Dom.Mem.add_heap loc v acc) locs acc ) in let reachable_locs = Dom.Mem.get_reachable_locs_from callee_formals locs callee_exit_mem in - PowLoc.fold copy (PowLoc.diff reachable_locs formal_locs) mem + LocSet.fold copy (LocSet.diff reachable_locs formal_locs) mem in let instantiate_ret_alias mem = let subst_loc l = @@ -136,7 +136,8 @@ module TransferFunctions = struct in Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem |> instantiate_ret_alias - |> copy_reachable_locs_from (PowLoc.join formal_locs (Dom.Val.get_all_locs ret_val)) + |> copy_reachable_locs_from + (LocSet.union formal_locs (Dom.Val.get_all_locs ret_val |> PowLoc.to_set)) |> instantiate_latest_prune ~ret_id ~callee_exit_mem eval_sym_trace location @@ -228,8 +229,8 @@ module TransferFunctions = struct Option.value_map (Dom.Mem.find_opt loc from_mem) ~default:acc ~f:(fun v -> Dom.Mem.add_heap loc v acc ) in - let reachable_locs = Dom.Mem.get_reachable_locs_from [] (PowLoc.singleton loc) from_mem in - PowLoc.fold copy reachable_locs to_mem + let reachable_locs = Dom.Mem.get_reachable_locs_from [] (LocSet.singleton loc) from_mem in + LocSet.fold copy reachable_locs to_mem in fun tenv get_summary exp mem -> Option.value_map (Exp.get_java_class_initializer tenv exp) ~default:mem diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 82b62740a..a13ef9a97 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -260,7 +260,7 @@ module Val = struct ; itv_updated_by= ItvUpdatedBy.Top ; modeled_range= ModeledRange.bottom ; taint= Taint.bottom - ; powloc= (if is_int then PowLoc.bottom else PowLoc.unknown) + ; powloc= (if is_int then PowLoc.bot else PowLoc.unknown) ; arrayblk= (if is_int then ArrayBlk.bottom else ArrayBlk.unknown) ; traces } @@ -484,7 +484,7 @@ module Val = struct Itv.is_bottom pruned_itv && (not (Itv.is_bottom x.itv)) && Itv.is_bottom y.itv - && not (PowLoc.is_bottom (get_all_locs y)) + && not (PowLoc.is_bot (get_all_locs y)) then x.itv else pruned_itv in @@ -929,12 +929,22 @@ module MemPure = struct (** Collect the location that was increased by one, i.e., [x -> x+1] *) let get_incr_locs m = - fold (fun l v acc -> if MVal.is_incr_of l v then PowLoc.add l acc else acc) m PowLoc.empty + fold (fun l v acc -> if MVal.is_incr_of l v then PowLoc.add l acc else acc) m PowLoc.bot let find_opt l m = Option.map (find_opt l m) ~f:MVal.get_val - let add ?(represents_multiple_values = false) l v m = + let add ?(represents_multiple_values = false) l ({Val.powloc; arrayblk} as v) m = + let v = + if Loc.is_unknown l then + (* We do not add the other locations except the unknown itself in its value. This spoiled + other values raising out of memory sometimes, rather than being helpful for analysis + precision. *) + { v with + Val.powloc= (if PowLoc.is_bot powloc then powloc else PowLoc.unknown) + ; arrayblk= (if ArrayBlk.is_bottom arrayblk then arrayblk else ArrayBlk.unknown) } + else v + in let f = function | None -> Some (represents_multiple_values || Loc.represents_multiple_values l, v) @@ -1030,7 +1040,7 @@ module AliasTarget = struct | IteratorOffset {java_tmp= None} | IteratorHasNext {java_tmp= None} | Top -> - PowLoc.empty + PowLoc.bot let use_loc l x = PowLoc.mem l (get_locs x) @@ -2093,7 +2103,7 @@ module MemReach = struct let add_iterator_alias_common ~cond ~alias_add id m = let locs = let accum_loc l v acc = if cond v then PowLoc.add l acc else acc in - MemPure.fold accum_loc m.mem_pure PowLoc.empty + MemPure.fold accum_loc m.mem_pure PowLoc.bot in {m with alias= alias_add id locs m.alias} @@ -2260,29 +2270,29 @@ module MemReach = struct let set_latest_prune : LatestPrune.t -> t -> t = fun latest_prune x -> {x with latest_prune} - let get_reachable_locs_from_aux : f:(Pvar.t -> bool) -> PowLoc.t -> _ t0 -> PowLoc.t = + let get_reachable_locs_from_aux : f:(Pvar.t -> bool) -> LocSet.t -> _ t0 -> LocSet.t = let add_reachable1 ~root loc v acc = - if Loc.equal root loc then PowLoc.union acc (Val.get_all_locs v) - else if Loc.is_field_of ~loc:root ~field_loc:loc then PowLoc.add loc acc + if Loc.equal root loc then LocSet.union acc (Val.get_all_locs v |> PowLoc.to_set) + else if Loc.is_field_of ~loc:root ~field_loc:loc then LocSet.add loc acc else acc in - let rec add_from_locs heap locs acc = PowLoc.fold (add_from_loc heap) locs acc + let rec add_from_locs heap locs acc = LocSet.fold (add_from_loc heap) locs acc and add_from_loc heap loc acc = - if PowLoc.mem loc acc then acc + if LocSet.mem loc acc then acc else - let reachable_locs = MemPure.fold (add_reachable1 ~root:loc) heap PowLoc.empty in - add_from_locs heap reachable_locs (PowLoc.add loc acc) + let reachable_locs = MemPure.fold (add_reachable1 ~root:loc) heap LocSet.empty in + add_from_locs heap reachable_locs (LocSet.add loc acc) in let add_param_locs ~f mem acc = - let add_loc loc _ acc = if Loc.exists_pvar ~f loc then PowLoc.add loc acc else acc in + let add_loc loc _ acc = if Loc.exists_pvar ~f loc then LocSet.add loc acc else acc in MemPure.fold add_loc mem acc in fun ~f locs m -> let locs = add_param_locs ~f m.mem_pure locs in - add_from_locs m.mem_pure locs PowLoc.empty + add_from_locs m.mem_pure locs LocSet.empty - let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> _ t0 -> PowLoc.t = + let get_reachable_locs_from : (Pvar.t * Typ.t) list -> LocSet.t -> _ t0 -> LocSet.t = fun formals locs m -> let is_formal pvar = List.exists formals ~f:(fun (formal, _) -> Pvar.equal pvar formal) in get_reachable_locs_from_aux ~f:is_formal locs m @@ -2304,9 +2314,9 @@ module MemReach = struct Pvar.is_return pvar || Pvar.is_global pvar || List.exists formals ~f:(fun (formal, _) -> Pvar.equal formal pvar) in - get_reachable_locs_from_aux ~f PowLoc.empty m + get_reachable_locs_from_aux ~f LocSet.empty m in - fun l -> PowLoc.mem l reachable_locs + fun l -> LocSet.mem l reachable_locs in let stack_locs = StackLocs.filter is_reachable m.stack_locs in let mem_pure = MemPure.filter (fun l _ -> is_reachable l) m.mem_pure in @@ -2536,9 +2546,9 @@ module Mem = struct let strong_update : PowLoc.t -> Val.t -> t -> t = fun p v -> map ~f:(MemReach.strong_update p v) - let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> _ t0 -> PowLoc.t = + let get_reachable_locs_from : (Pvar.t * Typ.t) list -> LocSet.t -> _ t0 -> LocSet.t = fun formals locs -> - f_lift_default ~default:PowLoc.empty (MemReach.get_reachable_locs_from formals locs) + f_lift_default ~default:LocSet.empty (MemReach.get_reachable_locs_from formals locs) let update_mem : PowLoc.t -> Val.t -> t -> t = fun ploc v -> map ~f:(MemReach.update_mem ploc v) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index c14875574..989b160d0 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -515,7 +515,7 @@ module Mem : sig val get_latest_prune : _ t0 -> LatestPrune.t - val get_reachable_locs_from : (Pvar.t * Typ.t) list -> AbsLoc.PowLoc.t -> _ t0 -> AbsLoc.PowLoc.t + val get_reachable_locs_from : (Pvar.t * Typ.t) list -> AbsLoc.LocSet.t -> _ t0 -> AbsLoc.LocSet.t (** Get reachable locations from [formals] and [locs] when called [get_reachable_locs_from formals locs mem] *) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 5fe21fc5c..58016bfd3 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -778,7 +778,7 @@ module JavaInteger = struct let intValue exp = let exec _ ~ret:(id, _) mem = let powloc = Sem.eval_locs exp mem in - let v = if PowLoc.is_empty powloc then Dom.Val.Itv.top else Dom.Mem.find_set powloc mem in + let v = if PowLoc.is_bot powloc then Dom.Val.Itv.top else Dom.Mem.find_set powloc mem in model_by_value v id mem in {exec; check= no_check} diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 1d665a288..7c498c6e8 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -285,7 +285,7 @@ let rec eval_locs : Exp.t -> Mem.t -> PowLoc.t = | BinOp ((Binop.MinusPI | Binop.PlusPI), e, _) | Cast (_, e) -> eval_locs e mem | BinOp _ | Closure _ | Const _ | Exn _ | Sizeof _ | UnOp _ -> - PowLoc.empty + PowLoc.bot | Lfield (e, fn, _) -> eval_locs e mem |> PowLoc.append_field ~fn | Lindex (((Lfield _ | Lindex _) as e), _) -> @@ -425,7 +425,7 @@ and eval_locpath ~mode params p mem = let locs = eval_locpath ~mode params prefix mem in PowLoc.append_star_field ~fn locs in - if PowLoc.is_empty res then ( + if PowLoc.is_bot res then ( match mode with | EvalPOReachability -> res @@ -510,7 +510,7 @@ let conservative_array_length ?traces arr_locs mem = let eval_array_locs_length arr_locs mem = - if PowLoc.is_empty arr_locs then Val.Itv.top + if PowLoc.is_bot arr_locs then Val.Itv.top else let arr = Mem.find_set arr_locs mem in let traces = Val.get_traces arr in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index a85748132..4c3f6582b 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -285,7 +285,7 @@ module Check = struct let arr = if Language.curr_language_is Java then let arr_locs = Sem.eval_locs array_exp mem in - if PowLoc.is_empty arr_locs then Dom.Val.Itv.top else Dom.Mem.find_set arr_locs mem + if PowLoc.is_bot arr_locs then Dom.Val.Itv.top else Dom.Mem.find_set arr_locs mem else Sem.eval_arr integer_type_widths array_exp mem in let latest_prune = Dom.Mem.get_latest_prune mem in diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 8878e8c51..3f8d5c01a 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -70,6 +70,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::fB_FP, 0, INTEGER_OVERFLOW_ codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::lI_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::unique_ptr,std::default_delete>>::operator->,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Parameter `*o`,Call,Parameter `*k`,Call,Parameter `*k`,Assignment,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::uI, 0, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::unique_ptr,std::default_delete>>::operator->,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Unknown value from: lo::~lo,Call,Assignment,Call,,Parameter `bi`,,Parameter `*this->b->cpp.vector_elem`,Array access: Offset: [-oo, +oo] Size: [0, +oo] by call to `ral_good` ] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Assignment,Call,,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_good` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,,Parameter `i`,,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector::access_at` ] codetoanalyze/cpp/bufferoverrun/smart_ptr.cpp, smart_ptr::call_method_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Assignment,Call,,Parameter `this->i`,,Array declaration,Array access: Offset: 8 Size: 5 by call to `smart_ptr::my_class::array_access` ] diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java index c99acf30e..037a8a660 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java @@ -251,7 +251,7 @@ class ArrayListTest { ArrayList unknown_array_list1; ArrayList unknown_array_list2; - void loop_on_unknown_iterator(MyI x, int j) { + void loop_on_unknown_iterator_FN(MyI x, int j) { ArrayList a = new ArrayList<>(); ArrayList b; if (unknown_bool) { @@ -264,8 +264,7 @@ class ArrayListTest { // precision with introducing a lot of FPs. To avoie that, we ignore the size of `Unknown` // array list here, instead we get some FNs. for (Integer i : b) { - // `a.size()` is evaluated to bottom, rather than [0,+oo] here, but which does not make - // branches unreachable. + // Since size of `b` is evaluted to [0,0], here is unreachable. if (a.size() <= -1) { int[] c = new int[5]; c[5] = 0; diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 0d7b19099..f7e220893 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -20,9 +20,8 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_i codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 12, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 13, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: [0, 2]] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 2, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1] -codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator(ArrayListTest$MyI,int):void, 12, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: ArrayList ArrayListTest$MyI.mk_unknown(),Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator(ArrayListTest$MyI,int):void, 17, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 5 Size: 5] -codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator(ArrayListTest$MyI,int):void, 20, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 12, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: ArrayList ArrayListTest$MyI.mk_unknown(),Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 12, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.multi_adds_in_loop_iterator_bad(java.util.ArrayList):void, 8, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `b.elements[*]`,Assignment,,Array declaration,Array access: Offset: b.length + 1 Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.remove_in_loop_iterator_good_FP(java.util.ArrayList):void, 14, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `b.elements[*]`,Assignment,,Parameter `b.elements[*]`,Array access: Offset: b.length Size: b.length] codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this.buf[*]`,Assignment,,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]