From 72ce05c039704d37baae4a46002378070a436194 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 6 Nov 2018 19:39:11 -0800 Subject: [PATCH] [inferbo] Fix width of bool Summary: The aligned width of bool should be 1-byte, while the range of bool [0,1]. Reviewed By: jvillard Differential Revision: D12932394 fbshipit-source-id: be1a5d6d1 --- infer/src/IR/Typ.ml | 6 ++-- .../codetoanalyze/cpp/bufferoverrun/arith.cpp | 30 +++++++++++++++++++ .../cpp/bufferoverrun/issues.exp | 3 ++ 3 files changed, 37 insertions(+), 2 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index e1aa6618f..68e221567 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -91,7 +91,7 @@ let ikind_to_string = function let width_of_ikind {IntegerWidths.char_width; short_width; int_width; long_width; longlong_width} = function | IBool -> - 1 + 8 | ISChar | IChar | IUChar -> char_width | IShort | IUShort -> @@ -120,7 +120,9 @@ let range_of_ikind = let bound = Z.(shift_left ~$1) (bits - 1) in Z.(~-bound, bound - ~$1) in - fun integer_widths x -> range (width_of_ikind integer_widths x) ~unsigned:(ikind_is_unsigned x) + fun integer_widths x -> + let bits_for_range = match x with IBool -> 1 | _ -> width_of_ikind integer_widths x in + range bits_for_range ~unsigned:(ikind_is_unsigned x) let ikind_is_char = function IChar | ISChar | IUChar -> true | _ -> false diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp new file mode 100644 index 000000000..9bdf95070 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp @@ -0,0 +1,30 @@ +/* + * 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. + */ +void sizeof_bool_Good() { + int a[2]; + int z = sizeof(bool); // z is 1 (byte) + a[z] = 0; +} + +void sizeof_bool_Bad() { + int a[1]; + int z = sizeof(bool); // z is 1 (byte) + a[z] = 0; +} + +// FP due to incomplete frontend translation of casting +void range_bool_Good_FP() { + int a[2]; + bool x = true + true; // x is 1 (true) + a[x] = 0; +} + +void range_bool_Bad() { + int a[1]; + bool x = true + false; // x is 1 (true) + a[x] = 0; +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index cca301db4..25c6678e0 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,5 +1,8 @@ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_erase, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (this[*].infer_size - [-oo, +oo]):unsigned64] INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_insert_>, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (this[*].infer_size + [-oo, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] +codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2] +codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: n,ArrayAccess: Offset: 15 Size: 10 by call to `my_class_access_nth` ] codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5]