[inferbo] Improve semantics of binary and

Reviewed By: mbouaziz

Differential Revision: D12921726

fbshipit-source-id: ed6777e69

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -207,6 +207,8 @@ module Val = struct
 
   let shiftrt : t -> t -> t = lift_itv Itv.shiftrt
 
+  let band_sem : t -> t -> t = lift_itv Itv.band_sem
+
   let lt_sem : t -> t -> t = lift_cmp_itv Itv.lt_sem
 
   let gt_sem : t -> t -> t = lift_cmp_itv Itv.gt_sem

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -229,7 +229,9 @@ and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t =
       Val.eq_sem v1 v2
   | Binop.Ne ->
       Val.ne_sem v1 v2
-  | Binop.BAnd | Binop.BXor | Binop.BOr ->
+  | Binop.BAnd ->
+      Val.band_sem v1 v2
+  | Binop.BXor | Binop.BOr ->
       Val.unknown_bit v1
   | Binop.LAnd ->
       Val.land_sem v1 v2

infer/src/bufferoverrun/itv.ml

@@ -696,6 +696,17 @@ module ItvPure = struct
         top
 
 
+  let band_sem : t -> t -> t =
+   fun x y ->
+    match (is_const x, is_const y) with
+    | Some x', Some y' ->
+        if Z.(equal x' y') then x else of_big_int Z.(x' land y')
+    | _, _ ->
+        if is_ge_zero x && is_ge_zero y then (Bound.zero, Bound.overapprox_min (ub x) (ub y))
+        else if is_le_zero x && is_le_zero y then (Bound.MInf, Bound.overapprox_min (ub x) (ub y))
+        else top
+
+
   let lt_sem : t -> t -> Boolean.t =
    fun (l1, u1) (l2, u2) ->
     if Bound.lt u1 l2 then Boolean.True else if Bound.le u2 l1 then Boolean.False else Boolean.Top
@@ -966,6 +977,8 @@ let shiftlt : t -> t -> t = lift2 ItvPure.shiftlt
 
 let shiftrt : t -> t -> t = lift2 ItvPure.shiftrt
 
+let band_sem : t -> t -> t = lift2 ItvPure.band_sem
+
 let lt_sem : t -> t -> Boolean.t = bind2b ItvPure.lt_sem
 
 let gt_sem : t -> t -> Boolean.t = bind2b ItvPure.gt_sem

infer/src/bufferoverrun/itv.mli

@@ -221,6 +221,8 @@ val shiftlt : t -> t -> t
 
 val shiftrt : t -> t -> t
 
+val band_sem : t -> t -> t
+
 val eq_sem : t -> t -> Boolean.t
 
 val ge_sem : t -> t -> Boolean.t

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

@@ -335,3 +335,85 @@ void two_safety_conditions2_Bad(uint32_t s) {
 void call_two_safety_conditions2_Bad() {
   two_safety_conditions2_Bad(15); // integer overflow L5: [0, +oo] + 15
 }
+
+void band_positive_constant_Good() {
+  char a[3];
+  int x = 6 & 2; // y is 2
+  a[x] = 0;
+}
+
+void band_positive_constant_Bad() {
+  char a[2];
+  int x = 6 & 2; // y is 2
+  a[x] = 0;
+}
+
+void band_negative_constant_Good() {
+  char a[1];
+  int x = (-3) & (-2); // x is -4
+  a[x + 4] = 0;
+}
+
+void band_negative_constant_Bad() {
+  char a[1];
+  int x = (-3) & (-2); // x is -4
+  a[x + 5] = 0;
+}
+
+void band_constant_Good() {
+  char a[2];
+  int x = (-3) & 1; // x is 1
+  a[x] = 0;
+}
+
+void band_constant_Bad() {
+  char a[1];
+  int x = (-3) & 1; // x is 1
+  a[x] = 0;
+}
+
+void band_positive_Good() {
+  char a[9];
+  int x = unknown_nat();
+  int y = unknown_nat();
+  if (x <= 10 && y <= 8) {
+    int z = x & y; // z is [0, 8]
+    a[z] = 0;
+  }
+}
+
+void band_positive_Bad() {
+  char a[5];
+  int x = unknown_nat();
+  int y = unknown_nat();
+  if (x <= 10 && y <= 8) {
+    int z = x & y; // z is [0, 8]
+    a[z] = 0;
+  }
+}
+
+void band_negative_Good() {
+  char a[3];
+  int x = unknown_function();
+  int y = unknown_function();
+  if (x <= -3 && y <= -2) {
+    int z = x & y; // z is [-oo, -3]
+    z = z + 5; // z is [-oo, 2]
+    if (z >= 0) {
+      a[z] = 0;
+    }
+  }
+}
+
+void band_negative_Bad() {
+  char a[2];
+  int x = unknown_function();
+  int y = unknown_function();
+  if (x <= -3 && y <= -2) {
+    int z = x & y; // z is [-oo, -3]
+    z = z + 5; // z is [-oo, 2]
+    if (z >= 0) {
+      a[z] = 0;
+    }
+  }
+}

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

@@ -1,3 +1,8 @@
+codetoanalyze/c/bufferoverrun/arith.c, band_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1]
+codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,Assignment,Assignment,ArrayAccess: Offset: [0, 2] Size: 2]
+codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1]
+codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 8] Size: 5]
+codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2]
 codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: s,Binop: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32]