[cost] add NSArray iterator

Summary:
As title.
This diff is co-authored by SungKeun Cho and me.

facebook
This diff is co-authored by skcho and me.

Original comments from skcho
"For the record:
1. Rory and I tried to write models for ObjC iterator.
2. We could not use Java's iterator semantics: In Java's, `hasNext` returns the size of collection, rather than a boolean, and which is used as a control variable. On the other hand, in ObjC, it calls only `nextObject`, not calling `hasNext`, and the return value of which is being checked as `null`.
3. We added an artificial field `objc_iterator_offset` to keep the index of the iterator, and the models added in this diff are handling that integer value.
A problem is that `array.objc_iterator_offset` is not included in the control variables, since the condition of the loop is `nextObject() != null` that does not include the iterator offset. We need to make `array.objc_iterator_offset` as a control variable, by changing the part collecting control variables.
"

Reviewed By: ezgicicek, skcho

Differential Revision: D22944278

fbshipit-source-id: 7e71b79c1

infer/src/bufferoverrun/absLoc.ml

@@ -280,6 +280,10 @@ module Loc = struct
         false
 
 
+  let get_parent_field field_loc =
+    match field_loc with BoField.(Field {prefix= l} | StarField {prefix= l}) -> l | _ -> field_loc
+
+
   let get_literal_string = function
     | BoField.Prim (Allocsite a) ->
         Allocsite.get_literal_string a
@@ -533,6 +537,17 @@ module PowLoc = struct
         LocSet.mem l ploc
 
 
+  let get_parent_field ploc =
+    match ploc with
+    | Bottom ->
+        (* Return the unknown location to avoid unintended unreachable nodes *)
+        Unknown
+    | Unknown ->
+        Unknown
+    | Known ploc ->
+        mk_known (LocSet.fold (fun l -> LocSet.add (Loc.get_parent_field l)) ploc LocSet.empty)
+
+
   let append_field ploc ~fn =
     match ploc with
     | Bottom ->

infer/src/bufferoverrun/absLoc.mli

@@ -107,6 +107,8 @@ module PowLoc : sig
 
   val compare : t -> t -> int
 
+  val get_parent_field : t -> t
+
   val append_field : t -> fn:Fieldname.t -> t
 
   val append_star_field : t -> fn:Fieldname.t -> t

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -414,6 +414,8 @@ module Val = struct
 
   let prune_lt : t -> t -> t = prune_binop Binop.Lt
 
