diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 2a24e1df4..b9aa1d47d 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -206,7 +206,7 @@ module Make (CFG : ProcCfg.S) = struct | Exp.Cast (_, e) -> eval e mem | Exp.Lfield (e, fn, _) -> - eval e mem |> Val.get_array_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc + eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc | Exp.Lindex (e1, e2) -> eval_lindex e1 e2 mem | Exp.Sizeof {nbytes= Some size} -> @@ -217,13 +217,23 @@ module Make (CFG : ProcCfg.S) = struct Val.Itv.top + (* NOTE: multidimensional array is not supported yet *) and eval_lindex array_exp index_exp mem = - let arr = Val.plus_pi (eval array_exp mem) (eval index_exp mem) in - let ploc = - if ArrayBlk.is_bot (Val.get_array_blk arr) then PowLoc.unknown else Val.get_all_locs arr - in - (* NOTE: multidimensional array is not supported yet *) - Val.join (Val.of_pow_loc ploc) arr + let array_v, index_v = (eval array_exp mem, eval index_exp mem) in + let arr = Val.plus_pi array_v index_v in + if ArrayBlk.is_bot (Val.get_array_blk arr) then + match array_exp with + | Exp.Lfield _ when not (PowLoc.is_bot (Val.get_pow_loc array_v)) -> + (* It handles the case accessing an array field of struct, + e.g., x.f[n] . Since our abstract domain distinguishes + memory sections for each array fields in struct, it finds + the memory section using the abstract memory, though the + memory lookup is not required to evaluate the address of + x.f[n] in the concrete semantics. *) + Mem.find_set (Val.get_pow_loc array_v) mem + | _ -> + Val.of_pow_loc PowLoc.unknown + else arr and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_field.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_field.c new file mode 100644 index 000000000..386bf1693 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_field.c @@ -0,0 +1,25 @@ +/* + * Copyright (c) 2018 - 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. + */ +struct S1 { + int f[2]; +}; + +void array_field_access_Good(struct S1 x, struct S1 y) { + int a[10]; + x.f[0] = 1; + y.f[0] = 20; + a[x.f[0]] = 0; +} + +void array_field_access_Bad(struct S1 x, struct S1 y) { + int a[10]; + y.f[0] = 20; + x.f[0] = 1; + a[y.f[0]] = 0; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 5ccf6c651..e909ca61b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,6 +1,7 @@ codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]] codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]] codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]] +codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [20, 20] Size: [10, 10]] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]]