[inferbo] Revise bit-and semantics on pointer value

Summary:
Inferbo analyzed some program points unreachable incorrectly, because of unsound semantics of band
operator, which did not handle the case when given parameters are pointer values.

Reviewed By: ngorogiannis

Differential Revision: D19392705

fbshipit-source-id: dd590508c

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -252,26 +252,27 @@ module Val = struct
 
   let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool}
 
-  let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> ?f_trace:_ -> t -> t -> t =
+  let lift_itv : ?may_ptr:bool -> (Itv.t -> Itv.t -> Itv.t) -> ?f_trace:_ -> t -> t -> t =
-   fun f ?f_trace x y ->
+    let no_ptr {powloc; arrayblk} = PowLoc.is_bot powloc && ArrayBlk.is_bot arrayblk in
-    let itv = f x.itv y.itv in
+    fun ?(may_ptr = false) f ?f_trace x y ->
-    let itv_thresholds = ItvThresholds.join x.itv_thresholds y.itv_thresholds in
+      let itv = if (not may_ptr) || (no_ptr x && no_ptr y) then f x.itv y.itv else Itv.top in
-    let itv_updated_by = ItvUpdatedBy.join x.itv_updated_by y.itv_updated_by in
+      let itv_thresholds = ItvThresholds.join x.itv_thresholds y.itv_thresholds in
-    let modeled_range = ModeledRange.join x.modeled_range y.modeled_range in
+      let itv_updated_by = ItvUpdatedBy.join x.itv_updated_by y.itv_updated_by in
-    let traces =
+      let modeled_range = ModeledRange.join x.modeled_range y.modeled_range in
-      match f_trace with
+      let traces =
-      | Some f_trace ->
+        match f_trace with
-          f_trace x.traces y.traces
+        | Some f_trace ->
-      | None -> (
+            f_trace x.traces y.traces
-        match (Itv.eq itv x.itv, Itv.eq itv y.itv) with
+        | None -> (
-        | true, false ->
+          match (Itv.eq itv x.itv, Itv.eq itv y.itv) with
-            x.traces
+          | true, false ->
-        | false, true ->
+              x.traces
-            y.traces
+          | false, true ->
-        | true, true | false, false ->
+              y.traces
-            TraceSet.join x.traces y.traces )
+          | true, true | false, false ->
-    in
+              TraceSet.join x.traces y.traces )
-    {bot with itv; itv_thresholds; itv_updated_by; modeled_range; traces}
+      in
+      {bot with itv; itv_thresholds; itv_updated_by; modeled_range; traces}
 
 
   let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t =
@@ -318,7 +319,7 @@ module Val = struct
 
   let shiftrt = lift_itv Itv.shiftrt
 
-  let band_sem = lift_itv Itv.band_sem
+  let band_sem = lift_itv ~may_ptr:true Itv.band_sem
 
   let lt_sem : t -> t -> t = lift_cmp_itv Itv.lt_sem Boolean.EqualOrder.strict_cmp
 

infer/tests/codetoanalyze/c/bufferoverrun/arith.c

@@ -546,3 +546,29 @@ void shift_right_zero_Bad(int x) {
 void use_intended_integer_underflow_Good() {
   unsigned long long x = INTENDED_INTEGER_UNDERFLOW;
 }
+
+void ptr_band1_Bad(int x, int* q) {
+  int a[5];
+  int* p;
+  if (x) {
+    p = q;
+  } else {
+    p = 0;
+  }
+  if ((int)p & x) {
+    a[10] = 0;
+  }
+}
+
+void ptr_band2_Bad(int x, int* q) {
+  int a[5];
+  int* p;
+  if (x) {
+    p = q;
+  } else {
+    p = 0;
+  }
+  if ((int)p & x) {
+  }
+  a[10] = 0;
+}

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

@@ -30,6 +30,8 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERR
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 25] Size: 20]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 19] Size: 19]
 codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Unknown value from: unknown_int,Assignment,Binary operation: ([-oo, 9223372036854775807] + 1):signed64]
+codetoanalyze/c/bufferoverrun/arith.c, ptr_band1_Bad, 9, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/c/bufferoverrun/arith.c, ptr_band2_Bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([-oo, 9] - 2):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Good_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, 9] - 1):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, scan_hex_Good, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]