Inferbo/perf: path rather than symbols

Reviewed By: ddino

Differential Revision: D8371727

fbshipit-source-id: 88e3bb3

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -34,12 +34,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   type extras = ProcData.no_extras
 
   let declare_symbolic_val
-      : Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> Loc.t -> Typ.typ -> inst_num:int
-        -> new_sym_num:Itv.Counter.t -> Domain.t -> Domain.t =
-   fun pname tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem ->
+      : Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t -> node_hash:int -> Location.t -> Loc.t
+        -> Typ.typ -> inst_num:int -> new_sym_num:Itv.Counter.t -> Domain.t -> Domain.t =
+   fun pname path tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem ->
     let max_depth = 2 in
     let new_alloc_num = Itv.Counter.make 1 in
-    let rec decl_sym_val pname tenv ~node_hash location ~depth ~may_last_field loc typ mem =
+    let rec decl_sym_val pname path tenv ~node_hash location ~depth ~may_last_field loc typ mem =
       if depth > max_depth then mem
       else
         let depth = depth + 1 in
@@ -47,18 +47,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         | Typ.Tint ikind ->
             let unsigned = Typ.ikind_is_unsigned ikind in
             let v =
-              Dom.Val.make_sym ~unsigned pname new_sym_num
+              Dom.Val.make_sym ~unsigned pname path new_sym_num
               |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
             in
             Dom.Mem.add_heap loc v mem
         | Typ.Tfloat _ ->
             let v =
-              Dom.Val.make_sym pname new_sym_num
+              Dom.Val.make_sym pname path new_sym_num
               |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
             in
             Dom.Mem.add_heap loc v mem
         | Typ.Tptr (typ, _) ->
-            BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname tenv
+            BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname path tenv
               ~node_hash location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem
         | Typ.Tarray {elt; length} ->
             let size =
@@ -71,18 +71,20 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             let offset = Itv.zero in
             BoUtils.Exec.decl_sym_arr
               ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-              pname tenv ~node_hash location ~depth loc elt ~offset ?size ~inst_num ~new_sym_num
-              ~new_alloc_num mem
+              pname path tenv ~node_hash location ~depth loc elt ~offset ?size ~inst_num
+              ~new_sym_num ~new_alloc_num mem
         | Typ.Tstruct typename -> (
           match Models.TypName.dispatch typename with
           | Some {Models.declare_symbolic} ->
               let model_env = Models.mk_model_env pname node_hash location tenv in
-              declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) model_env ~depth loc
-                ~inst_num ~new_sym_num ~new_alloc_num mem
+              declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~depth
+                loc ~inst_num ~new_sym_num ~new_alloc_num mem
           | None ->
               let decl_fld ~may_last_field mem (fn, typ, _) =
                 let loc_fld = Loc.append_field loc ~fn in
-                decl_sym_val pname tenv ~node_hash location ~depth loc_fld typ ~may_last_field mem
+                let path = Itv.SymbolPath.field path fn in
+                decl_sym_val pname path tenv ~node_hash location ~depth loc_fld typ ~may_last_field
+                  mem
               in
               let decl_flds str =
                 IList.fold_last ~f:(decl_fld ~may_last_field:false)
@@ -97,7 +99,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                 location ;
             mem
     in
-    decl_sym_val pname tenv ~node_hash location ~depth:0 ~may_last_field:true loc typ mem
+    decl_sym_val pname path tenv ~node_hash location ~depth:0 ~may_last_field:true loc typ mem
 
 
   let declare_symbolic_parameters
@@ -107,8 +109,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let new_sym_num = Itv.Counter.make 0 in
     let add_formal (mem, inst_num) (pvar, typ) =
       let loc = Loc.of_pvar pvar in
+      let path = Itv.SymbolPath.of_pvar pvar in
       let mem =
-        declare_symbolic_val pname tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem
+        declare_symbolic_val pname path tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem
       in
       (mem, inst_num + 1)
     in

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -100,9 +100,9 @@ module Val = struct
 
   let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i}
 
