From a8318b993e655b828452799b40cbef9ed4f08f8e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 6 Feb 2019 10:26:45 +0100
Subject: [PATCH] [Ival] Comments int_val signature.
---
.../abstract_interp/int_val.ml | 25 +--
.../abstract_interp/int_val.mli | 144 +++++++++++++-----
src/kernel_services/abstract_interp/ival.ml | 2 +-
3 files changed, 119 insertions(+), 52 deletions(-)
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index f18a3834a50..e5c43049220 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -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
diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli
index 99747b9d674..4d8d0c7d9e3 100644
--- a/src/kernel_services/abstract_interp/int_val.mli
+++ b/src/kernel_services/abstract_interp/int_val.mli
@@ -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
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 7437373792e..0d957509785 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -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
--
GitLab