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

[Ival] Implements complement_under in int_interval and int_set.

parent 77f80af0
...@@ -415,6 +415,23 @@ let cardinal_zero_or_one t = ...@@ -415,6 +415,23 @@ let cardinal_zero_or_one t =
let diff v _ = `Value v let diff v _ = `Value v
let diff_if_one v _ = `Value v let diff_if_one v _ = `Value v
let complement_under ~min ~max t =
let inject_range min max =
if Int.le min max
then `Value (inject_range (Some min) (Some max))
else `Bottom
in
match t.min, t.max with
| None, None -> `Bottom
| Some b, None -> inject_range min (Int.pred b)
| None, Some e -> inject_range (Int.succ e) max
| Some b, Some e ->
let delta_min = Int.sub b min in
let delta_max = Int.sub max e in
if Int.le delta_min delta_max
then inject_range (Int.succ e) max
else inject_range min (Int.pred b)
let fold_int ?(increasing=true) f t acc = let fold_int ?(increasing=true) f t acc =
match t.min, t.max with match t.min, t.max with
| None, _ | _, None -> raise Error_Top | None, _ | _, None -> raise Error_Top
......
...@@ -60,6 +60,10 @@ val mem: Integer.t -> t -> bool ...@@ -60,6 +60,10 @@ val mem: Integer.t -> t -> bool
Returns [None] if the interval represents an infinite number of integers. *) Returns [None] if the interval represents an infinite number of integers. *)
val cardinal: t -> Integer.t option 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.} *) (** {2 Interval semantics.} *)
(** See {!Int_val} for more details. *) (** See {!Int_val} for more details. *)
......
...@@ -586,6 +586,29 @@ let remove s v = ...@@ -586,6 +586,29 @@ let remove s v =
`Value (share_array r l) `Value (share_array r l)
else `Value s else `Value s
let complement_under ~min ~max set =
let l = Array.length set in
let get idx =
if idx < 0 then Int.pred min
else if idx >= l then Int.succ max
else set.(idx)
in
let index = ref (-1) in
let max_delta = ref Int.zero in
for i = 0 to l do
let delta = Int.pred (Int.sub (get i) (get (i-1))) in
if Int.gt delta !max_delta then begin
index := i;
max_delta := delta
end
done;
let b, e = Int.succ (get (!index-1)), Int.pred (get !index) in
let card = Int.(to_int (succ (sub e b))) in
if card <= 0 then `Bottom
else if card <= !small_cardinal
then `Set (Array.init card (fun i -> Int.add b (Int.of_int i)))
else `Top (b, e, Int.one)
(* ------------------------------ Arithmetics ------------------------------- *) (* ------------------------------ Arithmetics ------------------------------- *)
let add_singleton = apply_bin_1_strict_incr Int.add let add_singleton = apply_bin_1_strict_incr Int.add
......
...@@ -106,6 +106,8 @@ val meet: t -> t -> t or_bottom ...@@ -106,6 +106,8 @@ val meet: t -> t -> t or_bottom
val narrow: t -> t -> t or_bottom val narrow: t -> t -> t or_bottom
val intersects: t -> t -> bool val intersects: t -> t -> bool
val diff_if_one: t -> t -> t or_bottom val diff_if_one: t -> t -> t or_bottom
val complement_under:
min:Integer.t -> max:Integer.t -> t -> set_or_top_or_bottom
(** {2 Semantics.} *) (** {2 Semantics.} *)
......
...@@ -431,6 +431,16 @@ let intersects v1 v2 = ...@@ -431,6 +431,16 @@ let intersects v1 v2 =
| Set s, Itv itv | Itv itv, Set s -> | Set s, Itv itv | Itv itv, Set s ->
Int_set.exists (fun i -> Int_interval.mem i itv) s Int_set.exists (fun i -> Int_interval.mem i itv) s
let complement_under ~size ~signed i =
let max = Int.two_power_of_int (if signed then size - 1 else size) in
let min = if signed then Int.neg max else Int.zero in
let max = Int.pred max in
match i with
| Set set ->
inject_set_or_top_or_bottom (Int_set.complement_under ~min ~max set)
| Itv itv ->
Int_interval.complement_under ~min ~max itv >>-: inject_itv
(* -------------------------------- Arithmetics ----------------------------- *) (* -------------------------------- Arithmetics ----------------------------- *)
let add_singleton i = function let add_singleton i = function
......
...@@ -172,6 +172,10 @@ val all_values: size:Integer.t -> t -> bool ...@@ -172,6 +172,10 @@ val all_values: size:Integer.t -> t -> bool
val overlaps: partial:bool -> size:Integer.t -> t -> t -> bool val overlaps: partial:bool -> size:Integer.t -> t -> t -> bool
val complement_under: size:int -> signed:bool -> t -> t or_bottom
(** Returns an under-approximation of the integers of the given size and
signedness that are *not* represented by the given value. *)
(** Iterates on all integers represented by an abstraction, in increasing order (** Iterates on all integers represented by an abstraction, in increasing order
by default. If [increasing] is set to false, iterate by decreasing order. by default. If [increasing] is set to false, iterate by decreasing order.
@raise Abstract_interp.Error_Top if the abstraction is unbounded. *) @raise Abstract_interp.Error_Top if the abstraction is unbounded. *)
......
...@@ -21,6 +21,7 @@ ...@@ -21,6 +21,7 @@
(**************************************************************************) (**************************************************************************)
open Abstract_interp open Abstract_interp
open Bottom.Type
let emitter = Lattice_messages.register "Ival" let emitter = Lattice_messages.register "Ival"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s let log_imprecision s = Lattice_messages.emit_imprecision emitter s
...@@ -356,41 +357,9 @@ let join v1 v2 = ...@@ -356,41 +357,9 @@ let join v1 v2 =
pretty v1 pretty v2 pretty result; *) pretty v1 pretty v2 pretty result; *)
result result
let complement_int_under ~size ~signed i = let complement_int_under ~size ~signed = function
let e = Int.two_power_of_int (if signed then size - 1 else size) in | Bottom | Float _ -> `Bottom
let b = if signed then Int.neg e else Int.zero in | Int i -> Int_val.complement_under ~size ~signed i >>-: fun i -> Int i
let e = Int.pred e in
let inject_range min max = `Value (inject_range (Some min) (Some max)) in
match i with
| Float _ -> `Bottom
| Set [||] -> inject_range b e
| Set set ->
let l = Array.length set in
let array = Array.make (l + 2) Int.zero in
array.(0) <- b;
Array.blit set 0 array 1 l;
array.(l+1) <- e;
let index = ref (-1) in
let max_delta = ref Int.zero in
for i = 0 to l do
let delta = Int.sub array.(i+1) array.(i) in
if Int.gt delta !max_delta then begin
index := i;
max_delta := delta
end
done;
inject_range array.(!index) array.(!index + 1)
| Top (min, max, _rem, _modu) ->
match min, max with
| None, None -> `Bottom
| Some min, None -> inject_range b (Int.pred min)
| None, Some max -> inject_range (Int.succ max) e
| Some min, Some max ->
let delta_min = Int.sub min b in
let delta_max = Int.sub e max in
if Int.le delta_min delta_max
then inject_range (Int.succ max) e
else inject_range b (Int.pred min)
let fold_int f v acc = let fold_int f v acc =
match v with match v with
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment