From 9eeeecc338590a6e00d4f1b90ad5d892f82f89ef Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Tue, 10 Apr 2018 09:56:07 -0700
Subject: [PATCH] [inferbo] Prune zero should normalize too

Reviewed By: jvillard

Differential Revision: D7568573

fbshipit-source-id: 7635bcd
---
 infer/src/bufferoverrun/itv.ml | 25 +++++++++++--------------
 1 file changed, 11 insertions(+), 14 deletions(-)

diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index c87392671..4d54258cb 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -1210,14 +1210,14 @@ module ItvPure = struct
 
   let prune_gt : t -> t -> t = fun x y -> prune_ge x (plus y one)
 
-  let prune_diff : t -> Bound.t -> t =
-   fun (l, u) b ->
-    if Bound.eq l b then (Bound.plus_l l Bound.one, u)
-    else if Bound.eq u b then (l, Bound.plus_u u Bound.mone)
-    else (l, u)
+  let prune_diff : t -> Bound.t -> t bottom_lifted =
+   fun ((l, u) as itv) b ->
+    if Bound.eq l b then normalize (Bound.plus_l l Bound.one, u)
+    else if Bound.eq u b then normalize (l, Bound.plus_u u Bound.mone)
+    else NonBottom itv
 
 
-  let prune_ne_zero : t -> t = fun x -> prune_diff x Bound.zero
+  let prune_ne_zero : t -> t bottom_lifted = fun x -> prune_diff x Bound.zero
 
   let prune_comp : Binop.t -> t -> t -> t bottom_lifted =
    fun c x y ->
@@ -1248,18 +1248,15 @@ module ItvPure = struct
         prune_comp Binop.Ge x' y
 
 
-  let prune_eq_zero : t -> t =
+  let prune_eq_zero : t -> t bottom_lifted =
    fun x ->
     let x' = prune_le x zero in
-    prune_ge x' zero
+    prune_ge x' zero |> normalize
 
 
   let prune_ne : t -> t -> t bottom_lifted =
    fun x (l, u) ->
-    if is_invalid (l, u) then NonBottom x
-    else
-      let x = if Bound.eq l u then prune_diff x l else x in
-      normalize x
+    if is_invalid (l, u) then NonBottom x else if Bound.eq l u then prune_diff x l else NonBottom x
 
 
   let get_symbols : t -> Symbol.t list =
@@ -1394,9 +1391,9 @@ let lor_sem : t -> t -> t = lift2 ItvPure.lor_sem
 
 let min_sem : t -> t -> t = lift2 ItvPure.min_sem
 
-let prune_eq_zero : t -> t = lift1 ItvPure.prune_eq_zero
+let prune_eq_zero : t -> t = bind1 ItvPure.prune_eq_zero
 
-let prune_ne_zero : t -> t = lift1 ItvPure.prune_ne_zero
+let prune_ne_zero : t -> t = bind1 ItvPure.prune_ne_zero
 
 let prune_comp : Binop.t -> t -> t -> t = fun comp -> bind2 (ItvPure.prune_comp comp)