From de32a6728e1577f28bb2d1d23e3dfefc8d0e31a5 Mon Sep 17 00:00:00 2001
From: Kihong Heo <kihongh@fb.com>
Date: Sun, 28 May 2017 05:11:51 -0700
Subject: [PATCH] [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               |  4 +---
 infer/src/bufferoverrun/bufferOverrunDomain.ml    | 10 +++++++---
 .../codetoanalyze/c/bufferoverrun/issues.exp      |  3 ++-
 .../codetoanalyze/c/bufferoverrun/pointer_arith.c | 15 +++++++++++++++
 .../tests/codetoanalyze/c/bufferoverrun/sizeof.c  |  1 -
 5 files changed, 25 insertions(+), 8 deletions(-)
 create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c

diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml
index dfb39e7e7..ca7096137 100644
--- a/infer/src/bufferoverrun/arrayBlk.ml
+++ b/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
-      let i2 = Itv.mult arr2.offset arr2.stride in
-      Itv.minus i1 i2
+      Itv.minus arr1.offset arr2.offset
 
   let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t
     = fun arr subst_map ->
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index b9f191aaa..50c2834cf 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/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 ->
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
index 5337fb023..902540e50 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
+++ b/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]
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c
new file mode 100644
index 000000000..9f01f343a
--- /dev/null
+++ b/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;
+}
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c b/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c
index 4e3f8d1a5..d62ff479b 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c
+++ b/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
   }