[inferbo] Make Bound type abtract

Reviewed By: skcho

Differential Revision: D14184966

fbshipit-source-id: 4cf7a959b

infer/src/bufferoverrun/bounds.ml

@@ -14,6 +14,25 @@ exception Not_One_Symbol
 
 open Ints
 
+type sign = Plus | Minus [@@deriving compare]
+
+module Sign = struct
+  type t = sign [@@deriving compare]
+
+  let neg = function Plus -> Minus | Minus -> Plus
+
+  let eval_big_int x i1 i2 = match x with Plus -> Z.(i1 + i2) | Minus -> Z.(i1 - i2)
+
+  let eval_neg_if_minus x i = match x with Plus -> i | Minus -> Z.neg i
+
+  let pp ~need_plus : F.formatter -> t -> unit =
+   fun fmt -> function
+    | Plus ->
+        if need_plus then F.pp_print_char fmt '+'
+    | Minus ->
+        F.pp_print_char fmt '-'
+end
+
 module SymLinear = struct
   module M = Symb.SymbolMap
 
@@ -132,13 +151,11 @@ module SymLinear = struct
 
 
   let is_one_symbol_of : Symb.Symbol.t -> t -> bool =
-   fun s x ->
-    Option.value_map (get_one_symbol_opt x) ~default:false ~f:(fun s' -> Symb.Symbol.equal s s')
+   fun s x -> Option.exists (get_one_symbol_opt x) ~f:(fun s' -> Symb.Symbol.equal s s')
 
 
   let is_mone_symbol_of : Symb.Symbol.t -> t -> bool =
-   fun s x ->
-    Option.value_map (get_mone_symbol_opt x) ~default:false ~f:(fun s' -> Symb.Symbol.equal s s')
+   fun s x -> Option.exists (get_mone_symbol_opt x) ~f:(fun s' -> Symb.Symbol.equal s s')
 
 
   let get_symbols : t -> Symb.SymbolSet.t =
@@ -186,25 +203,6 @@ module SymLinear = struct
 end
 
 module Bound = struct
-  type sign = Plus | Minus [@@deriving compare]
-
-  module Sign = struct
-    type t = sign [@@deriving compare]
-
-    let neg = function Plus -> Minus | Minus -> Plus
-
-    let eval_big_int x i1 i2 = match x with Plus -> Z.(i1 + i2) | Minus -> Z.(i1 - i2)
-
-    let eval_neg_if_minus x i = match x with Plus -> i | Minus -> Z.neg i
-
-    let pp ~need_plus : F.formatter -> t -> unit =
-     fun fmt -> function
-      | Plus ->
-          if need_plus then F.pp_print_char fmt '+'
-      | Minus ->
-          F.pp_print_char fmt '-'
-  end
-
   type min_max = Min | Max [@@deriving compare]
 
   module MinMax = struct
@@ -254,13 +252,33 @@ module Bound = struct
 
   let of_bound_end = function Symb.BoundEnd.LowerBound -> MInf | Symb.BoundEnd.UpperBound -> PInf
 
-  let of_int : int -> t = fun n -> Linear (Z.of_int n, SymLinear.empty)
-
   let of_big_int : Z.t -> t = fun n -> Linear (n, SymLinear.empty)
 
-  let minus_one = of_int (-1)
+  let of_int : int -> t = fun n -> of_big_int (Z.of_int n)
+
+  let minf = MInf
 
