Commit 992926a5 authored by David Bühler's avatar David Bühler

[Ival] Moves the creation of integer sets in int_set.ml.

parent f36c3828
...@@ -59,7 +59,29 @@ let share_array a s = ...@@ -59,7 +59,29 @@ let share_array a s =
let share_array_or_bottom a s = let share_array_or_bottom a s =
if s = 0 then `Bottom else `Value (share_array a s) if s = 0 then `Bottom else `Value (share_array a s)
let inject_array = share_array let inject_periodic ~from ~period ~number =
let l = Int.to_int number in
let s = Array.make l Int.zero in
let v = ref from in
let i = ref 0 in
while (!i < l)
do
s.(!i) <- !v;
v := Int.add period !v;
incr i
done;
share_array s l
module O = FCSet.Make (Integer)
let inject_list list =
let o = List.fold_left (fun o r -> O.add r o) O.empty list in
let cardinal = O.cardinal o in
assert (cardinal > 0 && cardinal <= !small_cardinal);
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
let to_list = Array.to_list let to_list = Array.to_list
...@@ -180,8 +202,6 @@ let mem v a = ...@@ -180,8 +202,6 @@ let mem v a =
type set_or_top = [ `Set of t | `Top of Integer.t * Integer.t * Integer.t ] type set_or_top = [ `Set of t | `Top of Integer.t * Integer.t * Integer.t ]
type set_or_top_or_bottom = [ `Bottom | set_or_top ] type set_or_top_or_bottom = [ `Bottom | set_or_top ]
module O = FCSet.Make (Integer)
type pre_set = type pre_set =
| Pre_set of O.t * int | Pre_set of O.t * int
| Pre_top of Int.t * Int.t * Int.t | Pre_top of Int.t * Int.t * Int.t
......
...@@ -29,10 +29,9 @@ open Bottom.Type ...@@ -29,10 +29,9 @@ open Bottom.Type
include Datatype.S_with_collections include Datatype.S_with_collections
val rehash: t -> t
val inject_singleton: Integer.t -> t val inject_singleton: Integer.t -> t
val inject_array: Integer.t array -> int -> t val inject_periodic: from:Integer.t -> period:Integer.t -> number:Integer.t -> t
val inject_list: Integer.t list -> t
val to_list: t -> Integer.t list val to_list: t -> Integer.t list
...@@ -91,3 +90,5 @@ val get_small_cardinal: unit -> int ...@@ -91,3 +90,5 @@ val get_small_cardinal: unit -> int
(* This is used by the Value plugin. Do not use. *) (* This is used by the Value plugin. Do not use. *)
val set_small_cardinal: int -> unit val set_small_cardinal: int -> unit
val rehash: t -> t
...@@ -128,19 +128,7 @@ let make ~min ~max ~rem ~modu = ...@@ -128,19 +128,7 @@ let make ~min ~max ~rem ~modu =
else else
let l = Int.succ (Int.e_div (Int.sub mx mn) modu) in let l = Int.succ (Int.e_div (Int.sub mx mn) modu) in
if Int.le l (small_cardinal_Int ()) if Int.le l (small_cardinal_Int ())
then then Set (Int_set.inject_periodic ~from:mn ~period:modu ~number:l)
let l = Int.to_int l in
let s = Array.make l Int.zero in
let v = ref mn in
let i = ref 0 in
while (!i < l)
do
s.(!i) <- !v;
v := Int.add modu !v;
incr i
done;
assert (Int.equal !v (Int.add modu mx));
Set (Int_set.inject_array s l)
else Itv (Int_interval.make ~min ~max ~rem ~modu) else Itv (Int_interval.make ~min ~max ~rem ~modu)
| _ -> Itv (Int_interval.make ~min ~max ~rem ~modu) | _ -> Itv (Int_interval.make ~min ~max ~rem ~modu)
...@@ -158,7 +146,7 @@ let inject_interval ~min ~max ~rem:r ~modu = ...@@ -158,7 +146,7 @@ let inject_interval ~min ~max ~rem:r ~modu =
and max = fix_bound (fun max -> Int.round_down_to_r ~max ~r ~modu) max in and max = fix_bound (fun max -> Int.round_down_to_r ~max ~r ~modu) max in
make ~min ~max ~rem:r ~modu make ~min ~max ~rem:r ~modu
let inject_range min max = check_make ~min ~max ~rem:Int.zero ~modu:Int.one let inject_range min max = make ~min ~max ~rem:Int.zero ~modu:Int.one
let check_make_or_bottom ~min ~max ~rem ~modu = let check_make_or_bottom ~min ~max ~rem ~modu =
match min, max with match min, max with
...@@ -350,17 +338,11 @@ let diff_if_one value rem = ...@@ -350,17 +338,11 @@ let diff_if_one value rem =
| Some mn, Some mx when | Some mn, Some mx when
Int.equal (Int.sub mx mn) (Int.mul modu (small_cardinal_Int ())) Int.equal (Int.sub mx mn) (Int.mul modu (small_cardinal_Int ()))
&& Int_interval.mem v i -> && Int_interval.mem v i ->
let r = ref mn in (* We create a set with an element in excess, but we remove [v]
let small_cardinal = small_cardinal () in just after, so the resulting set is correct. *)
let array = let number = Int.succ (small_cardinal_Int ()) in
Array.init small_cardinal let set = Int_set.inject_periodic ~from:mn ~period:modu ~number in
(fun _ -> Int_set.remove set v >>-: inject_set
let c = !r in
let corrected_c = if Int.equal c v then Int.add c modu else c in
r := Int.add corrected_c modu;
corrected_c)
in
`Value (Set (Int_set.inject_array array small_cardinal))
| _, _ -> `Value value | _, _ -> `Value value
end end
| _ -> `Value value | _ -> `Value value
...@@ -610,11 +592,7 @@ let create_all_values ~signed ~size = ...@@ -610,11 +592,7 @@ let create_all_values ~signed ~size =
let b = Int.two_power_of_int size in let b = Int.two_power_of_int size in
Int.zero, Int.pred b Int.zero, Int.pred b
in in
let min = Some min inject_range (Some min) (Some max)
and max = Some max in
if size < Z.numbits (small_cardinal_Int ())
then make ~min ~max ~rem:Int.zero ~modu:Int.one
else Itv (Int_interval.inject_range min max)
let cast_int_to_int ~size ~signed value = let cast_int_to_int ~size ~signed value =
if equal top value if equal top value
...@@ -933,8 +911,6 @@ struct ...@@ -933,8 +911,6 @@ struct
then if Op.forward Both (extract_sign v2) = Both then n1 else n2 then if Op.forward Both (extract_sign v2) = Both then n1 else n2
else if Op.forward (extract_sign v1) Both = Both then n2 else n1 else if Op.forward (extract_sign v1) Both = Both then n2 else n1
module O = FCSet.Make(Integer)
exception Do_not_fit_small_sets exception Do_not_fit_small_sets
(* Try to build a small set. (* Try to build a small set.
...@@ -963,13 +939,8 @@ struct ...@@ -963,13 +939,8 @@ struct
acc := List.fold_left (set_bit (Bit i)) [] !acc; acc := List.fold_left (set_bit (Bit i)) [] !acc;
if List.length !acc > small_cardinal () then raise Do_not_fit_small_sets if List.length !acc > small_cardinal () then raise Do_not_fit_small_sets
done; done;
let o = List.fold_left (fun o (r,_,_) -> O.add r o) O.empty !acc in let list = List.map (fun (r, _, _) -> r) !acc in
let cardinal = O.cardinal o in Set (Int_set.inject_list list)
assert (cardinal > 0);
let a = Array.make cardinal Int.zero in
let i = ref 0 in
O.iter (fun e -> a.(!i) <- e; incr i) o;
Set (Int_set.inject_array a cardinal)
(* If lower is true (resp. false), compute the lower (resp. upper) bound of (* If lower is true (resp. false), compute the lower (resp. upper) bound of
the result interval when applying the bitwise operator to [v1] and [v2]. the result interval when applying the bitwise operator to [v1] and [v2].
......
...@@ -22,18 +22,16 @@ ...@@ -22,18 +22,16 @@
open Bottom.Type open Bottom.Type
type t include Datatype.S_with_collections
module Widen_Hints = Datatype.Integer.Set module Widen_Hints = Datatype.Integer.Set
type size_widen_hint = Integer.t type size_widen_hint = Integer.t
type generic_widen_hint = Widen_Hints.t type generic_widen_hint = Widen_Hints.t
include Datatype.S_with_collections with type t := t
include Eva_lattice_type.Full_AI_Lattice_with_cardinality include Eva_lattice_type.Full_AI_Lattice_with_cardinality
with type t := t with type t := t
and type widen_hint = size_widen_hint * generic_widen_hint and type widen_hint = size_widen_hint * generic_widen_hint
val zero : t val zero : t
val one : t val one : t
val minus_one : t val minus_one : t
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment