[inferbo] Fix evaluation of multi-dimensional arrays

Reviewed By: mbouaziz

Differential Revision: D13082043

fbshipit-source-id: 5a45b4eee

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -161,11 +161,9 @@ let rec eval : Exp.t -> Mem.astate -> Val.t =
         Val.Itv.top
 
 
-(* NOTE: multidimensional array is not supported yet *)
 and eval_lindex array_exp index_exp mem =
   let array_v, index_v = (eval array_exp mem, eval index_exp mem) in
-  let arr = Val.plus_pi array_v index_v in
-  if ArrayBlk.is_bot (Val.get_array_blk arr) then
+  if ArrayBlk.is_bot (Val.get_array_blk array_v) then
     match array_exp with
     | Exp.Lfield _ when not (PowLoc.is_bot (Val.get_pow_loc array_v)) ->
         (* It handles the case accessing an array field of struct,
@@ -177,7 +175,13 @@ and eval_lindex array_exp index_exp mem =
         Val.plus_pi (Mem.find_set (Val.get_pow_loc array_v) mem) index_v
     | _ ->
         Val.of_pow_loc PowLoc.unknown
-  else arr
+  else
+    match array_exp with
+    | Exp.Lindex _ ->
+        (* It handles multi-dimensional arrays. *)
+        Mem.find_set (Val.get_all_locs array_v) mem
+    | _ ->
+        Val.plus_pi array_v index_v
 
 
 and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t =

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

@@ -51,7 +51,7 @@ void multidim_arr5_Good() {
   a[0][5] = 0;
 }
 
-void multidim_arr5_Bad_FN() {
+void multidim_arr5_Bad() {
   int a[1][10];
   a[0][0] = 0;
   a[0][10] = 0;

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

@@ -40,6 +40,7 @@ codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVE
 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/array_multidim.c, multidim_arr5_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 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, []