From 66e737a3b47c5b513b9e935153d7801c80ea791d Mon Sep 17 00:00:00 2001 From: Julian Sutherland Date: Tue, 31 Jul 2018 08:09:42 -0700 Subject: [PATCH] refactoring itv, moved Ints and NonZeroInt module to seperate file Reviewed By: mbouaziz Differential Revision: D9028914 fbshipit-source-id: 5212c8a87 --- infer/src/bufferoverrun/ints.ml | 90 ++++++++++++++++++ infer/src/bufferoverrun/ints.mli | 84 +++++++++++++++++ infer/src/bufferoverrun/itv.ml | 154 ------------------------------- 3 files changed, 174 insertions(+), 154 deletions(-) create mode 100644 infer/src/bufferoverrun/ints.ml create mode 100644 infer/src/bufferoverrun/ints.mli diff --git a/infer/src/bufferoverrun/ints.ml b/infer/src/bufferoverrun/ints.ml new file mode 100644 index 000000000..b701e4312 --- /dev/null +++ b/infer/src/bufferoverrun/ints.ml @@ -0,0 +1,90 @@ +(* + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open! AbstractDomain.Types +module F = Format + +module NonZeroInt = struct + type t = int [@@deriving compare] + + exception DivisionNotExact + + let one = 1 + + let minus_one = -1 + + let of_int = function 0 -> None | i -> Some i + + let opt_to_int = function None -> 0 | Some i -> i + + let is_one = Int.equal 1 + + let is_minus_one = Int.equal (-1) + + let is_multiple mul div = Int.equal (mul mod div) 0 + + let is_negative x = x < 0 + + let is_positive x = x > 0 + + let ( ~- ) = Int.( ~- ) + + let ( * ) = Int.( * ) + + let plus x y = of_int (x + y) + + let exact_div_exn num den = + if not (is_multiple num den) then raise DivisionNotExact ; + num / den + + + let max = Int.max + + let min = Int.min +end + +module NonNegativeInt = struct + type t = int [@@deriving compare] + + let zero = 0 + + let one = 1 + + let is_zero = function 0 -> true | _ -> false + + let is_one = function 1 -> true | _ -> false + + let of_int i = if i < 0 then None else Some i + + let of_int_exn i = + assert (i >= 0) ; + i + + + let ( <= ) ~lhs ~rhs = Int.(lhs <= rhs) + + let ( + ) = Int.( + ) + + let ( * ) = Int.( * ) + + let max = Int.max + + let pp = F.pp_print_int +end + +module PositiveInt = struct + type t = NonNegativeInt.t [@@deriving compare] + + let one = 1 + + let of_int i = if i <= 0 then None else Some i + + let succ = Int.succ + + let pp = F.pp_print_int +end diff --git a/infer/src/bufferoverrun/ints.mli b/infer/src/bufferoverrun/ints.mli new file mode 100644 index 000000000..24c183ba2 --- /dev/null +++ b/infer/src/bufferoverrun/ints.mli @@ -0,0 +1,84 @@ +(* + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +module F = Format + +module NonZeroInt : sig + type t = private int [@@deriving compare] + + exception DivisionNotExact + + val one : t + + val minus_one : t + + val of_int : int -> t option + + val opt_to_int : t option -> int + + val is_one : t -> bool + + val is_minus_one : t -> bool + + val is_multiple : int -> t -> bool + + val is_negative : t -> bool + + val is_positive : t -> bool + + val ( ~- ) : t -> t + + val ( * ) : t -> t -> t + + val plus : t -> t -> t option + + val exact_div_exn : t -> t -> t + + val max : t -> t -> t + + val min : t -> t -> t +end + +module NonNegativeInt : sig + type t = private int [@@deriving compare] + + val zero : t + + val one : t + + val of_int : int -> t option + + val of_int_exn : int -> t + + val is_zero : t -> bool + + val is_one : t -> bool + + val ( <= ) : lhs:t -> rhs:t -> bool + + val ( + ) : t -> t -> t + + val ( * ) : t -> t -> t + + val max : t -> t -> t + + val pp : F.formatter -> t -> unit +end + +module PositiveInt : sig + type t = private NonNegativeInt.t [@@deriving compare] + + val one : t + + val of_int : int -> t option + + val succ : t -> t + + val pp : F.formatter -> t -> unit +end diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 51831048c..a4e24b450 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -140,160 +140,6 @@ module SymbolMap = struct if Symbol.equal kmin kmax then Some binding else None end -module NonZeroInt : sig - type t = private int [@@deriving compare] - - exception DivisionNotExact - - val one : t - - val minus_one : t - - val of_int : int -> t option - - val opt_to_int : t option -> int - - val is_one : t -> bool - - val is_minus_one : t -> bool - - val is_multiple : int -> t -> bool - - val is_negative : t -> bool - - val is_positive : t -> bool - - val ( ~- ) : t -> t - - val ( * ) : t -> t -> t - - val plus : t -> t -> t option - - val exact_div_exn : t -> t -> t - - val max : t -> t -> t - - val min : t -> t -> t -end = struct - type t = int [@@deriving compare] - - exception DivisionNotExact - - let one = 1 - - let minus_one = -1 - - let of_int = function 0 -> None | i -> Some i - - let opt_to_int = function None -> 0 | Some i -> i - - let is_one = Int.equal 1 - - let is_minus_one = Int.equal (-1) - - let is_multiple mul div = Int.equal (mul mod div) 0 - - let is_negative x = x < 0 - - let is_positive x = x > 0 - - let ( ~- ) = Int.( ~- ) - - let ( * ) = Int.( * ) - - let plus x y = of_int (x + y) - - let exact_div_exn num den = - if not (is_multiple num den) then raise DivisionNotExact ; - num / den - - - let max = Int.max - - let min = Int.min -end - -module Ints : sig - module NonNegativeInt : sig - type t = private int [@@deriving compare] - - val zero : t - - val one : t - - val of_int : int -> t option - - val of_int_exn : int -> t - - val is_zero : t -> bool - - val is_one : t -> bool - - val ( <= ) : lhs:t -> rhs:t -> bool - - val ( + ) : t -> t -> t - - val ( * ) : t -> t -> t - - val max : t -> t -> t - - val pp : F.formatter -> t -> unit - end - - module PositiveInt : sig - type t = private NonNegativeInt.t [@@deriving compare] - - val one : t - - val of_int : int -> t option - - val succ : t -> t - - val pp : F.formatter -> t -> unit - end -end = struct - module NonNegativeInt = struct - type t = int [@@deriving compare] - - let zero = 0 - - let one = 1 - - let is_zero = function 0 -> true | _ -> false - - let is_one = function 1 -> true | _ -> false - - let of_int i = if i < 0 then None else Some i - - let of_int_exn i = - assert (i >= 0) ; - i - - - let ( <= ) ~lhs ~rhs = Int.(lhs <= rhs) - - let ( + ) = Int.( + ) - - let ( * ) = Int.( * ) - - let max = Int.max - - let pp = F.pp_print_int - end - - module PositiveInt = struct - type t = NonNegativeInt.t [@@deriving compare] - - let one = 1 - - let of_int i = if i <= 0 then None else Some i - - let succ = Int.succ - - let pp = F.pp_print_int - end -end - open Ints exception Not_one_symbol