[inferbo] Add tests for relational analysis

Reviewed By: mbouaziz

Differential Revision: D7427283

fbshipit-source-id: a08bf63

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

@@ -18,6 +18,16 @@ codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, ERROR, [Offset: [7, 7] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [5, 5]]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: [0, +oo] Size: [5, 5] @ codetoanalyze/cpp/bufferoverrun/relation.cpp:50:5 by call to `loop()` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call2_minus_params_Ok, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: [8, 8] Size: [5, 5] @ codetoanalyze/cpp/bufferoverrun/relation.cpp:14:5 by call to `minus_params_Ok()` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: [-1, -1] Size: [5, 5] @ codetoanalyze/cpp/bufferoverrun/relation.cpp:38:5 by call to `plus_params2()` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params_Ok, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: [-1, -1] Size: [5, 5] @ codetoanalyze/cpp/bufferoverrun/relation.cpp:25:5 by call to `plus_params()` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, ERROR, [Assignment,Call,Assignment,Return,Assignment,ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [0, 6]]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: data,Assignment,ArrayAccess: Offset: [2, +oo] Size: [1, 1] @ codetoanalyze/cpp/bufferoverrun/relation.cpp:92:7 by call to `loop_with_type_casting()` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_loop2_Ok, 9, BUFFER_OVERRUN_L4, ERROR, [Assignment,ArrayDeclaration,Assignment,ArrayAccess: Offset: [2, +oo] Size: [12, 12]]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: [0, +oo] Size: [5, 5] @ codetoanalyze/cpp/bufferoverrun/relation.cpp:50:5 by call to `loop()` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params2_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: [11, 11] Size: [5, 5] @ codetoanalyze/cpp/bufferoverrun/relation.cpp:38:5 by call to `plus_params2()` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: [11, 11] Size: [5, 5] @ codetoanalyze/cpp/bufferoverrun/relation.cpp:25:5 by call to `plus_params()` ]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, WARNING, []
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, WARNING, []

infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp

@@ -0,0 +1,123 @@
+/*
+ * 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.
+ */
+#include <cstdlib>
+
+void minus_params_Ok(int x, int y) {
+  int a[5];
+  if (0 <= x - y && x - y < 5) {
+    a[x - y] = 0;
+  }
+}
+
+void call1_minus_params_Ok() { minus_params_Ok(5, 2); }
+
+void FP_call2_minus_params_Ok() { minus_params_Ok(10, 2); }
+
+void plus_params(int x, int y) {
+  int a[5];
+  if (x + y > 0) {
+    a[x + y - 1] = 0;
+  }
+}
+
+void call1_plus_params_Ok() { plus_params(1, 2); }
+
+void call2_plus_params_Bad() { plus_params(10, 2); }
+
+void FP_call3_plus_params_Ok() { plus_params(0, 0); }
+
+void plus_params2(int x, int y) {
+  int a[5];
+  if (-x < y) {
+    a[x + y - 1] = 0;
+  }
+}
+
+void call1_plus_params2_Ok() { plus_params2(1, 2); }
+
+void call2_plus_params2_Bad() { plus_params2(10, 2); }
+
+void FP_call3_plus_params2_Ok() { plus_params2(0, 0); }
+
+void loop(char* arr, int len) {
+  while (len > 0) {
+    arr[0] = 0;
+    arr += 1;
+    len -= 1;
+  }
+}
+
+void FP_call1_loop_Ok() {
+  char arr[5];
+  loop(arr, 5);
+}
+
+void call2_loop_Bad() {
+  char arr[5];
+  loop(arr, 10);
+}
+
+void FP_loop2_Ok() {
+  int len = 12;
+  char* arr = (char*)malloc(len * sizeof(char));
+  while (len >= 4) {
+    arr += 4;
+    len -= 4;
+  }
+  switch (len) {
+    case 3:
+      arr[2] = 0;
+    case 2:
+      arr[1] = 0;
+    case 1:
+      arr[0] = 0;
+  };
+}
+
+void loop_with_type_casting(void* data, int len) {
+  char* arr = (char*)data;
+  while (len >= 4) {
+    int k = *(int*)arr;
+    arr += 4;
+    len -= 4;
+  }
+  switch (len) {
+    case 3:
+      arr[2] = 0;
+    case 2:
+      arr[1] = 0;
+    case 1:
+      arr[0] = 0;
+  };
+}
+
+typedef struct s {
+  int a;
+  int b;
+} s_t;
+
+void FP_call_loop_with_type_casting_Ok() {
+  s_t* c = (s_t*)malloc(sizeof(s_t));
+  loop_with_type_casting(c, 8);
+}
+
+size_t id(size_t s) {
+  if (s == 0) {
+    return 0;
+  } else {
+    return s;
+  }
+}
+
+void FP_call_id_Ok() {
+  size_t s1 = 5;
+  size_t s2 = id(1 + s1);
+  char* arr = (char*)malloc(s2 * sizeof(char*));
+  arr[s1] = 0;
+}