Commit 957a6506 authored by David Bühler's avatar David Bühler

[Ival] Uses int_set.

parent 5b7b1b82
......@@ -65,7 +65,7 @@ let share_array_or_bottom a s =
let inject_array = share_array
let project_array t = t
let to_list = Array.to_list
(* ------------------------------- Datatype --------------------------------- *)
......
......@@ -31,7 +31,7 @@ val bottom: t
val inject_singleton: Integer.t -> t
val inject_array: Integer.t array -> int -> t
val project_array: t -> Integer.t array
val to_list: t -> Integer.t list
val remove: t -> Integer.t -> t or_bottom
......
......@@ -27,8 +27,6 @@ let small_cardinal = ref 8
let small_cardinal_Int = ref (Int.of_int !small_cardinal)
let small_cardinal_log = ref 3
let debug_cardinal = false
let set_small_cardinal i =
assert (2 <= i && i <= 1024);
let rec log j p =
......@@ -37,7 +35,9 @@ let set_small_cardinal i =
in
small_cardinal := i;
small_cardinal_Int := Int.of_int i;
small_cardinal_log := log 1 2
small_cardinal_log := log 1 2;
(* TODO: share this code with Int_set *)
Int_set.set_small_cardinal i
let get_small_cardinal () = !small_cardinal
......@@ -78,12 +78,8 @@ let opt1 f m =
module O = FCSet.Make(Integer)
type pre_set =
Pre_set of O.t * int
| Pre_top of Int.t * Int.t * Int.t
type t =
| Set of Int.t array
| Set of Int_set.t
| Float of Fval.t
| Itv of Int_interval.t
(* Binary abstract operations do not model precisely float/integer operations.
......@@ -97,35 +93,19 @@ 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 = Set (Array.make 0 Int.zero)
let bottom = Set Int_set.bottom
let top = Itv Int_interval.top
let hash v =
match v with
Set s -> Array.fold_left (fun acc v -> 1031 * acc + (Int.hash v)) 17 s
let hash = function
| Set s -> Int_set.hash s
| Itv i -> Int_interval.hash i
| Float(f) ->
3 + 17 * Fval.hash f
exception Unequal of int
3 + 17 * Fval.hash f
let compare e1 e2 =
if e1==e2 then 0 else
match e1,e2 with
| Set e1,Set e2 ->
let l1 = Array.length e1 in
let l2 = Array.length e2 in
if l1 <> l2
then l1 - l2 (* no overflow here *)
else
(try
for i=0 to l1 -1 do
let r = Int.compare e1.(i) e2.(i) in
if r <> 0 then raise (Unequal r)
done;
0
with Unequal v -> v )
| Set s1, Set s2 -> Int_set.compare s1 s2
| _, Set _ -> 1
| Set _, _ -> -1
| Itv i1, Itv i2 -> Int_interval.compare i1 i2
......@@ -143,15 +123,7 @@ let pretty fmt t =
| Itv i -> Int_interval.pretty fmt i
| Float (f) ->
Fval.pretty fmt f
| Set s ->
if Array.length s = 0 then Format.fprintf fmt "BottomMod"
else begin
Pretty_utils.pp_iter
~pre:"@[<hov 1>{"
~suf:"}@]"
~sep:";@ "
Array.iter Int.pretty fmt s
end
| Set s -> Int_set.pretty fmt s
let min_le_elt min elt =
match min with
......@@ -190,26 +162,20 @@ let check min max r modu =
let cardinal_zero_or_one v =
match v with
| Itv _ -> false
| Set s -> Array.length s <= 1
| Set s -> Int_set.cardinal s <= 1
| Float f -> Fval.is_singleton f
let is_singleton_int v = match v with
| Float _ | Itv _ -> false
| Set s -> Array.length s = 1
let is_bottom x = x == bottom
| Set s -> Int_set.cardinal s = 1
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
(* TODO *)
let is_bottom x = equal x bottom
let small_nums =
Array.init 33 (fun i -> Set [| (Integer.of_int i) |])
let zero = small_nums.(0)
let one = small_nums.(1)
let minus_one = Set [| Int.minus_one |]
let zero_or_one = Set [| Int.zero ; Int.one |]
let zero = Set Int_set.zero
let one = Set Int_set.one
let minus_one = Set Int_set.minus_one
let zero_or_one = Set Int_set.zero_or_one
let float_zeros = Float Fval.zeros
let positive_integers = Itv (Int_interval.inject_range (Some Int.zero) None)
......@@ -217,36 +183,7 @@ let negative_integers = Itv (Int_interval.inject_range None (Some Int.zero))
let is_zero x = x == zero
let inject_singleton e =
if Int.le Int.zero e && Int.le e Int.thirtytwo
then small_nums.(Int.to_int e)
else Set [| e |]
let share_set o s =
if s = 0 then bottom
else 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);
Set a
let share_array a s =
if s = 0 then bottom
else
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 Set a
let inject_singleton e = Set (Int_set.inject_singleton e)
let inject_float f =
if Fval.(equal plus_zero f)
......@@ -282,24 +219,10 @@ let is_int = function
| Itv _ | Set _ -> true
| Float _ -> false
let array_mem v a =
let l = Array.length a in
let rec c i =
if i = l then (-1)
else
let ae = a.(i) in
if Int.equal ae v
then i
else if Int.gt ae v
then (-1)
else c (succ i)
in
c 0
let contains_zero s =
match s with
| Itv i -> Int_interval.mem Int.zero i
| Set s -> (array_mem Int.zero s)>=0
| Set s -> Int_set.mem Int.zero s >= 0
| Float f -> Fval.contains_a_zero f
let contains_non_zero s =
......@@ -312,7 +235,8 @@ let contains_non_zero s =
exception Not_Singleton_Int
let project_int v = match v with
| Set [| e |] -> e
| Set s ->
if Int_set.cardinal s = 1 then Int_set.min s else raise Not_Singleton_Int
| _ -> raise Not_Singleton_Int
let is_small_set = function
......@@ -320,18 +244,18 @@ let is_small_set = function
| _ -> false
let project_small_set = function
| Set a -> Some (Array.to_list a)
| Set a -> Some (Int_set.to_list a)
| _ -> None
let cardinal v =
match v with
| Itv i -> Int_interval.cardinal i
| Set s -> Some (Int.of_int (Array.length s))
| Set s -> Some (Int.of_int (Int_set.cardinal s))
| Float f -> if Fval.is_singleton f then Some Int.one else None
let cardinal_estimate v ~size =
match v with
| Set s -> Int.of_int (Array.length s)
| Set s -> Int.of_int (Int_set.cardinal s)
| Itv i -> Extlib.opt_conv (Int.two_power size) (Int_interval.cardinal i)
| Float f ->
if Fval.is_singleton f
......@@ -352,7 +276,7 @@ let cardinal_less_than v n =
let c =
match v with
| Itv i -> Extlib.the ~exn:Not_less_than (Int_interval.cardinal i)
| Set s -> Int.of_int (Array.length s)
| Set s -> Int.of_int (Int_set.cardinal s)
| Float f ->
if Fval.is_singleton f then Int.one else raise Not_less_than
in
......@@ -383,7 +307,7 @@ let make ~min ~max ~rem ~modu =
incr i
done;
assert (Int.equal !v (Int.add modu mx));
share_array s l
Set (Int_set.inject_array s l)
else Itv (Int_interval.make ~min ~max ~rem ~modu)
else if Int.equal mx mn
then inject_singleton mn
......@@ -405,6 +329,10 @@ let inject_interval ~min ~max ~rem:r ~modu =
make ~min ~max ~rem:r ~modu
let inject_set_or_bottom = function
| `Bottom -> bottom
| `Value s -> Set s
let inject_itv_or_bottom = function
| `Bottom -> bottom
| `Value i ->
......@@ -421,16 +349,7 @@ let inject_itv_or_bottom = function
let subdiv_int v =
match v with
| Float _ -> raise Can_not_subdiv
| Set arr ->
let len = Array.length arr in
assert (len > 0 );
if len <= 1 then raise Can_not_subdiv;
let m = len lsr 1 in
let lenhi = len - m in
let lo = Array.sub arr 0 m in
let hi = Array.sub arr m lenhi in
share_array lo m,
share_array hi lenhi
| Set s -> let s1, s2 = Int_set.subdivide s in Set s1, Set s2
| Itv i ->
let i1, i2 = Int_interval.subdivide i in
(* Redo make in case an interval should be converted into a set. *)
......@@ -459,43 +378,24 @@ 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 unsafe_make_top_from_set_4 s =
if debug_cardinal then assert (O.cardinal s >= 2);
let m = O.min_elt s in
let modu = O.fold
(fun x acc ->
if Int.equal x m
then acc
else Int.pgcd (Int.sub x m) acc)
s
Int.zero
in
let r = Int.e_rem m modu in
let max = O.max_elt s in
let min = m in
(min,max,r,modu)
let unsafe_make_top_from_array_4 s =
let l = Array.length s in
assert (l >= 2);
let m = s.(0) in
let modu =
Array.fold_left
let make_top_from_set s =
let min = Int_set.min s in
let modu =
Int_set.fold
(fun acc x ->
if Int.equal x m
then acc
else Int.pgcd (Int.sub x m) acc)
if Int.equal x min
then acc
else Int.pgcd (Int.sub x min) acc)
Int.zero
s
in
let r = Int.e_rem m modu in
let max = Some s.(pred l) in
let min = Some m in
check min max r modu;
(min,max,r,modu)
let rem = Int.e_rem min modu in
let max = Some (Int_set.max s) in
let min = Some min in
min, max, rem, modu
let make_itv_from_set s =
let min, max, rem, modu = unsafe_make_top_from_array_4 s in
let min, max, rem, modu = make_top_from_set s in
Int_interval.make ~min ~max ~rem ~modu
let make_itv = function
......@@ -505,63 +405,34 @@ let make_itv = function
let make_range = function
| Itv i -> i
| Set s -> Int_interval.inject_range (Some s.(0)) (Some s.(Array.length s - 1))
| Set s ->
let min, max = Int_set.min s, Int_set.max s in
Int_interval.inject_range (Some min) (Some max)
| Float _ -> Int_interval.top
let empty_ps = Pre_set (O.empty, 0)
let add_ps ps x =
match ps with
| Pre_set(o,s) ->
if debug_cardinal then assert (O.cardinal o = s);
if (O.mem x o) (* TODO: improve *)
then ps
else
let no = O.add x o in
if s < !small_cardinal
then begin
if debug_cardinal then assert (O.cardinal no = succ s);
Pre_set (no, succ s)
end
else
let min, max, _r, modu = unsafe_make_top_from_set_4 no in
Pre_top (min, max, modu)
| Pre_top (min, max, modu) ->
let new_modu =
if Int.equal x min
then modu
else Int.pgcd (Int.sub x min) modu
in
let new_min = Int.min min x
in
let new_max = Int.max max x
in
Pre_top (new_min, new_max, new_modu)
let inject_pre_itv ~min ~max ~modu =
let rem = Int.e_rem min modu in
Itv (Int_interval.make ~min:(Some min) ~max:(Some max) ~rem ~modu)
let inject_ps ps =
match ps with
Pre_set(o, s) -> share_set o s
| Pre_top (min, max, modu) ->
let min = Some min
and max = Some max
and rem = Int.e_rem min modu in
Itv (Int_interval.make ~min ~max ~rem ~modu)
let inject_set_or_top = function
| `Set s -> Set s
| `Top (min, max, modu) -> inject_pre_itv ~min ~max ~modu
let min_max_r_mod t =
match t with
| Set s ->
assert (Array.length s >= 2);
unsafe_make_top_from_array_4 s
| Itv i-> Int_interval.min_max_rem_modu i
assert (Int_set.cardinal s >= 2);
make_top_from_set s
| Itv i -> Int_interval.min_max_rem_modu i
| Float _ -> None, None, Int.zero, Int.one
let min_and_max t =
match t with
| Set s ->
let l = Array.length s in
let l = Int_set.cardinal s in
if l = 0
then raise Error_Bottom
else Some s.(0), Some s.(pred l)
else Some (Int_set.min s), Some (Int_set.max s)
| Itv i -> Int_interval.min_and_max i
| Float _ -> None, None
......@@ -616,104 +487,15 @@ let widen (bitsize,(wh,fh)) t1 t2 =
and i2 = make_itv t2 in
inject_itv_or_bottom (`Value (Int_interval.widen (bitsize, wh) i1 i2))
let array_truncate r i =
if i = 0
then bottom
else if i = 1
then inject_singleton r.(0)
else begin
(Obj.truncate (Obj.repr r) i);
assert (Array.length r = i);
Set r
end
let array_filter (f : Int.t -> bool) (a : Int.t array) : t =
let l = Array.length a in
let r = Array.make l Int.zero in
let j = ref 0 in
for i = 0 to l - 1 do
let x = a.(i) in
if f x then begin
r.(!j) <- x;
incr j;
end
done;
array_truncate r !j
let array_map_reduce (f : 'a -> 'b) (g : 'b -> 'b -> 'b) (set : 'a array) : 'b =
if Array.length set <= 0 then
raise Error_Bottom
else
let acc = ref (f set.(0)) in
for i = 1 to Array.length set - 1 do
acc := g !acc (f set.(i))
done;
!acc
let array_inter a1 a2 =
let l1 = Array.length a1 in
let l2 = Array.length a2 in
let lr_max = min l1 l2 in
let r = Array.make lr_max Int.zero in
let rec c i i1 i2 =
if i1 = l1 || i2 = l2
then array_truncate r i
else
let e1 = a1.(i1) in
let e2 = a2.(i2) in
if Int.equal e1 e2
then begin
r.(i) <- e1;
c (succ i) (succ i1) (succ i2)
end
else if Int.lt e1 e2
then c i (succ i1) i2
else c i i1 (succ i2)
in
c 0 0 0
(* Do the two arrays have an integer in common *)
let arrays_intersect a1 a2 =
let l1 = Array.length a1 in
let l2 = Array.length a2 in
let rec aux i1 i2 =
if i1 = l1 || i2 = l2 then false
else
let e1 = a1.(i1) in
let e2 = a2.(i2) in
if Int.equal e1 e2 then true
else if Int.lt e1 e2 then aux (succ i1) i2
else aux i1 (succ i2)
in
aux 0 0
let meet v1 v2 =
if v1 == v2 then v1 else
let result =
match v1,v2 with
| Itv i1, Itv i2 -> inject_itv_or_bottom (Int_interval.meet i1 i2)
| Set s1 , Set s2 -> array_inter s1 s2
| Set s1 , Set s2 -> inject_set_or_bottom (Int_set.meet s1 s2)
| Set s, Itv itv
| Itv itv, Set s ->
let l = Array.length s in
let r = Array.make l Int.zero in
let rec c i j =
if i = l
then
array_truncate r j
else
let si = succ i in
let x = s.(i) in
if Int_interval.mem x itv
then begin
r.(j) <- x;
c si (succ j)
end
else
c si j
in
c 0 0
inject_set_or_bottom (Int_set.filter (fun i -> Int_interval.mem i itv) s)
| Float(f1), Float(f2) -> begin
match Fval.meet f1 f2 with
| `Value f -> inject_float f
......@@ -733,9 +515,9 @@ let intersects v1 v2 =
v1 == v2 ||
match v1, v2 with
| Itv _, Itv _ -> not (is_bottom (meet v1 v2)) (* YYY: slightly inefficient *)
| Set s1 , Set s2 -> arrays_intersect s1 s2
| Set s1 , Set s2 -> Int_set.intersects s1 s2
| Set s, Itv itv | Itv itv, Set s ->
Extlib.array_exists (fun x -> Int_interval.mem x itv) s
Int_set.exists (fun i -> Int_interval.mem i itv) s
| Float f1, Float f2 -> begin
match Fval.forward_comp Comp.Eq f1 f2 with
| Comp.False -> false
......@@ -746,7 +528,7 @@ let intersects v1 v2 =
let narrow v1 v2 =
match v1, v2 with
| _, Set [||] | Set [||], _ -> bottom
| Set s1, Set s2 -> inject_set_or_bottom (Int_set.narrow s1 s2)
| Float _, Float _ | (Itv _| Set _), (Itv _ | Set _) ->
meet v1 v2 (* meet is exact *)
| v, (Itv _ as t) when equal t top -> v
......@@ -760,70 +542,21 @@ let narrow v1 v2 =
(* ill-typed case. It is better to keep the operation symmetric *)
top
(* Given a set of elements that is an under-approximation, returns an
ival (while maintaining the ival invariants that the "Set"
constructor is used only for small sets of elements. *)
let set_to_ival_under set =
let card = Int.Set.cardinal set in
if card <= !small_cardinal
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);
share_array a card)
else
(* If by chance the set is contiguous. *)
if (Int.equal
(Int.sub (Int.Set.max_elt set) (Int.Set.min_elt set))
(Int.of_int (card - 1)))
then Itv( Int_interval.make
~min:(Some(Int.Set.min_elt set))
~max:(Some(Int.Set.max_elt set))
~rem:Int.one
~modu:Int.zero)
(* Else: arbitrarily drop some elements of the under approximation. *)
else
let a = Array.make !small_cardinal Int.zero in
log_imprecision "Ival.set_to_ival_under";
try
ignore(Int.Set.fold (fun elt i ->
if i = !small_cardinal then raise Exit;
Array.set a i elt;
i + 1) set 0);
assert false
with Exit -> Set a
;;
let link v1 v2 = match v1, v2 with
| Set a1, Set a2 ->
let s1 = Array.fold_right Int.Set.add a1 Int.Set.empty in
let s2 = Array.fold_right Int.Set.add a2 s1 in
set_to_ival_under s2
| Set s1, Set s2 -> inject_set_or_top (Int_set.link s1 s2)
| Itv i1, Itv i2 -> Itv (Int_interval.link i1 i2)
| Itv i, Set s | Set s, Itv i ->
let mn, mx, r, m = Int_interval.min_max_rem_modu i in
let max = match mx with
| None -> None
| Some