From 30ca51366d4b49efbd7bed2bad7948dde363b943 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 16 Apr 2020 04:00:52 -0700 Subject: [PATCH] [inferbo] Do not append field to the unknown location Summary: This diff revises how to handle the unknown location in inferbo in two ways: * stop appending field to the `Unknown` location, e.g. `Unknown.x.a` is evaluated to `Unknown` * redesign the abstract of multiple locations, like `Bottom` < `Unknown` < `Known` locations I am doing them in one diff since applying only one of them showed bad results. Background: `Unknown` was adopted for abstracting all unknown concrete locations, so we could avoid missing semantics of assignments to unknown locations. We tried to keep soundness. However, it brought some other problems related to precision and performance. 1. Sometimes especially when Inferbo failed to reason precise pointer values, `Unknown` may point to many other abstract locations. 2. At that time, value assignments to `*Unknown` makes the situation worse: many abstract locations are updated with imprecise values. This problem harmed not only its precision, but also its performance since it introduced more location entries in the abstract memory. Reviewed By: jvillard Differential Revision: D21017789 fbshipit-source-id: 0bb6bd8b5 --- infer/src/bufferoverrun/absLoc.ml | 187 ++++++++++++++++-- infer/src/bufferoverrun/absLoc.mli | 22 ++- infer/src/bufferoverrun/arrayBlk.ml | 2 +- .../bufferoverrun/bufferOverrunAnalysis.ml | 13 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 50 +++-- .../src/bufferoverrun/bufferOverrunDomain.mli | 2 +- .../src/bufferoverrun/bufferOverrunModels.ml | 2 +- .../bufferoverrun/bufferOverrunSemantics.ml | 6 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 2 +- .../cpp/bufferoverrun/issues.exp | 1 + .../java/bufferoverrun/ArrayListTest.java | 5 +- .../java/bufferoverrun/issues.exp | 5 +- 12 files changed, 242 insertions(+), 55 deletions(-) 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]