Commit 698a4697 authored by David Bühler's avatar David Bühler

[Ival] Simplifies create_all_values and removes create_all_values_modu.

parent 3f793898
......@@ -766,47 +766,20 @@ let c_rem x y =
Int_set.fold f bottom yy
module AllValueHashtbl =
type t = Int.t * bool * int
let equal (a,b,c:t) (d,e,f:t) = b=e && c=f && Int.equal a d
let hash (a,b,c:t) =
257 * (Hashtbl.hash b) + 17 * (Hashtbl.hash c) + Int.hash a
let all_values_table = AllValueHashtbl.create 7
let create_all_values_modu ~modu ~signed ~size =
let t = modu, signed, size in
AllValueHashtbl.find all_values_table t
with Not_found ->
let mn, mx =
if signed then
let b = Int.two_power_of_int (size-1) in
(Int.round_up_to_r ~min:(Int.neg b) ~modu,
Int.round_down_to_r ~max:(Int.pred b) ~modu
let b = Int.two_power_of_int size in,
Int.round_down_to_r ~max:(Int.pred b) ~modu
let r = inject_top (Some mn) (Some mx) modu in
AllValueHashtbl.add all_values_table t r;
let create_all_values ~signed ~size =
if size <= !small_cardinal_log then
(* We may need to create a set. Use slow path *)
create_all_values_modu ~signed ~size
if signed then
let b = Int.two_power_of_int (size-1) in
Itv (Int_interval.inject_range (Some (Int.neg b)) (Some (Int.pred b)))
let b = Int.two_power_of_int size in
Itv (Int_interval.inject_range (Some (Some (Int.pred b)))
let min, max =
if signed then
let b = Int.two_power_of_int (size - 1) in
Int.neg b, Int.pred b
let b = Int.two_power_of_int size in, Int.pred b
let min = Some min
and max = Some max in
if size <= !small_cardinal_log
then make ~min ~max
else Itv (Int_interval.inject_range min max)
let big_int_64 = Int.of_int 64
let big_int_32 = Int.thirtytwo
......@@ -247,7 +247,6 @@ val interp_boolean : contains_zero:bool -> contains_non_zero:bool -> t
(** Extract bits from [start] to [stop] from the given Ival, [start]
and [stop] being included. [size] is the size of the entire ival. *)
val extract_bits: start:Integer.t -> stop:Integer.t -> size:Integer.t -> t -> t
val create_all_values_modu: modu:Integer.t -> signed:bool -> size:int -> t
val create_all_values: signed:bool -> size:int -> t
(** [all_values ~size v] returns true iff v contains all integer values
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