Commit 5453a262 authored by David Bühler's avatar David Bühler

Merge branch 'feature/eva/ival' into 'master'

[Ival] Restructuring ival, split into 4 files

Closes #613

See merge request frama-c/frama-c!2192
parents 45a3ed03 e8654827
......@@ -587,6 +587,9 @@ 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/int_val.cmo \
src/kernel_services/abstract_interp/ival.cmo \
src/kernel_services/abstract_interp/base.cmo \
src/kernel_services/abstract_interp/origin.cmo \
......@@ -633,6 +636,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 \
......
......@@ -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,12 @@ 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/int_val.ml: CEA_LGPL
src/kernel_services/abstract_interp/int_val.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
......
(**************************************************************************)
(* *)
(* 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_if_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 diff is collapsed.
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
(** 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
include Eva_lattice_type.Full_AI_Lattice_with_cardinality
with type t := t
and type widen_hint = Integer.t * Datatype.Integer.Set.t
(** Checks that the interval defined by [min, max, rem, modu] is well formed. *)
val check:
min:Integer.t option -> max:Integer.t option ->
rem:Integer.t -> modu:Integer.t -> unit
(** 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 complement_under: min:Integer.t -> max:Integer.t -> t -> t or_bottom
(** Returns an under-approximation of the integers between [min] and [max]
that are *not* represented by the given interval. *)
(** {2 Interval semantics.} *)
(** 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
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 cast: size:Integer.t -> signed:bool -> t -> t
(** {2 Misc.} *)
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: ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
(**************************************************************************)
(* *)
(* 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 get_small_cardinal () = !small_cardinal
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
(* Small sets of integers, implemented as sorted non-empty arrays. *)
type set = Int.t array
(* Redefine functions creating arrays to forbid empty arrays and arrays with
more elements than [!small_cardinal]. *)
module Array = struct
include Array
(* Do not warn on unused functions: all functions creating arrays should be
refefined here, even if they are not used yet. *)
[@@@ warning "-32"]
(* This function creates a zero array of the same size as the array [a].
No need to check the length as the [a] must already satisfies the
invariants. *)
let zero_copy a =
let l = Array.length a in
make l Int.zero, l
let make n x = assert (n > 0 && n <= !small_cardinal); make n x
let init n f = assert (n > 0 && n <= !small_cardinal); init n f
let sub a start len = assert (len > 0); sub a start len
end
let zero = [| Int.zero |]
let one = [| Int.one |]
let minus_one = [| Int.minus_one |]
let zero_or_one = [| Int.zero ; Int.one |]
let inject_singleton e = [| e |]
let inject_periodic ~from ~period ~number =
let l = Int.to_int number in
let s = Array.make l Int.zero in
let v = ref from in
let i = ref 0 in
while (!i < l)
do
s.(!i) <- !v;
v := Int.add period !v;
incr i
done;
s
module O = FCSet.Make (Integer)
let inject_list list =
let o = List.fold_left (fun o r -> O.add r o) O.empty list in
let cardinal = O.cardinal o in
let a = Array.make cardinal Int.zero in
let i = ref 0 in
O.iter (fun e -> a.(!i) <- e; incr i) o;
a
let to_list = Array.to_list
(* ------------------------------- Datatype --------------------------------- *)
let hash s = Array.fold_left (fun acc v -> 1031 * acc + (Int.hash v)) 17 s
exception Unequal of int
let compare s1 s2 =
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 =
Pretty_utils.pp_iter
~pre:"@[<hov 1>{"
~suf:"}@]"
~sep:";@ "
Array.iter Int.pretty fmt s
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 x = x
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 =
if debug_cardinal
then
fun s ->
let l = Array.length s in
assert (l > 0 && l <= !small_cardinal);
l
else 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 ?(increasing=true) =
if increasing
then fun f array acc -> Array.fold_left (fun acc x -> f x acc) acc array
else Array.fold_right
let truncate_no_bottom r i =
if i = 1
then inject_singleton r.(0)
else Array.sub r 0 i
let truncate_or_bottom r i =
if i = 0 then `Bottom else `Value (truncate_no_bottom r i)
let map_reduce (f : 'a -> 'b) (g : 'b -> 'b -> 'b) (set : 'a array) : 'b =
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 r, l = Array.zero_copy a 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_or_bottom 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 ]
type set_or_top_or_bottom = [ `Bottom | set_or_top ]
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)
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 share_set o s =
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)
let inject_ps_or_bottom = function
| Pre_set (o, s) -> if s = 0 then `Bottom else `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 a
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 r, l = Array.zero_copy s in
let rec c i =
if i = l
then r
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 r, l = Array.zero_copy s in
let rec c i =
if i = l
then r
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_or_bottom
(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 r, l = Array.zero_copy s in
let rec c srcindex dstindex last =
if srcindex < 0
then begin
r.(dstindex) <- last;
truncate_no_bottom r (succ dstindex)
end
else
let v = f s.(srcindex) in