[inferbo] Revise division by constant

Summary:
This diff tries to make less imprecise division by constants results.

For example, the results of the division `[l, u] / c`, where `c` is a positive constant, are:

1. If `l/c` or `u/c` is representable in the bound domain, it uses the precise bounds, i.e., `[l/c, u/c]`.

2. If it is not representable, it tries to make conservative results:
    if `0<=l<=u`, it returns `[0, u]` because `0 <= [l/c, u/c] <= u`
    if `l<=u<=0`, it returns `[l, 0]` because `l <= [l/c, u/c] <= 0`
    if `l<=0<=u`, it returns `[l, u]` because `l <= [l/c, u/c] <= u`

3. otherwise, it returns top, `[-oo, +oo]`

Reviewed By: ezgicicek

Differential Revision: D18270380

fbshipit-source-id: 8fb14c0e4

infer/src/bufferoverrun/itv.ml

@@ -227,14 +227,32 @@ module ItvPure = struct
     | Some n ->
         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 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_l u n) in
-          let u' = Option.value ~default:Bound.pinf (Bound.div_const_u l n) in
-          (l', u')
+          let l', u' =
+            if NonZeroInt.is_positive n then (Bound.div_const_l l n, Bound.div_const_u u n)
+            else (Bound.div_const_l u n, Bound.div_const_u l n)
+          in
+          let default_l, default_u =
+            if Bound.(le zero l) then
+              if NonZeroInt.is_positive n then
+                (* if 0<=l<=u and 0<c, 0 <= [l/c, u/c] <= u *)
+                (Bound.zero, u)
+              else (* if 0<=l<=u and c<0, -u <= [u/c, l/c] <= 0 *)
+                (Bound.neg u, Bound.zero)
+            else if Bound.(le u zero) then
+              if NonZeroInt.is_positive n then
+                (* if l<=u<=0 and 0<c, l <= [l/c, u/c] <= 0 *)
+                (l, Bound.zero)
+              else (* if l<=u<=0 and c<0, 0 <= [u/c, l/c] <= -l *)
+                (Bound.zero, Bound.neg l)
+            else if Bound.(le l zero && le zero u) then
+              if NonZeroInt.is_positive n then (* if l<=0<=u and 0<c, l <= [l/c, u/c] <= u *)
+                (l, u)
+              else (* if l<=0<=u and c<0, -u <= [u/c, l/c] <= -l *)
+                (Bound.neg u, Bound.neg l)
+            else (Bound.minf, Bound.pinf)
+          in
+          (Option.value ~default:default_l l', Option.value ~default:default_u u')
 
 
   let mult : t -> t -> t =

infer/tests/codetoanalyze/c/performance/cost_test.c

@@ -158,3 +158,11 @@ void ignore_character_symbols_constant_FP(char c) {
     }
   }
 }
+
+unsigned int div_const(unsigned int n) { return n / 2; }
+
+void iter_div_const_constant() {
+  unsigned int n = div_const(20);
+  for (int i = 0; i < n; i++) {
+  }
+}