-  let make_sym : ?unsigned:bool -> Typ.Procname.t -> Itv.Counter.t -> t =
-   fun ?(unsigned= false) pname new_sym_num ->
-    {bot with itv= Itv.make_sym ~unsigned pname new_sym_num}
+  let make_sym : ?unsigned:bool -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t =
+   fun ?(unsigned= false) pname path new_sym_num ->
+    {bot with itv= Itv.make_sym ~unsigned pname (Itv.SymbolPath.normal path) new_sym_num}
 
 
   let unknown_bit : t -> t = fun x -> {x with itv= Itv.top}

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -31,8 +31,9 @@ type declare_local_fun =
   -> Dom.Mem.astate -> Dom.Mem.astate * int
 
 type declare_symbolic_fun =
-  decl_sym_val:BoUtils.Exec.decl_sym_val -> model_env -> depth:int -> Loc.t -> inst_num:int
-  -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate
+  decl_sym_val:BoUtils.Exec.decl_sym_val -> Itv.SymbolPath.partial -> model_env -> depth:int
+  -> Loc.t -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t
+  -> Dom.Mem.astate -> Dom.Mem.astate
 
 type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun}
 
@@ -238,12 +239,12 @@ module StdArray = struct
       BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num
         ~dimension mem
     in
-    let declare_symbolic ~decl_sym_val {pname; tenv; node_hash; location} ~depth loc ~inst_num
+    let declare_symbolic ~decl_sym_val path {pname; tenv; node_hash; location} ~depth loc ~inst_num
         ~new_sym_num ~new_alloc_num mem =
       let offset = Itv.zero in
       let size = Itv.of_int64 length in
-      BoUtils.Exec.decl_sym_arr ~decl_sym_val pname tenv ~node_hash location ~depth loc typ ~offset
-        ~size ~inst_num ~new_sym_num ~new_alloc_num mem
+      BoUtils.Exec.decl_sym_arr ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ
+        ~offset ~size ~inst_num ~new_sym_num ~new_alloc_num mem
     in
     {declare_local; declare_symbolic}
 
@@ -282,8 +283,8 @@ module StdArray = struct
     let declare_local ~decl_local:_ {pname; location} _loc ~inst_num ~dimension:_ mem =
       (no_model "local" pname location mem, inst_num)
     in
-    let declare_symbolic ~decl_sym_val:_ {pname; location} ~depth:_ _loc ~inst_num:_ ~new_sym_num:_
-        ~new_alloc_num:_ mem =
+    let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc ~inst_num:_
+        ~new_sym_num:_ ~new_alloc_num:_ mem =
       no_model "symbolic" pname location mem
     in
     {declare_local; declare_symbolic}

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -49,19 +49,24 @@ module Exec = struct
 
 
   type decl_sym_val =
-    Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t
-    -> Dom.Mem.astate -> Dom.Mem.astate
+    Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t -> node_hash:int -> Location.t -> depth:int
+    -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
 
   let decl_sym_arr
-      : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t
-        -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int
-        -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate
-        -> Dom.Mem.astate =
-   fun ~decl_sym_val pname tenv ~node_hash location ~depth loc typ ?offset ?size ~inst_num
+      : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t
+        -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t
+        -> ?size:Itv.t -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t
+        -> Dom.Mem.astate -> Dom.Mem.astate =
+   fun ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ ?offset ?size ~inst_num
        ~new_sym_num ~new_alloc_num mem ->
     let option_value opt_x default_f = match opt_x with Some x -> x | None -> default_f () in
-    let offset = option_value offset (fun () -> Itv.make_sym pname new_sym_num) in
-    let size = option_value size (fun () -> Itv.make_sym ~unsigned:true pname new_sym_num) in
+    let offset =
+      option_value offset (fun () -> Itv.make_sym pname (Itv.SymbolPath.offset path) new_sym_num)
+    in
+    let size =
+      option_value size (fun () ->
+          Itv.make_sym ~unsigned:true pname (Itv.SymbolPath.length path) new_sym_num )
+    in
     let alloc_num = Itv.Counter.next new_alloc_num in
     let elem = Trace.SymAssign (loc, location) in
     let arr =
