From b9c9f7177b92b59ef942a26a6c0a83aef68089c5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 31 Jan 2019 17:02:00 +0100
Subject: [PATCH] [Ival] Comments int_set and int_interval.
---
.../abstract_interp/int_interval.ml | 4 +-
.../abstract_interp/int_interval.mli | 33 ++++++++---
.../abstract_interp/int_set.ml | 4 +-
.../abstract_interp/int_set.mli | 55 +++++++++++++++----
.../abstract_interp/int_val.ml | 2 +-
5 files changed, 75 insertions(+), 23 deletions(-)
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index 0453c1260a7..cb8d0a9c2ba 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -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
diff --git a/src/kernel_services/abstract_interp/int_interval.mli b/src/kernel_services/abstract_interp/int_interval.mli
index 74cb8c36358..b3854e42dfb 100644
--- a/src/kernel_services/abstract_interp/int_interval.mli
+++ b/src/kernel_services/abstract_interp/int_interval.mli
@@ -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
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 5854fa30f8b..4f60e38cd03 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -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
diff --git a/src/kernel_services/abstract_interp/int_set.mli b/src/kernel_services/abstract_interp/int_set.mli
index b88c2cc4887..3743502d031 100644
--- a/src/kernel_services/abstract_interp/int_set.mli
+++ b/src/kernel_services/abstract_interp/int_set.mli
@@ -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
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 107bc49c1ee..f18a3834a50 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -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 *)
--
GitLab