Commit f1acb5da authored by David Bühler's avatar David Bühler

[Ival] new file int_val for int abstractions.

parent afd53042
......@@ -589,6 +589,7 @@ KERNEL_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 \
......
......@@ -430,6 +430,8 @@ 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). *)
(* *)
(**************************************************************************)
open Abstract_interp
(* Make sure all this is synchronized with the default value of -ilevel *)
let small_cardinal = ref 8
let small_cardinal_Int = ref (Int.of_int !small_cardinal)
let small_cardinal_log = ref 3
let set_small_cardinal i =
assert (2 <= i && i <= 1024);
let rec log j p =
if i <= p then j
else log (j+1) (2*p)
in
small_cardinal := i;
small_cardinal_Int := Int.of_int i;
small_cardinal_log := log 1 2;
(* TODO: share this code with Int_set *)
Int_set.set_small_cardinal i
let get_small_cardinal () = !small_cardinal
let emitter = Lattice_messages.register "Int_val"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s
module Widen_Hints = Datatype.Integer.Set
type size_widen_hint = Integer.t
type generic_widen_hint = Widen_Hints.t
type widen_hint = size_widen_hint * generic_widen_hint
(* --------------------------------- Datatype ------------------------------- *)
type int_val =
| Set of Int_set.t
| Itv of Int_interval.t
let bottom = Set Int_set.bottom
let top = Itv Int_interval.top
let hash = function
| Set s -> Int_set.hash s
| Itv i -> Int_interval.hash i
let compare e1 e2 =
match e1, e2 with
| Set s1, Set s2 -> Int_set.compare s1 s2
| Itv i1, Itv i2 -> Int_interval.compare i1 i2
| _, Set _ -> 1
| Set _, _ -> -1
let equal e1 e2 = compare e1 e2 = 0
let pretty fmt = function
| Itv i -> Int_interval.pretty fmt i
| Set s -> Int_set.pretty fmt s
let rehash = function
| Set s -> Set (Int_set.rehash s)
| x -> x
include Datatype.Make_with_collections
(struct
type t = int_val
let name = "int_val"
open Structural_descr
let structural_descr =
t_sum
[| [| Int_set.packed_descr |];
[| Int_interval.packed_descr |] |]
let reprs = [ top ; bottom ]
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)
(* ------------------------------- Constructors ---------------------------- *)
let zero = Set Int_set.zero
let one = Set Int_set.one
let minus_one = Set Int_set.minus_one
let zero_or_one = Set Int_set.zero_or_one
let positive_integers = Itv (Int_interval.inject_range (Some Int.zero) None)
let negative_integers = Itv (Int_interval.inject_range None (Some Int.zero))
let fail min max r modu =
let bound fmt = function
| None -> Format.fprintf fmt "--"
| Some x -> Int.pretty fmt x
in
Kernel.fatal "Int_val: broken Itv, 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 for Itv's arguments *)
let check ~min ~max ~rem ~modu =
if not (is_safe_modulo rem modu
&& is_safe_bound min rem modu
&& is_safe_bound max rem modu)
then fail min max rem modu
let inject_singleton e = Set (Int_set.inject_singleton e)
let make ~min ~max ~rem ~modu =
match min, max with
| Some mn, Some mx ->
if Int.gt mx mn then
let l = Int.succ (Int.e_div (Int.sub mx mn) modu) in
if Int.le l !small_cardinal_Int
then
let l = Int.to_int l in
let s = Array.make l Int.zero in
let v = ref mn in
let i = ref 0 in
while (!i < l)
do
s.(!i) <- !v;
v := Int.add modu !v;
incr i
done;
assert (Int.equal !v (Int.add modu mx));
Set (Int_set.inject_array s l)
else Itv (Int_interval.make ~min ~max ~rem ~modu)
else if Int.equal mx mn
then inject_singleton mn
else bottom
| _ -> Itv (Int_interval.make ~min ~max ~rem ~modu)
let check_make ~min ~max ~rem ~modu =
check ~min ~max ~rem ~modu;
make ~min ~max ~rem ~modu
let inject_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 inject_range min max = check_make ~min ~max ~rem:Int.zero ~modu:Int.one
(* ------------------------- Sets and Intervals ---------------------------- *)
(* TODO: comments *)
let inject_set_or_bottom = function
| `Bottom -> bottom
| `Value s -> Set s
let inject_itv_or_bottom = function
| `Bottom -> bottom
| `Value i ->
match Int_interval.cardinal i with
| None -> Itv i
| Some card ->
if Int.le card !small_cardinal_Int
then
let min, max, rem, modu = Int_interval.min_max_rem_modu i in
make ~min ~max ~rem ~modu
else Itv i
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)
let inject_set_or_top = function
| `Set s -> Set s
| `Top (min, max, modu) -> inject_pre_itv ~min ~max ~modu
(* TODO: more comment *)
let make_top_from_set s =
let min = Int_set.min s in
let modu =
Int_set.fold
(fun acc x ->
if Int.equal x min
then acc
else Int.pgcd (Int.sub x min) acc)
Int.zero
s
in
let rem = Int.e_rem min modu in
let max = Some (Int_set.max s) in
let min = Some min in
min, max, rem, modu
let make_itv_from_set s =
let min, max, rem, modu = make_top_from_set s in
Int_interval.make ~min ~max ~rem ~modu
let make_itv = function
| Itv i -> i
| Set s -> make_itv_from_set s
let make_range = function
| Itv i -> i
| Set s ->
let min, max = Int_set.min s, Int_set.max s in
Int_interval.inject_range (Some min) (Some max)
(* -------------------------------- 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
(* TODO *)
let is_bottom x = equal x bottom
let is_zero x = equal x zero
let is_one = equal one
let contains_zero = function
| Itv i -> Int_interval.mem Int.zero i
| Set s -> Int_set.mem Int.zero s >= 0
let contains_non_zero = function
| Itv _ -> true (* at least two values *)
| Set _ as s -> not (is_zero s || is_bottom s)
let fold_int f v acc =
match v with
| Itv i -> Int_interval.fold_int f i acc
| Set s -> Int_set.fold (fun acc x -> f x acc) acc s
let fold_enum f v acc = fold_int (fun x acc -> f (inject_singleton x) acc) v acc
(* -------------------------------- Accessors ------------------------------- *)
let min_int = function
| Itv i -> fst (Int_interval.min_and_max i)
| Set s ->
if Int_set.cardinal s = 0
then raise Error_Bottom
else Some (Int_set.min s)
let max_int = function
| Itv i -> snd (Int_interval.min_and_max i)
| Set s ->
if Int_set.cardinal s = 0
then raise Error_Bottom
else Some (Int_set.max s)
let min_and_max = function
| Set s ->
let l = Int_set.cardinal s in
if l = 0
then raise Error_Bottom
else Some (Int_set.min s), Some (Int_set.max s)
| Itv i -> Int_interval.min_and_max i
let min_max_rem_modu = function
| Set s ->
assert (Int_set.cardinal s >= 2);
make_top_from_set s
| Itv i -> Int_interval.min_max_rem_modu i
exception Not_Singleton_Int
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
let is_small_set = function
| Set _ -> true
| Itv _ -> false
let project_small_set = function
| Set a -> Some (Int_set.to_list a)
| Itv _ -> None
(* ----------------------------- Cardinality -------------------------------- *)
let is_singleton = function
| Itv _ -> false
| Set s -> Int_set.cardinal s = 1
let cardinal_zero_or_one = function
| Set s -> Int_set.cardinal s <= 1
| Itv _ -> false
let cardinal = function
| Set s -> Some (Int.of_int (Int_set.cardinal s))
| Itv i -> Int_interval.cardinal i
let cardinal_estimate ~size = function
| Set s -> Int.of_int (Int_set.cardinal s)
| Itv i -> Extlib.opt_conv (Int.two_power size) (Int_interval.cardinal i)
let cardinal_less_than v n =
let c =
match v with
| Set s -> Int.of_int (Int_set.cardinal s)
| Itv i -> Extlib.the ~exn:Not_less_than (Int_interval.cardinal i)
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_is_less_than v n =
match cardinal v with
| None -> false
| Some c -> Int.le c (Int.of_int n)
let diff_if_one value rem =
match rem with
| Set s when Int_set.cardinal s = 1 ->
begin
let v = Int_set.min s in
match value with
| Set s -> inject_set_or_bottom (Int_set.remove s v)
| Itv i ->
let min, max, rem, modu = Int_interval.min_max_rem_modu i in
match min, max with
| Some mn, _ when Int.equal v mn ->
check_make ~min:(Some (Int.add mn modu)) ~max ~rem ~modu
| _, Some mx when Int.equal v mx ->
check_make ~min ~max:(Some (Int.sub mx modu)) ~rem ~modu
| Some mn, Some mx when
Int.equal (Int.sub mx mn) (Int.mul modu !small_cardinal_Int)
&& Int_interval.mem v i ->
let r = ref mn in
let array =
Array.init !small_cardinal
(fun _ ->
let c = !r in
let corrected_c = if Int.equal c v then Int.add c modu else c in
r := Int.add corrected_c modu;
corrected_c)
in
Set (Int_set.inject_array array !small_cardinal)
| _, _ -> value
end
| _ -> value
let diff value rem =
log_imprecision "Ival.diff";
diff_if_one value rem
(* ------------------------------- Lattice ---------------------------------- *)
let is_included t1 t2 =
(t1 == t2) ||
match t1, t2 with
| Set s, _ when Int_set.cardinal s = 0 -> true
| Itv i1, Itv i2 -> Int_interval.is_included i1 i2
| Itv _, Set _ -> false (* Itv _ represents more elements
than can be represented by Set _ *)
| Set s, Itv i ->
let min, max, rem, modu = Int_interval.min_max_rem_modu i in
(* Inclusion of bounds is needed for the entire inclusion *)
min_le_elt min (Int_set.min s) && max_ge_elt max (Int_set.max s)
&& (Int.equal Int.one modu (* Top side contains all integers, we're done *)
|| Int_set.for_all (fun x -> Int.equal (Int.e_rem x modu) rem) s)
| Set s1, Set s2 -> Int_set.is_included s1 s2
let join v1 v2 =
if v1 == v2 then v1 else
match v1,v2 with
| Itv i1, Itv i2 -> Itv (Int_interval.join i1 i2)
| Set i1, Set i2 -> inject_set_or_top (Int_set.join i1 i2)
| Set s, (Itv i as t)
| (Itv i as t), Set s ->
let min, max, r, modu = Int_interval.min_max_rem_modu i in
let l = Int_set.cardinal s in
if l = 0 then t
else
let f modu elt = Int.pgcd modu (Int.abs (Int.sub r elt)) in
let modu = Int_set.fold f modu s in
let rem = Int.e_rem r modu in
let min = match min with
None -> None
| Some m -> Some (Int.min m (Int_set.min s))
in
let max = match max with
None -> None
| Some m -> Some (Int.max m (Int_set.max s))
in
check ~min ~max ~rem ~modu;
Itv (Int_interval.make ~min ~max ~rem ~modu)
let link v1 v2 =
match v1, v2 with
| Set s1, Set s2 -> inject_set_or_top (Int_set.link s1 s2)
| Itv i1, Itv i2 -> Itv (Int_interval.link i1 i2)
| Itv i, Set s | Set s, Itv i ->
let min, max, rem, modu = Int_interval.min_max_rem_modu i in
let move_bound add = function
| None -> None
| Some bound ->
let cur = ref bound in
Int_set.iter (fun e -> if Int.equal e (add !cur modu) then cur := e) s;
Some !cur
in
let min = move_bound Int.sub min
and max = move_bound Int.add max in
check_make ~min ~max ~rem ~modu
let meet v1 v2 =
if v1 == v2 then v1 else
match v1, v2 with
| Itv i1, Itv i2 -> inject_itv_or_bottom (Int_interval.meet i1 i2)
| Set s1 , Set s2 -> inject_set_or_bottom (Int_set.meet s1 s2)
| Set s, Itv itv
| Itv itv, Set s ->
inject_set_or_bottom (Int_set.filter (fun i -> Int_interval.mem i itv) s)
let narrow v1 v2 =
match v1, v2 with
| Set s1, Set s2 -> inject_set_or_bottom (Int_set.narrow s1 s2)
| (Itv _| Set _), (Itv _ | Set _) -> meet v1 v2 (* meet is exact *)
let widen widen_hints t1 t2 =
if equal t1 t2 || cardinal_zero_or_one t1 then t2
else
match t2 with
| Itv _ | Set _ ->
let i1 = make_itv t1
and i2 = make_itv t2 in
inject_itv_or_bottom (`Value (Int_interval.widen widen_hints i1 i2))
let intersects v1 v2 =
v1 == v2 ||
match v1, v2 with
| Itv _, Itv _ -> not (is_bottom (meet v1 v2)) (* YYY: slightly inefficient *)
| Set s1 , Set s2 -> Int_set.intersects s1 s2
| Set s, Itv itv | Itv itv, Set s ->
Int_set.exists (fun i -> Int_interval.mem i itv) s
(* -------------------------------- Arithmetics ----------------------------- *)
let add_singleton i = function
| Set s -> Set (Int_set.add_singleton i s)
| Itv itv -> Itv (Int_interval.add_singleton_int i itv)
let add v1 v2 =
match v1, v2 with
| Set s1, Set s2 -> inject_set_or_top (Int_set.add s1 s2)
| Itv i1, Itv i2 -> Itv (Int_interval.add i1 i2)
| Set s, Itv i | Itv i, Set s ->
let l = Int_set.cardinal s in
if l = 0
then bottom
else if l = 1
then Itv (Int_interval.add_singleton_int (Int_set.min s) i)
else Itv (Int_interval.add i (make_itv_from_set s))
let add_under v1 v2 =
match v1, v2 with
| Set s1, Set s2 -> inject_set_or_top (Int_set.add_under s1 s2)
| Itv i1, Itv i2 -> inject_itv_or_bottom (Int_interval.add_under i1 i2)
| Set s, Itv i | Itv i, Set s ->
let l = Int_set.cardinal s in
if l = 0
then bottom
else
begin
if l <> 1
then log_imprecision "Ival.add_int_under";
(* This is precise if [s] has only one element. Otherwise, this is not worse
than another computation. *)
Itv (Int_interval.add_singleton_int (Int_set.min s) i)
end
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
then zero
else
match v with
| Set s -> Set (Int_set.scale f s)
| Itv i-> Itv (Int_interval.scale f i)
let scale_div_common ~pos f v scale_interval =
assert (not (Int.is_zero f));
match v with
| Set s -> inject_set_or_bottom (Int_set.scale_div ~pos f s)
| Itv i -> inject_itv_or_bottom (scale_interval ~pos f i)
let scale_div ~pos f v =
let scale_div ~pos f v = `Value (Int_interval.scale_div ~pos f v) in
scale_div_common ~pos f v scale_div
(* TODO: a more precise result could be obtained by transforming
Itv(min,max,r,m) into Itv(min,max,r/f,m/gcd(m,f)). But this is
more complex to implement when pos or f is negative. *)
let scale_div_under ~pos f v =
scale_div_common ~pos f v Int_interval.scale_div_under
let mul v1 v2 =
if is_one v1 then v2
else if is_zero v2 || is_zero v1 then zero
else if is_one v2 then v1
else
match v1, v2 with
| Set s1, Set s2 -> inject_set_or_top (Int_set.mul s1 s2)
| Itv i1, Itv i2 -> Itv (Int_interval.mul i1 i2)
| Set s, Itv i | Itv i, Set s ->
let l = Int_set.cardinal s in
if l = 0
then bottom
else if l = 1
then Itv (Int_interval.scale (Int_set.min s) i)
else Itv (Int_interval.mul i (make_itv_from_set s))
let div x y =
match y with
| Set sy ->
Int_set.fold
(fun acc elt ->
if Int.is_zero elt then acc else join acc (scale_div ~pos:false elt x))
bottom sy
| Itv iy -> inject_itv_or_bottom (Int_interval.div (make_range x) iy)
(* [scale_rem ~pos:false f v] is an over-approximation of the set of
elements [x mod f] for [x] in [v].
[scale_rem ~pos:true f v] is an over-approximation of the set of
elements [x pos_rem f] for [x] in [v]. *)
let scale_rem ~pos f v =