From 3cd57849c438d0719a3b3a267155c170260e7e1a Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Fri, 23 Nov 2018 04:03:50 -0800
Subject: [PATCH] [inferbo] Remove duplicated module NonNegativeBound

Reviewed By: skcho

Differential Revision: D13173264

fbshipit-source-id: 4f2477889
---
 infer/src/bufferoverrun/bounds.ml  | 20 ++++++++++++++-
 infer/src/bufferoverrun/bounds.mli | 14 ++++++----
 infer/src/bufferoverrun/itv.ml     | 41 +-----------------------------
 3 files changed, 29 insertions(+), 46 deletions(-)

diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 6c8e330be..68e4d8dd3 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -937,9 +937,19 @@ type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop
 module NonNegativeBound = struct
   type t = Bound.t [@@deriving compare]
 
+  let pp = Bound.pp
+
   let zero = Bound.zero
 
-  let of_bound b = if Bound.le b Bound.zero then Bound.zero else b
+  let of_bound b = if Bound.le b zero then zero else b
+
+  let int_lb b =
+    Bound.big_int_lb b
+    |> Option.bind ~f:NonNegativeInt.of_big_int
+    |> Option.value ~default:NonNegativeInt.zero
+
+
+  let int_ub b = Bound.big_int_ub b |> Option.map ~f:NonNegativeInt.of_big_int_exn
 
   let classify = function
     | Bound.PInf ->
@@ -952,4 +962,12 @@ module NonNegativeBound = struct
           Symbolic b
       | Some c ->
           Constant (NonNegativeInt.of_big_int_exn c) )
+
+
+  let subst b map =
+    match Bound.subst_ub b map with
+    | Bottom ->
+        Constant NonNegativeInt.zero
+    | NonBottom b ->
+        of_bound b |> classify
 end
diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli
index e2500d031..a2ba76718 100644
--- a/infer/src/bufferoverrun/bounds.mli
+++ b/infer/src/bufferoverrun/bounds.mli
@@ -57,10 +57,6 @@ module Bound : sig
 
   val is_symbolic : t -> bool
 
-  val big_int_lb : t -> Z.t sexp_option
-
-  val big_int_ub : t -> Z.t sexp_option
-
   val le : t -> t -> bool
 
   val lt : t -> t -> bool
@@ -127,11 +123,19 @@ end
 type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop
 
 module NonNegativeBound : sig
-  type t = Bound.t
+  type t = Bound.t [@@deriving compare]
+
+  val pp : Format.formatter -> t -> unit
 
   val zero : t
 
   val of_bound : t -> t
 
+  val int_lb : t -> Ints.NonNegativeInt.t
+
+  val int_ub : t -> Ints.NonNegativeInt.t option
+
   val classify : t -> (Ints.NonNegativeInt.t, t) valclass
+
+  val subst : t -> Bound.eval_sym -> (Ints.NonNegativeInt.t, t) valclass
 end
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 6daad39cc..250ce2702 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -17,45 +17,6 @@ module SymbolPath = Symb.SymbolPath
 module SymbolTable = Symb.SymbolTable
 module SymbolSet = Symb.SymbolSet
 
-(** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *)
-module NonNegativeBound = struct
-  type t = Bound.t [@@deriving compare]
-
-  let pp = Bound.pp
-
-  let zero = Bound.zero
-
-  let of_bound b = if Bound.le b zero then zero else b
-
-  let int_lb b =
-    Bound.big_int_lb b
-    |> Option.bind ~f:NonNegativeInt.of_big_int
-    |> Option.value ~default:NonNegativeInt.zero
-
-
-  let int_ub b = Bound.big_int_ub b |> Option.map ~f:NonNegativeInt.of_big_int_exn
-
-  let classify = function
-    | Bound.PInf ->
-        Bounds.ValTop
-    | Bound.MInf ->
-        assert false
-    | b -> (
-      match Bound.is_const b with
-      | None ->
-          Bounds.Symbolic b
-      | Some c ->
-          Bounds.Constant (NonNegativeInt.of_big_int_exn c) )
-
-
-  let subst b map =
-    match Bound.subst_ub b map with
-    | Bottom ->
-        Bounds.Constant NonNegativeInt.zero
-    | NonBottom b ->
-        of_bound b |> classify
-end
-
 module type NonNegativeSymbol = sig
   type t [@@deriving compare]
 
@@ -363,7 +324,7 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
 end
 
 module NonNegativePolynomial = struct
-  module NonNegativeNonTopPolynomial = MakePolynomial (NonNegativeBound)
+  module NonNegativeNonTopPolynomial = MakePolynomial (Bounds.NonNegativeBound)
   include AbstractDomain.TopLifted (NonNegativeNonTopPolynomial)
 
   let zero = NonTop NonNegativeNonTopPolynomial.zero