[inferbo] Fix condition check of multi-dimensional array

Reviewed By: mbouaziz

Differential Revision: D13082491

fbshipit-source-id: 43775a1a1

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -261,10 +261,9 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t =
   | Exp.Lfield (e, fn, _) ->
       let locs = eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn in
       Mem.find_set locs mem
-  | Exp.Lindex (e1, e2) ->
-      let arr = eval e1 mem in
-      let idx = eval e2 mem in
-      Val.plus_pi arr idx
+  | Exp.Lindex (e, _) ->
+      let locs = eval e mem |> Val.get_all_locs in
+      Mem.find_set locs mem
   | Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ ->
       Val.bot
 

infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c

@@ -0,0 +1,58 @@
+/*
+ * 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 multidim_arr1_Good() {
+  int a[2][3];
+  a[1][0] = 0;
+}
+
+void multidim_arr1_Bad() {
+  int a[2][3];
+  a[2][0] = 0;
+}
+
+void multidim_arr2_Good() {
+  int a[2][3];
+  a[1][2] = 0;
+}
+
+void multidim_arr2_Bad() {
+  int a[2][3];
+  a[1][3] = 0;
+}
+
+void multidim_arr3_Good() {
+  int a[3][2] = {
+      {0, 1},
+      {0, 2},
+      {0, 3},
+  };
+}
+
+void multidim_arr4_Good_FP() {
+  int a[3][2];
+  int* p = a;
+  *(p + 5) = 0;
+}
+
+void multidim_arr4_Bad() {
+  int a[3][2];
+  int* p = a;
+  *(p + 6) = 0;
+}
+
+void multidim_arr5_Good() {
+  int a[1][10];
+  a[0][0] = 0;
+  a[0][5] = 0;
+}
+
+void multidim_arr5_Bad_FN() {
+  int a[1][10];
+  a[0][0] = 0;
+  a[0][10] = 0;
+}

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

@@ -36,6 +36,10 @@ codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, COND
 codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [3⋅len + 1, 3⋅len + 1] Size: [3⋅len + 1, 3⋅len + 1]]
 codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 20 Size: 10]
 codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2]
+codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 2 Size: 2]
+codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 3]
+codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 6 Size: 3]
+codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 5 Size: 3]
 codetoanalyze/c/bufferoverrun/big_array.c, use_big_array_bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,Return,Assignment,ArrayAccess: Offset: 999999999 Size: 26460]
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []