[inferbo][bugfix] Add index to offset at array fields

Summary: It corrects a bug that `&(x.f[n])` was evaluated to `&(x.f[0])`.

Reviewed By: mbouaziz

Differential Revision: D7179620

fbshipit-source-id: 04cbaa7

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -230,7 +230,7 @@ module Make (CFG : ProcCfg.S) = struct
              the memory section using the abstract memory, though the
              memory lookup is not required to evaluate the address of
              x.f[n] in the concrete semantics.  *)
-          Mem.find_set (Val.get_pow_loc array_v) mem
+          Val.plus_pi (Mem.find_set (Val.get_pow_loc array_v) mem) index_v
       | _ ->
           Val.of_pow_loc PowLoc.unknown
     else arr

infer/tests/codetoanalyze/c/bufferoverrun/array_field.c

@@ -23,3 +23,16 @@ void array_field_access_Bad(struct S1 x, struct S1 y) {
   x.f[0] = 1;
   a[y.f[0]] = 0;
 }
+
+void decreasing_pointer_Good(struct S1* x) {
+  int* p = &(x->f[1]);
+  p--;
+  *p = 0;
+}
+
+void decreasing_pointer_Bad(struct S1* x) {
+  int* p = &(x->f[1]);
+  p--;
+  p--;
+  *p = 0;
+}

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

@@ -2,6 +2,7 @@ codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3,
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]]
 codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]]
 codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [20, 20] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, [Assignment,Assignment,Assignment,ArrayAccess: Offset: [-1, -1] Size: [2, 2]]
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]]