[inferbo] Try division on minmax value conservatively

Summary: It tries division on minmax value approximately, rather than just returning infinities. For example, `[0,2+min(6,s)] / 2` returns `[0,4]`.

Reviewed By: mbouaziz

Differential Revision: D10867091

fbshipit-source-id: d3f49987b

infer/src/bufferoverrun/bounds.ml

@@ -733,8 +733,18 @@ module Bound = struct
 
   let mult_const_u = mult_const Symb.BoundEnd.UpperBound
 
-  let div_const : t -> NonZeroInt.t -> t option =
-   fun x n ->
+  let overapprox_minmax_div_const x (n : NonZeroInt.t) =
+    let c = if NonZeroInt.is_positive n then big_int_ub_of_minmax x else big_int_lb_of_minmax x in
+    Option.map c ~f:(fun c -> Z.(c / (n :> Z.t)))
+
+
+  let underapprox_minmax_div_const x (n : NonZeroInt.t) =
+    let c = if NonZeroInt.is_positive n then big_int_lb_of_minmax x else big_int_ub_of_minmax x in
+    Option.map c ~f:(fun c -> Z.(c / (n :> Z.t)))
+
+
+  let div_const : Symb.BoundEnd.t -> t -> NonZeroInt.t -> t option =
+   fun bound_end x n ->
     match x with
     | MInf ->
         Some (if NonZeroInt.is_positive n then MInf else PInf)
@@ -746,10 +756,23 @@ module Bound = struct
           Some (Linear (Z.(c / (n :> Z.t)), x''))
       | exception NonZeroInt.DivisionNotExact ->
           None )
+    | MinMax _ ->
+        let c =
+          match bound_end with
+          | Symb.BoundEnd.LowerBound ->
+              underapprox_minmax_div_const x n
+          | Symb.BoundEnd.UpperBound ->
+              overapprox_minmax_div_const x n
+        in
+        Option.map c ~f:of_big_int
     | _ ->
         None
 
 
+  let div_const_l = div_const Symb.BoundEnd.LowerBound
+
+  let div_const_u = div_const Symb.BoundEnd.UpperBound
+
   let get_symbols : t -> Symb.Symbol.t list = function
     | MInf | PInf ->
         []

infer/src/bufferoverrun/bounds.mli

@@ -99,7 +99,9 @@ module Bound : sig
 
   val neg : t -> t
 
-  val div_const : t -> Ints.NonZeroInt.t -> t sexp_option
+  val div_const_l : t -> Ints.NonZeroInt.t -> t sexp_option
+
+  val div_const_u : t -> Ints.NonZeroInt.t -> t sexp_option
 
   val get_symbols : t -> Symb.Symbol.t list
 

infer/src/bufferoverrun/itv.ml

@@ -611,12 +611,12 @@ module ItvPure = struct
         if NonZeroInt.is_one n then itv
         else if NonZeroInt.is_minus_one n then neg itv
         else if NonZeroInt.is_positive n then
-          let l' = Option.value ~default:Bound.MInf (Bound.div_const l n) in
-          let u' = Option.value ~default:Bound.PInf (Bound.div_const u n) in
+          let l' = Option.value ~default:Bound.MInf (Bound.div_const_l l n) in
+          let u' = Option.value ~default:Bound.PInf (Bound.div_const_u u n) in
           (l', u')
         else
-          let l' = Option.value ~default:Bound.MInf (Bound.div_const u n) in
-          let u' = Option.value ~default:Bound.PInf (Bound.div_const l n) in
+          let l' = Option.value ~default:Bound.MInf (Bound.div_const_l u n) in
+          let u' = Option.value ~default:Bound.PInf (Bound.div_const_u l n) in
           (l', u')
 
 

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

@@ -292,3 +292,17 @@ void unsigned_prune_gt(unsigned int x, unsigned int y) {
 }
 
 void call_unsigned_prune_gt_Good() { unsigned_prune_gt(0, 3); }
+
+void minmax_div_const_Good(int n) {
+  int a[9];
+  if (0 < n && n < 65) {
+    int x = a[n / 8];
+  }
+}
+
+void minmax_div_const_Bad(int n) {
+  int a[7];
+  if (0 < n && n < 65) {
+    int x = a[n / 8];
+  }
+}

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

@@ -8,6 +8,7 @@ codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 4
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-2000000000 - 2000000000):signed32]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
+codetoanalyze/c/bufferoverrun/arith.c, minmax_div_const_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [0, 8] Size: 7]
 codetoanalyze/c/bufferoverrun/arith.c, minus_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (0 - -9223372036854775808):signed64]
 codetoanalyze/c/bufferoverrun/arith.c, minus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([0, +oo] - 1):unsigned64]
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5]