Commit 2621f349 authored by David Bühler's avatar David Bühler

[Ival] Optimization: shares small singleton integers and top in memory.

parent d2defab5
......@@ -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
......
......@@ -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 ---------------------------------- *)
......
......@@ -130,5 +130,3 @@ val bitwise_signed_not: t -> t
(** {2 Misc} *)
val subdivide: t -> t * t
val rehash: t -> t
......@@ -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
......
......@@ -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
......@@ -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 =