[inferbo] First models for std::array

Reviewed By: jberdine

Differential Revision: D6408415

fbshipit-source-id: 114776c

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -206,9 +206,50 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
     end
   end
 
+  module StdArray = struct
+    let typ typ length =
+      let declare_local ~decl_local pname node location loc ~inst_num ~dimension mem =
+        (* should this be deferred to the constructor? *)
+        let length = Some (IntLit.of_int64 length) in
+        BoUtils.Exec.decl_local_array ~decl_local pname node location loc typ ~length ~inst_num
+          ~dimension mem
+      in
+      let declare_symbolic ~decl_sym_val pname tenv node 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 location ~depth loc typ ~offset
+          ~size ~inst_num ~new_sym_num ~new_alloc_num mem
+      in
+      {declare_local; declare_symbolic}
+
+
+    let constructor _size =
+      let exec _pname _ret _node _location mem = mem (* initialize? *) in
+      {exec; check= no_check}
+
+
+    let at _size (array_exp, _) (index_exp, _) =
+      (* TODO? use size *)
+      let exec _pname ret _node _location mem =
+        L.(debug BufferOverrun Verbose) "Using model std::array<_, %Ld>::at" _size ;
+        match ret with
+        | Some (id, _) ->
+            BoUtils.Exec.load_val id (Sem.eval_lindex array_exp index_exp mem) mem
+        | None ->
+            mem
+      and check pname _node location mem cond_set =
+        BoUtils.Check.lindex ~array_exp ~index_exp mem pname location cond_set
+      in
+      {exec; check}
+  end
+
   module Procname = struct
     let dispatch : model ProcnameDispatcher.dispatcher =
       let open ProcnameDispatcher.Procname in
+      let mk_std_array () = -"std" &:: "array" < any_typ &+ capt_int in
+      let std_array0 = mk_std_array () in
+      let std_array2 = mk_std_array () in
       make_dispatcher
         [ -"__inferbo_min" <>$ capt_exp $+ capt_exp $!--> inferbo_min
         ; -"__inferbo_set_size" <>$ capt_exp $+ capt_exp $!--> inferbo_set_size
@@ -224,11 +265,15 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
         ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg
           $+? any_arg $--> Boost.Split.std_vector
         ; -"folly" &:: "split" $ any_arg $+ any_arg $+ capt_arg_of_typ (-"std" &:: "vector")
-          $+? capt_exp $--> Folly.Split.std_vector ]
+          $+? capt_exp $--> Folly.Split.std_vector
+        ; std_array0 >:: "array" &--> StdArray.constructor
+        ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at
+        ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at ]
   end
 
   module TypName = struct
     let dispatch : typ_model ProcnameDispatcher.typ_dispatcher =
-      ProcnameDispatcher.TypName.make_dispatcher []
+      let open ProcnameDispatcher.TypName in
+      make_dispatcher [-"std" &:: "array" < capt_typ `T &+ capt_int >--> StdArray.typ]
   end
 end

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -24,13 +24,31 @@ module type S = sig
   type counter = unit -> int
 
   module Exec : sig
+    val load_val : Ident.t -> Dom.Val.astate -> Dom.Mem.astate -> Dom.Mem.astate
+
     type decl_local =
       Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t -> inst_num:int -> dimension:int
       -> Dom.Mem.astate -> Dom.Mem.astate * int
 
+    val decl_local_array :
+      decl_local:decl_local -> Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t
+      -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate
+      -> Dom.Mem.astate * int
+
     type decl_sym_val =
       Typ.Procname.t -> Tenv.t -> CFG.node -> 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 -> CFG.node -> Location.t -> depth:int
+      -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int -> new_sym_num:counter
+      -> new_alloc_num:counter -> Dom.Mem.astate -> Dom.Mem.astate
+  end
+
+  module Check : sig
+    val lindex :
+      array_exp:Exp.t -> index_exp:Exp.t -> Dom.Mem.astate -> Typ.Procname.t -> Location.t
+      -> PO.ConditionSet.t -> PO.ConditionSet.t
   end
 end
 

infer/src/bufferoverrun/itv.ml

@@ -1145,6 +1145,10 @@ let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n)
 
 let of_int_lit n = try of_int (IntLit.to_int n) with _ -> top
 
+let of_int64 : Int64.t -> astate =
+  fun n -> Int64.to_int n |> Option.value_map ~f:of_int ~default:top
+
+
 let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false
 
 let false_sem = NonBottom ItvPure.false_sem

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

@@ -13,6 +13,8 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_u_FP, 5, BUFFER_OVERRUN_S2,
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, [Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ]
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]

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

@@ -0,0 +1,19 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#include <array>
+
+int std_array_bo_Bad() {
+  std::array<int, 42> a;
+  return a[42];
+}
+
+int normal_array_bo() {
+  int b[42];
+  return b[42];
+}