[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

@@ -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

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;
+}

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

@@ -1,5 +1,8 @@
 INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector<Int_no_copy,std::allocator<Int_no_copy>>_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<int,std::allocator<int>>_insert<std::__list_iterator<int,_void_*>_>, 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]