+  let prune_le : t -> t -> t = prune_binop Binop.Le
+
   let is_pointer_to_non_array x = (not (PowLoc.is_bot x.powloc)) && ArrayBlk.is_bot x.arrayblk
 
   (* In the pointer arithmetics, it returns top, if we cannot
@@ -717,6 +719,22 @@ module MemPure = struct
     Option.map (find_opt linked_list_index mem) ~f:(fun (_, v) -> (linked_list_index, v))
 
 
+  let get_objc_iterator_offset loc mem =
+    match find_opt loc mem with
+    | Some (_, array_v) -> (
+        let elem_loc = Val.get_all_locs array_v in
+        let array_set = PowLoc.get_parent_field elem_loc |> PowLoc.to_set in
+        match LocSet.max_elt_opt array_set with
+        | Some array_loc ->
+            let offset = Loc.append_field array_loc BufferOverrunField.objc_iterator_offset in
+            if Loc.is_unknown offset then None
+            else Option.map (find_opt offset mem) ~f:(fun (_, v) -> (offset, v))
+        | _ ->
+            None )
+    | _ ->
+        None
+
+
   let range :
          filter_loc:(Loc.t -> LoopHeadLoc.t option)
       -> node_id:ProcCfg.Normal.Node.id
@@ -728,6 +746,7 @@ module MemPure = struct
         match filter_loc loc with
         | Some loop_head_loc -> (
             let loc, v = Option.value (get_linked_list_index loc mem) ~default:(loc, v) in
+            let loc, v = Option.value (get_objc_iterator_offset loc mem) ~default:(loc, v) in
             let itv_updated_by = Val.get_itv_updated_by v in
             match itv_updated_by with
             | Addition | Multiplication ->
@@ -854,6 +873,7 @@ module AliasTarget = struct
     | IteratorSimple of {i: IntLit.t; java_tmp: Loc.t option}
     | IteratorOffset of {alias_typ: alias_typ; i: IntLit.t; java_tmp: Loc.t option}
     | IteratorHasNext of {java_tmp: Loc.t option}
+    | IteratorNextObject of {objc_tmp: AbsLoc.Loc.t option}
     | Top
   [@@deriving compare]
 
@@ -887,6 +907,8 @@ module AliasTarget = struct
             alias_typ_pp alias_typ pp_rhs pp_intlit i
       | IteratorHasNext {java_tmp} ->
           F.fprintf fmt "%t%a=hasNext(%t)" pp_lhs pp_java_tmp java_tmp pp_rhs
+      | IteratorNextObject {objc_tmp} ->
+          F.fprintf fmt "%t%a=nextObject(%t)" pp_lhs pp_java_tmp objc_tmp pp_rhs
       | Top ->
           F.fprintf fmt "%t=?%t" pp_lhs pp_rhs
 
@@ -901,7 +923,8 @@ module AliasTarget = struct
     | Size {java_tmp= Some tmp}
     | IteratorSimple {java_tmp= Some tmp}
     | IteratorOffset {java_tmp= Some tmp}
-    | IteratorHasNext {java_tmp= Some tmp} ->
+    | IteratorHasNext {java_tmp= Some tmp}
+    | IteratorNextObject {objc_tmp= Some tmp} ->
         PowLoc.singleton tmp
     | Simple {java_tmp= None}
     | Size {java_tmp= None}
@@ -910,6 +933,7 @@ module AliasTarget = struct
     | IteratorSimple {java_tmp= None}
     | IteratorOffset {java_tmp= None}
     | IteratorHasNext {java_tmp= None}
+    | IteratorNextObject {objc_tmp= None}
     | Top ->
         PowLoc.bot
 
@@ -932,6 +956,8 @@ module AliasTarget = struct
         IteratorOffset {alias_typ; i; java_tmp= Option.bind java_tmp ~f}
     | IteratorHasNext {java_tmp} ->
         IteratorHasNext {java_tmp= Option.bind java_tmp ~f}
+    | IteratorNextObject {objc_tmp} ->
+        IteratorNextObject {objc_tmp= Option.bind objc_tmp ~f}
     | Top ->
         Top
 
@@ -1023,6 +1049,8 @@ module AliasTarget = struct
         IteratorOffset {a with java_tmp= Some loc}
     | IteratorHasNext _ ->
         IteratorHasNext {java_tmp= Some loc}
+    | IteratorNextObject _ ->
+        IteratorNextObject {objc_tmp= Some loc}
     | _ as alias ->
         alias
 end
@@ -1157,22 +1185,20 @@ module AliasMap = struct
 
   let store : Loc.t -> Ident.t -> t -> t =
    fun l id x ->
-    if Language.curr_language_is Java then
+    let tgts = find_id id x in
-      let tgts = find_id id x in
+    if Loc.is_frontend_tmp l then add_aliases ~lhs:(KeyLhs.of_loc l) tgts x
-      if Loc.is_frontend_tmp l then add_aliases ~lhs:(KeyLhs.of_loc l) tgts x
+    else
-      else
+      let accum_java_tmp_alias rhs tgt acc =
-        let accum_java_tmp_alias rhs tgt acc =
+        match tgt with
-          match tgt with
+        | AliasTarget.Simple {i} when IntLit.iszero i && Loc.is_frontend_tmp rhs ->
-          | AliasTarget.Simple {i} when IntLit.iszero i && Loc.is_frontend_tmp rhs ->
+            add_alias ~lhs:(KeyLhs.of_id id) ~rhs:l (AliasTarget.Simple {i; java_tmp= Some rhs}) acc
-              add_alias ~lhs:(KeyLhs.of_id id) ~rhs:l
+            |> add_alias ~lhs:(KeyLhs.of_loc rhs) ~rhs:l (AliasTarget.Simple {i; java_tmp= None})
-                (AliasTarget.Simple {i; java_tmp= Some rhs})
+        | AliasTarget.IteratorNextObject _ ->
-                acc
+            add_alias ~lhs:(KeyLhs.of_loc l) ~rhs tgt acc
-              |> add_alias ~lhs:(KeyLhs.of_loc rhs) ~rhs:l (AliasTarget.Simple {i; java_tmp= None})
+        | _ ->
-          | _ ->
+            acc
-              acc
+      in
-        in
+      AliasTargets.fold accum_java_tmp_alias tgts x
-        AliasTargets.fold accum_java_tmp_alias tgts x
-    else x
 
 
   let add_size_alias ~lhs ~lhs_v ~arr ~arr_size x =
@@ -1297,6 +1323,24 @@ module AliasMap = struct
         AliasTargets.fold accum_has_next_alias tgts x
     | _ ->
         x
+
+
+  let add_iterator_next_object_alias ~ret_id ~iterator x =
+    let accum_next_object_alias rhs tgt acc =
+      match tgt with
+      | AliasTarget.IteratorSimple _ ->
+          add_alias ~lhs:(KeyLhs.of_id ret_id) ~rhs
+            (AliasTarget.IteratorNextObject {objc_tmp= None})
+            acc
+      | _ ->
+          acc
+    in
+    let open IOption.Let_syntax in
+    M.find_opt (KeyLhs.of_id iterator) x
+    >>= AliasTargets.find_simple_alias
+    >>= (fun rhs -> M.find_opt (KeyLhs.of_loc rhs) x)
+    >>| (fun tgts -> AliasTargets.fold accum_next_object_alias tgts x)
+    |> Option.value ~default:x
 end
 
 module AliasRet = struct
@@ -1421,6 +1465,10 @@ module Alias = struct
    fun ~ret_id ~iterator a -> lift_map (AliasMap.add_iterator_has_next_alias ~ret_id ~iterator) a
 
 
+  let add_iterator_next_object_alias : ret_id:Ident.t -> iterator:Ident.t -> t -> t =
+   fun ~ret_id ~iterator a -> lift_map (AliasMap.add_iterator_next_object_alias ~ret_id ~iterator) a
+
+
   let remove_temp : Ident.t -> t -> t = fun temp -> lift_map (AliasMap.remove (KeyLhs.of_id temp))
 
   let forget_size_alias arr_locs = lift_map (AliasMap.forget_size_alias arr_locs)
@@ -1996,12 +2044,21 @@ module MemReach = struct
 
   let add_iterator_alias id m = add_iterator_offset_alias id m |> add_iterator_simple_alias id
 
+  let add_iterator_alias_objc id m =
+    let array_loc = find_stack (Loc.of_id id) m |> Val.get_pow_loc in
+    {m with alias= Alias.add_iterator_simple_alias id array_loc m.alias}
+
+
   let incr_iterator_offset_alias id m = {m with alias= Alias.incr_iterator_offset_alias id m.alias}
 
   let add_iterator_has_next_alias ~ret_id ~iterator m =
     {m with alias= Alias.add_iterator_has_next_alias ~ret_id ~iterator m.alias}
 
 
+  let add_iterator_next_object_alias ~ret_id ~iterator m =
+    {m with alias= Alias.add_iterator_next_object_alias ~ret_id ~iterator m.alias}
+
+
   let incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m =
     let callee_locs = MemPure.get_incr_locs callee_exit_mem.mem_pure in
     {m with alias= Alias.incr_iterator_simple_alias_on_call eval_sym_trace ~callee_locs m.alias}
@@ -2368,6 +2425,10 @@ module Mem = struct
 
   let add_iterator_alias : Ident.t -> t -> t = fun id -> map ~f:(MemReach.add_iterator_alias id)
 
+  let add_iterator_alias_objc : Ident.t -> t -> t =
+   fun id -> map ~f:(MemReach.add_iterator_alias_objc id)
+
+
   let incr_iterator_offset_alias : Exp.t -> t -> t =
    fun iterator m ->
     match iterator with Exp.Var id -> map ~f:(MemReach.incr_iterator_offset_alias id) m | _ -> m
@@ -2382,6 +2443,15 @@ module Mem = struct
         m
 
 
+  let add_iterator_next_object_alias : Ident.t -> Exp.t -> t -> t =
+   fun ret_id iterator m ->
+    match iterator with
+    | Exp.Var iterator ->
+        map ~f:(MemReach.add_iterator_next_object_alias ~ret_id ~iterator) m
+    | _ ->
+        m
+
+
   let incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m =
     match (callee_exit_mem, m) with
     | Reachable callee_exit_mem, Reachable m ->

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -221,6 +221,10 @@ module Val : sig
   (** Pruning semantics for [Binop.Lt]. This prunes value of [x] when given [x < y], i.e.,
       [prune_lt x y]. *)
 
+  val prune_le : t -> t -> t
+  (** Pruning semantics for [Binop.Lt]. This prunes value of [x] when given [x <= y], i.e.,
+      [prune_le x y]. *)
+
   val prune_ne_zero : t -> t
   (** Prune value of [x] when given [x != 0] *)
 
@@ -334,6 +338,9 @@ module AliasTarget : sig
     | IteratorHasNext of {java_tmp: AbsLoc.Loc.t option}
         (** This is for tracking return values of the [hasNext] function. If [%r] has an alias to
             [HasNext {l}], which means that [%r] is same to [l.hasNext()]. *)
+    | IteratorNextObject of {objc_tmp: AbsLoc.Loc.t option}
+        (** This is for tracking the return values of [nextObject] function. If [%r] has an alias to
+            [nextObject {l}], which means that [%r] is the same to [l.nextObject()]. *)
     | Top
 
   include AbstractDomain.S with type t := t
@@ -579,6 +586,9 @@ module Mem : sig
   val add_iterator_has_next_alias : Ident.t -> Exp.t -> t -> t
   (** Add an [AliasTarget.IteratorHasNext] alias when [ident = iterator.hasNext()] is called *)
 
+  val add_iterator_next_object_alias : Ident.t -> Exp.t -> t -> t
+  (** Add an [AliasTarget.IteratorNextObject] alias when [ident = iterator.nextObject()] is called *)
+
   val incr_iterator_simple_alias_on_call : eval_sym_trace -> callee_exit_mem:no_oenv_t -> t -> t
   (** Update [AliasTarget.IteratorSimple] alias at function calls *)
 
@@ -586,6 +596,8 @@ module Mem : sig
   (** Add [AliasTarget.IteratorSimple] and [AliasTarget.IteratorOffset] aliases when
       [Iteratable.iterator()] is called *)
 
+  val add_iterator_alias_objc : Ident.t -> t -> t
+
   val incr_iterator_offset_alias : Exp.t -> t -> t
   (** Update iterator offset alias when [iterator.next()] is called *)
 

infer/src/bufferoverrun/bufferOverrunField.ml

@@ -43,6 +43,8 @@ let is_java_collection_internal_array fn = Fieldname.equal fn java_collection_in
 
 let objc_collection_internal_array = mk "nscollection.elements" Typ.(mk_array void)
 
+let objc_iterator_offset = mk "nsiterator.offset" Typ.(mk_array void)
+
 let c_strlen () =
   if Language.curr_language_is Java then mk "length" Typ.uint else mk "c.strlen" Typ.uint
 

infer/src/bufferoverrun/bufferOverrunField.mli

@@ -50,6 +50,9 @@ val is_java_collection_internal_array : Fieldname.t -> bool
 val objc_collection_internal_array : Fieldname.t
 (** Field for ObjC's collection's elements *)
 
+val objc_iterator_offset : Fieldname.t
+(** Field for ObjC's nscollection's iterator offset *)
+
 (** {2 Field domain constructor} *)
 
 type field_typ = Typ.t option

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -1115,6 +1115,39 @@ module NSCollection = struct
       |> model_by_value coll id
     in
     {exec; check= no_check}
+
+
+  let iterator coll_exp =
+    let exec {integer_type_widths; location} ~ret:(ret_id, _) mem =
+      let traces = Trace.(Set.singleton location ArrayDeclaration) in
+      let array_v = Sem.eval integer_type_widths coll_exp mem in
+      let array_loc = Dom.Val.get_all_locs array_v in
+      let offset_loc = PowLoc.append_field ~fn:BufferOverrunField.objc_iterator_offset array_loc in
+      let mem = Dom.Mem.add_heap_set offset_loc Dom.Val.Itv.zero mem in
+      model_by_value (Dom.Val.of_pow_loc ~traces array_loc) ret_id mem
+      |> Dom.Mem.add_heap_set array_loc array_v
+      |> Dom.Mem.add_iterator_alias_objc ret_id
+    in
+    {exec; check= no_check}
+
+
+  let next_object iterator =
+    let exec {integer_type_widths} ~ret:(id, _) mem =
+      let iterator_v = Sem.eval integer_type_widths iterator mem in
+      let traces = Dom.Val.get_traces iterator_v in
+      let offset_loc =
+        Dom.Val.get_pow_loc iterator_v
+        |> PowLoc.append_field ~fn:BufferOverrunField.objc_iterator_offset
+      in
+      let next_offset_v =
+        Dom.Mem.find_set offset_loc mem |> Dom.Val.get_itv |> Itv.incr |> Dom.Val.of_itv
+      in
+      let locs = eval_collection_internal_array_locs iterator mem in
+      model_by_value (Dom.Val.of_pow_loc ~traces locs) id mem
+      |> Dom.Mem.add_heap_set offset_loc next_offset_v
+      |> Dom.Mem.add_iterator_next_object_alias id iterator
+    in
+    {exec; check= no_check}
 end
 
 module JavaClass = struct
@@ -1640,6 +1673,10 @@ module Call = struct
         &:: "arrayWithObjects:count:" <>$ capt_exp $+ capt_exp $--> NSCollection.create_from_array
       ; +PatternMatch.ObjectiveC.implements "NSArray"
         &:: "arrayWithObjects" &++> NSCollection.of_list
+      ; +PatternMatch.ObjectiveC.implements "NSArray"
+        &:: "objectEnumerator" <>$ capt_exp $--> NSCollection.iterator
+      ; +PatternMatch.ObjectiveC.implements "NSEnumerator"
+        &:: "nextObject" <>$ capt_exp $--> NSCollection.next_object
       ; +PatternMatch.ObjectiveC.implements "NSMutableArray"
         &:: "addObject:" <>$ capt_var_exn $+ capt_exp $--> NSCollection.add
       ; +PatternMatch.ObjectiveC.implements "NSMutableArray"

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -582,6 +582,32 @@ module Prune = struct
             update_mem_in_prune lv_linked_list_index pruned_v acc ) )
 
 
