Fixed a bug that caused the stride of symbolic arrays to not be set.

Reviewed By: jvillard

Differential Revision: D9850740

fbshipit-source-id: ac3be9980

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -287,7 +287,7 @@ module Init = struct
             BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname
               symbol_table path tenv ~node_hash location ~depth loc typ ~inst_num ~new_sym_num
               ~new_alloc_num mem
-        | Typ.Tarray {elt; length} ->
+        | Typ.Tarray {elt; length; stride} ->
             let size =
               match length with
               | Some length when may_last_field && (IntLit.iszero length || IntLit.isone length) ->
@@ -296,9 +296,10 @@ module Init = struct
                   Option.map ~f:Itv.of_int_lit length
             in
             let offset = Itv.zero in
+            let stride = Option.map ~f:IntLit.to_int_exn stride in
             BoUtils.Exec.decl_sym_arr
               ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-              pname symbol_table path tenv ~node_hash location ~depth loc elt ~offset ?size
+              pname symbol_table path tenv ~node_hash location ~depth loc elt ~offset ?size ?stride
               ~inst_num ~new_sym_num ~new_alloc_num mem
         | Typ.Tstruct typename -> (
           match Models.TypName.dispatch tenv typename with

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -124,13 +124,14 @@ module Exec = struct
       -> Typ.t
       -> ?offset:Itv.t
       -> ?size:Itv.t
+      -> ?stride:int
       -> 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 symbol_table path tenv ~node_hash location ~depth loc typ ?offset ?size
-       ~inst_num ~new_sym_num ~new_alloc_num mem ->
+       ?stride ~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 () ->
@@ -147,7 +148,7 @@ module Exec = struct
       Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some path)
     in
     let arr =
-      Dom.Val.of_array_alloc allocsite ~stride:None ~offset ~size |> Dom.Val.add_trace_elem elem
+      Dom.Val.of_array_alloc allocsite ~stride ~offset ~size |> Dom.Val.add_trace_elem elem
     in
     let mem =
       mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -76,6 +76,7 @@ module Exec : sig
     -> Typ.t
     -> ?offset:Itv.t
     -> ?size:Itv.t
+    -> ?stride:int
     -> inst_num:int
     -> new_sym_num:Itv.Counter.t
     -> new_alloc_num:Itv.Counter.t

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

@@ -37,6 +37,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bu
 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 Size: v[*]._size 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 Size: 42]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42]
+codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 6 Size: 5]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 4 Size: [0, +oo]]

infer/tests/codetoanalyze/cpp/bufferoverrun/symb_arr.cpp

@@ -0,0 +1,11 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+struct symb_arr_alloc {
+  char h[10];
+  void symb_arr_access_ok() { h[9] = '\0'; }
+  void symb_arr_access_bad() { h[10] = '\0'; }
+};