[inferbo] New tests

Reviewed By: skcho

Differential Revision: D13048352

fbshipit-source-id: f0a2dc7a4

infer/tests/codetoanalyze/c/bufferoverrun/arith.c

@@ -445,3 +445,8 @@ void band_negative_Bad() {
     }
   }
 }
+
+#define FOUR_GIGABYTES 0xFFFFFFFF
+#define ALMOST_FOUR_GIGABYTES (85 * FOUR_GIGABYTES / 100)
+
+void simple_overflow_Bad() { auto x = ALMOST_FOUR_GIGABYTES; }

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

@@ -25,6 +25,7 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERR
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: 19]
 codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_int,Assignment,Binop: ([-oo, 9223372036854775807] + 1):signed64]
+codetoanalyze/c/bufferoverrun/arith.c, simple_overflow_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Binop: (85 * 4294967295):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, two_safety_conditions2_Bad, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 80]):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
@@ -198,5 +199,10 @@ codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_true_with_else_bad
 codetoanalyze/c/bufferoverrun/unreachable.c, infinite_loop_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/unreachable.c, never_loops_bad, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/unreachable.c, unreachable_statement_exit_bad, 1, UNREACHABLE_CODE, no_bucket, ERROR, []
+codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times2_Good_FP, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 4] Size: 1 by call to `do_two_times2_Good` ]
+codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times_Good_FP, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 4] Size: 1 by call to `do_two_times_Good` ]
 codetoanalyze/c/bufferoverrun/while_loop.c, diverge_on_narrowing, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
+codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([-oo, +oo] + 1):signed32]
+codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: x,Binop: (x + [-oo, +oo]):signed32]
+codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 12, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Offset: [0, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [0, 10] Size: 10]

infer/tests/codetoanalyze/c/bufferoverrun/unrolling.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.
+ */
+
+void do_two_times_Good(int n) {
+  char a[1];
+  for (int i = 0; i < n; i++) {
+    n = 1;
+    a[i] = 3;
+  }
+}
+
+void do_two_times2_Good(int n) {
+  char a[1];
+  int k = n;
+  for (int i = 0; i < k; i++) {
+    k = 1;
+    a[i] = 3;
+  }
+}
+
+void call_do_two_times_Good_FP() { do_two_times_Good(5); }
+
+void call_do_two_times2_Good_FP() { do_two_times2_Good(5); }

infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c

@@ -27,3 +27,34 @@ void diverge_on_narrowing() {
     x = x->f;
   }
 }
+
+void join_minmax_with_sum_unsigned_Good(unsigned int x, unsigned int y) {
+  char a[x + y + 1];
+  int i = 0;
+  while (i < x + y) {
+    if (i > 5) {
+      y = 0;
+    }
+    i++;
+  }
+  a[i] = 2;
+}
+
+void call_join_minmax_with_sum_unsigned_Good() {
+  join_minmax_with_sum_unsigned_Good(15, 50);
+}
+
+void join_minmax_with_sum_signed_Good_FP(int x, int y) {
+  int s = x + y;
+  if (s < 0)
+    s = 0;
+  char a[s + 1];
+  int i = 0;
+  while (i < x + y) {
+    if (i > 5) {
+      y = 0;
+    }
+    i++;
+  }
+  a[i] = 2;
+}

infer/tests/codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp

@@ -0,0 +1,31 @@
+/*
+ * 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 <vector>
+
+namespace CppIsTricky {
+void vector_size_Bad() {
+  const auto vec = std::vector<int>{1, 2, 3};
+  const int numExpectedElements = 1;
+  const auto delta = numExpectedElements - vec.size();
+}
+
+void minus1_Bad_FN() {
+  const unsigned long i2 = 18446744073709551614u;
+  const unsigned long i1 = 446744073709551614u;
+  const int d1 = i2 - i1;
+}
+void minus2_Bad_FN() {
+  const unsigned long i2 = 18446744073709551614u;
+  const unsigned long i1 = 446744073709551614u;
+  const long d2 = i2 - i1;
+}
+void minus3_Good() {
+  const unsigned long i2 = 18446744073709551614u;
+  const unsigned long i1 = 446744073709551614u;
+  const auto d3 = i2 - i1;
+}
+} // namespace CppIsTricky

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

@@ -24,6 +24,8 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFE
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Return,ArrayAccess: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 32 Size: 30]
+codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: (1 - [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 30 Size: 10]
 codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned64]