+  let nscollection_length_of_iterator loc mem =
+    let arr_locs =
+      Mem.find loc mem |> Val.get_all_locs
+      |> PowLoc.append_field ~fn:BufferOverrunField.objc_collection_internal_array
+    in
+    eval_array_locs_length arr_locs mem
+
+
+  let prune_iterator_offset_objc next_object mem acc =
+    let tgts = Mem.find_alias_loc next_object mem in
+    AliasTargets.fold
+      (fun rhs tgt acc ->
+        match tgt with
+        | AliasTarget.IteratorNextObject _ ->
+            let array_length = nscollection_length_of_iterator rhs mem in
+            let iterator_offset_loc =
+              Loc.append_field rhs BufferOverrunField.objc_iterator_offset
+            in
+            let iterator_offset_v = Mem.find iterator_offset_loc mem in
+            let iterator_offset_v' = Val.prune_le iterator_offset_v array_length in
+            update_mem_in_prune iterator_offset_loc iterator_offset_v' acc
+        | _ ->
+            acc )
+      tgts acc
+
+
   let prune_unop : Exp.t -> t -> t =
    fun e ({mem} as astate) ->
     match e with
@@ -595,6 +621,7 @@ module Prune = struct
                  let v' = Val.prune_ne_zero v in
                  update_mem_in_prune rhs v' acc )
               |> prune_linked_list_index rhs mem
