From 2621f349fde01ca82b19e92ba458d7e57cc90da7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 7 Jan 2020 16:05:58 +0100
Subject: [PATCH] [Ival] Optimization: shares small singleton integers and top
in memory.
---
.../abstract_interp/int_interval.ml | 40 ++-
.../abstract_interp/int_set.ml | 92 +++----
.../abstract_interp/int_set.mli | 2 -
.../abstract_interp/int_val.ml | 67 +++--
.../abstract_interp/int_val.mli | 3 -
src/kernel_services/abstract_interp/ival.ml | 230 ++++++++++--------
6 files changed, 206 insertions(+), 228 deletions(-)
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index ba4889551ba..1e3cf647bad 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -102,9 +102,6 @@ include Datatype.Make_with_collections
(* ------------------------------ Building ---------------------------------- *)
-let share_top t =
- if equal t top then top else t
-
let fail min max r modu =
let bound fmt = function
| None -> Format.fprintf fmt "--"
@@ -130,14 +127,13 @@ let check t =
let make ~min ~max ~rem ~modu =
let t = { min; max; rem; modu } in
check t;
- share_top t
+ t
let inject_singleton e =
{ min = Some e; max = Some e; rem = Int.zero; modu = Int.one }
let inject_range min max =
- let t = { min; max; rem = Int.zero; modu = Int.one } in
- share_top t
+ { min; max; rem = Int.zero; modu = Int.one }
let build_interval ~min ~max ~rem:r ~modu =
assert (is_safe_modulo r modu);
@@ -209,7 +205,6 @@ let rem_is_included r1 m1 r2 m2 =
(Int.is_zero (Int.e_rem m1 m2)) && (Int.equal (Int.e_rem r1 m2) r2)
let is_included t1 t2 =
- (t1 == t2) ||
(min_is_lower t2.min t1.min) &&
(max_is_greater t2.max t1.max) &&
rem_is_included t1.rem t1.modu t2.rem t2.modu
@@ -225,17 +220,13 @@ let max_max x y =
| Some x, Some y -> Some (Int.max x y)
let join t1 t2 =
- if t1 == t2 then t1 else
- begin
- check t1;
- check t2;
- let modu = Int.(pgcd (pgcd t1.modu t2.modu) (abs (sub t1.rem t2.rem))) in
- let rem = Int.e_rem t1.rem modu in
- let min = min_min t1.min t2.min in
- let max = max_max t1.max t2.max in
- let r = make ~min ~max ~rem ~modu in
- r
- end
+ check t1;
+ check t2;
+ let modu = Int.(pgcd (pgcd t1.modu t2.modu) (abs (sub t1.rem t2.rem))) in
+ let rem = Int.e_rem t1.rem modu in
+ let min = min_min t1.min t2.min in
+ let max = max_max t1.max t2.max in
+ make ~min ~max ~rem ~modu
let link t1 t2 =
if Int.equal t1.rem t2.rem && Int.equal t1.modu t2.modu
@@ -335,13 +326,12 @@ let compute_last_common mx1 mx2 r modu =
Some (Int.round_down_to_r m r modu)
let meet t1 t2 =
- if t1 == t2 then `Value t1 else
- try
- let rem, modu = compute_r_common t1.rem t1.modu t2.rem t2.modu in
- let min = compute_first_common t1.min t2.min rem modu in
- let max = compute_last_common t1.max t2.max rem modu in
- make_or_bottom ~min ~max ~rem ~modu
- with Error_Bottom -> `Bottom
+ try
+ let rem, modu = compute_r_common t1.rem t1.modu t2.rem t2.modu in
+ let min = compute_first_common t1.min t2.min rem modu in
+ let max = compute_last_common t1.max t2.max rem modu in
+ make_or_bottom ~min ~max ~rem ~modu
+ with Error_Bottom -> `Bottom
let narrow = meet
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 76786297af9..5ccb3eafff9 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -33,8 +33,6 @@ let debug_cardinal = false
let emitter = Lattice_messages.register "Int_set";;
let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-let small_nums = Array.init 33 (fun i -> [| (Integer.of_int i) |])
-
(* Small sets of integers, implemented as sorted non-empty arrays. *)
type set = Int.t array
@@ -59,23 +57,12 @@ module Array = struct
let sub a start len = assert (len > 0); sub a start len
end
-let zero = small_nums.(0)
-let one = small_nums.(1)
+let zero = [| Int.zero |]
+let one = [| Int.one |]
let minus_one = [| Int.minus_one |]
let zero_or_one = [| Int.zero ; Int.one |]
-let inject_singleton e =
- if Int.le Int.zero e && Int.le e Int.thirtytwo
- then small_nums.(Int.to_int e)
- else [| e |]
-
-let share_array a s =
- let e = a.(0) in
- if s = 1 && Int.le Int.zero e && Int.le e Int.thirtytwo
- then small_nums.(Int.to_int e)
- else if s = 2 && Int.is_zero e && Int.is_one a.(1)
- then zero_or_one
- else a
+let inject_singleton e = [| e |]
let inject_periodic ~from ~period ~number =
let l = Int.to_int number in
@@ -88,7 +75,7 @@ let inject_periodic ~from ~period ~number =
v := Int.add period !v;
incr i
done;
- share_array s l
+ s
module O = FCSet.Make (Integer)
@@ -98,7 +85,7 @@ let inject_list list =
let a = Array.make cardinal Int.zero in
let i = ref 0 in
O.iter (fun e -> a.(!i) <- e; incr i) o;
- share_array a cardinal
+ a
let to_list = Array.to_list
@@ -106,24 +93,21 @@ let to_list = Array.to_list
let hash s = Array.fold_left (fun acc v -> 1031 * acc + (Int.hash v)) 17 s
-let rehash s = share_array s (Array.length s)
-
exception Unequal of int
let compare s1 s2 =
- if s1 == s2 then 0 else
- let l1 = Array.length s1 in
- let l2 = Array.length s2 in
- if l1 <> l2
- then l1 - l2 (* no overflow here *)
- else
- (try
- for i = 0 to l1 - 1 do
- let r = Int.compare s1.(i) s2.(i) in
- if r <> 0 then raise (Unequal r)
- done;
- 0
- with Unequal v -> v)
+ let l1 = Array.length s1 in
+ let l2 = Array.length s2 in
+ if l1 <> l2
+ then l1 - l2 (* no overflow here *)
+ else
+ (try
+ for i = 0 to l1 - 1 do
+ let r = Int.compare s1.(i) s2.(i) in
+ if r <> 0 then raise (Unequal r)
+ done;
+ 0
+ with Unequal v -> v)
let equal e1 e2 = compare e1 e2 = 0
@@ -145,7 +129,7 @@ include Datatype.Make_with_collections
let compare = compare
let hash = hash
let pretty = pretty
- let rehash = rehash
+ let rehash x = x
let internal_pretty_code = Datatype.pp_fail
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
@@ -265,24 +249,12 @@ let add_ps ps x =
let new_max = Int.max max x in
Pre_top (new_min, new_max, new_modu)
-let o_zero = O.singleton Int.zero
-let o_one = O.singleton Int.one
-let o_zero_or_one = O.union o_zero o_one
-
let share_set o s =
- if s = 1
- then begin
- let e = O.min_elt o in
- inject_singleton e
- end
- else if O.equal o o_zero_or_one
- then zero_or_one
- else
- let a = Array.make s Int.zero in
- let i = ref 0 in
- O.iter (fun e -> a.(!i) <- e; incr i) o;
- assert (!i = s);
- a
+ let a = Array.make s Int.zero in
+ let i = ref 0 in
+ O.iter (fun e -> a.(!i) <- e; incr i) o;
+ assert (!i = s);
+ a
let inject_ps = function
| Pre_set (o, s) -> `Set (share_set o s)
@@ -301,7 +273,7 @@ let set_to_ival_under set =
then
let a = Array.make card Int.zero in
ignore (Int.Set.fold (fun elt i -> Array.set a i elt; i + 1) set 0);
- `Set (share_array a card)
+ `Set a
else
(* If by chance the set is contiguous. *)
if (Int.equal
@@ -326,7 +298,7 @@ let apply_bin_1_strict_incr f x (s : Integer.t array) =
let r, l = Array.zero_copy s in
let rec c i =
if i = l
- then share_array r l
+ then r
else
let v = f x s.(i) in
r.(i) <- v;
@@ -338,7 +310,7 @@ let apply_bin_1_strict_decr f x (s : Integer.t array) =
let r, l = Array.zero_copy s in
let rec c i =
if i = l
- then share_array r l
+ then r
else
let v = f x s.(i) in
r.(l - i - 1) <- v;
@@ -396,7 +368,7 @@ let map_set_strict_decr f (s : Integer.t array) =
let r, l = Array.zero_copy s in
let rec c i =
if i = l
- then share_array r l
+ then r
else
let v = f s.(i) in
r.(l - i - 1) <- v;
@@ -497,12 +469,12 @@ let join l1 s1 l2 s2 =
if i1 = l1
then begin
Array.blit s2 i2 r i (l2 - i2);
- share_array r uniq
+ r
end
else if i2 = l2
then begin
Array.blit s1 i1 r i (l1 - i1);
- share_array r uniq
+ r
end
else
let si = succ i in
@@ -583,7 +555,7 @@ let remove s v =
let r = Array.make l Int.zero in
Array.blit s 0 r 0 index;
Array.blit s (succ index) r index (l-index);
- `Value (share_array r l)
+ `Value r
else `Value s
let complement_under ~min ~max set =
@@ -672,9 +644,7 @@ let subdivide s =
let lenhi = len - m in
let lo = Array.sub s 0 m in
let hi = Array.sub s m lenhi in
- share_array lo m,
- share_array hi lenhi
-
+ lo, hi
(* -------------------------------- Export ---------------------------------- *)
diff --git a/src/kernel_services/abstract_interp/int_set.mli b/src/kernel_services/abstract_interp/int_set.mli
index 4c0a12ca1f0..777909b5289 100644
--- a/src/kernel_services/abstract_interp/int_set.mli
+++ b/src/kernel_services/abstract_interp/int_set.mli
@@ -130,5 +130,3 @@ val bitwise_signed_not: t -> t
(** {2 Misc} *)
val subdivide: t -> t * t
-
-val rehash: t -> t
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index a62c3dcb1c8..427fc4522b0 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -59,10 +59,6 @@ let pretty fmt = function
| Itv i -> Int_interval.pretty fmt i
| Set s -> Int_set.pretty fmt s
-let rehash = function
- | Set s -> Set (Int_set.rehash s)
- | x -> x
-
include Datatype.Make_with_collections
(struct
type t = int_val
@@ -77,7 +73,7 @@ include Datatype.Make_with_collections
let compare = compare
let hash = hash
let pretty = pretty
- let rehash = rehash
+ let rehash x = x
let internal_pretty_code = Datatype.pp_fail
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
@@ -348,9 +344,9 @@ let diff value rem =
(* ------------------------------- Lattice ---------------------------------- *)
let is_included t1 t2 =
- (t1 == t2) ||
match t1, t2 with
| Itv i1, Itv i2 -> Int_interval.is_included i1 i2
+ | Set s1, Set s2 -> Int_set.is_included s1 s2
| Itv _, Set _ -> false (* Itv _ represents more elements
than can be represented by Set _ *)
| Set s, Itv i ->
@@ -359,29 +355,27 @@ let is_included t1 t2 =
min_le_elt min (Int_set.min s) && max_ge_elt max (Int_set.max s)
&& (Int.equal Int.one modu (* Top side contains all integers, we're done *)
|| Int_set.for_all (fun x -> Int.equal (Int.e_rem x modu) rem) s)
- | Set s1, Set s2 -> Int_set.is_included s1 s2
let join v1 v2 =
- if v1 == v2 then v1 else
- match v1,v2 with
- | Itv i1, Itv i2 -> Itv (Int_interval.join i1 i2)
- | Set i1, Set i2 -> inject_set_or_top (Int_set.join i1 i2)
- | Set s, Itv i
- | Itv i, Set s ->
- let min, max, r, modu = Int_interval.min_max_rem_modu i in
- let f elt modu = Int.pgcd modu (Int.abs (Int.sub r elt)) in
- let modu = Int_set.fold f s modu in
- let rem = Int.e_rem r modu in
- let min = match min with
- None -> None
- | Some m -> Some (Int.min m (Int_set.min s))
- in
- let max = match max with
- None -> None
- | Some m -> Some (Int.max m (Int_set.max s))
- in
- check ~min ~max ~rem ~modu;
- Itv (Int_interval.make ~min ~max ~rem ~modu)
+ match v1, v2 with
+ | Itv i1, Itv i2 -> Itv (Int_interval.join i1 i2)
+ | Set s1, Set s2 -> inject_set_or_top (Int_set.join s1 s2)
+ | Set s, Itv i
+ | Itv i, Set s ->
+ let min, max, r, modu = Int_interval.min_max_rem_modu i in
+ let f elt modu = Int.pgcd modu (Int.abs (Int.sub r elt)) in
+ let modu = Int_set.fold f s modu in
+ let rem = Int.e_rem r modu in
+ let min = match min with
+ None -> None
+ | Some m -> Some (Int.min m (Int_set.min s))
+ in
+ let max = match max with
+ None -> None
+ | Some m -> Some (Int.max m (Int_set.max s))
+ in
+ check ~min ~max ~rem ~modu;
+ Itv (Int_interval.make ~min ~max ~rem ~modu)
let link v1 v2 =
match v1, v2 with
@@ -401,18 +395,14 @@ let link v1 v2 =
check_make ~min ~max ~rem ~modu
let meet v1 v2 =
- if v1 == v2 then `Value v1 else
- match v1, v2 with
- | Itv i1, Itv i2 -> Int_interval.meet i1 i2 >>-: inject_itv
- | Set s1 , Set s2 -> Int_set.meet s1 s2 >>-: inject_set
- | Set s, Itv itv
- | Itv itv, Set s ->
- Int_set.filter (fun i -> Int_interval.mem i itv) s >>-: inject_set
-
-let narrow v1 v2 =
match v1, v2 with
- | Set s1, Set s2 -> Int_set.narrow s1 s2 >>-: inject_set
- | (Itv _| Set _), (Itv _ | Set _) -> meet v1 v2 (* meet is exact *)
+ | Itv i1, Itv i2 -> Int_interval.meet i1 i2 >>-: inject_itv
+ | Set s1 , Set s2 -> Int_set.meet s1 s2 >>-: inject_set
+ | Set s, Itv itv
+ | Itv itv, Set s ->
+ Int_set.filter (fun i -> Int_interval.mem i itv) s >>-: inject_set
+
+let narrow = meet (* meet is exact *)
let widen widen_hints t1 t2 =
if equal t1 t2 || cardinal_zero_or_one t1 then t2
@@ -424,7 +414,6 @@ let widen widen_hints t1 t2 =
inject_itv (Int_interval.widen widen_hints i1 i2)
let intersects v1 v2 =
- v1 == v2 ||
match v1, v2 with
| Itv _, Itv _ -> not (meet v1 v2 = `Bottom) (* YYY: slightly inefficient *)
| Set s1 , Set s2 -> Int_set.intersects s1 s2
diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli
index 8187397e75d..0c8f672ede2 100644
--- a/src/kernel_services/abstract_interp/int_val.mli
+++ b/src/kernel_services/abstract_interp/int_val.mli
@@ -180,6 +180,3 @@ val complement_under: size:int -> signed:bool -> t -> t or_bottom
by default. If [increasing] is set to false, iterate by decreasing order.
@raise Abstract_interp.Error_Top if the abstraction is unbounded. *)
val fold_int: ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
-
-(** Low-level operation for demarshalling *)
-val rehash: t -> t
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index f635675a6ca..f7c2c341eda 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -26,24 +26,79 @@ open Bottom.Type
let emitter = Lattice_messages.register "Ival"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-type t =
- | Bottom
- | Int of Int_val.t
- | Float of Fval.t
+module type Type = sig
(* Binary abstract operations do not model precisely float/integer operations.
- It is the responsibility of the callers to have two operands of the same
- implicit type. The only exception is for [singleton_zero], which is the
- correct representation of [0.] *)
+ It is the responsibility of the callers to have two operands of the same
+ implicit type. The only exception is for [singleton_zero], which is the
+ correct representation of [0.] *)
+ type t = private
+ | Bottom
+ | Int of Int_val.t
+ | Float of Fval.t
+
+ val bottom: t
+ val zero: t
+ val one: t
+ val top: t
+ val inject_singleton: Int.t -> t
+ val inject_int: Int_val.t -> t
+ val inject_float: Fval.t -> t
+ val inject_float_interval: float -> float -> t
+end
+
+(* This module ensures that small integer singletons (and especially zero) and
+ the top value are shared in memory. This enables some optimizations where we
+ check the physical identity instead of the equality. Outside this module,
+ values of type t can only be created by calling [inject_] constructors. *)
+module Type : Type = struct
+ type t =
+ | Bottom
+ | Int of Int_val.t
+ | Float of Fval.t
+
+ let small_nums =
+ Array.init 33 (fun i -> Int (Int_val.inject_singleton (Int.of_int i)))
+
+ let bottom = Bottom
+ let zero = small_nums.(0)
+ let one = small_nums.(1)
+ let top = Int Int_val.top
+
+ let inject_singleton e =
+ if Int.le Int.zero e && Int.le e Int.thirtytwo
+ then small_nums.(Int.to_int e)
+ else Int (Int_val.inject_singleton e)
+
+ let inject_int i =
+ try
+ let e = Int_val.project_int i in
+ if Int.le Int.zero e && Int.le e Int.thirtytwo
+ then small_nums.(Int.to_int e)
+ else Int i
+ with Int_val.Not_Singleton ->
+ if Int_val.(equal top i) then top else Int i
+
+ let inject_float f =
+ if Fval.(equal plus_zero f)
+ then zero
+ else Float f
+
+ let inject_float_interval flow fup =
+ let flow = Fval.F.of_float flow in
+ let fup = Fval.F.of_float fup in
+ (* make sure that zero float is also zero int *)
+ if Fval.F.equal Fval.F.plus_zero flow && Fval.F.equal Fval.F.plus_zero fup
+ then zero
+ else Float (Fval.inject Fval.Double flow fup)
+end
+include Type
module Widen_Hints = Datatype.Integer.Set
type size_widen_hint = Integer.t
type numerical_widen_hint = Widen_Hints.t * Fc_float.Widen_Hints.t
type widen_hint = size_widen_hint * numerical_widen_hint
-let bottom = Bottom
-let top = Int Int_val.top
-
let hash = function
| Bottom -> 311
| Int i -> Int_val.hash i
@@ -78,42 +133,23 @@ let is_singleton_int = function
| Float _ -> false
| Int i -> Int_val.is_singleton i
-let is_bottom x = equal x bottom
-
-let zero = Int Int_val.zero
-let one = Int Int_val.one
-let minus_one = Int Int_val.minus_one
-let zero_or_one = Int Int_val.zero_or_one
-let float_zeros = Float Fval.zeros
+let is_bottom = (==) bottom
+let is_zero = (==) zero
+let is_one = (==) one
-let positive_integers = Int Int_val.positive_integers
-let negative_integers = Int Int_val.negative_integers
+let minus_one = inject_int Int_val.minus_one
+let zero_or_one = inject_int Int_val.zero_or_one
+let float_zeros = inject_float Fval.zeros
-let is_zero x = equal x zero
-
-let inject_singleton e = Int (Int_val.inject_singleton e)
-
-let inject_float f =
- if Fval.(equal plus_zero f)
- then zero
- else Float f
-
-let inject_float_interval flow fup =
- let flow = Fval.F.of_float flow in
- let fup = Fval.F.of_float fup in
- (* make sure that zero float is also zero int *)
- if Fval.F.equal Fval.F.plus_zero flow && Fval.F.equal Fval.F.plus_zero fup
- then zero
- else Float (Fval.inject Fval.Double flow fup)
+let positive_integers = inject_int Int_val.positive_integers
+let negative_integers = inject_int Int_val.negative_integers
let inject_int_or_bottom = function
| `Bottom -> bottom
- | `Value i -> Int i
+ | `Value i -> inject_int i
(* let minus_zero = Float (Fval.minus_zero, Fval.minus_zero) *)
-let is_one = equal one
-
let project_float v =
if is_zero v
then Fval.plus_zero
@@ -194,13 +230,13 @@ let cardinal_is_less_than v n =
let inject_top min max rem modu =
match min, max with
- | Some mn, Some mx when Int.gt mn mx -> Bottom
- | _, _ -> Int (Int_val.make ~min ~max ~rem ~modu)
+ | Some mn, Some mx when Int.gt mn mx -> bottom
+ | _, _ -> inject_int (Int_val.make ~min ~max ~rem ~modu)
let inject_interval ~min ~max ~rem ~modu =
match min, max with
- | Some mn, Some mx when Int.gt mn mx -> Bottom
- | _, _ -> Int (Int_val.inject_interval ~min ~max ~rem ~modu)
+ | Some mn, Some mx when Int.gt mn mx -> bottom
+ | _, _ -> inject_int (Int_val.inject_interval ~min ~max ~rem ~modu)
let subdivide ~size = function
| Bottom -> raise Can_not_subdiv
@@ -212,12 +248,14 @@ let subdivide ~size = function
in
let f1, f2 = Fval.subdiv_float_interval fkind fval in
inject_float f1, inject_float f2
- | Int i -> let i1, i2 = Int_val.subdivide i in Int i1, Int i2
+ | Int i ->
+ let i1, i2 = Int_val.subdivide i in
+ inject_int i1, inject_int i2
let inject_range min max = inject_top min max Int.zero Int.one
-let top_float = Float Fval.top
-let top_single_precision_float = Float Fval.top
+let top_float = inject_float Fval.top
+let top_single_precision_float = inject_float Fval.top
let min_max_r_mod = function
@@ -276,14 +314,14 @@ let widen (bitsize,(wh,fh)) t1 t2 =
then Float_sig.Long_Double
else Float_sig.Single
in
- Float (Fval.widen fh prec f1 f2)
+ inject_float (Fval.widen fh prec f1 f2)
| Int i2 ->
let i1 = match t1 with
| Bottom -> assert false
| Int i1 -> i1
| Float _ -> Int_val.top
in
- Int (Int_val.widen (bitsize,wh) i1 i2)
+ inject_int (Int_val.widen (bitsize,wh) i1 i2)
let meet v1 v2 =
if v1 == v2 then v1 else
@@ -291,7 +329,7 @@ let meet v1 v2 =
match v1, v2 with
| Bottom, _ | _, Bottom -> bottom
| Int i1, Int i2 -> inject_int_or_bottom (Int_val.meet i1 i2)
- | Float(f1), Float(f2) -> begin
+ | Float f1, Float f2 -> begin
match Fval.meet f1 f2 with
| `Value f -> inject_float f
| `Bottom -> bottom
@@ -320,46 +358,41 @@ let intersects v1 v2 =
equal top other || (Fval.contains_plus_zero f && contains_zero other)
let narrow v1 v2 =
- match v1, v2 with
- | Bottom, _ | _, Bottom -> bottom
- | Float _, Float _ -> meet v1 v2 (* meet is exact *)
- | v, (Int _ as t) when equal t top -> v
- | (Int _ as t), v when equal t top -> v
- | Int i1, Int i2 -> inject_int_or_bottom (Int_val.narrow i1 i2)
- | Float f, (Int _ as s) | (Int _ as s), Float f when is_zero s -> begin
- match Fval.narrow f Fval.zeros with
- | `Value f -> inject_float f
- | `Bottom -> bottom
- end
- | Float _, Int _ | Int _, Float _ ->
- (* ill-typed case. It is better to keep the operation symmetric *)
- top
+ if v1 == v2 then v1 else
+ match v1, v2 with
+ | Bottom, _ | _, Bottom -> bottom
+ | Float _, Float _ -> meet v1 v2 (* meet is exact *)
+ | v, (Int _ as t) when equal t top -> v
+ | (Int _ as t), v when equal t top -> v
+ | Int i1, Int i2 -> inject_int_or_bottom (Int_val.narrow i1 i2)
+ | Float f, (Int _ as s) | (Int _ as s), Float f when is_zero s -> begin
+ match Fval.narrow f Fval.zeros with
+ | `Value f -> inject_float f
+ | `Bottom -> bottom
+ end
+ | Float _, Int _ | Int _, Float _ ->
+ (* ill-typed case. It is better to keep the operation symmetric *)
+ top
let link v1 v2 = match v1, v2 with
- | Int i1, Int i2 -> Int (Int_val.link i1 i2)
+ | Int i1, Int i2 -> inject_int (Int_val.link i1 i2)
| _ -> bottom
let join v1 v2 =
- let result =
- if v1 == v2 then v1 else
- match v1,v2 with
- | Bottom, t | t, Bottom -> t
- | Int i1, Int i2 -> Int (Int_val.join i1 i2)
- | Float(f1), Float(f2) ->
- inject_float (Fval.join f1 f2)
- | Float (f) as ff, other | other, (Float (f) as ff) ->
- if is_zero other
- then inject_float (Fval.join Fval.plus_zero f)
- else if is_bottom other then ff
- else top
- in
- (* Format.printf "mod_join %a %a -> %a@."
- pretty v1 pretty v2 pretty result; *)
- result
+ if v1 == v2 then v1 else
+ match v1, v2 with
+ | Bottom, t | t, Bottom -> t
+ | Int i1, Int i2 -> inject_int (Int_val.join i1 i2)
+ | Float f1, Float f2 -> inject_float (Fval.join f1 f2)
+ | Float f as ff, other | other, (Float f as ff) ->
+ if is_zero other
+ then inject_float (Fval.join Fval.plus_zero f)
+ else if is_bottom other then ff
+ else top
let complement_int_under ~size ~signed = function
| Bottom | Float _ -> `Bottom
- | Int i -> Int_val.complement_under ~size ~signed i >>-: fun i -> Int i
+ | Int i -> Int_val.complement_under ~size ~signed i >>-: inject_int
let fold_int f v acc =
match v with
@@ -393,13 +426,13 @@ let is_included t1 t2 =
let add_singleton_int i = function
| Bottom -> bottom
| Float _ -> assert false
- | Int itv -> Int (Int_val.add_singleton i itv)
+ | Int itv -> inject_int (Int_val.add_singleton i itv)
let add_int v1 v2 =
match v1, v2 with
| Bottom, _ | _, Bottom -> bottom
| Float _, _ | _, Float _ -> assert false
- | Int i1, Int i2 -> Int (Int_val.add i1 i2)
+ | Int i1, Int i2 -> inject_int (Int_val.add i1 i2)
let add_int_under v1 v2 =
match v1, v2 with
@@ -410,7 +443,7 @@ let add_int_under v1 v2 =
let neg_int = function
| Bottom -> bottom
| Float _ -> assert false
- | Int i -> Int (Int_val.neg i)
+ | Int i -> inject_int (Int_val.neg i)
let sub_int v1 v2 = add_int v1 (neg_int v2)
let sub_int_under v1 v2 = add_int_under v1 (neg_int v2)
@@ -434,11 +467,11 @@ let scale f v =
match v with
| Bottom -> bottom
| Float _ -> top
- | Int i -> Int (Int_val.scale f i)
+ | Int i -> inject_int (Int_val.scale f i)
let scale_div ~pos f = function
| Bottom -> bottom
- | Int i -> Int (Int_val.scale_div ~pos f i)
+ | Int i -> inject_int (Int_val.scale_div ~pos f i)
| Float _ -> top
let scale_div_under ~pos f = function
@@ -463,7 +496,7 @@ let scale_rem ~pos f v =
else
match v with
| Bottom -> bottom
- | Int i -> Int (Int_val.scale_rem ~pos f i)
+ | Int i -> inject_int (Int_val.scale_rem ~pos f i)
| Float _ -> top
let c_rem v1 v2 =
@@ -473,14 +506,14 @@ let c_rem v1 v2 =
| Int i1, Int i2 -> inject_int_or_bottom (Int_val.c_rem i1 i2)
let create_all_values ~signed ~size =
- Int (Int_val.create_all_values ~signed ~size)
+ inject_int (Int_val.create_all_values ~signed ~size)
let big_int_64 = Int.of_int 64
let big_int_32 = Int.thirtytwo
let cast_int_to_int ~size ~signed = function
| Bottom -> bottom
- | Int i -> Int (Int_val.cast_int_to_int ~size ~signed i)
+ | Int i -> inject_int (Int_val.cast_int_to_int ~size ~signed i)
| Float _ -> assert false
let reinterpret_float_as_int ~signed ~size f =
@@ -533,7 +566,7 @@ let mul v1 v2 =
match v1, v2 with
| Bottom, _ | _, Bottom -> bottom
| Float _, _ | _, Float _ -> top
- | Int i1, Int i2 -> Int (Int_val.mul i1 i2)
+ | Int i1, Int i2 -> inject_int (Int_val.mul i1 i2)
let shift_right v1 v2 =
match v1, v2 with
@@ -621,13 +654,13 @@ let backward_le_int max v =
match v with
| Bottom -> bottom
| Float _ -> v
- | Int _ -> narrow v (Int (Int_val.inject_range None max))
+ | Int _ -> narrow v (inject_int (Int_val.inject_range None max))
let backward_ge_int min v =
match v with
| Bottom -> bottom
| Float _ -> v
- | Int _ -> narrow v (Int (Int_val.inject_range min None))
+ | Int _ -> narrow v (inject_int (Int_val.inject_range min None))
let backward_lt_int max v = backward_le_int (Extlib.opt_map Int.pred max) v
let backward_gt_int min v = backward_ge_int (Extlib.opt_map Int.succ min) v
@@ -698,7 +731,7 @@ let backward_comp_float_left_false op fkind f1 f2 =
let rec extract_bits ~start ~stop ~size v =
match v with
| Bottom -> bottom
- | Int i -> Int (Int_val.extract_bits ~start ~stop i)
+ | Int i -> inject_int (Int_val.extract_bits ~start ~stop i)
| Float f ->
let inject (b, e) = inject_range (Some b) (Some e) in
let itvs =
@@ -760,8 +793,9 @@ let forward_comp_int op i1 i2 =
| Ne -> inv_truth (forward_eq_int i1 i2)
let rehash = function
- | Int i -> Int (Int_val.rehash i)
- | x -> x
+ | Bottom -> bottom
+ | Int i -> inject_int i
+ | Float f -> inject_float f
include (
Datatype.Make_with_collections
@@ -895,7 +929,7 @@ let cast_float_to_int_inverse ~single_precision i =
in
assert (Fval.F.is_finite (Fval.F.of_float minf));
assert (Fval.F.is_finite (Fval.F.of_float maxf));
- Float (Fval.inject fkind (Fval.F.of_float minf) (Fval.F.of_float maxf))
+ inject_float (Fval.inject fkind (Fval.F.of_float minf) (Fval.F.of_float maxf))
| _ -> if single_precision then top_single_precision_float else top_float
@@ -1019,7 +1053,7 @@ let overlaps ~partial ~size t1 t2 =
let bitwise_int f_int v1 v2 =
match v1, v2 with
- | Int i1, Int i2 -> Int (f_int i1 i2)
+ | Int i1, Int i2 -> inject_int (f_int i1 i2)
| _, _ -> top
let bitwise_or = bitwise_int Int_val.bitwise_or
@@ -1029,12 +1063,12 @@ let bitwise_xor = bitwise_int Int_val.bitwise_xor
let bitwise_signed_not = function
| Bottom -> bottom
| Float _ -> assert false
- | Int i -> Int (Int_val.bitwise_signed_not i)
+ | Int i -> inject_int (Int_val.bitwise_signed_not i)
let bitwise_unsigned_not ~size = function
| Bottom -> bottom
| Float _ -> assert false
- | Int i -> Int (Int_val.bitwise_unsigned_not ~size i)
+ | Int i -> inject_int (Int_val.bitwise_unsigned_not ~size i)
let bitwise_not ~size ~signed v =
if signed then
--
GitLab