@@ -73,7 +78,8 @@ module Exec = struct
     let deref_loc =
       Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num)
     in
-    decl_sym_val pname tenv ~node_hash location ~depth deref_loc typ mem
+    let path = Itv.SymbolPath.index path in
+    decl_sym_val pname path tenv ~node_hash location ~depth deref_loc typ mem
 
 
   let init_array_fields tenv pname ~node_hash typ locs ?dyn_length mem =

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -23,13 +23,14 @@ module Exec : sig
     -> Dom.Mem.astate * int
 
   type decl_sym_val =
-    Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t
-    -> Dom.Mem.astate -> Dom.Mem.astate
+    Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t -> node_hash:int -> Location.t -> depth:int
+    -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
 
   val decl_sym_arr :
-    decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t
-    -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int
-    -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate
+    decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t
+    -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t
+    -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate
+    -> Dom.Mem.astate
 
   val init_array_fields :
     Tenv.t -> Typ.Procname.t -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t

infer/src/bufferoverrun/itv.ml

@@ -42,22 +42,71 @@ module Boolean = struct
   let is_true = function True -> true | _ -> false
 end
 
-exception Not_one_symbol
+module BoundEnd = struct
+  type t = LowerBound | UpperBound
+
+  let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound
+
+  let to_string = function LowerBound -> "lb" | UpperBound -> "ub"
+end
+
+module SymbolPath = struct
+  type partial = Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial
+
+  type t = Normal of partial | Offset of partial | Length of partial
+
+  let of_pvar pvar = Pvar pvar
+
+  let field p fn = Field (fn, p)
+
+  let index p = Index p
+
+  let normal p = Normal p
+
+  let offset p = Offset p
+
+  let length p = Length p
+
+  let rec pp_partial fmt = function
+    | Pvar pvar ->
+        Pvar.pp_value fmt pvar
+    | Index p ->
+        F.fprintf fmt "%a[*]" pp_partial p
+    | Field (fn, p) ->
+        F.fprintf fmt "%a.%a" pp_partial p Typ.Fieldname.pp fn
+
+
+  let pp fmt = function
+    | Normal p ->
+        pp_partial fmt p
+    | Offset p ->
+        F.fprintf fmt "%a.offset" pp_partial p
+    | Length p ->
+        F.fprintf fmt "%a.length" pp_partial p
+end
 
 module Symbol = struct
