diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index a6eb3d32bead52571d35d58dfe6fd631b93c04c8..ba4889551ba81a2219bc360683ff6261b3d24978 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -415,6 +415,23 @@ let cardinal_zero_or_one t =
let diff 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 =
match t.min, t.max with
| None, _ | _, None -> raise Error_Top
diff --git a/src/kernel_services/abstract_interp/int_interval.mli b/src/kernel_services/abstract_interp/int_interval.mli
index 1ff9f2500762b8cd68048f483e63c7041dcf0a05..074fa0f07d2ceed5e2747658d8fb7eb755b5e172 100644
--- a/src/kernel_services/abstract_interp/int_interval.mli
+++ b/src/kernel_services/abstract_interp/int_interval.mli
@@ -60,6 +60,10 @@ val mem: Integer.t -> t -> bool
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. *)
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index e45dc95743f1d7bcaa62134a90ccab6597799470..76786297af9b4e4694a6eec8bf0506067bb9d344 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -586,6 +586,29 @@ let remove s v =
`Value (share_array r l)
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 ------------------------------- *)
let add_singleton = apply_bin_1_strict_incr Int.add
diff --git a/src/kernel_services/abstract_interp/int_set.mli b/src/kernel_services/abstract_interp/int_set.mli
index 5157d4eaba9cead2269f23a2386e8a782a2adc87..4c0a12ca1f0299298791031ce5de17ae88bd8a28 100644
--- a/src/kernel_services/abstract_interp/int_set.mli
+++ b/src/kernel_services/abstract_interp/int_set.mli
@@ -106,6 +106,8 @@ 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 complement_under:
+ min:Integer.t -> max:Integer.t -> t -> set_or_top_or_bottom
(** {2 Semantics.} *)
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 60c1c969c402fb6221d716482b743b1248aa650c..a62c3dcb1c882dd5f6e6ff8f28537fe83f5e20ba 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -431,6 +431,16 @@ let intersects v1 v2 =
| Set s, Itv itv | Itv itv, Set 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 ----------------------------- *)
let add_singleton i = function
diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli
index 2f760b0c025d45340e1c81599e018c70ddd5d4cb..8187397e75d8a7adf819502afcc0095a1715074a 100644
--- a/src/kernel_services/abstract_interp/int_val.mli
+++ b/src/kernel_services/abstract_interp/int_val.mli
@@ -172,6 +172,10 @@ val all_values: size:Integer.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
by default. If [increasing] is set to false, iterate by decreasing order.
@raise Abstract_interp.Error_Top if the abstraction is unbounded. *)
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index a0601a432396347902a0cd2058a4f81537b5fc3b..f635675a6caca1cc0abfd15a0d2bf4c64aba22d0 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Abstract_interp
+open Bottom.Type
let emitter = Lattice_messages.register "Ival"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s
@@ -356,41 +357,9 @@ let join v1 v2 =
pretty v1 pretty v2 pretty result; *)
result
-let complement_int_under ~size ~signed i =
- let e = Int.two_power_of_int (if signed then size - 1 else size) in
- let b = if signed then Int.neg e else Int.zero in
- 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 complement_int_under ~size ~signed = function
+ | Bottom | Float _ -> `Bottom
+ | Int i -> Int_val.complement_under ~size ~signed i >>-: fun i -> Int i
let fold_int f v acc =
match v with