+              |> prune_iterator_offset_objc rhs mem
           | AliasTarget.Empty ->
               let v = Mem.find rhs mem in
               if Val.is_bot v then acc

infer/src/checkers/purityModels.ml

@@ -50,6 +50,7 @@ module ProcName = struct
       ; -"__variable_initialization" <>--> PurityDomain.pure
       ; +(fun _ name -> BuiltinDecl.is_declared (Procname.from_string_c_fun name))
         <>--> PurityDomain.impure_global
+      ; +PatternMatch.ObjectiveC.implements "NSEnumerator" &:: "nextObject" <>--> modifies_first
       ; +PatternMatch.Java.implements_android "text.TextUtils" &:: "isEmpty" <>--> PurityDomain.pure
       ; +PatternMatch.Java.implements_android "view.ViewGroup"
         &:: "getChildAt" <>--> PurityDomain.pure

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

@@ -163,7 +163,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun2_Bad, 2, BUFFER
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: [max(10, i), i] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: [i, min(-1, i)] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: unknown_function,Binary operation: ([-oo, +oo] × 10):signed32]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
@@ -274,7 +274,7 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Bad, 6, BUFFER_OVERRU
 codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Good, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: unknown1,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-28, 16] Size: 17]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-28, 16] Size: 17]
-codetoanalyze/c/bufferoverrun/prune_constant.c, call_greater_than_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/prune_constant.c, call_greater_than_Good, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_3_Good_FP, 7, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `a`,Assignment,<Length trace>,Parameter `a`,Assignment,Array declaration,Array access: Offset: [-1, 9] Size: [0, 10] by call to `null_pruning_symbols` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_3_Good_FP, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Call,<LHS trace>,Parameter `a`,Assignment,Binary operation: ([0, 10] - 1):unsigned32 by call to `null_pruning_symbols` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_add2` ]

infer/tests/codetoanalyze/objc/performance/NSArray.m

@@ -145,14 +145,14 @@ NSArray* nsarray_sort_using_descriptors_nlogn_FN(NSArray* array) {
 
 // iterate through array
 
-void nsarray_iterate_linear_FN(NSArray* array) {
+void nsarray_iterate_linear(NSArray* array) {
   NSInteger sum = 0;
   for (id obj in array) {
     sum += (NSInteger)obj;
   }
 }
 
-void nsarray_enumerator_linear_FN(NSArray* array) {
+void nsarray_enumerator_linear_FP(NSArray* array) {
   NSEnumerator* enumerator = [array objectEnumerator];
 
   id obj;
@@ -163,7 +163,13 @@ void nsarray_enumerator_linear_FN(NSArray* array) {
   }
 }
 
-void nsarray_next_object_linear_FN(NSArray* array) {
+void nsarray_next_object_linear(NSArray* array) {
+  for (id item in array) {
+  }
+}
+
+void nsarray_next_object_constant_FP() {
+  NSArray* array = @[ @1, @2 ];
   for (id item in array) {
   }
 }

infer/tests/codetoanalyze/objc/performance/block.m

@@ -6,7 +6,7 @@
  */
 #import <Foundation/Foundation.h>
 
-NSInteger block_multiply_array_linear_FN(NSArray* array) {
+NSInteger block_multiply_array_linear(NSArray* array) {
   NSInteger (^sum_array)(NSArray*) = ^(NSArray* array) {
     NSInteger n = 0;
     for (id value in array) {

infer/tests/codetoanalyze/objc/performance/cost-issues.exp

@@ -7,7 +7,7 @@ codetoanalyze/objc/performance/NSArray.m, nsarray_binary_search_log_FN, 10,  OnU
 codetoanalyze/objc/performance/NSArray.m, nsarray_contains_object_linear, 3 + array->elements.length.ub,  OnUIThread:false, [{array->elements.length.ub},Modeled call to NSArray.containsObject:]
 codetoanalyze/objc/performance/NSArray.m, nsarray_count_bounded_linear, 3 + 3 ⋅ array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_empty_array_constant, 8,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_linear_FN, 14,  OnUIThread:false, []
+codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_linear_FP, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_find_linear, 4 + 9 ⋅ array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_first_object_constant, 4,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_get_first_constant, 27,  OnUIThread:false, []
@@ -17,9 +17,10 @@ codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_copy_linear, 7
 codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_linear, 6 + 3 ⋅ array->elements.length.ub + array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Modeled call to NSArray.initWithArray:,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_objects_constant, 39,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_is_equal_to_array_linear, 4 + array1->elements.length.ub,  OnUIThread:false, [{array1->elements.length.ub},Modeled call to NSArray.isEqualToArray:]
-codetoanalyze/objc/performance/NSArray.m, nsarray_iterate_linear_FN, 14,  OnUIThread:false, []
+codetoanalyze/objc/performance/NSArray.m, nsarray_iterate_linear, 6 + 4 ⋅ array->elements.length.ub + 4 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_last_object_constant, 4,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSArray.m, nsarray_next_object_linear_FN, 10,  OnUIThread:false, []
+codetoanalyze/objc/performance/NSArray.m, nsarray_next_object_constant_FP, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
+codetoanalyze/objc/performance/NSArray.m, nsarray_next_object_linear, 5 + array->elements.length.ub + 4 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_object_at_indexed_constant, 34,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_sort_using_descriptors_constant, 34,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_sort_using_descriptors_nlogn_FN, 10,  OnUIThread:false, []
@@ -77,8 +78,8 @@ codetoanalyze/objc/performance/araii.m, Araii.dealloc, 4,  OnUIThread:false, []
 codetoanalyze/objc/performance/araii.m, Araii.initWithBuffer, 15,  OnUIThread:false, []
 codetoanalyze/objc/performance/araii.m, Araii.setBuffer:, 4,  OnUIThread:false, []
 codetoanalyze/objc/performance/araii.m, memory_leak_raii_main, 18,  OnUIThread:false, []
-codetoanalyze/objc/performance/block.m, block_multiply_array_linear_FN, 22,  OnUIThread:false, []
+codetoanalyze/objc/performance/block.m, block_multiply_array_linear, 13 + 5 ⋅ array->elements.length.ub + 4 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Call to objc_blockblock_multiply_array_linear_1,Loop,{array->elements.length.ub},Call to objc_blockblock_multiply_array_linear_1,Loop]
-codetoanalyze/objc/performance/block.m, objc_blockblock_multiply_array_linear_FN_1, 17,  OnUIThread:false, []
+codetoanalyze/objc/performance/block.m, objc_blockblock_multiply_array_linear_1, 8 + 5 ⋅ array->elements.length.ub + 4 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/break.m, break_constant_FP, 8 + 5 ⋅ p + 2 ⋅ (1+max(0, p)),  OnUIThread:false, [{1+max(0, p)},Call to break_loop,Loop,{p},Call to break_loop,Loop]
 codetoanalyze/objc/performance/break.m, break_loop, 5 + 5 ⋅ p + 2 ⋅ (1+max(0, p)),  OnUIThread:false, [{1+max(0, p)},Loop,{p},Loop]
 codetoanalyze/objc/performance/break.m, break_loop_with_t, 7 + 5 ⋅ p + 2 ⋅ (1+max(0, p)),  OnUIThread:false, [{1+max(0, p)},Loop,{p},Loop]

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

@@ -1,9 +1,7 @@
 codetoanalyze/objc/performance/NSArray.m, nsarray_empty_array_constant, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_linear_FN, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: NSEnumerator.nextObject,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed64]
+codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_linear_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_init_constant, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/objc/performance/NSArray.m, nsarray_iterate_linear_FN, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: NSEnumerator.nextObject,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed64]
+codetoanalyze/objc/performance/NSArray.m, nsarray_next_object_constant_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
-codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_enumerate_constant, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: NSEnumerator.nextObject,Assignment,<Length trace>,Unknown value from: NSEnumerator.nextObject,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [-oo, +oo]) Size: [0, +oo]]
-codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_find_key_linear_FN, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: NSEnumerator.nextObject,Assignment,<Length trace>,Unknown value from: NSEnumerator.nextObject,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [-oo, +oo]) Size: [0, +oo]]
 codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_init_with_dictionary_linear_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
 codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_init_with_dictionary_linear_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSDictionary.initWithDictionary:,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_add_in_loop_constant_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
@@ -20,7 +18,6 @@ codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_set_linear, 2, INTEGER
 codetoanalyze/objc/performance/NSString.m, init_string_constant, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/NSString.m, replace_linear_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
 codetoanalyze/objc/performance/NSString.m, replace_linear_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSString.stringByReplacingOccurrencesOfString:withString:,Binary operation: ([0, +oo] + 1):signed32]
-codetoanalyze/objc/performance/block.m, objc_blockblock_multiply_array_linear_FN_1, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: NSEnumerator.nextObject,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed64]
 codetoanalyze/objc/performance/compound_loop_guard.m, compound_while, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/compound_loop_guard.m, nested_while_and_or_constant, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/compound_loop_guard.m, nested_while_and_or_constant, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]