-  type t = {pname: Typ.Procname.t; id: int; unsigned: bool} [@@deriving compare]
+  type t =
+    {id: int; pname: Typ.Procname.t; unsigned: bool; path: SymbolPath.t; bound_end: BoundEnd.t}
+
+  let compare s1 s2 =
+    (* Symbols only make sense within a given function, so shouldn't be compared across function boundaries. *)
+    assert (phys_equal s1.pname s2.pname) ;
+    Int.compare s1.id s2.id
+
 
   let equal = [%compare.equal : t]
 
-  let make : unsigned:bool -> Typ.Procname.t -> int -> t =
-   fun ~unsigned pname id -> {pname; id; unsigned}
+  let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t =
+   fun ~unsigned pname path bound_end id -> {id; pname; unsigned; path; bound_end}
 
 
   let pp : F.formatter -> t -> unit =
-   fun fmt {pname; id; unsigned} ->
-    let symbol_name = if unsigned then "u" else "s" in
-    if Config.bo_debug <= 1 then F.fprintf fmt "%s$%d" symbol_name id
-    else F.fprintf fmt "%s-%s$%d" (Typ.Procname.to_string pname) symbol_name id
+   fun fmt {pname; id; unsigned; path; bound_end} ->
+    F.fprintf fmt "%a.%s" SymbolPath.pp path (BoundEnd.to_string bound_end) ;
+    if Config.bo_debug > 1 then
+      let symbol_name = if unsigned then 'u' else 's' in
+      F.fprintf fmt "(%s-%c$%d)" (Typ.Procname.to_string pname) symbol_name id
 
 
   let is_unsigned : t -> bool = fun x -> x.unsigned
@@ -233,6 +282,8 @@ end
 
 open Ints
 
+exception Not_one_symbol
+
 module SymLinear = struct
   module M = SymbolMap
 
@@ -268,8 +319,9 @@ module SymLinear = struct
     M.for_all2 ~f:le_one_pair x y
 
 
-  let make : unsigned:bool -> Typ.Procname.t -> int -> t =
-   fun ~unsigned pname i -> singleton_one (Symbol.make ~unsigned pname i)
+  let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t =
+   fun ~unsigned pname path bound_end i ->
+    singleton_one (Symbol.make ~unsigned pname path bound_end i)
 
 
   let eq : t -> t -> bool =
@@ -369,12 +421,6 @@ module SymLinear = struct
   let int_ub x = if is_le_zero x then Some 0 else None
 end
 
-module BoundEnd = struct
-  type t = LowerBound | UpperBound
-
-  let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound
-end
-
 module Bound = struct
   type sign = Plus | Minus [@@deriving compare]
 
@@ -1435,10 +1481,16 @@ module ItvPure = struct
 
   let of_int n = of_bound (Bound.of_int n)
 
-  let make_sym : unsigned:bool -> Typ.Procname.t -> Counter.t -> t =
-   fun ~unsigned pname new_sym_num ->
-    let lower = Bound.of_sym (SymLinear.make ~unsigned pname (Counter.next new_sym_num)) in
-    let upper = Bound.of_sym (SymLinear.make ~unsigned pname (Counter.next new_sym_num)) in
+  let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> Counter.t -> t =
+   fun ~unsigned pname path new_sym_num ->
+    let lower =
+      Bound.of_sym
+        (SymLinear.make ~unsigned pname path BoundEnd.LowerBound (Counter.next new_sym_num))
+    in
+    let upper =
+      Bound.of_sym
+        (SymLinear.make ~unsigned pname path BoundEnd.UpperBound (Counter.next new_sym_num))
+    in
     (lower, upper)
 
 
@@ -1873,9 +1925,9 @@ let plus : t -> t -> t = lift2 ItvPure.plus
 
 let minus : t -> t -> t = lift2 ItvPure.minus
 
-let make_sym : ?unsigned:bool -> Typ.Procname.t -> Counter.t -> t =
- fun ?(unsigned= false) pname new_sym_num ->
-  NonBottom (ItvPure.make_sym ~unsigned pname new_sym_num)
+let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> Counter.t -> t =
+ fun ?(unsigned= false) pname path new_sym_num ->
+  NonBottom (ItvPure.make_sym ~unsigned pname path new_sym_num)
 
 
 let neg : t -> t = lift1 ItvPure.neg

infer/src/bufferoverrun/itv.mli

@@ -29,6 +29,24 @@ module Boolean : sig
   val is_true : t -> bool
 end
 
+module SymbolPath : sig
+  type partial
+
+  type t
+
+  val of_pvar : Pvar.t -> partial
+
+  val index : partial -> partial
+
+  val field : partial -> Typ.Fieldname.t -> partial
+
+  val normal : partial -> t
+
+  val offset : partial -> t
+
+  val length : partial -> t
+end
+
 module Symbol : sig
   type t
 end
@@ -175,7 +193,7 @@ val of_int_lit : IntLit.t -> t
 
 val of_int64 : Int64.t -> t
 
-val make_sym : ?unsigned:bool -> Typ.Procname.t -> Counter.t -> t
+val make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> Counter.t -> t
 
 val lb : t -> Bound.t
 

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

@@ -3,7 +3,7 @@ codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: [20, 20]]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: [19, 19]]
-codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]]
+codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [3xlen.lb + 1, 3xlen.ub + 1] Size: [3xlen.lb + 1, 3xlen.ub + 1]]
 codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [20, 20] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: [-1, -1] Size: [2, 2]]
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
@@ -36,14 +36,14 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFER
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, s$0), s$1] Size: [10, 10]]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [s$0, min(-1, s$1)] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, i.lb), i.ub] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [i.lb, min(-1, i.ub)] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: [9, 9]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: [9, 9]]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_symbolic_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [s$0, s$1] Size: [s$0, s$1]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_symbolic_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [n.lb, n.ub] Size: [n.lb, n.ub]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Offset: [0, 10] Size: [5, 15]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Offset: [0, 10] Size: [5, 15]]
@@ -51,8 +51,8 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_underrun_Bad, 2, BUFFER
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [10, 10]]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [s$0, +oo] Size: [s$0, s$1]]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [s$0, +oo] Size: [s$0, s$1]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n.lb, +oo] Size: [n.lb, n.ub]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n.lb, +oo] Size: [n.lb, n.ub]]
 codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, []
 codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 255] Size: [255, 255]]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 256] Size: [256, 256]]

