Library IntSet
Require Import
Coqlib Utf8 String PrintPos ToString
Integers
Maps TreeAl
LatticeSignatures AdomLib
IntervalDomain.
Module P := Tree_Properties( ZTree ).
Definition int_set : Type := ZTree.t unit.
Definition proj (i: int) : Z := Int.unsigned i.
Notation "x ∈ S" := (ZTree.get x S = Some tt): int_set_scope.
Local Open Scope int_set_scope.
Definition Mem (x: int) (S: int_set) := (proj x) ∈ S.
Definition mem x S : { x ∈ S } + { ¬ x ∈ S }.
Notation "x ∈? S" := (mem x S) (at level 19): int_set_scope.
Definition empty : int_set := ZTree.empty _.
Definition forallb (f: Z → bool) (s: int_set) : bool :=
P.for_all s (fun x _ ⇒ f x).
Lemma forallb_forall {f x r} :
forallb f r = true → x ∈ r → f x = true.
Definition of_list' (l: list int) : int_set → int_set :=
List.fold_left
(fun acc i ⇒ ZTree.set (proj i) tt acc)
l.
Definition of_list (l: list int) : int_set :=
of_list' l (ZTree.empty _).
Lemma of_list'_iff : ∀ l acc i, List.In i l ∨ (proj i) ∈ acc ↔ (proj i) ∈ (of_list' l acc).
Lemma of_list_iff : ∀ l i, List.In i l ↔ (proj i) ∈ (of_list l).
Definition fold {A} (f: A → int → A) : int_set → A → A :=
ZTree.fold (fun x y (_:unit) ⇒ f x (Int.repr y)).
Definition as_list (m: int_set) : list int :=
fold (λ l i, i :: l) m nil.
Lemma as_list_iff : ∀ m i, List.In i (as_list m) ↔ ∃ j, j ∈ m ∧ Int.repr j = i.
Definition fs_size (x: int_set) : N :=
ZTree.fold (fun n _ _ ⇒ Nsucc n) x N0.
Definition int_set_LE (x y: int_set) :=
∀ i : Z, i ∈ x → i ∈ y.
Definition int_set_LE_dec (x y: int_set) : { int_set_LE x y } + { ¬ int_set_LE x y }.
Definition is_empty (x: int_set) : bool :=
int_set_LE_dec x (ZTree.empty _).
Lemma is_empty_correct (x: int_set) :
is_empty x = true →
∀ y, ¬ y ∈ x.
Definition singleton (i: int) : int_set := ZTree.set (proj i) tt (ZTree.empty _).
Definition union (x y: int_set) : int_set :=
ZTree.combine
(fun l r ⇒
match l, r with
| None, None ⇒ None
| Some tt, _
| _, Some tt ⇒ Some tt
end) x y.
Lemma union_comm (x y: int_set) : union x y = union y x.
Lemma union_in_l (x y: int_set) :
∀ i: Z, i ∈ x → i ∈ union x y.
Lemma union_in_r (x y: int_set) :
∀ i: Z, i ∈ y → i ∈ union x y.
Definition intersection (x y: int_set) : int_set :=
ZTree.combine
(fun l r ⇒
match l, r with
| Some tt, Some tt ⇒ Some tt
| _, _ ⇒ None
end) x y.
Lemma intersection_correct (x y: int_set) :
∀ i : Z, i ∈ x → i ∈ y → i ∈ intersection x y.
Lemma intersection_exact (x y: int_set) :
∀ i : Z, i ∈ intersection x y → i ∈ x ∧ i ∈ y.
Instance toString : ToString int_set :=
{ to_string x :=
("{ " ++
ZTree.fold
(fun s i _ ⇒ string_of_z i ++ "; " ++ s)
x
"}"
)%string
}.
Coqlib Utf8 String PrintPos ToString
Integers
Maps TreeAl
LatticeSignatures AdomLib
IntervalDomain.
Module P := Tree_Properties( ZTree ).
Definition int_set : Type := ZTree.t unit.
Definition proj (i: int) : Z := Int.unsigned i.
Notation "x ∈ S" := (ZTree.get x S = Some tt): int_set_scope.
Local Open Scope int_set_scope.
Definition Mem (x: int) (S: int_set) := (proj x) ∈ S.
Definition mem x S : { x ∈ S } + { ¬ x ∈ S }.
Notation "x ∈? S" := (mem x S) (at level 19): int_set_scope.
Definition empty : int_set := ZTree.empty _.
Definition forallb (f: Z → bool) (s: int_set) : bool :=
P.for_all s (fun x _ ⇒ f x).
Lemma forallb_forall {f x r} :
forallb f r = true → x ∈ r → f x = true.
Definition of_list' (l: list int) : int_set → int_set :=
List.fold_left
(fun acc i ⇒ ZTree.set (proj i) tt acc)
l.
Definition of_list (l: list int) : int_set :=
of_list' l (ZTree.empty _).
Lemma of_list'_iff : ∀ l acc i, List.In i l ∨ (proj i) ∈ acc ↔ (proj i) ∈ (of_list' l acc).
Lemma of_list_iff : ∀ l i, List.In i l ↔ (proj i) ∈ (of_list l).
Definition fold {A} (f: A → int → A) : int_set → A → A :=
ZTree.fold (fun x y (_:unit) ⇒ f x (Int.repr y)).
Definition as_list (m: int_set) : list int :=
fold (λ l i, i :: l) m nil.
Lemma as_list_iff : ∀ m i, List.In i (as_list m) ↔ ∃ j, j ∈ m ∧ Int.repr j = i.
Definition fs_size (x: int_set) : N :=
ZTree.fold (fun n _ _ ⇒ Nsucc n) x N0.
Definition int_set_LE (x y: int_set) :=
∀ i : Z, i ∈ x → i ∈ y.
Definition int_set_LE_dec (x y: int_set) : { int_set_LE x y } + { ¬ int_set_LE x y }.
Definition is_empty (x: int_set) : bool :=
int_set_LE_dec x (ZTree.empty _).
Lemma is_empty_correct (x: int_set) :
is_empty x = true →
∀ y, ¬ y ∈ x.
Definition singleton (i: int) : int_set := ZTree.set (proj i) tt (ZTree.empty _).
Definition union (x y: int_set) : int_set :=
ZTree.combine
(fun l r ⇒
match l, r with
| None, None ⇒ None
| Some tt, _
| _, Some tt ⇒ Some tt
end) x y.
Lemma union_comm (x y: int_set) : union x y = union y x.
Lemma union_in_l (x y: int_set) :
∀ i: Z, i ∈ x → i ∈ union x y.
Lemma union_in_r (x y: int_set) :
∀ i: Z, i ∈ y → i ∈ union x y.
Definition intersection (x y: int_set) : int_set :=
ZTree.combine
(fun l r ⇒
match l, r with
| Some tt, Some tt ⇒ Some tt
| _, _ ⇒ None
end) x y.
Lemma intersection_correct (x y: int_set) :
∀ i : Z, i ∈ x → i ∈ y → i ∈ intersection x y.
Lemma intersection_exact (x y: int_set) :
∀ i : Z, i ∈ intersection x y → i ∈ x ∧ i ∈ y.
Instance toString : ToString int_set :=
{ to_string x :=
("{ " ++
ZTree.fold
(fun s i _ ⇒ string_of_z i ++ "; " ++ s)
x
"}"
)%string
}.
Returns the minimal and maximal elements. None if empty.
Definition min_max (interp: Z → Z) (x: int_set) : option (Z × Z) :=
ZTree.fold
(fun m k _ ⇒
match m with
| None ⇒ Some (k,k)
| Some (l, r) ⇒
let k' := interp k in
let l' := interp l in
let r' := interp r in
if Z_le_gt_dec k' l' then Some (k, r)
else if Z_le_gt_dec r' k' then Some (l, k)
else m
end)
x
None.
Lemma min_max_spec (interp: Z → Z) (x: int_set) :
match min_max interp x with
| None ⇒ is_empty x = true
| Some (l,r) ⇒ l ∈ x ∧ r ∈ x ∧ ∀ i, i ∈ x → interp l ≤ interp i ≤ interp r
end.
Definition fint_set : Type := int_set+⊤.
Definition fempty : fint_set := Just (ZTree.empty _).
Definition fs_widen (old new: int_set) : fint_set :=
if int_set_LE_dec new old
then Just old
else
let j : int_set := union old new in
if N.leb 10%N (fs_size j)
then All
else Just j.
Instance fs_gamma : gamma_op fint_set int := fun x ⇒
match x with
| All ⇒ fun _ ⇒ True
| Just s ⇒ fun i ⇒ proj i ∈ s
end.
Lemma fempty_gamma i : ¬ fs_gamma fempty i.
Definition int_set_pl : pre_lattice int_set :=
{| pl_leb x y := int_set_LE_dec x y
; pl_join x y := Just (union x y)
; pl_widen x y := fs_widen x y
|}.
Instance int_set_wl : weak_lattice fint_set :=
weak_lattice_of_pre_lattice int_set_pl.
Lemma int_set_adom : adom fint_set int int_set_wl fs_gamma.
Definition fs_reduce (x: int_set) : fint_set+⊥ :=
if is_empty x
then Bot
else NotBot (Just x).
Definition fs_meet (x y: fint_set) : fint_set+⊥ :=
match x, y with
| All, _ ⇒ NotBot y
| _, All ⇒ NotBot x
| Just x', Just y' ⇒ fs_reduce (intersection x' y')
end.
Lemma fs_meet_sound : ∀ x y: fint_set, (γ x) ∩ (γ y) ⊆ γ (fs_meet x y).
Lemma fs_meet_glb : ∀ x y: fint_set, γ (fs_meet x y) ⊆ (γ x) ∩ (γ y).
Definition fs_const : int → fint_set := @Just _ ∘ singleton.
Definition fs_booleans : fint_set :=
Just (union (singleton Int.zero) (singleton Int.one)).
Definition map (f: Z → Z) (s: int_set) : int_set :=
ZTree.fold (fun m k _ ⇒ ZTree.set (f k) tt m) s (ZTree.empty unit).
Lemma map_in f (s: int_set) : ∀ x, x ∈ s → f x ∈ map f s.
Definition fs_unop (op: int → int) : fint_set → fint_set+⊥ :=
fun x ⇒
match x with
| All ⇒ NotBot x
| Just x' ⇒ NotBot (Just (map (fun i ⇒ proj (op (Int.repr i))) x'))
end.
Definition map2 (f: Z → Z → Z) (l r: int_set) : int_set :=
ZTree.fold (fun m i _ ⇒
ZTree.fold (fun m j _ ⇒ ZTree.set (f i j) tt m) r m ) l (ZTree.empty unit).
Lemma map2_in f (l r: int_set) : ∀ x y, x ∈ l → y ∈ r → f x y ∈ map2 f l r.
Definition fs_binop (op: int → int → int) (x: fint_set) (y: fint_set) : fint_set+⊥ :=
match x, y with
| All, _
| _, All ⇒ NotBot All
| Just x', Just y' ⇒ NotBot (Just (map2 (fun a b ⇒ proj (op (Int.repr a) (Int.repr b))) x' y'))
end.
Definition int_set_unsigned_range (x: int_set) :=
match min_max (fun i ⇒ i) x with
| None ⇒ Bot
| Some (l,r) ⇒ NotBot {| Interval.min := l; Interval.max := r |}
end.
Definition int_set_signed_range (x: int_set) :=
let interp := Int.signed ∘ Int.repr in
match min_max interp x with
| None ⇒ Bot
| Some (l,r) ⇒ NotBot {| Interval.min := interp l; Interval.max := interp r |}
end.
Definition fs_range (x: fint_set) :=
match x with
| All ⇒ fun s ⇒ NotBot (match s with Signed ⇒ Interval.top | Unsigned ⇒ Interval.utop end)
| Just x' ⇒ fun s ⇒
match s with
| Signed ⇒ int_set_signed_range x'
| Unsigned ⇒ int_set_unsigned_range x'
end
end.
Definition fs_is_in_itv (l r: int) (x: fint_set) : bool :=
match x with
| All ⇒ false
| Just x' ⇒ forallb (fun i ⇒ negb (Int.lt r (Int.repr i)) && negb (Int.lt (Int.repr i) l)) x'
end.
ZTree.fold
(fun m k _ ⇒
match m with
| None ⇒ Some (k,k)
| Some (l, r) ⇒
let k' := interp k in
let l' := interp l in
let r' := interp r in
if Z_le_gt_dec k' l' then Some (k, r)
else if Z_le_gt_dec r' k' then Some (l, k)
else m
end)
x
None.
Lemma min_max_spec (interp: Z → Z) (x: int_set) :
match min_max interp x with
| None ⇒ is_empty x = true
| Some (l,r) ⇒ l ∈ x ∧ r ∈ x ∧ ∀ i, i ∈ x → interp l ≤ interp i ≤ interp r
end.
Definition fint_set : Type := int_set+⊤.
Definition fempty : fint_set := Just (ZTree.empty _).
Definition fs_widen (old new: int_set) : fint_set :=
if int_set_LE_dec new old
then Just old
else
let j : int_set := union old new in
if N.leb 10%N (fs_size j)
then All
else Just j.
Instance fs_gamma : gamma_op fint_set int := fun x ⇒
match x with
| All ⇒ fun _ ⇒ True
| Just s ⇒ fun i ⇒ proj i ∈ s
end.
Lemma fempty_gamma i : ¬ fs_gamma fempty i.
Definition int_set_pl : pre_lattice int_set :=
{| pl_leb x y := int_set_LE_dec x y
; pl_join x y := Just (union x y)
; pl_widen x y := fs_widen x y
|}.
Instance int_set_wl : weak_lattice fint_set :=
weak_lattice_of_pre_lattice int_set_pl.
Lemma int_set_adom : adom fint_set int int_set_wl fs_gamma.
Definition fs_reduce (x: int_set) : fint_set+⊥ :=
if is_empty x
then Bot
else NotBot (Just x).
Definition fs_meet (x y: fint_set) : fint_set+⊥ :=
match x, y with
| All, _ ⇒ NotBot y
| _, All ⇒ NotBot x
| Just x', Just y' ⇒ fs_reduce (intersection x' y')
end.
Lemma fs_meet_sound : ∀ x y: fint_set, (γ x) ∩ (γ y) ⊆ γ (fs_meet x y).
Lemma fs_meet_glb : ∀ x y: fint_set, γ (fs_meet x y) ⊆ (γ x) ∩ (γ y).
Definition fs_const : int → fint_set := @Just _ ∘ singleton.
Definition fs_booleans : fint_set :=
Just (union (singleton Int.zero) (singleton Int.one)).
Definition map (f: Z → Z) (s: int_set) : int_set :=
ZTree.fold (fun m k _ ⇒ ZTree.set (f k) tt m) s (ZTree.empty unit).
Lemma map_in f (s: int_set) : ∀ x, x ∈ s → f x ∈ map f s.
Definition fs_unop (op: int → int) : fint_set → fint_set+⊥ :=
fun x ⇒
match x with
| All ⇒ NotBot x
| Just x' ⇒ NotBot (Just (map (fun i ⇒ proj (op (Int.repr i))) x'))
end.
Definition map2 (f: Z → Z → Z) (l r: int_set) : int_set :=
ZTree.fold (fun m i _ ⇒
ZTree.fold (fun m j _ ⇒ ZTree.set (f i j) tt m) r m ) l (ZTree.empty unit).
Lemma map2_in f (l r: int_set) : ∀ x y, x ∈ l → y ∈ r → f x y ∈ map2 f l r.
Definition fs_binop (op: int → int → int) (x: fint_set) (y: fint_set) : fint_set+⊥ :=
match x, y with
| All, _
| _, All ⇒ NotBot All
| Just x', Just y' ⇒ NotBot (Just (map2 (fun a b ⇒ proj (op (Int.repr a) (Int.repr b))) x' y'))
end.
Definition int_set_unsigned_range (x: int_set) :=
match min_max (fun i ⇒ i) x with
| None ⇒ Bot
| Some (l,r) ⇒ NotBot {| Interval.min := l; Interval.max := r |}
end.
Definition int_set_signed_range (x: int_set) :=
let interp := Int.signed ∘ Int.repr in
match min_max interp x with
| None ⇒ Bot
| Some (l,r) ⇒ NotBot {| Interval.min := interp l; Interval.max := interp r |}
end.
Definition fs_range (x: fint_set) :=
match x with
| All ⇒ fun s ⇒ NotBot (match s with Signed ⇒ Interval.top | Unsigned ⇒ Interval.utop end)
| Just x' ⇒ fun s ⇒
match s with
| Signed ⇒ int_set_signed_range x'
| Unsigned ⇒ int_set_unsigned_range x'
end
end.
Definition fs_is_in_itv (l r: int) (x: fint_set) : bool :=
match x with
| All ⇒ false
| Just x' ⇒ forallb (fun i ⇒ negb (Int.lt r (Int.repr i)) && negb (Int.lt (Int.repr i) l)) x'
end.