[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

@@ -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 is_bot = is_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 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
+    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

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

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

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

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)

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] *)
 

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}

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

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

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -70,6 +70,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>::fB_FP, 0, INTEGER_OVERFLOW_
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>::lI_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::unique_ptr<LMB<TFM>,std::default_delete<LMB<TFM>>>::operator->,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>::lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,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<TFM>::uI, 0, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::unique_ptr<LMB<TFM>,std::default_delete<LMB<TFM>>>::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,<Offset trace>,Parameter `bi`,<Length trace>,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,<LHS trace>,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,<Offset trace>,Parameter `i`,<Length trace>,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,<Offset trace>,Parameter `this->i`,<Length trace>,Array declaration,Array access: Offset: 8 Size: 5 by call to `smart_ptr::my_class::array_access` ]

infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java

@@ -251,7 +251,7 @@ class ArrayListTest {
   ArrayList<Integer> unknown_array_list1;
   ArrayList<Integer> unknown_array_list2;
 
-  void loop_on_unknown_iterator(MyI x, int j) {
+  void loop_on_unknown_iterator_FN(MyI x, int j) {
     ArrayList<Integer> a = new ArrayList<>();
     ArrayList<Integer> 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;

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, [<Length trace>,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, [<Length trace>,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, [<Length trace>,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, [<Length trace>,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, [<Length trace>,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, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,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, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,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, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]