diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 5004ff575..dff34d994 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 731b60b3d..5a8c7b1e0 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 552c7affe..1f4215340 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 497cdfc92..dee60773e 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/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]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/symb_arr.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/symb_arr.cpp new file mode 100644 index 000000000..441888734 --- /dev/null +++ b/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'; } +};