Commit b9b4b79e authored by David Bühler's avatar David Bühler
Browse files

[Ival] New files int_set and int_interval.

They respectively implements the semantics of small integer sets and integer
intervals.
parent fb1d7bf4
...@@ -587,6 +587,8 @@ KERNEL_CMO=\ ...@@ -587,6 +587,8 @@ KERNEL_CMO=\
src/kernel_services/abstract_interp/fc_float.cmo \ src/kernel_services/abstract_interp/fc_float.cmo \
src/kernel_services/abstract_interp/float_interval.cmo \ src/kernel_services/abstract_interp/float_interval.cmo \
src/kernel_services/abstract_interp/fval.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/ival.cmo \
src/kernel_services/abstract_interp/base.cmo \ src/kernel_services/abstract_interp/base.cmo \
src/kernel_services/abstract_interp/origin.cmo \ src/kernel_services/abstract_interp/origin.cmo \
...@@ -633,6 +635,7 @@ MLI_ONLY+=\ ...@@ -633,6 +635,7 @@ MLI_ONLY+=\
src/kernel_services/abstract_interp/float_sig.mli \ src/kernel_services/abstract_interp/float_sig.mli \
src/kernel_services/abstract_interp/float_interval_sig.mli \ src/kernel_services/abstract_interp/float_interval_sig.mli \
src/kernel_services/abstract_interp/lattice_type.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/int_Intervals_sig.mli \
src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli \ src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli \
src/kernel_services/abstract_interp/offsetmap_sig.mli \ src/kernel_services/abstract_interp/offsetmap_sig.mli \
......
...@@ -412,6 +412,7 @@ src/kernel_services/abstract_interp/base.ml: CEA_LGPL ...@@ -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/base.mli: CEA_LGPL
src/kernel_services/abstract_interp/bottom.ml: 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/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.ml: CEA_LGPL
src/kernel_services/abstract_interp/fc_float.mli: CEA_LGPL src/kernel_services/abstract_interp/fc_float.mli: CEA_LGPL
src/kernel_services/abstract_interp/float_sig.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 ...@@ -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.ml: CEA_LGPL
src/kernel_services/abstract_interp/int_Intervals.mli: 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_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.ml: CEA_LGPL
src/kernel_services/abstract_interp/ival.mli: CEA_LGPL src/kernel_services/abstract_interp/ival.mli: CEA_LGPL
src/kernel_services/abstract_interp/lattice_messages.ml: CEA_LGPL src/kernel_services/abstract_interp/lattice_messages.ml: CEA_LGPL
......
(**************************************************************************)
(* *)
(* 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:
*)
(**************************************************************************)
(* *)
(* 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