[inferbo] remove bottoms in pointer arithmetic

Summary:
This diff fixes unintentional bottoms in pointer arithmetic of inferbo.
The pointer arithmetic on addresses of variables (not array) just returns
the operand.

Reviewed By: jvillard

Differential Revision: D5060424

fbshipit-source-id: 495d8b8

infer/src/bufferoverrun/arrayBlk.ml

@@ -78,9 +78,7 @@ struct
 
   let diff : t -> t -> Itv.astate
     = fun arr1 arr2 ->
-      let i1 = Itv.mult arr1.offset arr1.stride in
+      Itv.minus arr1.offset arr2.offset
-      let i2 = Itv.mult arr2.offset arr2.stride in
-      Itv.minus i1 i2
 
   let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t
     = fun arr subst_map ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -378,15 +378,19 @@ struct
 
   let plus_pi : t -> t -> t
     = fun x y ->
-      { bot with arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv }
+      { bot with powloc = x.powloc; arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv }
 
   let minus_pi : t -> t -> t
     = fun x y ->
-      { bot with arrayblk = ArrayBlk.minus_offset x.arrayblk y.itv }
+      { bot with powloc = x.powloc; arrayblk = ArrayBlk.minus_offset x.arrayblk y.itv }
 
   let minus_pp : t -> t -> t
     = fun x y ->
-      { bot with itv = ArrayBlk.diff x.arrayblk y.arrayblk }
+      (* when we cannot precisely follow the physical memory model, return top *)
+      if (not (PowLoc.is_bot x.powloc) && ArrayBlk.is_bot x.arrayblk) ||
+         (not (PowLoc.is_bot y.powloc) && ArrayBlk.is_bot y.arrayblk)
+      then { bot with itv = Itv.top }
+      else { bot with itv = ArrayBlk.diff x.arrayblk y.arrayblk }
 
   let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t
     = fun x subst_map ->

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

@@ -9,8 +9,9 @@ codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_O
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/pointer_arith.c:14:5]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/prune_alias.c:107:5]
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0] @ codetoanalyze/c/bufferoverrun/sizeof.c:16:5]
-codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 8, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0] @ codetoanalyze/c/bufferoverrun/sizeof.c:33:5]
+codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0] @ codetoanalyze/c/bufferoverrun/sizeof.c:32:5]
 codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3]
 codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10]

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

@@ -0,0 +1,15 @@
+/*
+ * Copyright (c) 2017 - 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.
+ */
+
+void pointer_arith_bad() {
+  char arr[10];
+  int x = 0;
+  if (&x - 1 == 0)
+    arr[10] = 1;
+}

infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c

@@ -28,7 +28,6 @@ void static_stride_bad() {
   x = &(a[5]);
   y = &(a[4]);
   if (sizeof(struct some_struct) == x - y) {
-    // always true, but inferbo sends all pointer arithmetic to _|_ (t18130404)
     int a[0];
     a[1]; // report
   }