From 5c4de212fb34b913e15cad41eabee0631d7231ec Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 13 Dec 2018 06:40:31 -0800 Subject: [PATCH] [inferbo] New test + more debug Reviewed By: jvillard Differential Revision: D13450070 fbshipit-source-id: d6f53baca --- .../src/bufferoverrun/bufferOverrunDomain.ml | 22 +++++++++++---- .../c/bufferoverrun/flexible_array.c | 27 +++++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 2 ++ 3 files changed, 46 insertions(+), 5 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/flexible_array.c diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index a6dc9a593..870f909bb 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -343,6 +343,9 @@ module Val = struct let of_path ~may_last_field integer_type_widths location typ path = let is_java = Language.curr_language_is Java in + L.d_printfln "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ + (if may_last_field then ", may_last_field" else "") + (if is_java then ", is_java" else "") ; match typ.Typ.desc with | Tint _ | Tfloat _ | Tvoid | Tfun _ | TVar _ -> let l = Loc.of_path path in @@ -395,11 +398,20 @@ module Val = struct let on_demand : default:t -> OndemandEnv.t -> Loc.t -> t = fun ~default {typ_of_param_path; may_last_field; entry_location; integer_type_widths} l -> - Option.value_map (Loc.get_path l) ~default ~f:(fun path -> - Option.value_map (typ_of_param_path path) ~default ~f:(fun typ -> - let may_last_field = may_last_field path in - let path = OndemandEnv.canonical_path typ_of_param_path path in - of_path ~may_last_field integer_type_widths entry_location typ path ) ) + match Loc.get_path l with + | None -> + L.d_printfln "Val.on_demand for %a -> no path" Loc.pp l ; + default + | Some path -> ( + match typ_of_param_path path with + | None -> + L.d_printfln "Val.on_demand for %a -> no type" Loc.pp l ; + default + | Some typ -> + L.d_printfln "Val.on_demand for %a" Loc.pp l ; + let may_last_field = may_last_field path in + let path = OndemandEnv.canonical_path typ_of_param_path path in + of_path ~may_last_field integer_type_widths entry_location typ path ) module Itv = struct diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/flexible_array.c b/infer/tests/codetoanalyze/c/bufferoverrun/flexible_array.c new file mode 100644 index 000000000..6123cc4a0 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/flexible_array.c @@ -0,0 +1,27 @@ +/* + * 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. + */ + +#include + +struct s { + int useless_field_because_flexible_array_members_are_not_allowed_in_otherwise_empty_struct; + int arr[]; +}; + +void access_to_incomplete_array_type(struct s* a, int i) { a->arr[i] = 0; } + +void call_access_to_incomplete_array_type_Good_FP() { + struct s* x = malloc(sizeof(struct s) + sizeof(int)); + access_to_incomplete_array_type(x, 0); +} + +void call_access_to_incomplete_array_type_Bad() { + struct s* x = malloc(sizeof(struct s) + sizeof(int)); + access_to_incomplete_array_type(x, 1); +} + +// For tests with last field of size 0 or 1, see class.cpp diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index d8485fb8a..d700d568a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -82,6 +82,8 @@ codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRU codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: 1 Size: 1 by call to `two_symbolic_accesses` ] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 30 Size: 10] +codetoanalyze/c/bufferoverrun/flexible_array.c, call_access_to_incomplete_array_type_Bad, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,,Parameter `i`,,Parameter `a->arr[*]`,Array access: Offset: 1 Size: [0, +oo] by call to `access_to_incomplete_array_type` ] +codetoanalyze/c/bufferoverrun/flexible_array.c, call_access_to_incomplete_array_type_Good_FP, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,,Parameter `i`,,Parameter `a->arr[*]`,Array access: Offset: 0 Size: [0, +oo] by call to `access_to_incomplete_array_type` ] codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,,Assignment,,Parameter `*arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ] codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Call,Parameter `m`,Assignment,,Array declaration,Array access: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: [5, 10]]