[inferbo] Fix bug in integer pruning by pointer

Summary:
This diff avoids that an integer value is pruned to the bottom by
comparing to a pointer.

For example, before this diff,

assume((int*)x == p);
assume((int*)x != p);

where x is an integer, x is pruned to the bottom in both of the assume
cases.  So, there were some, unintentional and false, unreachable
code.

Depends on D16960199

Reviewed By: ezgicicek

Differential Revision: D16964735

fbshipit-source-id: 90a3c8c80

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -288,7 +288,16 @@ module Val = struct
   let lift_prune2 :
       (Itv.t -> Itv.t -> Itv.t) -> (ArrayBlk.t -> ArrayBlk.t -> ArrayBlk.t) -> t -> t -> t =
    fun f g x y ->
-    let itv = f x.itv y.itv in
+    let itv =
+      let pruned_itv = f x.itv y.itv in
+      if
+        Itv.is_bottom pruned_itv
+        && (not (Itv.is_bottom x.itv))
+        && Itv.is_bottom y.itv
+        && not (PowLoc.is_bottom (get_all_locs y))
+      then x.itv
+      else pruned_itv
+    in
     let itv_thresholds =
       Option.value_map (Itv.is_const y.itv) ~default:x.itv_thresholds ~f:(fun z ->
           x.itv_thresholds

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

@@ -264,6 +264,7 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 7, CONDITION_AL
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 11, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_int_by_pointer_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
 codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Bad, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: unknown1,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Good, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: unknown1,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]

infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c

@@ -377,3 +377,11 @@ void prune_linear_by_minmax(size_t s, size_t t) {
 void call_prune_linear_by_minmax_Good() {
   prune_linear_by_minmax(unknown_function(), unknown_function());
 }
+
+void prune_int_by_pointer_Bad(int* p) {
+  int* x = (int*)100;
+  if (x == p) {
+  }
+  int a[5];
+  a[5] = 0;
+}