-  let _255 = of_int 255
+  let mone = of_big_int Z.minus_one
+
+  let z255 = of_int 255
+
+  let zero = of_big_int Z.zero
+
+  let one = of_big_int Z.one
+
+  let pinf = PInf
+
+  let is_some_const : Z.t -> t -> bool =
+   fun c x -> match x with Linear (c', y) -> Z.equal c c' && SymLinear.is_zero y | _ -> false
+
+
+  let is_zero : t -> bool = is_some_const Z.zero
+
+  let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true
+
+  let is_minf = function MInf -> true | _ -> false
+
+  let is_pinf = function PInf -> true | _ -> false
 
   let of_sym : SymLinear.t -> t = fun s -> Linear (Z.zero, s)
 
@@ -631,8 +649,6 @@ module Bound = struct
         overapprox_max
 
 
-  let zero : t = Linear (Z.zero, SymLinear.zero)
-
   module Thresholds : sig
     type bound = t
 
@@ -709,16 +725,6 @@ module Bound = struct
 
   let widen_u : t -> t -> t = fun x y -> widen_u_thresholds ~thresholds:[] x y
 
-  let one : t = Linear (Z.one, SymLinear.zero)
-
-  let mone : t = Linear (Z.minus_one, SymLinear.zero)
-
-  let is_some_const : Z.t -> t -> bool =
-   fun c x -> match x with Linear (c', y) -> Z.equal c c' && SymLinear.is_zero y | _ -> false
-
-
-  let is_zero : t -> bool = is_some_const Z.zero
-
   let is_const : t -> Z.t option =
    fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None
 
@@ -851,8 +857,6 @@ module Bound = struct
 
   let are_similar b1 b2 = Symb.SymbolSet.equal (get_symbols b1) (get_symbols b2)
 
-  let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true
-
   (** Substitutes ALL symbols in [x] with respect to [eval_sym]. Under/over-Approximate as good as possible according to [subst_pos]. *)
   let subst : subst_pos:Symb.BoundEnd.t -> t -> eval_sym -> t bottom_lifted =
     let lift1 : (t -> t) -> t bottom_lifted -> t bottom_lifted =

infer/src/bufferoverrun/bounds.mli

@@ -8,24 +8,8 @@
 open! IStd
 module F = Format
 
-exception Not_One_Symbol
-
-module SymLinear : sig
-  module M = Symb.SymbolMap
-
-  type t = Ints.NonZeroInt.t M.t
-end
-
 module Bound : sig
-  type sign = Plus | Minus
-
-  type min_max = Min | Max
-
-  type t =
-    | MInf
-    | Linear of Z.t * SymLinear.t
-    | MinMax of Z.t * sign * min_max * Z.t * Symb.Symbol.t
-    | PInf
+  type t
 
   type eval_sym = t Symb.Symbol.eval
 
@@ -39,9 +23,17 @@ module Bound : sig
 
   val of_big_int : Z.t -> t
 
-  val minus_one : t
+  val minf : t
 
-  val _255 : t
+  val mone : t
+
+  val zero : t
+
+  val one : t
+
+  val z255 : t
+
+  val pinf : t
 
   val of_normal_path :
        (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t)
@@ -55,6 +47,14 @@ module Bound : sig
   val of_length_path :
     (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) -> Symb.SymbolPath.partial -> t
 
+  val is_zero : t -> bool
+
+  val is_not_infty : t -> bool
+
+  val is_minf : t -> bool
+
+  val is_pinf : t -> bool
+
   val is_symbolic : t -> bool
 
   val le : t -> t -> bool
@@ -83,14 +83,6 @@ module Bound : sig
 
   val widen_u_thresholds : thresholds:Z.t list -> t -> t -> t
 
-  val zero : t
-
-  val one : t
-
-  val mone : t
-
-  val is_zero : t -> bool
-
   val is_const : t -> Z.t sexp_option
 
   val plus_l : t -> t -> t
@@ -111,8 +103,6 @@ module Bound : sig
 
   val are_similar : t -> t -> bool
 
-  val is_not_infty : t -> bool
-
   val subst_lb : t -> eval_sym -> t AbstractDomain.Types.bottom_lifted
 
   val subst_ub : t -> eval_sym -> t AbstractDomain.Types.bottom_lifted

infer/src/bufferoverrun/itv.ml

@@ -40,7 +40,7 @@ module ItvPure = struct
 
   let ub : t -> Bound.t = snd
 
-  let is_lb_infty : t -> bool = function MInf, _ -> true | _ -> false
+  let is_lb_infty : t -> bool = fun (l, _) -> Bound.is_minf l
 
   let is_finite : t -> bool =
    fun (l, u) ->
@@ -49,7 +49,7 @@ module ItvPure = struct
 
   let have_similar_bounds (l1, u1) (l2, u2) = Bound.are_similar l1 l2 && Bound.are_similar u1 u2
 
-  let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false
+  let has_infty (l, u) = Bound.is_minf l || Bound.is_pinf u
 
   let exists_str ~f (l, u) = Bound.exists_str ~f l || Bound.exists_str ~f u
 
@@ -121,19 +121,19 @@ module ItvPure = struct
 
   let mone = of_bound Bound.mone
 
-  let zero_255 = (Bound.zero, Bound._255)
+  let zero_255 = (Bound.zero, Bound.z255)
 
-  let m1_255 = (Bound.minus_one, Bound._255)
+  let m1_255 = (Bound.mone, Bound.z255)
 
-  let nat = (Bound.zero, Bound.PInf)
+  let nat = (Bound.zero, Bound.pinf)
 
   let one = of_bound Bound.one
 
-  let pos = (Bound.one, Bound.PInf)
+  let pos = (Bound.one, Bound.pinf)
 
   let set_lb_zero (_, ub) = (Bound.zero, ub)
 
-  let top = (Bound.MInf, Bound.PInf)
+  let top = (Bound.minf, Bound.pinf)
 
   let zero = of_bound Bound.zero
 
@@ -145,9 +145,9 @@ module ItvPure = struct
 
   let unknown_bool = join false_sem true_sem
 
-  let is_top : t -> bool = function Bound.MInf, Bound.PInf -> true | _ -> false
+  let is_top : t -> bool = fun (l, u) -> Bound.is_minf l && Bound.is_pinf u
 
-  let is_nat : t -> bool = function l, Bound.PInf -> Bound.is_zero l | _ -> false
+  let is_nat : t -> bool = fun (l, u) -> Bound.is_zero l && Bound.is_pinf u
 
   let is_const : t -> Z.t option =
    fun (l, u) ->
@@ -222,12 +222,12 @@ module ItvPure = struct
         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
+          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
+          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')
 
 
@@ -296,7 +296,7 @@ module ItvPure = struct
         if Z.(equal x' y') then x else of_big_int Z.(x' land y')
     | _, _ ->
         if is_ge_zero x && is_ge_zero y then (Bound.zero, Bound.overapprox_min (ub x) (ub y))
-        else if is_le_zero x && is_le_zero y then (Bound.MInf, Bound.overapprox_min (ub x) (ub y))
+        else if is_le_zero x && is_le_zero y then (Bound.minf, Bound.overapprox_min (ub x) (ub y))
         else top
 
 
@@ -336,12 +336,7 @@ module ItvPure = struct
    fun (l1, u1) (l2, u2) -> (Bound.underapprox_min l1 l2, Bound.overapprox_min u1 u2)
 
 
-  let is_invalid : t -> bool = function
-    | Bound.PInf, _ | _, Bound.MInf ->
-        true
-    | l, u ->
-        Bound.lt u l
-
+  let is_invalid : t -> bool = fun (l, u) -> Bound.is_pinf l || Bound.is_minf u || Bound.lt u l
 
   let normalize : t -> t bottom_lifted = fun x -> if is_invalid x then Bottom else NonBottom x
 

infer/src/checkers/costModels.ml

@@ -17,7 +17,7 @@ module Collections = struct
         BufferOverrunModels.Collection.eval_collection_length coll_exp inferbo_mem
         |> BufferOverrunDomain.Val.get_itv
       in
-      match itv with Bottom -> Bounds.Bound.PInf | NonBottom itv_pure -> Itv.ItvPure.ub itv_pure
+      match itv with Bottom -> Bounds.Bound.pinf | NonBottom itv_pure -> Itv.ItvPure.ub itv_pure
     in
     Bounds.NonNegativeBound.of_modeled_function "List.length" loc upper_bound