[Inferbo][Itv] Some rewrites

Summary:
- `NonZeroInt` for added guarantees on the invariants of `SymLinear` coefficients
- some simplifications
- some optimizations

Reviewed By: jvillard

Differential Revision: D6833968

fbshipit-source-id: 39e28a0
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent 653f212023
commit 59edaf4670

@ -525,11 +525,9 @@ module Make (CFG : ProcCfg.S) = struct
match formal with match formal with
| Itv.Bound.Linear (_, se1) when Itv.SymLinear.is_zero se1 -> | Itv.Bound.Linear (_, se1) when Itv.SymLinear.is_zero se1 ->
(bound_map, trace_map) (bound_map, trace_map)
| Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0 -> | Itv.Bound.Linear (0, se1) ->
let symbol, coeff = Itv.SymLinear.min_binding se1 in let symbol = Itv.SymLinear.get_one_symbol se1 in
if Int.equal coeff 1 then (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map)
(Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map)
else assert false
| Itv.Bound.MinMax (0, Itv.Bound.Plus, Itv.Bound.Max, 0, symbol) -> | Itv.Bound.MinMax (0, Itv.Bound.Plus, Itv.Bound.Max, 0, symbol) ->
(Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map) (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map)
| _ -> | _ ->

@ -20,7 +20,7 @@ exception Not_one_symbol
module Symbol = struct module Symbol = struct
type t = {pname: Typ.Procname.t; id: int; unsigned: bool} [@@deriving compare] type t = {pname: Typ.Procname.t; id: int; unsigned: bool} [@@deriving compare]
let eq = [%compare.equal : t] let equal = [%compare.equal : t]
let make : unsigned:bool -> Typ.Procname.t -> int -> t = let make : unsigned:bool -> Typ.Procname.t -> int -> t =
fun ~unsigned pname id -> {pname; id; unsigned} fun ~unsigned pname id -> {pname; id; unsigned}
@ -38,6 +38,62 @@ end
module SubstMap = Caml.Map.Make (Symbol) module SubstMap = Caml.Map.Make (Symbol)
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 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 exact_div_exn : 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 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 exact_div_exn num den =
if not (is_multiple num den) then raise DivisionNotExact ;
num / den
end
module SymLinear = struct module SymLinear = struct
module M = struct module M = struct
include Caml.Map.Make (Symbol) include Caml.Map.Make (Symbol)
@ -46,111 +102,137 @@ module SymLinear = struct
fun cond x y -> fun cond x y ->
let merge_function k x y = if cond k x y then None else raise Exit in let merge_function k x y = if cond k x y then None else raise Exit in
match merge merge_function x y with _ -> true | exception Exit -> false match merge merge_function x y with _ -> true | exception Exit -> false
let is_singleton : 'a t -> (key * 'a) option =
fun m ->
if is_empty m then None
else
let (kmin, _) as binding = min_binding m in
let kmax, _ = max_binding m in
if Symbol.equal kmin kmax then Some binding else None
end end
type t = int M.t [@@deriving compare] (**
Map from symbols to integer coefficients.
{ x -> 2, y -> 5 } represents the value 2 * x + 5 * y
*)
type t = NonZeroInt.t M.t [@@deriving compare]
let empty : t = M.empty let empty : t = M.empty
let is_empty : t -> bool = M.is_empty let is_empty : t -> bool = fun x -> M.is_empty x
let add : Symbol.t -> int -> t -> t = M.add let remove : Symbol.t -> t -> t = fun s x -> M.remove s x
let cardinal : t -> int = M.cardinal let singleton_one : Symbol.t -> t = fun s -> M.singleton s NonZeroInt.one
let min_binding : t -> Symbol.t * int = M.min_binding let singleton_minus_one : Symbol.t -> t = fun s -> M.singleton s NonZeroInt.minus_one
let singleton : Symbol.t -> int -> t = M.singleton let find : Symbol.t -> t -> NonZeroInt.t = fun s x -> M.find s x
let find : Symbol.t -> t -> int = fun s x -> try M.find s x with Not_found -> 0 let use_symbol : Symbol.t -> t -> bool = fun s x -> M.mem s x
let is_le_zero : t -> bool = let is_le_zero : t -> bool =
fun x -> M.for_all (fun s v -> Int.equal v 0 || Symbol.is_unsigned s && v <= 0) x fun x -> M.for_all (fun s v -> Symbol.is_unsigned s && NonZeroInt.is_negative v) x
let is_ge_zero : t -> bool = let is_ge_zero : t -> bool =
fun x -> M.for_all (fun s v -> Int.equal v 0 || Symbol.is_unsigned s && v >= 0) x fun x -> M.for_all (fun s v -> Symbol.is_unsigned s && NonZeroInt.is_positive v) x
let le : t -> t -> bool = let le : t -> t -> bool =
fun x y -> fun x y ->
let le_one_pair s v1_opt v2_opt = let le_one_pair s (v1_opt: NonZeroInt.t option) (v2_opt: NonZeroInt.t option) =
let v1, v2 = (Option.value v1_opt ~default:0, Option.value v2_opt ~default:0) in let v1 = Option.value (v1_opt :> int option) ~default:0 in
let v2 = Option.value (v2_opt :> int option) ~default:0 in
Int.equal v1 v2 || Symbol.is_unsigned s && v1 <= v2 Int.equal v1 v2 || Symbol.is_unsigned s && v1 <= v2
in in
M.for_all2 le_one_pair x y M.for_all2 le_one_pair x y
let make : unsigned:bool -> Typ.Procname.t -> int -> t = let make : unsigned:bool -> Typ.Procname.t -> int -> t =
fun ~unsigned pname i -> M.add (Symbol.make ~unsigned pname i) 1 empty fun ~unsigned pname i -> singleton_one (Symbol.make ~unsigned pname i)
let eq : t -> t -> bool = fun x y -> le x y && le y x let eq : t -> t -> bool =
fun x y ->
let eq_pair _ (coeff1: NonZeroInt.t option) (coeff2: NonZeroInt.t option) =
[%compare.equal : int option] (coeff1 :> int option) (coeff2 :> int option)
in
M.for_all2 eq_pair x y
let pp1 : F.formatter -> Symbol.t * int -> unit = let pp1 : F.formatter -> Symbol.t * NonZeroInt.t -> unit =
fun fmt (s, c) -> fun fmt (s, c) ->
if Int.equal c 0 then () let c = (c :> int) in
else if Int.equal c 1 then F.fprintf fmt "%a" Symbol.pp s if Int.equal c 1 then F.fprintf fmt "%a" Symbol.pp s
else if c < 0 then F.fprintf fmt "(%d)x%a" c Symbol.pp s else if c < 0 then F.fprintf fmt "(%d)x%a" c Symbol.pp s
else F.fprintf fmt "%dx%a" c Symbol.pp s else F.fprintf fmt "%dx%a" c Symbol.pp s
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
fun fmt x -> fun fmt x ->
if M.is_empty x then F.fprintf fmt "empty" if M.is_empty x then F.fprintf fmt "empty" else Pp.seq ~sep:" + " pp1 fmt (M.bindings x)
else
let s1, c1 = M.min_binding x in
pp1 fmt (s1, c1) ;
M.iter (fun s c -> F.fprintf fmt " + %a" pp1 (s, c)) (M.remove s1 x)
let zero : t = M.empty let zero : t = M.empty
let is_zero : t -> bool = fun x -> M.for_all (fun _ v -> Int.equal v 0) x let is_zero : t -> bool = M.is_empty
let is_mod_zero : t -> int -> bool =
fun x n ->
assert (n <> 0) ;
M.for_all (fun _ v -> Int.equal (v mod n) 0) x
let neg : t -> t = fun x -> M.map ( ~- )x
(* Returns (Some n) only when n is not 0. *) let neg : t -> t = fun x -> M.map NonZeroInt.( ~- ) x
let is_non_zero : int -> int option = fun n -> if Int.equal n 0 then None else Some n
let plus : t -> t -> t = let plus : t -> t -> t =
fun x y -> fun x y ->
let plus' _ n_opt m_opt = let plus' _ (n_opt: NonZeroInt.t option) (m_opt: NonZeroInt.t option) =
match (n_opt, m_opt) with match (n_opt, m_opt) with
| None, None -> | None, None ->
None None
| Some v, None | None, Some v -> | (Some _ as some_v), None | None, (Some _ as some_v) ->
is_non_zero v some_v
| Some n, Some m -> | Some n, Some m ->
is_non_zero (n + m) NonZeroInt.of_int ((n :> int) + (m :> int))
in in
M.merge plus' x y M.merge plus' x y
let mult_const : t -> int -> t = fun x n -> M.map (( * ) n) x (** [se1] * [c] + [se2] *)
let mult_const_plus : t -> NonZeroInt.t -> t -> t =
fun se1 c se2 ->
let f _ (coeff1: NonZeroInt.t option) (coeff2: NonZeroInt.t option) =
match (coeff1, coeff2) with
| None, None ->
None
| None, (Some _ as some_v) ->
some_v
| Some v, None ->
Some (NonZeroInt.( * ) v c)
| Some v1, Some v2 ->
NonZeroInt.of_int ((v1 :> int) * (c :> int) + (v2 :> int))
in
M.merge f se1 se2
let mult_const : t -> NonZeroInt.t -> t = fun x n -> M.map (NonZeroInt.( * ) n) x
let exact_div_const_exn : t -> NonZeroInt.t -> t =
fun x n -> M.map (fun c -> NonZeroInt.exact_div_exn c n) x
let div_const : t -> int -> t = fun x n -> M.map (fun c -> c / n) x
(* Returns a symbol when the map contains only one symbol s with a (* Returns a symbol when the map contains only one symbol s with a
given coefficient. *) given coefficient. *)
let one_symbol_of_coeff : int -> t -> Symbol.t option = let one_symbol_of_coeff : NonZeroInt.t -> t -> Symbol.t option =
fun coeff x -> fun coeff x ->
let x = M.filter (fun _ v -> v <> 0) x in match M.is_singleton x with
if Int.equal (M.cardinal x) 1 then | Some (k, v) when Int.equal (v :> int) (coeff :> int) ->
let k, v = M.min_binding x in Some k
if Int.equal v coeff then Some k else None | _ ->
else None None
let get_one_symbol_opt : t -> Symbol.t option = one_symbol_of_coeff 1 let get_one_symbol_opt : t -> Symbol.t option = one_symbol_of_coeff NonZeroInt.one
let get_mone_symbol_opt : t -> Symbol.t option = one_symbol_of_coeff (-1) let get_mone_symbol_opt : t -> Symbol.t option = one_symbol_of_coeff NonZeroInt.minus_one
let get_one_symbol : t -> Symbol.t = let get_one_symbol : t -> Symbol.t =
fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_one_symbol fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_one_symbol
@ -168,41 +250,49 @@ module SymLinear = struct
fun x -> match get_mone_symbol_opt x with Some _ -> true | None -> false fun x -> match get_mone_symbol_opt x with Some _ -> true | None -> false
let get_symbols : t -> Symbol.t list = fun x -> List.map ~f:fst (M.bindings x) let get_symbols : t -> Symbol.t list =
fun x -> M.fold (fun symbol _coeff acc -> symbol :: acc) x []
end end
module Bound = struct module Bound = struct
type sign_t = Plus | Minus [@@deriving compare] type sign = Plus | Minus [@@deriving compare]
module Sign = struct
type t = sign [@@deriving compare]
let sign_equal = [%compare.equal : sign_t] let equal = [%compare.equal : t]
let neg_sign = function Plus -> Minus | Minus -> Plus let neg = function Plus -> Minus | Minus -> Plus
type min_max_t = Min | Max [@@deriving compare] let pp ~need_plus : F.formatter -> t -> unit =
fun fmt ->
function Plus -> if need_plus then F.fprintf fmt "+" | Minus -> F.fprintf fmt "-"
end
let min_max_equal = [%compare.equal : min_max_t] type min_max = Min | Max [@@deriving compare]
let neg_min_max = function Min -> Max | Max -> Min module MinMax = struct
type t = min_max [@@deriving compare]
let equal = [%compare.equal : t]
let neg = function Min -> Max | Max -> Min
let pp : F.formatter -> t -> unit =
fun fmt -> function Min -> F.fprintf fmt "min" | Max -> F.fprintf fmt "max"
end
(* MinMax constructs a bound that is in the "int [+|-] [min|max](int, symbol)" format. (* MinMax constructs a bound that is in the "int [+|-] [min|max](int, symbol)" format.
e.g. `MinMax (1, Minus, Max, 2, s)` means "1 - max (2, s)". *) e.g. `MinMax (1, Minus, Max, 2, s)` means "1 - max (2, s)". *)
type t = type t =
| MInf | MInf
| Linear of int * SymLinear.t | Linear of int * SymLinear.t
| MinMax of int * sign_t * min_max_t * int * Symbol.t | MinMax of int * Sign.t * MinMax.t * int * Symbol.t
| PInf | PInf
[@@deriving compare] [@@deriving compare]
let equal = [%compare.equal : t] let equal = [%compare.equal : t]
let pp_sign ~need_plus : F.formatter -> sign_t -> unit =
fun fmt -> function Plus -> if need_plus then F.fprintf fmt "+" | Minus -> F.fprintf fmt "-"
let pp_min_max : F.formatter -> min_max_t -> unit =
fun fmt -> function Min -> F.fprintf fmt "min" | Max -> F.fprintf fmt "max"
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
fun fmt -> fun fmt ->
function function
@ -215,9 +305,9 @@ module Bound = struct
else if Int.equal c 0 then F.fprintf fmt "%a" SymLinear.pp x else if Int.equal c 0 then F.fprintf fmt "%a" SymLinear.pp x
else F.fprintf fmt "%a + %d" SymLinear.pp x c else F.fprintf fmt "%a + %d" SymLinear.pp x c
| MinMax (c, sign, m, d, x) -> | MinMax (c, sign, m, d, x) ->
if Int.equal c 0 then F.fprintf fmt "%a" (pp_sign ~need_plus:false) sign if Int.equal c 0 then F.fprintf fmt "%a" (Sign.pp ~need_plus:false) sign
else F.fprintf fmt "%d%a" c (pp_sign ~need_plus:true) sign ; else F.fprintf fmt "%d%a" c (Sign.pp ~need_plus:true) sign ;
F.fprintf fmt "%a(%d, %a)" pp_min_max m d Symbol.pp x F.fprintf fmt "%a(%d, %a)" MinMax.pp m d Symbol.pp x
let of_int : int -> t = fun n -> Linear (n, SymLinear.empty) let of_int : int -> t = fun n -> Linear (n, SymLinear.empty)
@ -237,29 +327,22 @@ module Bound = struct
true true
let opt_lift : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool =
fun f a_opt b_opt ->
match (a_opt, b_opt) with None, _ | _, None -> false | Some a, Some b -> f a b
let eq_symbol : Symbol.t -> t -> bool = let eq_symbol : Symbol.t -> t -> bool =
fun s -> fun s ->
function function
| Linear (0, se) -> | Linear (0, se) -> (
opt_lift Symbol.eq (SymLinear.get_one_symbol_opt se) (Some s) match SymLinear.get_one_symbol_opt se with None -> false | Some s' -> Symbol.equal s s' )
| _ -> | _ ->
false false
let lift_get_one_symbol : (SymLinear.t -> Symbol.t option) -> t -> Symbol.t option = let lift_symlinear : (SymLinear.t -> 'a option) -> t -> 'a option =
fun f -> function Linear (0, se) -> f se | _ -> None fun f -> function Linear (0, se) -> f se | _ -> None
let get_one_symbol_opt : t -> Symbol.t option = lift_get_one_symbol SymLinear.get_one_symbol_opt let get_one_symbol_opt : t -> Symbol.t option = lift_symlinear SymLinear.get_one_symbol_opt
let get_mone_symbol_opt : t -> Symbol.t option =
lift_get_one_symbol SymLinear.get_mone_symbol_opt
let get_mone_symbol_opt : t -> Symbol.t option = lift_symlinear SymLinear.get_mone_symbol_opt
let get_one_symbol : t -> Symbol.t = let get_one_symbol : t -> Symbol.t =
fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_one_symbol fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_one_symbol
@ -281,9 +364,9 @@ module Bound = struct
| Max when d <= 0 -> ( | Max when d <= 0 -> (
match sign with match sign with
| Plus -> | Plus ->
Linear (c, SymLinear.singleton s 1) Linear (c, SymLinear.singleton_one s)
| Minus -> | Minus ->
Linear (c, SymLinear.singleton s (-1)) ) Linear (c, SymLinear.singleton_minus_one s) )
| _ -> | _ ->
MinMax (c, sign, m, d, s) MinMax (c, sign, m, d, s)
else MinMax (c, sign, m, d, s) else MinMax (c, sign, m, d, s)
@ -295,11 +378,12 @@ module Bound = struct
| PInf | MInf -> | PInf | MInf ->
false false
| Linear (_, se) -> | Linear (_, se) ->
SymLinear.find s se <> 0 SymLinear.use_symbol s se
| MinMax (_, _, _, _, s') -> | MinMax (_, _, _, _, s') ->
Symbol.eq s s' Symbol.equal s s'
(** substitutes [s] with [y0] in [x0], if the result is not expressible, return [default] *)
let subst1 : default:t -> t bottom_lifted -> Symbol.t -> t bottom_lifted -> t bottom_lifted = let subst1 : default:t -> t bottom_lifted -> Symbol.t -> t bottom_lifted -> t bottom_lifted =
fun ~default x0 s y0 -> fun ~default x0 s y0 ->
match (x0, y0) with match (x0, y0) with
@ -316,9 +400,9 @@ module Bound = struct
match (x, y) with match (x, y) with
| Linear (c1, se1), Linear (c2, se2) -> | Linear (c1, se1), Linear (c2, se2) ->
let coeff = SymLinear.find s se1 in let coeff = SymLinear.find s se1 in
let c' = c1 + coeff * c2 in let c' = c1 + (coeff :> int) * c2 in
let se1 = SymLinear.add s 0 se1 in let se1 = SymLinear.remove s se1 in
let se' = SymLinear.plus se1 (SymLinear.mult_const se2 coeff) in let se' = SymLinear.mult_const_plus se2 coeff se1 in
Linear (c', se') Linear (c', se')
| MinMax (_, Plus, Min, _, _), MInf -> | MinMax (_, Plus, Min, _, _), MInf ->
MInf MInf
@ -347,7 +431,7 @@ module Bound = struct
| MinMax (c, sign, m, d, _), _ when is_one_symbol y -> | MinMax (c, sign, m, d, _), _ when is_one_symbol y ->
mk_MinMax (c, sign, m, d, get_one_symbol y) mk_MinMax (c, sign, m, d, get_one_symbol y)
| MinMax (c, sign, m, d, _), _ when is_mone_symbol y -> | MinMax (c, sign, m, d, _), _ when is_mone_symbol y ->
mk_MinMax (c, neg_sign sign, neg_min_max m, -d, get_mone_symbol y) mk_MinMax (c, Sign.neg sign, MinMax.neg m, -d, get_mone_symbol y)
| MinMax (c1, Plus, Min, d1, _), MinMax (c2, Plus, Min, d2, s') -> | MinMax (c1, Plus, Min, d1, _), MinMax (c2, Plus, Min, d2, s') ->
mk_MinMax (c1 + c2, Plus, Min, min (d1 - c2) d2, s') mk_MinMax (c1 + c2, Plus, Min, min (d1 - c2) d2, s')
| MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, s') -> | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, s') ->
@ -398,9 +482,9 @@ module Bound = struct
let linear_ub_of_minmax = function let linear_ub_of_minmax = function
| MinMax (c, Plus, Min, _, x) -> | MinMax (c, Plus, Min, _, x) ->
Some (Linear (c, SymLinear.singleton x 1)) Some (Linear (c, SymLinear.singleton_one x))
| MinMax (c, Minus, Max, _, x) -> | MinMax (c, Minus, Max, _, x) ->
Some (Linear (c, SymLinear.singleton x (-1))) Some (Linear (c, SymLinear.singleton_minus_one x))
| MinMax _ -> | MinMax _ ->
None None
| MInf | PInf | Linear _ -> | MInf | PInf | Linear _ ->
@ -409,9 +493,9 @@ module Bound = struct
let linear_lb_of_minmax = function let linear_lb_of_minmax = function
| MinMax (c, Plus, Max, _, x) -> | MinMax (c, Plus, Max, _, x) ->
Some (Linear (c, SymLinear.singleton x 1)) Some (Linear (c, SymLinear.singleton_one x))
| MinMax (c, Minus, Min, _, x) -> | MinMax (c, Minus, Min, _, x) ->
Some (Linear (c, SymLinear.singleton x (-1))) Some (Linear (c, SymLinear.singleton_minus_one x))
| MinMax _ -> | MinMax _ ->
None None
| MInf | PInf | Linear _ -> | MInf | PInf | Linear _ ->
@ -436,18 +520,18 @@ module Bound = struct
| Linear (c0, x0), Linear (c1, x1) -> | Linear (c0, x0), Linear (c1, x1) ->
c0 <= c1 && SymLinear.le x0 x1 c0 <= c1 && SymLinear.le x0 x1
| MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2) | MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2)
when sign_equal sign1 sign2 && min_max_equal m1 m2 -> when Sign.equal sign1 sign2 && MinMax.equal m1 m2 ->
c1 <= c2 && Int.equal d1 d2 && Symbol.eq x1 x2 c1 <= c2 && Int.equal d1 d2 && Symbol.equal x1 x2
| MinMax _, MinMax _ when le_minmax_by_int x y -> | MinMax _, MinMax _ when le_minmax_by_int x y ->
true true
| MinMax (c1, Plus, Min, _, x1), MinMax (c2, Plus, Max, _, x2) | MinMax (c1, Plus, Min, _, x1), MinMax (c2, Plus, Max, _, x2)
| MinMax (c1, Minus, Max, _, x1), MinMax (c2, Minus, Min, _, x2) -> | MinMax (c1, Minus, Max, _, x1), MinMax (c2, Minus, Min, _, x2) ->
c1 <= c2 && Symbol.eq x1 x2 c1 <= c2 && Symbol.equal x1 x2
| MinMax _, Linear (c, se) -> | MinMax _, Linear (c, se) ->
SymLinear.is_ge_zero se && le_opt1 ( <= ) (int_ub_of_minmax x) c SymLinear.is_ge_zero se && le_opt1 Int.( <= ) (int_ub_of_minmax x) c
|| le_opt1 le (linear_ub_of_minmax x) y || le_opt1 le (linear_ub_of_minmax x) y
| Linear (c, se), MinMax _ -> | Linear (c, se), MinMax _ ->
SymLinear.is_le_zero se && le_opt2 ( <= ) c (int_lb_of_minmax y) SymLinear.is_le_zero se && le_opt2 Int.( <= ) c (int_lb_of_minmax y)
|| le_opt2 le x (linear_lb_of_minmax y) || le_opt2 le x (linear_lb_of_minmax y)
| _, _ -> | _, _ ->
false false
@ -488,9 +572,9 @@ module Bound = struct
fun x -> fun x ->
match x with match x with
| MinMax (c, Plus, Max, _, s) -> | MinMax (c, Plus, Max, _, s) ->
Linear (c, SymLinear.singleton s 1) Linear (c, SymLinear.singleton_one s)
| MinMax (c, Minus, Min, _, s) -> | MinMax (c, Minus, Min, _, s) ->
Linear (c, SymLinear.singleton s (-1)) Linear (c, SymLinear.singleton_minus_one s)
| _ -> | _ ->
x x
@ -653,35 +737,34 @@ module Bound = struct
PInf PInf
let mult_const : t -> int -> t option = let mult_const : t -> NonZeroInt.t -> t option =
fun x n -> fun x n ->
assert (n <> 0) ;
match x with match x with
| MInf -> | MInf ->
Some (if n > 0 then MInf else PInf) Some (if NonZeroInt.is_positive n then MInf else PInf)
| PInf -> | PInf ->
Some (if n > 0 then PInf else MInf) Some (if NonZeroInt.is_positive n then PInf else MInf)
| Linear (c, x') -> | Linear (c, x') ->
Some (Linear (c * n, SymLinear.mult_const x' n)) Some (Linear (c * (n :> int), SymLinear.mult_const x' n))
| _ -> | _ ->
None None
let div_const : t -> int -> t option = let div_const : t -> NonZeroInt.t -> t option =
fun x n -> fun x n ->
if Int.equal n 0 then Some zero match x with
else | MInf ->
match x with Some (if NonZeroInt.is_positive n then MInf else PInf)
| MInf -> | PInf ->
Some (if n > 0 then MInf else PInf) Some (if NonZeroInt.is_positive n then PInf else MInf)
| PInf -> | Linear (c, x') when NonZeroInt.is_multiple c n -> (
Some (if n > 0 then PInf else MInf) match SymLinear.exact_div_const_exn x' n with
| Linear (c, x') -> | x'' ->
if Int.equal (c mod n) 0 && SymLinear.is_mod_zero x' n then Some (Linear (c / (n :> int), x''))
Some (Linear (c / n, SymLinear.div_const x' n)) | exception NonZeroInt.DivisionNotExact ->
else None None )
| _ -> | _ ->
None None
let neg : t -> t option = function let neg : t -> t option = function
@ -692,7 +775,7 @@ module Bound = struct
| Linear (c, x) -> | Linear (c, x) ->
Some (Linear (-c, SymLinear.neg x)) Some (Linear (-c, SymLinear.neg x))
| MinMax (c, sign, min_max, d, x) -> | MinMax (c, sign, min_max, d, x) ->
Some (mk_MinMax (-c, neg_sign sign, min_max, d, x)) Some (mk_MinMax (-c, Sign.neg sign, min_max, d, x))
let get_symbols : t -> Symbol.t list = function let get_symbols : t -> Symbol.t list = function
@ -869,31 +952,41 @@ module ItvPure = struct
let minus : t -> t -> t = fun i1 i2 -> plus i1 (neg i2) let minus : t -> t -> t = fun i1 i2 -> plus i1 (neg i2)
let mult_const : t -> int -> t = let mult_const : t -> int -> t =
fun (l, u) n -> fun ((l, u) as itv) n ->
if Int.equal n 0 then zero match NonZeroInt.of_int n with
else if n > 0 then | None ->
let l' = Option.value ~default:Bound.MInf (Bound.mult_const l n) in zero
let u' = Option.value ~default:Bound.PInf (Bound.mult_const u n) in | Some n ->
(l', u') if NonZeroInt.is_one n then itv
else else if NonZeroInt.is_minus_one n then neg itv
let l' = Option.value ~default:Bound.MInf (Bound.mult_const u n) in else if NonZeroInt.is_positive n then
let u' = Option.value ~default:Bound.PInf (Bound.mult_const l n) in let l' = Option.value ~default:Bound.MInf (Bound.mult_const l n) in
(l', u') let u' = Option.value ~default:Bound.PInf (Bound.mult_const u n) in
(l', u')
else
(* Returns a correct value only when all coefficients are divided by let l' = Option.value ~default:Bound.MInf (Bound.mult_const u n) in
let u' = Option.value ~default:Bound.PInf (Bound.mult_const l n) in
(l', u')
(* Returns a precise value only when all coefficients are divided by
n without remainder. *) n without remainder. *)
let div_const : t -> int -> t = let div_const : t -> int -> t =
fun (l, u) n -> fun ((l, u) as itv) n ->
assert (n <> 0) ; match NonZeroInt.of_int n with
if n > 0 then | None ->
let l' = Option.value ~default:Bound.MInf (Bound.div_const l n) in top
let u' = Option.value ~default:Bound.PInf (Bound.div_const u n) in | Some n ->
(l', u') if NonZeroInt.is_one n then itv
else else if NonZeroInt.is_minus_one n then neg itv
let l' = Option.value ~default:Bound.MInf (Bound.div_const u n) in else if NonZeroInt.is_positive n then
let u' = Option.value ~default:Bound.PInf (Bound.div_const l n) in let l' = Option.value ~default:Bound.MInf (Bound.div_const l n) in
(l', u') let u' = Option.value ~default:Bound.PInf (Bound.div_const u n) in
(l', u')
else
let l' = Option.value ~default:Bound.MInf (Bound.div_const u n) in
let u' = Option.value ~default:Bound.PInf (Bound.div_const l n) in
(l', u')
let mult : t -> t -> t = let mult : t -> t -> t =
@ -907,39 +1000,41 @@ module ItvPure = struct
top top
let div : t -> t -> t = let div : t -> t -> t = fun x y -> match is_const y with None -> top | Some n -> div_const x n
fun x y -> match is_const y with Some n when n <> 0 -> div_const x n | _ -> top
(* x % [0,0] does nothing. *)
let mod_sem : t -> t -> t = let mod_sem : t -> t -> t =
fun x y -> fun x y ->
match (is_const x, is_const y) with match is_const y with
| _, Some 0 -> | None ->
x
| Some n, Some m ->
of_int (n mod m)
| _, Some m ->
let abs_m = abs m in
if is_ge_zero x then (Bound.zero, Bound.of_int (abs_m - 1))
else if is_le_zero x then (Bound.of_int (-abs_m + 1), Bound.zero)
else (Bound.of_int (-abs_m + 1), Bound.of_int (abs_m - 1))
| _, None ->
top top
| Some 0 ->
x (* x % [0,0] does nothing. *)
| Some m ->
match is_const x with
| Some n ->
of_int (n mod m)
| None ->
let abs_m = abs m in
if is_ge_zero x then (Bound.zero, Bound.of_int (abs_m - 1))
else if is_le_zero x then (Bound.of_int (-abs_m + 1), Bound.zero)
else (Bound.of_int (-abs_m + 1), Bound.of_int (abs_m - 1))
(* x << [-1,-1] does nothing. *) (* x << [-1,-1] does nothing. *)
let shiftlt : t -> t -> t = let shiftlt : t -> t -> t =
fun x y -> fun x y -> match is_const y with Some n -> mult_const x (1 lsl n) | None -> top
match is_const y with Some n -> if n >= 0 then mult_const x (1 lsl n) else x | None -> top
(* x >> [-1,-1] does nothing. *) (* x >> [-1,-1] does nothing. *)
let shiftrt : t -> t -> t = let shiftrt : t -> t -> t =
fun x y -> fun x y ->
match is_const y with match is_const y with
| Some n when Int.( <= ) n 0 ->
x
| Some n when n >= 64 ->
zero
| Some n -> | Some n ->
if n >= 0 && n < 63 then div_const x (1 lsl n) else x div_const x (1 lsl n)
| None -> | None ->
top top
@ -1016,7 +1111,7 @@ module ItvPure = struct
(l1, Bound.mk_MinMax (c2, Bound.Plus, Bound.Min, min (c1 - c2) d2, se')) (l1, Bound.mk_MinMax (c2, Bound.Plus, Bound.Min, min (c1 - c2) d2, se'))
| ( (l1, Bound.MinMax (c1, Bound.Plus, Bound.Min, d1, se1)) | ( (l1, Bound.MinMax (c1, Bound.Plus, Bound.Min, d1, se1))
, (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se2)) ) , (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se2)) )
when Int.equal c1 c2 && Symbol.eq se1 se2 -> when Int.equal c1 c2 && Symbol.equal se1 se2 ->
(l1, Bound.mk_MinMax (c1, Bound.Plus, Bound.Min, min d1 d2, se1)) (l1, Bound.mk_MinMax (c1, Bound.Plus, Bound.Min, min d1 d2, se1))
| _ -> | _ ->
x x
@ -1043,7 +1138,7 @@ module ItvPure = struct
(Bound.mk_MinMax (c2, Bound.Plus, Bound.Max, max (c1 - c2) d2, se'), u1) (Bound.mk_MinMax (c2, Bound.Plus, Bound.Max, max (c1 - c2) d2, se'), u1)
| ( (Bound.MinMax (c1, Bound.Plus, Bound.Max, d1, se1), u1) | ( (Bound.MinMax (c1, Bound.Plus, Bound.Max, d1, se1), u1)
, (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se2), _) ) , (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se2), _) )
when Int.equal c1 c2 && Symbol.eq se1 se2 -> when Int.equal c1 c2 && Symbol.equal se1 se2 ->
(Bound.mk_MinMax (c1, Bound.Plus, Bound.Max, max d1 d2, se1), u1) (Bound.mk_MinMax (c1, Bound.Plus, Bound.Max, max d1 d2, se1), u1)
| _ -> | _ ->
x x

Loading…
Cancel
Save