[inferbo] Fix evaluation of Lindex

Reviewed By: mbouaziz

Differential Revision: D6371898

fbshipit-source-id: ba0508d

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -207,13 +207,13 @@ module Make (CFG : ProcCfg.S) = struct
             eval e mem
         | Exp.Lfield (e, fn, _) ->
             eval e mem |> Val.get_array_locs |> Fn.flip PowLoc.append_field fn |> Val.of_pow_loc
-        | Exp.Lindex (e1, _) ->
-            let arr = eval e1 mem |> Val.get_array_blk in
-            (* must have array blk *)
-            (* let idx = eval e2 mem in *)
-            let ploc = if ArrayBlk.is_bot arr then PowLoc.unknown else ArrayBlk.get_pow_loc arr in
-            (* if nested array, add the array blk *)
-            let arr = Mem.find_heap_set ploc mem in
+        | Exp.Lindex (e1, e2) ->
+            let arr = Val.plus_pi (eval e1 mem) (eval e2 mem) in
+            let ploc =
+              if ArrayBlk.is_bot (Val.get_array_blk arr) then PowLoc.unknown
+              else Val.get_all_locs arr
+            in
+            (* NOTE: multidimensional array is not supported yet *)
             Val.join (Val.of_pow_loc ploc) arr
         | Exp.Sizeof {nbytes= Some size} ->
             Val.of_int size

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

@@ -45,6 +45,7 @@ codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, [Ar
 codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, 255] Size: [10000, 10000]]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [1, 1]]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, []

infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c

@@ -13,3 +13,9 @@ void pointer_arith_bad() {
   if (&x - 1 == 0)
     arr[10] = 1;
 }
+
+void array_pointer_arith_Bad() {
+  int arr[10];
+  int* p = &arr[5];
+  p[5] = 1;
+}