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

[Ival] Comments int_val signature.

parent b9c9f717
......@@ -155,8 +155,9 @@ let check_make_or_bottom ~min ~max ~rem ~modu =
(* ------------------------- Sets and Intervals ---------------------------- *)
(* TODO: comments *)
(* If an interval represents less than [small_cardinal_Int] integers, then
converts the interval into a set. Used for the return of Int_interval
functions that may reduce intervals.*)
let inject_itv i =
match Int_interval.cardinal i with
| None -> Itv i
......@@ -169,6 +170,10 @@ let inject_itv i =
let inject_set s = Set s
(* Int_set functions that enlarge sets returns either a small integer set,
or an interval as `Top (min, max, modu). The following functions inject
these results as proper integer abstractions of type t.*)
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)
......@@ -182,8 +187,7 @@ let inject_set_or_top_or_bottom = function
| `Set s -> `Value (Set s)
| `Top (min, max, modu) -> `Value (inject_pre_itv ~min ~max ~modu)
(* TODO: more comment *)
(* Computes [min], [max], [rem] and [modu] from an integer set. *)
let make_top_from_set s =
let min = Int_set.min s in
let modu =
......@@ -200,6 +204,8 @@ let make_top_from_set s =
let min = Some min in
min, max, rem, modu
(* Converts an integer set into an interval, regardless of the set cardinal.
Useful for functions not implemented (or irrelevant) in Int_set. *)
let make_itv_from_set s =
let min, max, rem, modu = make_top_from_set s in
Int_interval.make ~min ~max ~rem ~modu
......@@ -274,11 +280,11 @@ let min_max_rem_modu = function
make_top_from_set s
| Itv i -> Int_interval.min_max_rem_modu i
exception Not_Singleton_Int
exception Not_Singleton
let project_int = function
| Set s ->
if Int_set.cardinal s = 1 then Int_set.min s else raise Not_Singleton_Int
| Itv _ -> raise Not_Singleton_Int
if Int_set.cardinal s = 1 then Int_set.min s else raise Not_Singleton
| Itv _ -> raise Not_Singleton
let is_small_set = function
| Set _ -> true
......@@ -475,9 +481,6 @@ let neg = function
| Set s -> Set (Int_set.neg s)
| Itv i -> Itv (Int_interval.neg i)
let sub v1 v2 = add v1 (neg v2)
let sub_under v1 v2 = add_under v1 (neg v2)
let scale f v =
if Int.is_zero f
......@@ -653,7 +656,7 @@ let extract_bits ~start ~stop = function
top
let overlaps ~partial ~size t1 t2 =
let diff = sub t1 t2 in
let diff = add t1 (neg t2) in
match diff with
| Set array ->
not (Int_set.for_all
......
......@@ -20,6 +20,12 @@
(* *)
(**************************************************************************)
(** Integer values abstractions: an abstraction represents a set of integers.
Provided with a lattice structure and over-approximations of arithmetic
operations. *)
(** Abstractions do not represent the empty set. Instead, operations creating
empty sets return `Bottom. *)
open Bottom.Type
include Datatype.S_with_collections
......@@ -32,86 +38,144 @@ include Eva_lattice_type.Full_AI_Lattice_with_cardinality
with type t := t
and type widen_hint = size_widen_hint * generic_widen_hint
val zero : t
val one : t
val minus_one : t
val zero_or_one : t
val zero: t
val one: t
val minus_one: t
val zero_or_one: t
val positive_integers: t (** All positive integers, including 0. *)
val negative_integers: t (** All negative integers, including 0. *)
(** {2 Building.} *)
val positive_integers : t
val negative_integers : t
(** Returns an exact abstraction of the given integer. *)
val inject_singleton: Integer.t -> t
val inject_singleton : Integer.t -> t
val inject_range : Integer.t option -> Integer.t option -> t
(** [inject_range min max] returns an abstraction of all integers between
[min] and [max] included. [None] means that the abstraction is unbounded. *)
val inject_range: Integer.t option -> Integer.t option -> t
(** Builds an abstraction of all integers between [min] and [max] included and
congruent to [rem] modulo [modu]. For [min] and [max], [None] is the
corresponding infinity. Checks that [min] <= [max], [modu] > 0 and
0 <= [rest] < [modu], and fails otherwise. If possible, reduces [min] and
[max] according to the modulo. *)
val inject_interval:
min: Integer.t option -> max: Integer.t option ->
rem: Integer.t -> modu: Integer.t ->
t
(** As [inject_interval], but also checks that [min] and [max] are congruent to
[rem] modulo [modu]. *)
val make:
min: Integer.t option -> max: Integer.t option ->
rem: Integer.t -> modu: Integer.t ->
t
val create_all_values: signed:bool -> size:int -> t
(** {2 Accessors.} *)
(** Returns the smallest integer represented by an abstraction.
Returns None if it does not exist, i.e. if the abstraction is unbounded. *)
val min_int: t -> Integer.t option
(** Returns the highest integer represented by an abstraction.
Returns None if it does not exist, i.e. if the abstraction is unbouded. *)
val max_int: t -> Integer.t option
(** Returns the smallest and highest integers represented by an abstraction. *)
val min_and_max: t -> Integer.t option * Integer.t option
val min_int : t -> Integer.t option
val max_int : t -> Integer.t option
val min_max_rem_modu :
(** Returns [min, max, rem, modu] such that for all integers [i] represented by
the given abstraction, [i] satisfies min ≤ i ≤ max and i ≅ rem [modu].
The abstraction must not be a singleton. *)
val min_max_rem_modu:
t -> Integer.t option * Integer.t option * Integer.t * Integer.t
val min_and_max :
t -> Integer.t option * Integer.t option
exception Not_Singleton_Int
val project_int : t -> Integer.t
exception Not_Singleton
(** Projects a singleton abstraction into an integer.
@raise Not_Singleton if the cardinal of the argument is not 1. *)
val project_int: t -> Integer.t
(** Is an abstraction internally represented as a small integer set? *)
val is_small_set: t -> bool
val project_small_set: t -> Integer.t list option
(** {2 Cardinality.} *)
val is_singleton: t -> bool
val cardinal_zero_or_one : t -> bool
val cardinal_zero_or_one: t -> bool
val cardinal: t -> Integer.t option
val cardinal_estimate: size:Integer.t -> t -> Integer.t
val cardinal_less_than : t -> int -> int
val cardinal_less_than: t -> int -> int
val cardinal_is_less_than: t -> int -> bool
val is_zero: t -> bool
val contains_zero : t -> bool
val contains_non_zero : t -> bool
val add : t -> t -> t
val add_under : t -> t -> t or_bottom
val add_singleton: Integer.t -> t -> t
val neg : t -> t
val sub : t -> t -> t
val sub_under: t -> t -> t or_bottom
val contains_zero: t -> bool
val contains_non_zero: t -> bool
val scale : Integer.t -> t -> t
val scale_div : pos:bool -> Integer.t -> t -> t
val scale_div_under : pos:bool -> Integer.t -> t -> t or_bottom
val scale_rem : pos:bool -> Integer.t -> t -> t
(** {2 Arithmetics.} *)
val mul : t -> t -> t
val div : t -> t -> t or_bottom
val c_rem : t -> t -> t or_bottom
val add: t -> t -> t
(** Addition of two integer abstractions. *)
val add_under: t -> t -> t or_bottom
(** Under-approximation of the addition of two integer abstractions *)
val add_singleton: Integer.t -> t -> t
(** Addition of an integer abstraction with a singleton integer.
Exact operation. *)
val neg: t -> t
(** Negation of an integer abstraction. *)
val scale: Integer.t -> t -> t
(** [scale f v] returns an abstraction of the integers [f * x]
for all [x] in [v]. This operation is exact. *)
val scale_div: pos:bool -> Integer.t -> t -> t
(** [scale_div f v] is an over-approximation of the elements [x / f] for all
elements [x] in [v]. Uses the computer division (like in C99) if [pos] is
false, and the euclidean division if [pos] is true. *)
val scale_div_under: pos:bool -> Integer.t -> t -> t or_bottom
(** Under-approximation of the division. *)
val scale_rem: pos:bool -> Integer.t -> t -> t
(** Over-approximation of the remainder of the division. Uses the computer
division (like in C99) if [pos] is false, and the euclidean division if
[pos] is true. *)
val mul: t -> t -> t
val div: t -> t -> t or_bottom
val c_rem: t -> t -> t or_bottom
val shift_left: t -> t -> t or_bottom
val shift_right: t -> t -> t or_bottom
val bitwise_and : t -> t -> t
val bitwise_or : t -> t -> t
val bitwise_xor : t -> t -> t
val bitwise_and: t -> t -> t
val bitwise_or: t -> t -> t
val bitwise_xor: t -> t -> t
val bitwise_signed_not: t -> t
val bitwise_unsigned_not: size:int -> t -> t
val cast_int_to_int : size:Integer.t -> signed:bool -> t -> t
(** {2 Misc} *)
val cast_int_to_int: size:Integer.t -> signed:bool -> t -> t
(** Splits an abstraction into two abstractions. *)
val subdivide: t -> t * t
(** Extracts bits from [start] to [stop] from the given integer abstraction,
[start] and [stop] being included. *)
val extract_bits: start:Integer.t -> stop:Integer.t -> t -> t
(** Builds an abstraction of all integers in a C integer type. *)
val create_all_values: signed:bool -> size:int -> t
(** [all_values ~size v] returns true iff v contains all integer values
representable in [size] bits. *)
val all_values: size:Integer.t -> t -> bool
val overlaps: partial:bool -> size:Integer.t -> t -> t -> bool
val fold_int : (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
(** Iterates on all integers represented by an abstraction.
@raise Abstract_interp.Error_Top if the abstraction is unbounded. *)
val fold_int: (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
(** Low-level operation for demarshalling *)
val rehash: t -> t
......@@ -140,7 +140,7 @@ let contains_non_zero = function
| Float f -> Fval.contains_non_zero f
exception Not_Singleton_Int = Int_val.Not_Singleton_Int
exception Not_Singleton_Int = Int_val.Not_Singleton
let project_int = function
| Int i -> Int_val.project_int i
......
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