[inferbo] Add models for basic array iterator

Reviewed By: mbouaziz

Differential Revision: D13858898

fbshipit-source-id: 4518dad05

infer/src/bufferoverrun/arrayBlk.ml

@@ -219,6 +219,17 @@ module ArrInfo = struct
         Top
 
 
+  let set_offset : Itv.t -> t -> t =
+   fun offset arr ->
+    match arr with
+    | C {size; stride} ->
+        C {offset; size; stride}
+    | Java _ ->
+        L.(die InternalError) "Unexpected offset setting on Java array"
+    | Top ->
+        Top
+
+
   let offsetof = function C {offset} -> offset | Java _ -> Itv.zero | Top -> Itv.top
 
   let sizeof = function C {size} -> size | Java {length} -> length | Top -> Itv.top
@@ -337,6 +348,8 @@ let set_length : Itv.t -> t -> t = fun length a -> map (ArrInfo.set_length lengt
 
 let set_stride : Z.t -> t -> t = fun stride a -> map (ArrInfo.set_stride stride) a
 
+let set_offset : Itv.t -> t -> t = fun offset a -> map (ArrInfo.set_offset offset) a
+
 let lift_cmp_itv cmp_itv cmp_loc arr1 arr2 =
   match (is_singleton_or_more arr1, is_singleton_or_more arr2) with
   | IContainer.Singleton (as1, ai1), IContainer.Singleton (as2, ai2) ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -390,6 +390,13 @@ module Val = struct
     ; traces= Trace.(Set.add_elem location (through ~risky_fun:None)) v.traces }
 
 
+  let set_array_offset : Location.t -> Itv.t -> t -> t =
+   fun location offset v ->
+    { v with
+      arrayblk= ArrayBlk.set_offset offset v.arrayblk
+    ; traces= Trace.(Set.add_elem location (through ~risky_fun:None)) v.traces }
+
+
   let set_array_stride : Z.t -> t -> t =
    fun new_stride v ->
     PhysEqual.optim1 v ~res:{v with arrayblk= ArrayBlk.set_stride new_stride v.arrayblk}

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -420,6 +420,38 @@ module StdArray = struct
         location cond_set
     in
     {exec; check}
+
+
+  let begin_ _size (array_exp, _) =
+    let exec {location; integer_type_widths} ~ret:(id, _) mem =
+      let v =
+        Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location Itv.zero
+      in
+      Dom.Mem.add_stack (Loc.of_id id) v mem
+    in
+    {exec; check= no_check}
+
+
+  let end_ size (array_exp, _) =
+    let exec {location; integer_type_widths} ~ret:(id, _) mem =
+      let v =
+        let offset = Itv.of_int_lit (IntLit.of_int64 size) in
+        Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location offset
+      in
+      Dom.Mem.add_stack (Loc.of_id id) v mem
+    in
+    {exec; check= no_check}
+
+
+  let back size (array_exp, _) =
+    let exec {location; integer_type_widths} ~ret:(id, _) mem =
+      let v =
+        let offset = Itv.of_int_lit (IntLit.of_int64 Int64.(size - one)) in
+        Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location offset
+      in
+      Dom.Mem.add_stack (Loc.of_id id) v mem
+    in
+    {exec; check= no_check}
 end
 
 module StdBasicString = struct
@@ -629,6 +661,7 @@ module Call = struct
     let open ProcnameDispatcher.Call in
     let mk_std_array () = -"std" &:: "array" < any_typ &+ capt_int in
     let std_array0 = mk_std_array () in
+    let std_array1 = mk_std_array () in
     let std_array2 = mk_std_array () in
     let char_ptr = Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)) in
     make_dispatcher
@@ -667,6 +700,12 @@ module Call = struct
         $+ capt_arg_of_typ (-"std" &:: "vector")
         $+? capt_exp $--> Folly.Split.std_vector
       ; std_array0 >:: "array" &--> StdArray.constructor
+      ; std_array1 >:: "begin" $ capt_arg $!--> StdArray.begin_
+      ; std_array1 >:: "cbegin" $ capt_arg $!--> StdArray.begin_
+      ; std_array1 >:: "end" $ capt_arg $!--> StdArray.end_
+      ; std_array1 >:: "cend" $ capt_arg $!--> StdArray.end_
+      ; std_array1 >:: "front" $ capt_arg $!--> StdArray.begin_
+      ; std_array1 >:: "back" $ capt_arg $!--> StdArray.back
       ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at
       ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at
       ; -"std" &:: "array" &::.*--> no_model

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

@@ -77,6 +77,15 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, gal_FP, 4, INTEGER_OVERFLOW_L5, no_b
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter `t->bI`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [-1+max(1, t->bI.lb), -1+max(1, t->bI.ub)] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
 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/std_array.cpp, array_iter1_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: [0, +oo] Size: 5]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Good_FP, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: [0, +oo] Size: 11]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_front_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_rev_iter_Bad, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_rev_iter_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 11]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 4611686018427387903]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 9223372036854775807]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 9223372036854775807):unsigned64]

infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp

@@ -51,3 +51,90 @@ void std_array_contents_Bad() {
   a[0] = 10;
   a[a[0]] = 0;
 }
+
+void array_iter1_Good() {
+  std::array<int, 11> a;
+  for (auto it = a.begin(); it < a.end(); ++it) {
+    *it = 10;
+  }
+  a[a[0]] = 0;
+}
+
+void array_iter1_Bad() {
+  std::array<int, 5> a;
+  for (auto it = a.begin(); it < a.end(); ++it) {
+    *it = 10;
+  }
+  a[a[0]] = 0;
+}
+
+// TODO: Inferbo should give a preciser widening threshold.
+void array_iter2_Good_FP() {
+  std::array<int, 11> a;
+  for (auto it = a.begin(); it != a.end(); ++it) {
+    *it = 10;
+  }
+  a[a[0]] = 0;
+}
+
+void array_iter2_Bad() {
+  std::array<int, 5> a;
+  for (auto it = a.begin(); it != a.end(); ++it) {
+    *it = 10;
+  }
+  a[a[0]] = 0;
+}
+
+void array_iter3_Good() {
+  std::array<int, 11> a = {10};
+  for (auto it = a.cbegin(); it < a.cend(); ++it) {
+    a[*it] = 10;
+  }
+}
+
+void array_iter3_Bad() {
+  std::array<int, 5> a = {10};
+  for (auto it = a.cbegin(); it < a.cend(); ++it) {
+    a[*it] = 10;
+  }
+}
+
+void array_iter_front_Good() {
+  std::array<int, 11> a;
+  a.front() = 10;
+  a[a[0]] = 0;
+}
+
+void array_iter_front_Bad() {
+  std::array<int, 5> a;
+  a.front() = 10;
+  a[a[0]] = 0;
+}
+
+void array_iter_back_Good() {
+  std::array<int, 11> a;
+  a.back() = 10;
+  a[a[0]] = 0;
+}
+
+void array_iter_back_Bad() {
+  std::array<int, 5> a;
+  a.back() = 10;
+  a[a[0]] = 0;
+}
+
+void array_rev_iter_Good_FP() {
+  std::array<int, 11> a;
+  for (auto it = a.rbegin(); it < a.rend(); ++it) {
+    *it = 10;
+  }
+  a[a[0]] = 0;
+}
+
+void array_rev_iter_Bad() {
+  std::array<int, 5> a;
+  for (auto it = a.rbegin(); it < a.rend(); ++it) {
+    *it = 10;
+  }
+  a[a[0]] = 0;
+}