From 88813fdaa7f5fa246769b392ccb484aca7d1a3e0 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Fri, 1 Nov 2019 08:44:15 -0700
Subject: [PATCH] [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                | 32 +++++++++++++++----
 .../codetoanalyze/c/performance/cost_test.c   |  8 +++++
 2 files changed, 33 insertions(+), 7 deletions(-)

diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index a6e024c5e..7fb3448e1 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/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 =
diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c
index 7f607a2be..c8c16ca97 100644
--- a/infer/tests/codetoanalyze/c/performance/cost_test.c
+++ b/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++) {
+  }
+}