infer/tests/codetoanalyze/c/performance/issues.exp

@@ -1,17 +1,17 @@
-codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * s$1]
-codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * s$1]
-codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * s$1]
-codetoanalyze/c/performance/break.c, break_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * s$1]
-codetoanalyze/c/performance/break.c, break_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * s$1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * s$1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * s$1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * s$1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * s$1]
+codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * p.ub]
+codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * p.ub]
+codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * p.ub]
+codetoanalyze/c/performance/break.c, break_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * p.ub]
+codetoanalyze/c/performance/break.c, break_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * p.ub]
+codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * p.ub]
+codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * p.ub]
+codetoanalyze/c/performance/break.c, break_loop_with_t, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * p.ub]
+codetoanalyze/c/performance/break.c, break_loop_with_t, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * p.ub]
 codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * s$1]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * s$1]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * s$1]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 7 * s$1]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * m.ub]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * m.ub]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * m.ub]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 7 * m.ub]
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
@@ -26,10 +26,10 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_an
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 8, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_shortcut, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * s$1]
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * s$1]
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * s$1]
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * s$1]
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * p.ub]
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * p.ub]
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * p.ub]
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * p.ub]
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/performance/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 604]
@@ -39,16 +39,16 @@ codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1104]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1104]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1106]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 11 * s$1]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 11 * s$1]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 11 * s$1]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * (-s$0 + s$1 + 15)]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * (-s$0 + s$1 + 15)]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 11 * (-s$0 + s$1 + 15)]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 11 * k.ub]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 11 * k.ub]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 11 * k.ub]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * (-k.lb + k.ub + 15)]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * (-k.lb + k.ub + 15)]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 11 * (-k.lb + k.ub + 15)]
 codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 211]
-codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 * (-s$0 + 20)]
-codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 * (-s$0 + 20)]
-codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * (-s$0 + 20)]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 * (-m.lb + 20)]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 * (-m.lb + 20)]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * (-m.lb + 20)]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201]
 codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1204]
 codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1204]
@@ -75,16 +75,16 @@ codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545]
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 547]
 codetoanalyze/c/performance/instantiate.c, do_2K_times_Bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 12004]
-codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * (s$1 + -1) * s$1 + 10 * s$1]
-codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * (s$1 + -1) * s$1 + 10 * s$1]
-codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 * s$1 + 6 * s$1^2]
-codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 * s$1 + 6 * s$1^2]
-codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * s$1]
-codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * s$1]
-codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * s$1]
-codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * s$1]
-codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 8 * s$1]
-codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 8 * s$1]
+codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * (m.ub + -1) * m.ub + 10 * m.ub]
+codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * (m.ub + -1) * m.ub + 10 * m.ub]
+codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 * m.ub + 6 * m.ub^2]
+codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 * m.ub + 6 * m.ub^2]
+codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * n.ub]
+codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * n.ub]
+codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * n.ub]
+codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * n.ub]
+codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 8 * n.ub]
+codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 8 * n.ub]
 codetoanalyze/c/performance/invariant.c, do_n_m_times_nested_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/c/performance/invariant.c, while_infinite_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
@@ -118,15 +118,15 @@ codetoanalyze/c/performance/switch_continue.c, test_switch, 17, EXPENSIVE_EXECUT
 codetoanalyze/c/performance/switch_continue.c, test_switch, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 603]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * s$1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * s$1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 * s$1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 * s$1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 * s$1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 12 * s$1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * s$1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * s$1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 * s$1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 * s$1 + 6 * s$3]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 * s$1 + 6 * s$3]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 6 * s$1 + 6 * s$3]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * m.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * m.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 * m.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 * m.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 * m.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 12 * m.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * m.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * m.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 * m.ub + 6 * k.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 * m.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 * m.ub + 6 * k.ub]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 6 * m.ub + 6 * k.ub]

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

@@ -32,11 +32,11 @@ codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_u_FP, 5, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$8), -1+max(1, s$9)] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_u_FP, 5, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, t[*].bI.lb), -1+max(1, t[*].bI.ub)] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Call,Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] by call to `int_vector_access_at()` ]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, t[*].bI.lb), -1+max(1, t[*].bI.ub)] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: [v[*]._size.lb, v[*]._size.ub] Size: [v[*]._size.lb, v[*]._size.ub] by call to `int_vector_access_at()` ]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
@@ -45,7 +45,7 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter: __n,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [v[*].infer_size.lb, v[*].infer_size.ub] Size: [v[*].infer_size.lb, v[*].infer_size.ub]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, -1] Size: [10, 10] by call to `access_minus_one()` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: [10, 10] by call to `access_minus_one()` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [1, 1]]

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -2,15 +2,15 @@ codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(i
 codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 882]
 codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 882]
 codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 889]
-codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * u$7]
-codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * u$7]
-codetoanalyze/java/performance/Break.java, int Break.break_constant(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * s$1]
-codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 7 * s$1]
-codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * s$1]
+codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * mag.length.ub]
+codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * mag.length.ub]
+codetoanalyze/java/performance/Break.java, int Break.break_constant(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * p.ub]
+codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 7 * p.ub]
+codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * p.ub]
 codetoanalyze/java/performance/Break.java, void Break.break_outer_loop_FN(int,int), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.compound_while(int), 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
-codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.compound_while(int), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * s$1]
-codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.compound_while(int), 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * s$1]
+codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.compound_while(int), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * m.ub]
+codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.compound_while(int), 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * m.ub]
 codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.nested_while_and_or(int), 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.nested_while_and_or(int), 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.nested_while_and_or(int), 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
@@ -18,10 +18,10 @@ codetoanalyze/java/performance/Compound_loop.java, int Compound_loop.nested_whil
 codetoanalyze/java/performance/Compound_loop.java, void Compound_loop.while_and_or(int), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/Compound_loop.java, void Compound_loop.while_and_or(int), 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/java/performance/Continue.java, int Continue.continue_outer_loop_FN(), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop2(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * s$1]
-codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop2(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 * s$1]
-codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * (-s$0 + s$1 + 15)]
-codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 * (-s$0 + s$1 + 15)]
+codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop2(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * k.ub]
+codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop2(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 * k.ub]
+codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 * (-k.lb + k.ub + 15)]
+codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * (-k.lb + k.ub + 15)]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop0_bad(), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1101]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop0_bad(), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1102]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop1_bad(), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1203]