Commit b9c9f717 authored by David Bühler's avatar David Bühler

[Ival] Comments int_set and int_interval.

parent ff844c36
......@@ -412,8 +412,8 @@ let cardinal_zero_or_one t =
| Some min, Some max -> Integer.equal min max
(* TODO? *)
let diff _ _ = assert false
let diff_if_one _ _ = assert false
let diff v _ = `Value v
let diff_if_one v _ = `Value v
let fold_int f t acc =
match t.min, t.max with
......
......@@ -20,6 +20,12 @@
(* *)
(**************************************************************************)
(** Integer intervals with congruence.
An interval defined by [min, max, rem, modu] represents all integers
between the bounds [min] and [max] and congruent to [rem] modulo [modu].
A value of [None] for [min] (resp. [max]) represents -infinity
(resp. +infinity). [modu] is > 0, and [0 <= rem < modu]. *)
open Bottom.Type
include Datatype.S_with_collections
......@@ -28,31 +34,40 @@ include Eva_lattice_type.Full_AI_Lattice_with_cardinality
with type t := t
and type widen_hint = Integer.t * Datatype.Integer.Set.t
(** Makes the interval of all integers between [min] and [max] and congruent
to [rem] modulo [modu]. Fails if these conditions does not hold:
- min ≤ max
- 0 ≤ rem < modu
- min ≅ rem [modu] ∧ max ≅ rem [modu] *)
val make:
min:Integer.t option -> max:Integer.t option ->
rem:Integer.t -> modu:Integer.t -> t
(** Makes the interval of all integers between [min] and [max]. *)
val inject_range: Integer.t option -> Integer.t option -> t
(** Returns the bounds of the given interval. [None] means infinity. *)
val min_and_max: t -> Integer.t option * Integer.t option
(** Returns the bounds and the modulo of the given interval. *)
val min_max_rem_modu:
t -> Integer.t option * Integer.t option * Integer.t * Integer.t
(** [mem i t] returns true iff the integer [i] is in the interval [t]. *)
val mem: Integer.t -> t -> bool
(** Returns the number of integers represented by the given interval.
Returns [None] if the interval represents an infinite number of integers. *)
val cardinal: t -> Integer.t option
val add : t -> t -> t
(** Addition of two integer (ie. not [Float]) ivals. *)
val add_under : t -> t -> t or_bottom
(** Underapproximation of the same operation *)
val add_singleton_int: Integer.t -> t -> t
(** Addition of an integer ival with an integer. Exact operation. *)
(** {2 Interval semantics.} *)
val neg : t -> t
(** Negation of an integer ival. Exact operation. *)
(** See {!Int_val} for more details. *)
val add_singleton_int: Integer.t -> t -> t
val add: t -> t -> t
val add_under: t -> t -> t or_bottom
val neg: t -> t
val scale: Integer.t -> t -> t
val scale_div: pos:bool -> Integer.t -> t -> t
......@@ -65,6 +80,8 @@ val c_rem: t -> t -> t or_bottom
val cast: size:Integer.t -> signed:bool -> t -> t
(** {2 Misc.} *)
val subdivide: t -> t * t
val reduce_sign: t -> bool -> t or_bottom
......
......@@ -61,6 +61,7 @@ let share_array_or_bottom a s =
let inject_periodic ~from ~period ~number =
let l = Int.to_int number in
assert (l > 0);
let s = Array.make l Int.zero in
let v = ref from in
let i = ref 0 in
......@@ -208,7 +209,6 @@ type pre_set =
let empty_ps = Pre_set (O.empty, 0)
(* TODO: share this code with ival2.make_itv_from_set? *)
let make_top_from_set s =
if debug_cardinal then assert (O.cardinal s >= 2);
let min = O.min_elt s in
......@@ -651,3 +651,5 @@ let subdivide s =
let min t = t.(0)
let max t = t.(Array.length t - 1)
let mem i t = mem i t >= 0
......@@ -27,27 +27,50 @@
open Bottom.Type
(** Returns the limit above which integer sets are converted into intervals. *)
val get_small_cardinal: unit -> int
(** Sets the limit above which integer sets are converted into intervals.
This is used by the Eva plugin according to the -eva-ilevel option.
Do not use. *)
val set_small_cardinal: int -> unit
include Datatype.S_with_collections
(** Creates the set containing only the given integer. *)
val inject_singleton: Integer.t -> t
(** Creates the set with integers [from + k*period] for [k] in {0 ... number-1}.
The resulting set contains [number] integers. There is no verification
about [number], but it should be stritly positive. *)
val inject_periodic: from:Integer.t -> period:Integer.t -> number:Integer.t -> t
(** Creates a set from an integer list. The list must not be empty, and the list
length must not exceed the small cardinal limit. *)
val inject_list: Integer.t list -> t
(** Returns the set as an integer list. *)
val to_list: t -> Integer.t list
(** Removes an integer from a set.
Returns Bottom if the resulting set is empty. *)
val remove: t -> Integer.t -> t or_bottom
(** [mem i s] is true iff the set [s] contains the integer [i]. *)
val mem: Integer.t -> t -> bool
val one: t
val zero: t
val minus_one: t
val zero_or_one: t
val min: t -> Integer.t
val max: t -> Integer.t
val min: t -> Integer.t (** Returns the smallest integer of a set. *)
val max: t -> Integer.t (** Returns the highest integer of a set. *)
(** Returns the number of integers in a set. *)
val cardinal: t -> int
val mem: Integer.t -> t -> int
(** {2 Iterators on the integers of a set.} *)
val for_all: (Integer.t -> bool) -> t -> bool
val exists: (Integer.t -> bool) -> t -> bool
......@@ -57,9 +80,20 @@ val map: (Integer.t -> Integer.t) -> t -> t
val filter: (Integer.t -> bool) -> t -> t or_bottom
val map_reduce: (Integer.t -> 'a) -> ('a -> 'a -> 'a) -> t -> 'a
type set_or_top = [ `Set of t | `Top of Integer.t * Integer.t * Integer.t ]
(** Sets whose cardinal exceeds a certain limit must be converted into
intervals. Functions that make sets grow returns either a set small enough,
or the information needed to construct the corresponding interval: the
smallest and highest elements, and the periodicity of the integers of
the set. *)
type set_or_top =
[ `Set of t (** Small set. *)
| `Top of Integer.t * Integer.t * Integer.t (** Interval: min, max, modu *)
]
type set_or_top_or_bottom = [ `Bottom | set_or_top ]
(** {2 Lattice structure.} *)
val is_included: t -> t -> bool
val join: t -> t -> set_or_top
val link: t -> t -> set_or_top
......@@ -68,6 +102,10 @@ val narrow: t -> t -> t or_bottom
val intersects: t -> t -> bool
val diff_if_one: t -> t -> t or_bottom
(** {2 Semantics.} *)
(** See {!Int_val} for more details. *)
val add_singleton: Integer.t -> t -> t
val add: t -> t -> set_or_top
val add_under: t -> t -> set_or_top
......@@ -82,13 +120,8 @@ val scale_rem: pos:bool -> Integer.t -> t -> t
val bitwise_signed_not: t -> t
val subdivide: t -> t * t
(**/**)
(** {2 Misc} *)
val get_small_cardinal: unit -> int
(* This is used by the Value plugin. Do not use. *)
val set_small_cardinal: int -> unit
val subdivide: t -> t * t
val rehash: t -> t
......@@ -231,7 +231,7 @@ let is_one = equal one
let contains_zero = function
| Itv i -> Int_interval.mem Int.zero i
| Set s -> Int_set.mem Int.zero s >= 0
| Set s -> Int_set.mem Int.zero s
let contains_non_zero = function
| Itv _ -> true (* at least two 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