Skip to content

GitLab

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

[Ival] int_set and int_val complies with the or_bottom type. 

In Ival, bottom is now a special constructor.
parent f1acb5da
Hide whitespace changes
Inline Side-by-side
Showing with 289 additions and 251 deletions
src/kernel_services/abstract_interp/int_set.ml
View file @ ff44491d
......@@ -34,8 +34,6 @@ 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)
......@@ -48,7 +46,8 @@ let inject_singleton e =
then small_nums.(Int.to_int e)
else [| e |]
let unsafe_share_array a s =
let share_array a s =
assert (s > 0);
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)
......@@ -56,12 +55,8 @@ let unsafe_share_array a s =
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)
if s = 0 then `Bottom else `Value (share_array a s)
let inject_array = share_array
......@@ -93,14 +88,11 @@ let compare s1 s2 =
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
Pretty_utils.pp_iter
~pre:"@[<hov 1>{"
~suf:"}@]"
~sep:";@ "
Array.iter Int.pretty fmt s
include Datatype.Make_with_collections
(struct
......@@ -134,28 +126,26 @@ 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))
let truncate_no_bottom r i =
assert (i > 0);
if i = 1
then inject_singleton r.(0)
else begin
(Obj.truncate (Obj.repr r) i);
assert (Array.length r = i);
`Value r
r
end
exception Empty
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 =
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
assert (Array.length set > 0);
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
......@@ -168,7 +158,7 @@ let filter (f : Int.t -> bool) (a : Int.t array) : t or_bottom =
incr j;
end
done;
truncate r !j
truncate_or_bottom r !j
let mem v a =
let l = Array.length a in
......@@ -187,6 +177,7 @@ let mem v a =
(* ------------------------------- 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 ]
module O = FCSet.Make (Integer)
......@@ -239,8 +230,8 @@ 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
assert (s > 0);
if s = 1
then begin
let e = O.min_elt o in
inject_singleton e
......@@ -258,6 +249,10 @@ 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. *)
......@@ -327,7 +322,7 @@ let apply2_n f (s1 : Integer.t array) (s2 : Integer.t array) =
inject_ps !ps
let apply2_notzero f (s1 : Integer.t array) s2 =
inject_ps
inject_ps_or_bottom
(Array.fold_left
(fun acc v1 ->
Array.fold_left
......@@ -342,27 +337,25 @@ let apply2_notzero f (s1 : Integer.t array) s2 =
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
assert (l > 0);
let r = Array.make l Int.zero 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
if Int.equal v last
then
c (pred srcindex) dstindex last
else begin
r.(dstindex) <- last;
truncate r (succ dstindex)
c (pred srcindex) (succ dstindex) v
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))
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
......@@ -379,27 +372,25 @@ let map_set_strict_decr f (s : Integer.t array) =
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
assert (l > 0);
let r = Array.make l Int.zero in
let rec c srcindex dstindex last =
if srcindex = l
then begin
r.(dstindex) <- last;
truncate_no_bottom 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;
truncate r (succ dstindex)
c (succ srcindex) (succ dstindex) v
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))
in
c 1 0 (f s.(0))
let map f s =
let pre_set =
......@@ -522,7 +513,7 @@ let meet s1 s2 =
let r = Array.make lr_max Int.zero in
let rec c i i1 i2 =
if i1 = l1 || i2 = l2
then truncate r i
then truncate_or_bottom r i
else
let e1 = s1.(i1) in
let e2 = s2.(i2) in
......@@ -601,6 +592,7 @@ let mul s1 s2 =
| _, _ -> apply2_n Int.mul s1 s2
let scale_div ~pos f s =
assert (not (Int.is_zero f));
let div_f =
if pos
then fun a -> Int.e_div a f
......@@ -611,17 +603,10 @@ let scale_div ~pos f s =
else map_set_incr div_f s
let scale_rem ~pos f s =
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 pre_set =
Array.fold_left
(fun acc v -> add_ps acc (rem_f v))
empty_ps
s
in
inject_ps pre_set
let rem_f a = if pos then Int.e_rem a f else Int.c_rem a f in
map rem_f s
let c_rem s1 s2 = apply2_notzero Int.c_rem s1 s2
......@@ -631,7 +616,7 @@ let bitwise_signed_not = map_set_strict_decr Int.lognot
let subdivide s =
let len = Array.length s in
assert (len > 0 );
assert (len > 0);
if len <= 1 then raise Can_not_subdiv;
let m = len lsr 1 in
let lenhi = len - m in
......
src/kernel_services/abstract_interp/int_set.mli
View file @ ff44491d
......@@ -20,14 +20,17 @@
(* *)
(**************************************************************************)
(** Small sets of integers. Above a certain limit fixed by [set_small_cardinal],
these sets must be converted into intervals. The functions that make the
set grow returns a [set_or_top] type : either the resulting sets is small
enough, or it is converted into an interval. *)
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
......@@ -49,25 +52,21 @@ 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 ]
type set_or_top_or_bottom = [ `Bottom | set_or_top ]
val is_included: t -> t -> bool
val join: t -> t -> [`Set of t | `Top of (Integer.t * Integer.t * Integer.t)]
val join: t -> t -> set_or_top
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
......@@ -76,18 +75,16 @@ 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 c_rem: t -> t -> set_or_top_or_bottom
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 scale_div: pos:bool -> Integer.t -> t -> t
val scale_rem: pos:bool -> Integer.t -> t -> t
val bitwise_signed_not: t -> t
val subdivide: t -> t * t
(**/**)
(* This is used by the Value plugin. Do not use. *)
......
src/kernel_services/abstract_interp/int_val.ml
View file @ ff44491d
......@@ -21,6 +21,7 @@
(**************************************************************************)
open Abstract_interp
open Bottom.Type
(* Make sure all this is synchronized with the default value of -ilevel *)
let small_cardinal = ref 8
......@@ -56,7 +57,6 @@ 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
......@@ -89,7 +89,7 @@ include Datatype.Make_with_collections
t_sum
[| [| Int_set.packed_descr |];
[| Int_interval.packed_descr |] |]
let reprs = [ top ; bottom ]
let reprs = [ top ]
let equal = equal
let compare = compare
let hash = hash
......@@ -139,7 +139,10 @@ 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
assert (Int.le mn mx);
if Int.equal mx mn
then inject_singleton mn
else
let l = Int.succ (Int.e_div (Int.sub mx mn) modu) in
if Int.le l !small_cardinal_Int
then
......@@ -156,9 +159,6 @@ let make ~min ~max ~rem ~modu =
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 =
......@@ -177,25 +177,26 @@ let inject_interval ~min ~max ~rem:r ~modu =
let inject_range min max = check_make ~min ~max ~rem:Int.zero ~modu:Int.one
let check_make_or_bottom ~min ~max ~rem ~modu =
match min, max with
| Some mn, Some mx when Int.gt mn mx -> `Bottom
| _, _ -> `Value (check_make ~min ~max ~rem ~modu)
(* ------------------------- 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_itv 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_set s = Set s
let inject_pre_itv ~min ~max ~modu =
let rem = Int.e_rem min modu in
......@@ -205,6 +206,11 @@ let inject_set_or_top = function
| `Set s -> Set s
| `Top (min, max, modu) -> inject_pre_itv ~min ~max ~modu
let inject_set_or_top_or_bottom = function
| `Bottom -> `Bottom
| `Set s -> `Value (Set s)
| `Top (min, max, modu) -> `Value (inject_pre_itv ~min ~max ~modu)
(* TODO: more comment *)
let make_top_from_set s =
......@@ -249,8 +255,6 @@ let max_ge_elt max elt =
| 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
......@@ -260,7 +264,7 @@ let contains_zero = function
let contains_non_zero = function
| Itv _ -> true (* at least two values *)
| Set _ as s -> not (is_zero s || is_bottom s)
| Set _ as s -> not (is_zero s)
let fold_int f v acc =
match v with
......@@ -352,14 +356,14 @@ let diff_if_one value rem =
begin
let v = Int_set.min s in
match value with
| Set s -> inject_set_or_bottom (Int_set.remove s v)
| Set s -> Int_set.remove s v >>-: fun s -> Set s
| 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
check_make_or_bottom ~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
check_make_or_bottom ~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 ->
......@@ -372,10 +376,10 @@ let diff_if_one value rem =
r := Int.add corrected_c modu;
corrected_c)
in
Set (Int_set.inject_array array !small_cardinal)
| _, _ -> value
`Value (Set (Int_set.inject_array array !small_cardinal))
| _, _ -> `Value value
end
| _ -> value
| _ -> `Value value
let diff value rem =
log_imprecision "Ival.diff";
......@@ -441,17 +445,17 @@ let link v1 v2 =
check_make ~min ~max ~rem ~modu
let meet v1 v2 =
if v1 == v2 then v1 else
if v1 == v2 then `Value 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)
| Itv i1, Itv i2 -> Int_interval.meet i1 i2 >>-: inject_itv
| Set s1 , Set s2 -> Int_set.meet s1 s2 >>-: inject_set
| Set s, Itv itv
| Itv itv, Set s ->
inject_set_or_bottom (Int_set.filter (fun i -> Int_interval.mem i itv) s)
Int_set.filter (fun i -> Int_interval.mem i itv) s >>-: inject_set
let narrow v1 v2 =
match v1, v2 with
| Set s1, Set s2 -> inject_set_or_bottom (Int_set.narrow s1 s2)
| Set s1, Set s2 -> Int_set.narrow s1 s2 >>-: inject_set
| (Itv _| Set _), (Itv _ | Set _) -> meet v1 v2 (* meet is exact *)
let widen widen_hints t1 t2 =
......@@ -461,12 +465,12 @@ let widen widen_hints t1 t2 =
| 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))
inject_itv (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 *)
| Itv _, Itv _ -> not (meet v1 v2 = `Bottom) (* 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
......@@ -483,28 +487,23 @@ let add v1 v2 =
| 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
assert (l > 0);
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 s1, Set s2 -> `Value (inject_set_or_top (Int_set.add_under s1 s2))
| Itv i1, Itv i2 -> Int_interval.add_under i1 i2 >>-: inject_itv
| 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
assert (l > 0);
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. *)
`Value (Itv (Int_interval.add_singleton_int (Int_set.min s) i))
let neg = function
| Set s -> Set (Int_set.neg s)
......@@ -522,21 +521,23 @@ let scale f v =
| 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 =
let scale_div ~pos f v =
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)
| Set s -> Set (Int_set.scale_div ~pos f s)
| Itv i -> inject_itv (Int_interval.scale_div ~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
let scale_div_or_bottom ~pos f v =
if Int.is_zero f then `Bottom else `Value (scale_div ~pos f v)
(* 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
assert (not (Int.is_zero f));
match v with
| Set s -> `Value (Set (Int_set.scale_div ~pos f s))
| Itv i -> Int_interval.scale_div_under ~pos f i >>-: inject_itv
let mul v1 v2 =
if is_one v1 then v2
......@@ -548,9 +549,8 @@ let mul v1 v2 =
| Itv i1, Itv i2 -> Itv (Int_interval.mul i1 i2)