From b9b4b79ee02bb02ca1f6d40ef296a43c36af5147 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 14 Jan 2019 15:51:55 +0100
Subject: [PATCH] [Ival] New files int_set and int_interval.
They respectively implements the semantics of small integer sets and integer
intervals.
---
Makefile | 3 +
headers/header_spec.txt | 5 +
.../abstract_interp/eva_lattice_type.mli | 88 +++
.../abstract_interp/int_interval.ml | 737 ++++++++++++++++++
.../abstract_interp/int_interval.mli | 71 ++
.../abstract_interp/int_set.ml | 647 +++++++++++++++
.../abstract_interp/int_set.mli | 94 +++
7 files changed, 1645 insertions(+)
create mode 100644 src/kernel_services/abstract_interp/eva_lattice_type.mli
create mode 100644 src/kernel_services/abstract_interp/int_interval.ml
create mode 100644 src/kernel_services/abstract_interp/int_interval.mli
create mode 100644 src/kernel_services/abstract_interp/int_set.ml
create mode 100644 src/kernel_services/abstract_interp/int_set.mli
diff --git a/Makefile b/Makefile
index 483ffe220a2..6c41594b0d7 100644
--- a/Makefile
+++ b/Makefile
@@ -587,6 +587,8 @@ KERNEL_CMO=\
src/kernel_services/abstract_interp/fc_float.cmo \
src/kernel_services/abstract_interp/float_interval.cmo \
src/kernel_services/abstract_interp/fval.cmo \
+ src/kernel_services/abstract_interp/int_interval.cmo \
+ src/kernel_services/abstract_interp/int_set.cmo \
src/kernel_services/abstract_interp/ival.cmo \
src/kernel_services/abstract_interp/base.cmo \
src/kernel_services/abstract_interp/origin.cmo \
@@ -633,6 +635,7 @@ MLI_ONLY+=\
src/kernel_services/abstract_interp/float_sig.mli \
src/kernel_services/abstract_interp/float_interval_sig.mli \
src/kernel_services/abstract_interp/lattice_type.mli \
+ src/kernel_services/abstract_interp/eva_lattice_type.mli \
src/kernel_services/abstract_interp/int_Intervals_sig.mli \
src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli \
src/kernel_services/abstract_interp/offsetmap_sig.mli \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 5167c3bb180..a84301e7133 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -412,6 +412,7 @@ src/kernel_services/abstract_interp/base.ml: CEA_LGPL
src/kernel_services/abstract_interp/base.mli: CEA_LGPL
src/kernel_services/abstract_interp/bottom.ml: CEA_LGPL
src/kernel_services/abstract_interp/bottom.mli: CEA_LGPL
+src/kernel_services/abstract_interp/eva_lattice_type.mli: CEA_LGPL
src/kernel_services/abstract_interp/fc_float.ml: CEA_LGPL
src/kernel_services/abstract_interp/fc_float.mli: CEA_LGPL
src/kernel_services/abstract_interp/float_sig.mli: CEA_LGPL
@@ -425,6 +426,10 @@ src/kernel_services/abstract_interp/int_Base.mli: CEA_LGPL
src/kernel_services/abstract_interp/int_Intervals.ml: CEA_LGPL
src/kernel_services/abstract_interp/int_Intervals.mli: CEA_LGPL
src/kernel_services/abstract_interp/int_Intervals_sig.mli: CEA_LGPL
+src/kernel_services/abstract_interp/int_interval.ml: CEA_LGPL
+src/kernel_services/abstract_interp/int_interval.mli: CEA_LGPL
+src/kernel_services/abstract_interp/int_set.ml: CEA_LGPL
+src/kernel_services/abstract_interp/int_set.mli: CEA_LGPL
src/kernel_services/abstract_interp/ival.ml: CEA_LGPL
src/kernel_services/abstract_interp/ival.mli: CEA_LGPL
src/kernel_services/abstract_interp/lattice_messages.ml: CEA_LGPL
diff --git a/src/kernel_services/abstract_interp/eva_lattice_type.mli b/src/kernel_services/abstract_interp/eva_lattice_type.mli
new file mode 100644
index 00000000000..99d58f9ed1b
--- /dev/null
+++ b/src/kernel_services/abstract_interp/eva_lattice_type.mli
@@ -0,0 +1,88 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Lattice signatures using the Bottom type:
+ these lattices do not include a bottom element, and return `Bottom instead
+ when needed. Except that, they are identical to the module signatures in
+ {!Lattice_type}. *)
+
+open Bottom.Type
+
+module type Join_Semi_Lattice = Lattice_type.Join_Semi_Lattice
+module type With_Top = Lattice_type.With_Top
+module type With_Intersects = Lattice_type.With_Intersects
+module type With_Enumeration = Lattice_type.With_Enumeration
+module type With_Cardinal_One = Lattice_type.With_Cardinal_One
+module type With_Widening = Lattice_type.With_Widening
+
+module type With_Narrow = sig
+ type t
+ val narrow: t -> t -> t or_bottom (** over-approximation of intersection *)
+end
+
+module type With_Under_Approximation = sig
+ type t
+ val link: t -> t -> t (** under-approximation of union *)
+ val meet: t -> t -> t or_bottom (** under-approximation of intersection *)
+end
+
+module type With_Diff = sig
+ type t
+ val diff : t -> t -> t or_bottom
+ (** [diff t1 t2] is an over-approximation of [t1-t2]. [t2] must
+ be an under-approximation or exact. *)
+end
+
+module type With_Diff_One = sig
+ type t
+ val diff_if_one : t -> t -> t or_bottom
+ (** [diff_of_one t1 t2] is an over-approximation of [t1-t2].
+ @return [t1] if [t2] is not a singleton. *)
+end
+
+(** {2 Common signatures} *)
+
+(** Signature shared by some functors of module {!Abstract_interp}. *)
+module type AI_Lattice_with_cardinal_one = sig
+ include Join_Semi_Lattice
+ include With_Top with type t:= t
+ include With_Widening with type t:= t
+ include With_Cardinal_One with type t := t
+ include With_Narrow with type t := t
+ include With_Under_Approximation with type t := t
+ include With_Intersects with type t := t
+end
+
+(** Most complete lattices: all operations plus widening, notion of cardinal
+ (including enumeration) and difference. *)
+module type Full_AI_Lattice_with_cardinality = sig
+ include AI_Lattice_with_cardinal_one
+ include With_Diff with type t := t
+ include With_Diff_One with type t := t
+ include With_Enumeration with type t := t
+end
+
+(*
+Local Variables:
+compile-command: "make -C ../../.."
+End:
+*)
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
new file mode 100644
index 00000000000..c8af47fe9bf
--- /dev/null
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -0,0 +1,737 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Abstract_interp
+
+let emitter = Lattice_messages.register "Int_interval";;
+let log_imprecision s = Lattice_messages.emit_imprecision emitter s
+
+(* Represents the interval between [min] and [max], congruent to [rem] modulo
+ [modulo]. A value of [None] for [min] (resp. [max]) represents -infinity
+ (resp. +infinity). [modulo] is > 0, and [0 <= rem < modulo]. *)
+type itv = { min: Int.t option;
+ max: Int.t option;
+ rem: Int.t;
+ modu: Int.t; }
+
+let top = { min = None; max = None; rem = Int.zero; modu = Int.one }
+
+(* ------------------------------ Datatype ---------------------------------- *)
+
+let bound_compare x y =
+ match x, y with
+ | None, None -> 0
+ | None, Some _ -> 1
+ | Some _, None -> -1
+ | Some x, Some y -> Int.compare x y
+
+let compare t1 t2 =
+ let r1 = bound_compare t1.min t2.min in
+ if r1 <> 0 then r1
+ else
+ let r2 = bound_compare t1.max t2.max in
+ if r2 <> 0 then r2
+ else
+ let r3 = Int.compare t1.rem t2.rem in
+ if r3 <> 0 then r3
+ else Int.compare t1.modu t2.modu
+
+let equal t1 t2 = compare t1 t2 = 0
+
+let hash_v_option = function
+ | None -> 97
+ | Some v -> Int.hash v
+
+let hash t =
+ hash_v_option t.min + 5501 * (hash_v_option t.max) +
+ 59 * (Int.hash t.rem) + 13031 * (Int.hash t.modu)
+
+let pretty fmt t =
+ let print_bound fmt = function
+ | None -> Format.fprintf fmt "--"
+ | Some v -> Int.pretty fmt v
+ in
+ Format.fprintf fmt "[%a..%a]%t"
+ print_bound t.min
+ print_bound t.max
+ (fun fmt ->
+ if Int.is_zero t.rem && Int.is_one t.modu then Format.fprintf fmt ""
+ else Format.fprintf fmt ",%a%%%a" Int.pretty t.rem Int.pretty t.modu)
+
+include Datatype.Make_with_collections
+ (struct
+ type t = itv
+ let name = "int_interval"
+ open Structural_descr
+ let structural_descr =
+ let s_int = Descr.str Int.descr in
+ t_record [| pack (t_option s_int);
+ pack (t_option s_int);
+ Int.packed_descr;
+ Int.packed_descr |]
+ let reprs = [ top ]
+ let equal = equal
+ let compare = compare
+ let hash = hash
+ let pretty = pretty
+ let rehash = Datatype.identity
+ let internal_pretty_code = Datatype.pp_fail
+ let mem_project = Datatype.never_any_project
+ let copy = Datatype.undefined
+ let varname = Datatype.undefined
+ end)
+
+(* ------------------------------ Building ---------------------------------- *)
+
+let share_top t =
+ if equal t top then top else t
+
+let fail min max r modu =
+ let bound fmt = function
+ | None -> Format.fprintf fmt "--"
+ | Some(x) -> Int.pretty fmt x
+ in
+ Kernel.fatal "Ival: broken interval, min=%a max=%a r=%a modu=%a"
+ bound min bound max Int.pretty r Int.pretty modu
+
+let is_safe_modulo r modu =
+ (Int.ge r Int.zero ) && (Int.ge modu Int.one) && (Int.lt r modu)
+
+let is_safe_bound bound r modu = match bound with
+ | None -> true
+ | Some m -> Int.equal (Int.e_rem m modu) r
+
+(* Sanity check. *)
+let check t =
+ if not (is_safe_modulo t.rem t.modu
+ && is_safe_bound t.min t.rem t.modu
+ && is_safe_bound t.max t.rem t.modu)
+ then fail t.min t.max t.rem t.modu
+
+let make ~min ~max ~rem ~modu =
+ let t = { min; max; rem; modu } in
+ check t;
+ share_top t
+
+let inject_singleton e =
+ { min = Some e; max = Some e; rem = Int.zero; modu = Int.one }
+
+let inject_range min max =
+ let t = { min; max; rem = Int.zero; modu = Int.one } in
+ share_top t
+
+let build_interval ~min ~max ~rem:r ~modu =
+ assert (is_safe_modulo r modu);
+ let fix_bound fix bound = match bound with
+ | None -> None
+ | Some b -> Some (if Int.equal b (Int.e_rem r modu) then b else fix b)
+ in
+ let min = fix_bound (fun min -> Int.round_up_to_r ~min ~r ~modu) min
+ and max = fix_bound (fun max -> Int.round_down_to_r ~max ~r ~modu) max in
+ make ~min ~max ~rem:r ~modu
+
+let make_or_bottom ~min ~max ~rem ~modu =
+ match min, max with
+ | Some min, Some max when Int.gt min max -> `Bottom
+ | _, _ -> `Value (make ~min ~max ~rem ~modu)
+
+(* ---------------------------------- Utils --------------------------------- *)
+
+let min_le_elt min elt =
+ match min with
+ | None -> true
+ | Some m -> Int.le m elt
+
+let max_ge_elt max elt =
+ match max with
+ | None -> true
+ | Some m -> Int.ge m elt
+
+let all_positives t =
+ match t.min with
+ | None -> false
+ | Some m -> Int.ge m Int.zero
+
+let all_negatives t =
+ match t.max with
+ | None -> false
+ | Some m -> Int.le m Int.zero
+
+let min_and_max t = t.min, t.max
+
+let min_max_rem_modu t = t.min, t.max, t.rem, t.modu
+
+let mem i t =
+ Int.equal (Int.e_rem i t.modu) t.rem
+ && min_le_elt t.min i && max_ge_elt t.max i
+
+let cardinal t =
+ match t.min, t.max with
+ | None, _ | _, None -> None
+ | Some mn, Some mx -> Some Int.(succ ((e_div (sub mx mn) t.modu)))
+
+(* --------------------------------- Lattice -------------------------------- *)
+
+(** [min_is_lower mn1 mn2] is true iff mn1 is a lower min than mn2 *)
+let min_is_lower min1 min2 =
+ match min1, min2 with
+ | None, _ -> true
+ | _, None -> false
+ | Some m1, Some m2 -> Int.le m1 m2
+
+(** [max_is_greater mx1 mx2] is true iff mx1 is a greater max than mx2 *)
+let max_is_greater max1 max2 =
+ match max1, max2 with
+ | None, _ -> true
+ | _, None -> false
+ | Some m1, Some m2 -> Int.ge m1 m2
+
+let rem_is_included r1 m1 r2 m2 =
+ (Int.is_zero (Int.e_rem m1 m2)) && (Int.equal (Int.e_rem r1 m2) r2)
+
+let is_included t1 t2 =
+ (t1 == t2) ||
+ (min_is_lower t2.min t1.min) &&
+ (max_is_greater t2.max t1.max) &&
+ rem_is_included t1.rem t1.modu t2.rem t2.modu
+
+let min_min x y =
+ match x, y with
+ | None,_ | _, None -> None
+ | Some x, Some y -> Some (Int.min x y)
+
+let max_max x y =
+ match x, y with
+ | None,_ | _, None -> None
+ | Some x, Some y -> Some (Int.max x y)
+
+let join t1 t2 =
+ if t1 == t2 then t1 else
+ begin
+ check t1;
+ check t2;
+ let modu = Int.(pgcd (pgcd t1.modu t2.modu) (abs (sub t1.rem t2.rem))) in
+ let rem = Int.e_rem t1.rem modu in
+ let min = min_min t1.min t2.min in
+ let max = max_max t1.max t2.max in
+ let r = make ~min ~max ~rem ~modu in
+ r
+ end
+
+let link t1 t2 =
+ if Int.equal t1.rem t2.rem && Int.equal t1.modu t2.modu
+ then
+ let min = match t1.min, t2.min with
+ | Some a, Some b -> Some (Int.min a b)
+ | _ -> None in
+ let max = match t1.max, t2.max with
+ | Some a, Some b -> Some (Int.max a b)
+ | _ -> None in
+ make ~min ~max ~rem:t1.rem ~modu:t1.modu
+ else t1 (* No best abstraction anyway. *)
+
+(* [extended_euclidian_algorithm a b] returns x,y,gcd such that
+ a*x+b*y=gcd(x,y). *)
+let extended_euclidian_algorithm a b =
+ assert (Int.gt a Int.zero);
+ assert (Int.gt b Int.zero);
+ let a = ref a and b = ref b in
+ let x = ref Int.zero and lastx = ref Int.one in
+ let y = ref Int.one and lasty = ref Int.zero in
+ while not (Int.is_zero !b) do
+ let (q,r) = Int.e_div_rem !a !b in
+ a := !b;
+ b := r;
+ let tmpx = !x in
+ (x:= Int.sub !lastx (Int.mul q !x); lastx := tmpx);
+ let tmpy = !y in
+ (y:= Int.sub !lasty (Int.mul q !y); lasty := tmpy);
+ done;
+ (!lastx, !lasty, !a)
+
+(* This function provides solutions to the Chinese remainder theorem,
+ i.e. it finds the solutions x such that:
+ x == r1 mod m1 && x == r2 mod m2.
+ If no such solution exists, it raises Error_Bottom; else it returns
+ (r,m) such that all solutions x are such that x == r mod m. *)
+let compute_r_common r1 m1 r2 m2 =
+ (* (E1) x == r1 mod m1 && x == r2 mod m2
+ <=> \E k1,k2: x = r1 + k1*m1 && x = r2 + k2*m2
+ <=> \E k1,k2: x = r1 + k1*m1 && k1*m1 - k2*m2 = r2 - r1
+
+ Let r = r2 - r1. The equation (E2): k1*m1 - k2*m2 = r is
+ diophantine; there are solutions x to (E1) iff there are
+ solutions (k1,k2) to (E2).
+
+ Let d = pgcd(m1,m2). There are solutions to (E2) only if d
+ divides r (because d divides k1*m1 - k2*m2). Else we raise
+ [Error_Bottom]. *)
+ let (x1,_,pgcd) = extended_euclidian_algorithm m1 m2 in
+ let r = Int.sub r2 r1 in
+ let (r_div, r_rem) = Int.e_div_rem r pgcd in
+ if not (Int.equal r_rem Int.zero)
+ then raise Error_Bottom
+ (* The extended euclidian algorithm has provided solutions x1,x2 to
+ the Bezout identity x1*m1 + x2*m2 = d.
+
+ x1*m1 + x2*m2 = d ==> x1*(r/d)*m1 + x2*(r/d)*m2 = d*(r/d).
+
+ Thus, k1 = x1*(r/d), k2=-x2*(r/d) are solutions to (E2)
+ Thus, x = r1 + x1*(r/d)*m1 is a particular solution to (E1). *)
+ else
+ let k1 = Int.mul x1 r_div in
+ let x = Int.add r1 (Int.mul k1 m1) in
+ (* If two solutions x and y exist, they are equal modulo ppcm(m1,m2).
+ We have x == r1 mod m1 && y == r1 mod m1 ==> \E k1: x - y = k1*m1
+ x == r2 mod m2 && y == r2 mod m2 ==> \E k2: x - y = k2*m2
+
+ Thus k1*m1 = k2*m2 is a multiple of m1 and m2, i.e. is a multiple
+ of ppcm(m1,m2). Thus x = y mod ppcm(m1,m2). *)
+ let ppcm = Integer.ppcm m1 m2 in
+ (* x may be bigger than the ppcm, we normalize it. *)
+ (Int.e_rem x ppcm, ppcm)
+
+let compute_first_common mn1 mn2 r modu =
+ if mn1 = None && mn2 = None
+ then None
+ else
+ let m =
+ match mn1, mn2 with
+ | Some m, None | None, Some m -> m
+ | Some m1, Some m2 -> Int.max m1 m2
+ | None, None -> assert false (* already tested above *)
+ in
+ Some (Int.round_up_to_r m r modu)
+
+let compute_last_common mx1 mx2 r modu =
+ if mx1 = None && mx2 = None
+ then None
+ else
+ let m =
+ match mx1, mx2 with
+ | Some m, None | None, Some m -> m
+ | Some m1, Some m2 -> Int.min m1 m2
+ | None, None -> assert false (* already tested above *)
+ in
+ Some (Int.round_down_to_r m r modu)
+
+let meet t1 t2 =
+ if t1 == t2 then `Value t1 else
+ try
+ let rem, modu = compute_r_common t1.rem t1.modu t2.rem t2.modu in
+ let min = compute_first_common t1.min t2.min rem modu in
+ let max = compute_last_common t1.max t2.max rem modu in
+ make_or_bottom ~min ~max ~rem ~modu
+ with Error_Bottom -> `Bottom
+
+let narrow = meet
+
+type size_widen_hint = Integer.t
+type generic_widen_hint = Datatype.Integer.Set.t
+type widen_hint = size_widen_hint * generic_widen_hint
+
+let widen (bitsize,wh) t1 t2 =
+ if equal t1 t2 then t2
+ else
+ (* Add possible interval limits deducted from the bitsize *)
+ let wh =
+ (* If bitsize > 128, the values do not correspond to a scalar type.
+ This can (rarely) happen on structures or arrays that have been
+ reinterpreted as one value by the offsetmaps. In this case, do not
+ use limits, and do not create arbitrarily large integers. *)
+ if Integer.gt bitsize (Integer.of_int 128)
+ then Datatype.Integer.Set.empty
+ else if Integer.is_zero bitsize
+ then wh
+ else
+ let limits =
+ [ Integer.neg (Integer.two_power (Integer.pred bitsize));
+ Integer.pred (Integer.two_power (Integer.pred bitsize));
+ Integer.pred (Integer.two_power bitsize); ]
+ in
+ Datatype.Integer.Set.(union wh (of_list limits))
+ in
+ let modu = Int.(pgcd (pgcd t1.modu t2.modu) (abs (sub t1.rem t2.rem))) in
+ let rem = Int.e_rem t1.rem modu in
+ let min =
+ if bound_compare t1.min t2.min = 0 then t2.min else
+ match t2.min with
+ | None -> None
+ | Some min2 ->
+ try
+ let v = Datatype.Integer.Set.nearest_elt_le min2 wh
+ in Some (Int.round_up_to_r ~r:rem ~modu ~min:v)
+ with Not_found -> None
+ in
+ let max =
+ if bound_compare t1.max t2.max = 0 then t2.max else
+ match t2.max with
+ | None -> None
+ | Some max2 ->
+ try
+ let v = Datatype.Integer.Set.nearest_elt_ge max2 wh
+ in Some (Int.round_down_to_r ~r:rem ~modu ~max:v)
+ with Not_found -> None
+ in
+ make ~min ~max ~rem ~modu
+
+let intersects v1 v2 =
+ v1 == v2 || not (meet v1 v2 = `Bottom) (* YYY: slightly inefficient *)
+
+let cardinal_less_than t n =
+ let c = match t.min, t.max with
+ | None, _ | _, None -> raise Not_less_than
+ | Some min, Some max -> Int.succ ((Int.e_div (Int.sub max min) t.modu))
+ in
+ if Int.le c (Int.of_int n)
+ then Int.to_int c (* This is smaller than the original [n] *)
+ else raise Not_less_than
+
+let cardinal_zero_or_one t =
+ match t.min, t.max with
+ | None, _ | _, None -> false
+ | Some min, Some max -> Integer.equal min max
+
+(* TODO? *)
+let diff _ _ = assert false
+let diff_if_one _ _ = assert false
+
+let fold_int f t acc =
+ match t.min, t.max with
+ | None, _ | _, None -> raise Error_Top
+ | Some inf, Some sup -> Int.fold f ~inf ~sup ~step:t.modu acc
+
+let fold_enum f v acc =
+ fold_int (fun x acc -> f (inject_singleton x) acc) v acc
+
+(* ------------------------------ Arithmetics ------------------------------- *)
+
+let opt_map2 f m1 m2 =
+ match m1, m2 with
+ | None, _ | _, None -> None
+ | Some m1, Some m2 -> Some (f m1 m2)
+
+let add_singleton_int i t =
+ let incr = Int.add i in
+ let min = Extlib.opt_map incr t.min in
+ let max = Extlib.opt_map incr t.max in
+ let rem = Int.e_rem (incr t.rem) t.modu in
+ make ~min ~max ~rem ~modu:t.modu
+
+let add t1 t2 =
+ let modu = Int.pgcd t1.modu t2.modu in
+ let rem = Int.e_rem (Int.add t1.rem t2.rem) modu in
+ let min =
+ opt_map2
+ (fun min1 min2 -> Int.round_up_to_r ~min:(Int.add min1 min2) ~r:rem ~modu)
+ t1.min t2.min
+ in
+ let max =
+ opt_map2
+ (fun m1 m2 -> Int.round_down_to_r ~max:(Int.add m1 m2) ~r:rem ~modu)
+ t1.max t2.max
+ in
+ make ~min ~max ~rem ~modu
+
+let add_under t1 t2 =
+ if Int.equal t1.modu t2.modu
+ then
+ (* Note: min1+min2 % modu = max1 + max2 % modu = r1 + r2 % modu;
+ no need to trim the bounds here. *)
+ let rem = Int.e_rem (Int.add t1.rem t2.rem) t1.modu in
+ let min = opt_map2 Int.add t1.min t2.min
+ and max = opt_map2 Int.add t1.max t2.max in
+ `Value (make ~min ~max ~rem ~modu:t1.modu)
+ else
+ (* In many cases, there is no best abstraction; for instance when
+ modu1 divides modu2, a part of the resulting interval is
+ congruent to modu1, and a larger part is congruent to modu2. In
+ general, one can take the intersection. In any case, this code
+ should be rarely called. *)
+ `Bottom
+
+let neg t =
+ make
+ ~min:(Extlib.opt_map Int.neg t.max)
+ ~max:(Extlib.opt_map Int.neg t.min)
+ ~rem:(Int.e_rem (Int.neg t.rem) t.modu)
+ ~modu:t.modu
+
+type ext_value = Ninf | Pinf | Val of Int.t
+let inject_min = function None -> Ninf | Some m -> Val m
+let inject_max = function None -> Pinf | Some m -> Val m
+let ext_neg = function Ninf -> Pinf | Pinf -> Ninf | Val v -> Val (Int.neg v)
+let ext_mul x y =
+ match x, y with
+ | Ninf, Ninf | Pinf, Pinf -> Pinf
+ | Ninf, Pinf | Pinf, Ninf -> Ninf
+ | Val v1, Val v2 -> Val (Int.mul v1 v2)
+ | (Ninf | Pinf as x), Val v | Val v, (Ninf | Pinf as x) ->
+ if Int.gt v Int.zero then x
+ else if Int.lt v Int.zero then ext_neg x
+ else Val Int.zero
+
+let ext_min x y =
+ match x,y with
+ Ninf, _ | _, Ninf -> Ninf
+ | Pinf, x | x, Pinf -> x
+ | Val x, Val y -> Val(Int.min x y)
+
+let ext_max x y =
+ match x,y with
+ Pinf, _ | _, Pinf -> Pinf
+ | Ninf, x | x, Ninf -> x
+ | Val x, Val y -> Val(Int.max x y)
+
+let ext_proj = function Val x -> Some x | _ -> None
+
+let scale f t =
+ let incr = Int.mul f in
+ if Int.gt f Int.zero
+ then
+ let modu = incr t.modu in
+ make
+ ~min:(Extlib.opt_map incr t.min) ~max:(Extlib.opt_map incr t.max)
+ ~rem:(Int.e_rem (incr t.rem) modu) ~modu
+ else
+ let modu = Int.neg (incr t.modu) in
+ make
+ ~min:(Extlib.opt_map incr t.max) ~max:(Extlib.opt_map incr t.min)
+ ~rem:(Int.e_rem (incr t.rem) modu) ~modu
+
+let scale_div_common ~pos f t degenerate =
+ assert (not (Int.is_zero f));
+ let div_f =
+ if pos
+ then fun a -> Int.e_div a f
+ else fun a -> Int.c_div a f
+ in
+ let rem, modu =
+ let negative = max_is_greater (Some Int.zero) t.max in
+ if (negative (* all negative *)
+ || pos (* good div *)
+ || (min_is_lower (Some Int.zero) t.min) (* all positive *)
+ || (Int.is_zero (Int.e_rem t.rem f))) (* exact *)
+ && (Int.is_zero (Int.e_rem t.modu f))
+ then
+ let modu = Int.abs (div_f t.modu) in
+ let r = if negative then Int.sub t.rem t.modu else t.rem in
+ (Int.e_rem (div_f r) modu), modu
+ else (* degeneration*)
+ degenerate t.rem t.modu
+ in
+ let divf_mn1 = Extlib.opt_map div_f t.min in
+ let divf_mx1 = Extlib.opt_map div_f t.max in
+ let min, max =
+ if Int.gt f Int.zero
+ then divf_mn1, divf_mx1
+ else divf_mx1, divf_mn1
+ in
+ make ~min ~max ~rem ~modu
+
+let scale_div ~pos f v =
+ scale_div_common ~pos f v (fun _ _ -> Int.zero, Int.one)
+
+let scale_div_under ~pos f v =
+ try
+ (* TODO: a more precise result could be obtained by transforming
+ Top(min,max,r,m) into Top(min,max,r/f,m/gcd(m,f)). But this is
+ more complex to implement when pos or f is negative. *)
+ `Value (scale_div_common ~pos f v (fun _r _m -> raise Exit))
+ with Exit -> `Bottom
+
+let scale_rem ~pos f t =
+ assert (not (Int.is_zero f));
+ let f = if Int.lt f Int.zero then Int.neg f else f in
+ let rem_f a = if pos then Int.e_rem a f else Int.c_rem a f in
+ let modu = Int.pgcd f t.modu in
+ let rr = Int.e_rem t.rem modu in
+ let binf, bsup =
+ if pos
+ then Int.round_up_to_r ~min:Int.zero ~r:rr ~modu,
+ Int.round_down_to_r ~max:(Int.pred f) ~r:rr ~modu
+ else
+ let min = if all_positives t then Int.zero else Int.neg (Int.pred f) in
+ let max = if all_negatives t then Int.zero else Int.pred f in
+ Int.round_up_to_r ~min ~r:rr ~modu,
+ Int.round_down_to_r ~max ~r:rr ~modu
+ in
+ let mn_rem, mx_rem =
+ match t.min, t.max with
+ | Some mn, Some mx ->
+ let div_f a = if pos then Int.e_div a f else Int.c_div a f in
+ (* See if [mn..mx] is included in [k*f..(k+1)*f] for some [k]. In
+ this case, [%] is monotonic and [mn%f .. mx%f] is a more precise
+ result. *)
+ if Int.equal (div_f mn) (div_f mx)
+ then rem_f mn, rem_f mx
+ else binf,bsup
+ | _ -> binf,bsup
+ in
+ make ~min:(Some mn_rem) ~max:(Some mx_rem) ~rem:rr ~modu
+
+let c_rem t1 t2 =
+ match t2.min, t2.max with
+ | None, _ | _, None -> `Value top
+ | Some min2, Some max2 ->
+ if Int.equal max2 Int.zero
+ then `Bottom (* completely undefined. *)
+ else
+ (* Result is of the sign of x. Also, compute |x| to bound the result *)
+ let neg, pos, max_x =
+ min_le_elt t1.min Int.minus_one,
+ max_ge_elt t1.max Int.one,
+ (match t1.min, t1.max with
+ | Some mn, Some mx -> Some (Int.max (Int.abs mn) (Int.abs mx))
+ | _ -> None)
+ in
+ (* Bound the result: no more than |x|, and no more than |y|-1 *)
+ let pos_rem = Integer.max (Int.abs min2) (Int.abs max2) in
+ let bound = Int.pred pos_rem in
+ let bound = Extlib.may_map (Int.min bound) ~dft:bound max_x in
+ (* Compute result bounds using sign information *)
+ let min = if neg then Some (Int.neg bound) else Some Int.zero in
+ let max = if pos then Some bound else Some Int.zero in
+ (* TODO: inject_range_or_bottom? *)
+ `Value (inject_range min max)
+
+let mul t1 t2 =
+ check t1;
+ check t2;
+ let min1 = inject_min t1.min in
+ let max1 = inject_max t1.max in
+ let min2 = inject_min t2.min in
+ let max2 = inject_max t2.max in
+ let a = ext_mul min1 min2 in
+ let b = ext_mul min1 max2 in
+ let c = ext_mul max1 min2 in
+ let d = ext_mul max1 max2 in
+ let min = ext_min (ext_min a b) (ext_min c d) in
+ let max = ext_max (ext_max a b) (ext_max c d) in
+ (* let multipl1 = Int.pgcd m1 r1 in
+ let multipl2 = Int.pgcd m2 r2 in
+ let modu1 = Int.pgcd m1 m2 in
+ let modu2 = Int.mul multipl1 multipl2 in
+ let modu = Int.ppcm modu1 modu2 in *)
+ let modu =
+ Int.(pgcd
+ (pgcd (mul t1.modu t2.modu) (mul t1.rem t2.modu))
+ (mul t2.rem t1.modu))
+ in
+ let rem = Int.e_rem (Int.mul t1.rem t2.rem) modu in
+ make ~min:(ext_proj min) ~max:(ext_proj max) ~rem ~modu
+
+(* ymin and ymax must be the same sign *)
+let div_range x ymn ymx =
+ match min_and_max x with
+ | Some xmn, Some xmx ->
+ let c1 = Int.c_div xmn ymn in
+ let c2 = Int.c_div xmx ymn in
+ let c3 = Int.c_div xmn ymx in
+ let c4 = Int.c_div xmx ymx in
+ let min = Int.min (Int.min c1 c2) (Int.min c3 c4) in
+ let max = Int.max (Int.max c1 c2) (Int.max c3 c4) in
+ inject_range (Some min) (Some max)
+ | _ ->
+ log_imprecision "Ival.div_range";
+ top
+
+let div x y =
+ match y.min, y.max with
+ | None, _ | _, None -> log_imprecision "Ival.div"; `Value top
+ | Some min, Some max ->
+ let result_pos =
+ if Int.gt max Int.zero
+ then
+ let lpos =
+ if Int.gt min Int.zero
+ then min
+ else Int.round_up_to_r ~min:Int.one ~r:y.rem ~modu:y.modu
+ in
+ `Value (div_range x lpos max)
+ else `Bottom
+ in
+ let result_neg =
+ if Int.lt min Int.zero
+ then
+ let gneg =
+ if Int.lt max Int.zero
+ then max
+ else Int.round_down_to_r ~max:Int.minus_one ~r:y.rem ~modu:y.modu
+ in
+ `Value (div_range x min gneg)
+ else `Bottom
+ in
+ Bottom.join join result_neg result_pos
+
+(* ----------------------------------- Misc --------------------------------- *)
+
+let subdivide t =
+ match t.min, t.max with
+ | Some min, Some max ->
+ let mean = Int.e_div (Int.add min max) Int.two in
+ let succmean = Int.succ mean in
+ build_interval ~min:(Some min) ~max:(Some mean) ~rem:t.rem ~modu:t.modu,
+ build_interval ~min:(Some succmean) ~max:(Some max) ~rem:t.rem ~modu:t.modu
+ | _, _ -> raise Can_not_subdiv
+
+let reduce_sign t b =
+ let r, modu = t.rem, t.modu in
+ if b
+ then
+ if all_positives t
+ then `Value t
+ else
+ let max = Some Int.(round_down_to_r ~max:minus_one ~r ~modu) in
+ make_or_bottom ~min:t.min ~max ~rem:r ~modu
+ else
+ if all_negatives t
+ then `Value t
+ else
+ let min = Some Int.(round_up_to_r ~min:zero ~r ~modu) in
+ make_or_bottom ~min ~max:t.max ~rem:r ~modu
+
+let reduce_bit i t b =
+ let r, modu = t.rem, t.modu in
+ let power = Int.(two_power_of_int i) in (* 001000 *)
+ let mask = Int.(pred (two_power_of_int (i+1))) in (* 001111 *)
+ (* Reduce bounds to the nearest satisfying bound *)
+ let min = match t.min with
+ | Some l when Z.testbit l i <> b ->
+ let min =
+ if b
+ then Int.(logor (logand l (lognot mask)) power) (* ll1000 *)
+ else Int.(succ (logor l mask)) (* ll1111 + 1 *)
+ in
+ Some (Int.round_up_to_r ~min ~r ~modu)
+ | l -> l
+ and max = match t.max with
+ | Some u when Z.testbit u i <> b ->
+ let max =
+ if b
+ then Int.(pred (logand u (lognot mask))) (* uu0000 - 1 *)
+ else Int.(logand (logor u mask) (lognot power)) (* uu0111 *)
+ in
+ Some (Int.round_down_to_r ~max ~r ~modu)
+ | u -> u
+ in
+ make_or_bottom ~min ~max ~rem:r ~modu
diff --git a/src/kernel_services/abstract_interp/int_interval.mli b/src/kernel_services/abstract_interp/int_interval.mli
new file mode 100644
index 00000000000..b9d18d50d45
--- /dev/null
+++ b/src/kernel_services/abstract_interp/int_interval.mli
@@ -0,0 +1,71 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Bottom.Type
+
+include Datatype.S_with_collections
+
+include Eva_lattice_type.Full_AI_Lattice_with_cardinality
+ with type t := t
+ and type widen_hint = Integer.t * Datatype.Integer.Set.t
+
+val make:
+ min:Integer.t option -> max:Integer.t option ->
+ rem:Integer.t -> modu:Integer.t -> t
+
+val inject_range: Integer.t option -> Integer.t option -> t
+
+val min_and_max: t -> Integer.t option * Integer.t option
+
+val min_max_rem_modu:
+ t -> Integer.t option * Integer.t option * Integer.t * Integer.t
+
+val mem: Integer.t -> t -> bool
+
+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. *)
+
+val neg : t -> t
+(** Negation of an integer ival. Exact operation. *)
+
+
+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
+
+val mul: t -> t -> t
+val div: t -> t -> t or_bottom
+val c_rem: t -> t -> t or_bottom
+
+val subdivide: t -> t * t
+
+val reduce_sign: t -> bool -> t or_bottom
+val reduce_bit: int -> t -> bool -> t or_bottom
+
+val fold_int: (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
new file mode 100644
index 00000000000..b04d23e1f60
--- /dev/null
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -0,0 +1,647 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Abstract_interp
+open Bottom.Type
+
+(* Make sure all this is synchronized with the default value of -ilevel *)
+let small_cardinal = ref 8
+let set_small_cardinal i = small_cardinal := i
+
+let debug_cardinal = false
+
+let emitter = Lattice_messages.register "Int_set";;
+let log_imprecision s = Lattice_messages.emit_imprecision emitter s
+
+type set = Int.t array
+
+let bottom = Array.make 0 Int.zero
+
+let small_nums = Array.init 33 (fun i -> [| (Integer.of_int i) |])
+
+let zero = small_nums.(0)
+let one = small_nums.(1)
+let minus_one = [| Int.minus_one |]
+let zero_or_one = [| Int.zero ; Int.one |]
+
+let inject_singleton e =
+ if Int.le Int.zero e && Int.le e Int.thirtytwo
+ then small_nums.(Int.to_int e)
+ else [| e |]
+
+let unsafe_share_array a s =
+ let e = a.(0) in
+ if s = 1 && Int.le Int.zero e && Int.le e Int.thirtytwo
+ then small_nums.(Int.to_int e)
+ else if s = 2 && Int.is_zero e && Int.is_one a.(1)
+ then zero_or_one
+ else a
+
+(* TODO: assert s <> 0 *)
+let share_array a s =
+ if s = 0 then bottom else unsafe_share_array a s
+
+let share_array_or_bottom a s =
+ if s = 0 then `Bottom else `Value (unsafe_share_array a s)
+
+let inject_array = share_array
+
+let project_array t = t
+
+(* ------------------------------- Datatype --------------------------------- *)
+
+let hash s = Array.fold_left (fun acc v -> 1031 * acc + (Int.hash v)) 17 s
+
+let rehash s = share_array s (Array.length s)
+
+exception Unequal of int
+
+let compare s1 s2 =
+ if s1 == s2 then 0 else
+ let l1 = Array.length s1 in
+ let l2 = Array.length s2 in
+ if l1 <> l2
+ then l1 - l2 (* no overflow here *)
+ else
+ (try
+ for i = 0 to l1 - 1 do
+ let r = Int.compare s1.(i) s2.(i) in
+ if r <> 0 then raise (Unequal r)
+ done;
+ 0
+ with Unequal v -> v)
+
+let equal e1 e2 = compare e1 e2 = 0
+
+let pretty fmt s =
+ if Array.length s = 0 then Format.fprintf fmt "BottomMod"
+ else begin
+ Pretty_utils.pp_iter
+ ~pre:"@[<hov 1>{"
+ ~suf:"}@]"
+ ~sep:";@ "
+ Array.iter Int.pretty fmt s
+ end
+
+include Datatype.Make_with_collections
+ (struct
+ type t = set
+ let name = "int_set"
+ open Structural_descr
+ let structural_descr = t_array (Descr.str Int.descr)
+ let reprs = [ zero ]
+ let equal = equal
+ let compare = compare
+ let hash = hash
+ let pretty = pretty
+ let rehash = rehash
+ let internal_pretty_code = Datatype.pp_fail
+ let mem_project = Datatype.never_any_project
+ let copy = Datatype.undefined
+ let varname = Datatype.undefined
+ end)
+
+(* ---------------------------------- Utils --------------------------------- *)
+
+let cardinal = Array.length
+
+let for_all f (a : Integer.t array) =
+ let l = Array.length a in
+ let rec c i = i = l || ((f a.(i)) && c (succ i)) in
+ c 0
+
+let exists = Extlib.array_exists
+
+let iter = Array.iter
+let fold = Array.fold_left
+
+let truncate r i =
+ if i = 0
+ then `Bottom
+ else if i = 1
+ then `Value (inject_singleton r.(0))
+ else begin
+ (Obj.truncate (Obj.repr r) i);
+ assert (Array.length r = i);
+ `Value r
+ end
+
+exception Empty
+
+let map_reduce (f : 'a -> 'b) (g : 'b -> 'b -> 'b) (set : 'a array) : 'b =
+ if Array.length set <= 0 then
+ raise Empty
+ else
+ let acc = ref (f set.(0)) in
+ for i = 1 to Array.length set - 1 do
+ acc := g !acc (f set.(i))
+ done;
+ !acc
+
+let filter (f : Int.t -> bool) (a : Int.t array) : t or_bottom =
+ let l = Array.length a in
+ let r = Array.make l Int.zero in
+ let j = ref 0 in
+ for i = 0 to l - 1 do
+ let x = a.(i) in
+ if f x then begin
+ r.(!j) <- x;
+ incr j;
+ end
+ done;
+ truncate r !j
+
+let mem v a =
+ let l = Array.length a in
+ let rec c i =
+ if i = l then (-1)
+ else
+ let ae = a.(i) in
+ if Int.equal ae v
+ then i
+ else if Int.gt ae v
+ then (-1)
+ else c (succ i)
+ in
+ c 0
+
+(* ------------------------------- Set or top ------------------------------- *)
+
+type set_or_top = [ `Set of t | `Top of Integer.t * Integer.t * Integer.t ]
+
+module O = FCSet.Make (Integer)
+
+type pre_set =
+ | Pre_set of O.t * int
+ | Pre_top of Int.t * Int.t * Int.t
+
+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
+ let max = O.max_elt s in
+ let modu = O.fold
+ (fun x acc ->
+ if Int.equal x min then acc else Int.pgcd (Int.sub x min) acc)
+ s Int.zero
+ in
+ (min, max, modu)
+
+let add_ps ps x =
+ match ps with
+ | Pre_set (o, s) ->
+ if debug_cardinal then assert (O.cardinal o = s);
+ if O.mem x o (* TODO: improve *)
+ then ps
+ else
+ let no = O.add x o in
+ if s < !small_cardinal
+ then begin
+ if debug_cardinal then assert (O.cardinal no = succ s);
+ Pre_set (no, succ s)
+ end
+ else
+ let min, max, modu = make_top_from_set no in
+ Pre_top (min, max, modu)
+ | Pre_top (min, max, modu) ->
+ let new_modu =
+ if Int.equal x min
+ then modu
+ else Int.pgcd (Int.sub x min) modu
+ in
+ let new_min = Int.min min x in
+ let new_max = Int.max max x in
+ Pre_top (new_min, new_max, new_modu)
+
+let o_zero = O.singleton Int.zero
+let o_one = O.singleton Int.one
+let o_zero_or_one = O.union o_zero o_one
+
+let share_set o s =
+ if s = 0 then bottom
+ else if s = 1
+ then begin
+ let e = O.min_elt o in
+ inject_singleton e
+ end
+ else if O.equal o o_zero_or_one
+ then zero_or_one
+ else
+ let a = Array.make s Int.zero in
+ let i = ref 0 in
+ O.iter (fun e -> a.(!i) <- e; incr i) o;
+ assert (!i = s);
+ a
+
+let inject_ps = function
+ | Pre_set (o, s) -> `Set (share_set o s)
+ | Pre_top (min, max, modu) -> `Top (min, max, modu)
+
+(* Given a set of elements that is an under-approximation, returns an
+ ival (while maintaining the ival invariants that the "Set"
+ constructor is used only for small sets of elements. *)
+let set_to_ival_under set =
+ let card = Int.Set.cardinal set in
+ if card <= !small_cardinal
+ then
+ let a = Array.make card Int.zero in
+ ignore (Int.Set.fold (fun elt i -> Array.set a i elt; i + 1) set 0);
+ `Set (share_array a card)
+ else
+ (* If by chance the set is contiguous. *)
+ if (Int.equal
+ (Int.sub (Int.Set.max_elt set) (Int.Set.min_elt set))
+ (Int.of_int (card - 1)))
+ then `Top (Int.Set.min_elt set, Int.Set.max_elt set, Int.one)
+ (* Else: arbitrarily drop some elements of the under approximation. *)
+ else
+ let a = Array.make !small_cardinal Int.zero in
+ log_imprecision "Ival.set_to_ival_under";
+ try
+ ignore (Int.Set.fold (fun elt i ->
+ if i = !small_cardinal then raise Exit;
+ Array.set a i elt;
+ i + 1) set 0);
+ assert false
+ with Exit -> `Set a
+
+(* ------------------------------ Apply and map ----------------------------- *)
+
+let apply_bin_1_strict_incr f x (s : Integer.t array) =
+ let l = Array.length s in
+ let r = Array.make l Int.zero in
+ let rec c i =
+ if i = l
+ then share_array r l
+ else
+ let v = f x s.(i) in
+ r.(i) <- v;
+ c (succ i)
+ in
+ c 0
+
+let apply_bin_1_strict_decr f x (s : Integer.t array) =
+ let l = Array.length s in
+ let r = Array.make l Int.zero in
+ let rec c i =
+ if i = l
+ then share_array r l
+ else
+ let v = f x s.(i) in
+ r.(l - i - 1) <- v;
+ c (succ i)
+ in
+ c 0
+
+let apply2_n f (s1 : Integer.t array) (s2 : Integer.t array) =
+ let ps = ref empty_ps in
+ let l1 = Array.length s1 in
+ let l2 = Array.length s2 in
+ for i1 = 0 to pred l1 do
+ let e1 = s1.(i1) in
+ for i2 = 0 to pred l2 do
+ ps := add_ps !ps (f e1 s2.(i2))
+ done
+ done;
+ inject_ps !ps
+
+let apply2_notzero f (s1 : Integer.t array) s2 =
+ inject_ps
+ (Array.fold_left
+ (fun acc v1 ->
+ Array.fold_left
+ (fun acc v2 ->
+ if Int.is_zero v2
+ then acc
+ else add_ps acc (f v1 v2))
+ acc
+ s2)
+ empty_ps
+ s1)
+
+let map_set_decr f (s : Integer.t array) =
+ let l = Array.length s in
+ if l = 0
+ then `Bottom
+ else
+ let r = Array.make l Int.zero in
+ let rec c srcindex dstindex last =
+ if srcindex < 0
+ then begin
+ r.(dstindex) <- last;
+ truncate r (succ dstindex)
+ end
+ else
+ let v = f s.(srcindex) in
+ if Int.equal v last
+ then
+ c (pred srcindex) dstindex last
+ else begin
+ r.(dstindex) <- last;
+ c (pred srcindex) (succ dstindex) v
+ end
+ in
+ c (l-2) 0 (f s.(pred l))
+
+let map_set_strict_decr f (s : Integer.t array) =
+ let l = Array.length s in
+ let r = Array.make l Int.zero in
+ let rec c i =
+ if i = l
+ then share_array r l
+ else
+ let v = f s.(i) in
+ r.(l - i - 1) <- v;
+ c (succ i)
+ in
+ c 0
+
+let map_set_incr f (s : Integer.t array) =
+ let l = Array.length s in
+ if l = 0
+ then `Bottom
+ else
+ let r = Array.make l Int.zero in
+ let rec c srcindex dstindex last =
+ if srcindex = l
+ then begin
+ r.(dstindex) <- last;
+ truncate r (succ dstindex)
+ end
+ else
+ let v = f s.(srcindex) in
+ if Int.equal v last
+ then
+ c (succ srcindex) dstindex last
+ else begin
+ r.(dstindex) <- last;
+ c (succ srcindex) (succ dstindex) v
+ end
+ in
+ c 1 0 (f s.(0))
+
+let map f s =
+ let pre_set =
+ Array.fold_left (fun acc elt -> add_ps acc (f elt)) empty_ps s
+ in
+ match pre_set with
+ | Pre_set (o, s) -> share_set o s
+ | Pre_top _ -> assert false
+
+(* --------------------------------- Lattice -------------------------------- *)
+
+let is_included s1 s2 =
+ let l1 = Array.length s1 in
+ let l2 = Array.length s2 in
+ if l1 > l2 then false
+ else
+ let rec c i1 i2 =
+ if i1 = l1 then true
+ else if i2 = l2 then false
+ else
+ let e1 = s1.(i1) in
+ let e2 = s2.(i2) in
+ let si2 = succ i2 in
+ if Int.equal e1 e2
+ then c (succ i1) si2
+ else if Int.lt e1 e2
+ then false
+ else c i1 si2 (* TODO: improve by not reading a1.(i1) all the time *)
+ in
+ c 0 0
+
+(* Join [s1] of length [l1] and [s2] of length [l2]. *)
+let join l1 s1 l2 s2 =
+ (* first pass: count unique elements and detect inclusions *)
+ let rec first i1 i2 uniq inc1 inc2 =
+ if i1 = l1
+ then (uniq + l2 - i2), false, inc2
+ else if i2 = l2
+ then (uniq + l1 - i1), inc1, false
+ else
+ let e1 = s1.(i1) in
+ let e2 = s2.(i2) in
+ if Int.lt e2 e1
+ then first i1 (succ i2) (succ uniq) false inc2
+ else if Int.gt e2 e1
+ then first (succ i1) i2 (succ uniq) inc1 false
+ else first (succ i1) (succ i2) (succ uniq) inc1 inc2
+ in
+ let uniq, incl1, incl2 = first 0 0 0 true true in
+ if incl1 then `Set s1 else
+ if incl2 then `Set s2 else
+ (* second pass: make a set or make a top *)
+ if uniq > !small_cardinal
+ then
+ let min = Int.min s1.(0) s2.(0) in
+ let accum acc x =
+ if Int.equal x min
+ then acc
+ else Int.pgcd (Int.sub x min) acc
+ in
+ let modu = ref Int.zero in
+ for j = 0 to pred l1 do
+ modu := accum !modu s1.(j)
+ done;
+ for j = 0 to pred l2 do
+ modu := accum !modu s2.(j)
+ done;
+ `Top (min, Int.max s1.(pred l1) s2.(pred l2), !modu)
+ else
+ let r = Array.make uniq Int.zero in
+ let rec c i i1 i2 =
+ if i1 = l1
+ then begin
+ Array.blit s2 i2 r i (l2 - i2);
+ share_array r uniq
+ end
+ else if i2 = l2
+ then begin
+ Array.blit s1 i1 r i (l1 - i1);
+ share_array r uniq
+ end
+ else
+ let si = succ i in
+ let e1 = s1.(i1) in
+ let e2 = s2.(i2) in
+ if Int.lt e2 e1
+ then begin
+ r.(i) <- e2;
+ c si i1 (succ i2)
+ end
+ else begin
+ r.(i) <- e1;
+ let si1 = succ i1 in
+ if Int.equal e1 e2
+ then c si si1 (succ i2)
+ else c si si1 i2
+ end
+ in
+ `Set (c 0 0 0)
+
+let join s1 s2 =
+ let l1 = Array.length s1 in
+ if l1 = 0
+ then `Set s2
+ else
+ let l2 = Array.length s2 in
+ if l2 = 0
+ then `Set s1
+ else join l1 s1 l2 s2
+
+let link s1 s2 =
+ let s1 = Array.fold_right Int.Set.add s1 Int.Set.empty in
+ let s2 = Array.fold_right Int.Set.add s2 s1 in
+ set_to_ival_under s2
+
+let meet s1 s2 =
+ let l1 = Array.length s1 in
+ let l2 = Array.length s2 in
+ let lr_max = min l1 l2 in
+ let r = Array.make lr_max Int.zero in
+ let rec c i i1 i2 =
+ if i1 = l1 || i2 = l2
+ then truncate r i
+ else
+ let e1 = s1.(i1) in
+ let e2 = s2.(i2) in
+ if Int.equal e1 e2
+ then begin
+ r.(i) <- e1;
+ c (succ i) (succ i1) (succ i2)
+ end
+ else if Int.lt e1 e2
+ then c i (succ i1) i2
+ else c i i1 (succ i2)
+ in
+ c 0 0 0
+
+let narrow = meet (* meet is exact. *)
+
+let intersects s1 s2 =
+ let l1 = Array.length s1 in
+ let l2 = Array.length s2 in
+ let rec aux i1 i2 =
+ if i1 = l1 || i2 = l2 then false
+ else
+ let e1 = s1.(i1) in
+ let e2 = s2.(i2) in
+ if Int.equal e1 e2 then true
+ else if Int.lt e1 e2 then aux (succ i1) i2
+ else aux i1 (succ i2)
+ in
+ aux 0 0
+
+let diff_if_one _value _rem = assert false
+
+let remove s v =
+ let index = mem v s in
+ if index >= 0
+ then
+ let l = Array.length s in
+ let pl = pred l in
+ let r = Array.make pl Int.zero in
+ Array.blit s 0 r 0 index;
+ Array.blit s (succ index) r index (pl-index);
+ share_array_or_bottom r pl
+ else `Value s
+
+(* ------------------------------ Arithmetics ------------------------------- *)
+
+let add_singleton = apply_bin_1_strict_incr Int.add
+
+let add s1 s2 =
+ match s1, s2 with
+ | [| x |], s | s, [| x |] -> `Set (apply_bin_1_strict_incr Int.add x s)
+ | _, _ -> apply2_n Int.add s1 s2
+
+let add_under s1 s2 =
+ match s1, s2 with
+ | [| x |], s | s, [| x |] -> `Set (apply_bin_1_strict_incr Int.add x s)
+ | _, _ ->
+ let set =
+ Array.fold_left (fun acc i1 ->
+ Array.fold_left (fun acc i2 ->
+ Int.Set.add (Int.add i1 i2) acc) acc s2)
+ Int.Set.empty s1
+ in
+ set_to_ival_under set
+
+let neg s = map_set_strict_decr Int.neg s
+
+let scale f s =
+ if Int.ge f Int.zero
+ then apply_bin_1_strict_incr Int.mul f s
+ else apply_bin_1_strict_decr Int.mul f s
+
+let mul s1 s2 =
+ match s1, s2 with
+ | s, [| x |] | [| x |], s -> `Set (scale x s)
+ | _, _ -> apply2_n Int.mul s1 s2
+
+let scale_div ~pos f s =
+ let div_f =
+ if pos
+ then fun a -> Int.e_div a f
+ else fun a -> Int.c_div a f
+ in
+ if Int.lt f Int.zero
+ then map_set_decr div_f s
+ else map_set_incr div_f s
+
+let scale_rem ~pos f s =
+ let f = if Int.lt f Int.zero then Int.neg f else f in
+ let rem_f a =
+ if pos then Int.e_rem a f else Int.c_rem a f
+ in
+ let pre_set =
+ Array.fold_left
+ (fun acc v -> add_ps acc (rem_f v))
+ empty_ps
+ s
+ in
+ inject_ps pre_set
+
+let c_rem s1 s2 = apply2_notzero Int.c_rem s1 s2
+
+let bitwise_signed_not = map_set_strict_decr Int.lognot
+
+(* ------------------------------- Subdivide -------------------------------- *)
+
+let subdivide s =
+ let len = Array.length s in
+ assert (len > 0 );
+ if len <= 1 then raise Can_not_subdiv;
+ let m = len lsr 1 in
+ let lenhi = len - m in
+ let lo = Array.sub s 0 m in
+ let hi = Array.sub s m lenhi in
+ share_array lo m,
+ share_array hi lenhi
+
+
+(* -------------------------------- Export ---------------------------------- *)
+
+let min t = t.(0)
+let max t = t.(Array.length t - 1)
diff --git a/src/kernel_services/abstract_interp/int_set.mli b/src/kernel_services/abstract_interp/int_set.mli
new file mode 100644
index 00000000000..207ff16e960
--- /dev/null
+++ b/src/kernel_services/abstract_interp/int_set.mli
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Bottom.Type
+
+include Datatype.S_with_collections
+
+val rehash: t -> t
+
+val bottom: t
+
+val inject_singleton: Integer.t -> t
+val inject_array: Integer.t array -> int -> t
+
+val project_array: t -> Integer.t array
+
+val remove: t -> Integer.t -> t or_bottom
+
+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 cardinal: t -> int
+
+val mem: Integer.t -> t -> int
+
+val for_all: (Integer.t -> bool) -> t -> bool
+val exists: (Integer.t -> bool) -> t -> bool
+
+val iter: (Integer.t -> unit) -> t -> unit
+val fold: ('a -> Integer.t -> 'a) -> 'a -> t -> 'a
+val map: (Integer.t -> Integer.t) -> t -> t
+val filter: (Integer.t -> bool) -> t -> t or_bottom
+
+exception Empty
+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 ]
+
+val is_included: t -> t -> bool
+val join: t -> t -> [`Set of t | `Top of (Integer.t * Integer.t * Integer.t)]
+val link: t -> t -> set_or_top
+val meet: t -> t -> t or_bottom
+val narrow: t -> t -> t or_bottom
+
+val intersects: t -> t -> bool
+
+val diff_if_one: t -> t -> t or_bottom
+
+val add_singleton: Integer.t -> t -> t
+val add: t -> t -> set_or_top
+val add_under: t -> t -> set_or_top
+val neg: t -> t
+
+val mul: t -> t -> set_or_top
+
+val c_rem: t -> t -> set_or_top
+
+val scale: Integer.t -> t -> t
+val scale_div: pos:bool -> Integer.t -> t -> t or_bottom
+val scale_rem: pos:bool -> Integer.t -> t -> set_or_top
+
+val bitwise_signed_not: t -> t
+
+val subdivide: t -> t * t
+
+
+(**/**)
+
+(* This is used by the Value plugin. Do not use. *)
+val set_small_cardinal: int -> unit
--
GitLab