[inferbo] Remove duplicated module NonNegativeBound

Reviewed By: skcho

Differential Revision: D13173264

fbshipit-source-id: 4f2477889

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

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

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