[inferbo][bugfix] Pointer arithmetics on pointers to non-array

Summary: In the pointer arithmetics, it returns top, if we cannot precisely follow the physical memory model, e.g., (&x + 1).

Reviewed By: mbouaziz

Differential Revision: D7453510

fbshipit-source-id: db8738e

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -186,8 +186,15 @@ module Val = struct
 
   let prune_ne : t -> t -> t = lift_prune2 Itv.prune_ne ArrayBlk.prune_ne
 
+  let is_pointer_to_non_array x = not (PowLoc.is_bot x.powloc) && ArrayBlk.is_bot x.arrayblk
+
+  (* In the pointer arithmetics, it returns top, if we cannot
+     precisely follow the physical memory model, e.g., (&x + 1). *)
   let lift_pi : (ArrayBlk.astate -> Itv.t -> ArrayBlk.astate) -> t -> t -> t =
-   fun f x y -> {bot with arrayblk= f x.arrayblk y.itv; traces= TraceSet.join x.traces y.traces}
+   fun f x y ->
+    let traces = TraceSet.join x.traces y.traces in
+    if is_pointer_to_non_array x then {bot with itv= Itv.top; traces}
+    else {bot with arrayblk= f x.arrayblk y.itv; traces}
 
 
   let plus_pi : t -> t -> t = fun x y -> lift_pi ArrayBlk.plus_offset x y
@@ -196,12 +203,11 @@ module Val = struct
 
   let minus_pp : t -> t -> t =
    fun x y ->
-    (* 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; traces= TraceSet.join x.traces y.traces}
+    let itv =
+      if is_pointer_to_non_array x && is_pointer_to_non_array y then Itv.top
+      else ArrayBlk.diff x.arrayblk y.arrayblk
+    in
+    {bot with itv; traces= TraceSet.join x.traces y.traces}
 
 
   let get_symbols : t -> Itv.Symbol.t list =

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

@@ -59,9 +59,8 @@ codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, ERR
 codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, 255] Size: [10000, 10000]]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, ERROR, [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, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
-codetoanalyze/c/bufferoverrun/pointer_arith.c, FN_pointer_arith_bad, 3, CONDITION_ALWAYS_FALSE, WARNING, []
-codetoanalyze/c/bufferoverrun/pointer_arith.c, FN_pointer_arith_bad, 3, CONDITION_ALWAYS_TRUE, WARNING, []
 codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [15, 5] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/prune_alias.c:135:5 by call to `prune_arrblk_eq()` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [1, 1]]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [5, 5] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/prune_alias.c:117:5 by call to `prune_arrblk_ne()` ]

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

@@ -7,7 +7,7 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  */
 
-void FN_pointer_arith_bad() {
+void pointer_arith_bad() {
   char arr[10];
   int x = 0;
   if (&x - 1 == 0)