Library StridedIntervals
Require Import
Utf8 Coqlib String PrintPos ToString
Integers
aritmo DLib
LatticeSignatures
AbMachineNonrel AdomLib
DebugAbMachineNonrel
IntervalDomain.
Require Psatz.
Utf8 Coqlib String PrintPos ToString
Integers
aritmo DLib
LatticeSignatures
AbMachineNonrel AdomLib
DebugAbMachineNonrel
IntervalDomain.
Require Psatz.
Numerical domain of Strided Intervals.
Reference: Gogul Balakrishnan. “WYSINWYX: what you see is not what you eXecute.”
PhD thesis. Madison: University of Wisconsin, 2007.
Abstract values are triples (s, l, u) representing all integers i, s.t.
l ≤ i ≤ u ∧ i ≡ l (mod s).
It is supposed to precisely capture common families of addresses,
e.g., contiguous cells in an array.
Since the congruence domain is not very precise on machine integers (moduli must
be powers of two since any operation might overflow), this domain is strictly
more precise than the reduced product of intervals and congruences on machine integers.
Moreover, it is more precise than the projection to machine integers of the reduced
product of the congruence domain on Z and the interval domain on Z in case of overflows.
Data type.
Not a dependent type. In particular the type does neither enforce that bounds
are correctly ordered nor that the upper bound is tight.
However, some operations assume it (they are otherwise unprecise).
The operations that would be unsound do the appropriate checks.
Record strided_interval : Type :=
{ si_stride : N
; si_low_bound: Z
; si_up_bound : Z
}.
Definition si_valid (s: strided_interval) : Prop :=
s.(si_low_bound) ≤ s.(si_up_bound).
Definition si_reduced (s: strided_interval) : Prop :=
(s.(si_low_bound) ≡ s.(si_up_bound) [ s.(si_stride) ])
∧ (s.(si_low_bound) = s.(si_up_bound) → s.(si_stride) = N0).
Definition si_LE (x y: strided_interval) : Prop :=
y.(si_low_bound) ≤ x.(si_low_bound)
∧ x.(si_up_bound) ≤ y.(si_up_bound)
∧ ( y.(si_stride) | x.(si_stride) )
∧ ( x.(si_low_bound) ≡ y.(si_low_bound) [y.(si_stride)] ).
Definition si_LE_dec (x y: strided_interval) : { si_LE x y } + { ¬ si_LE x y }.
Definition si_join (x y: strided_interval) : strided_interval :=
{| si_stride := N.gcd (N.gcd x.(si_stride) y.(si_stride))
(Nabs_diff x.(si_low_bound) y.(si_low_bound))
; si_low_bound := Zmin x.(si_low_bound) y.(si_low_bound)
; si_up_bound := Zmax x.(si_up_bound) y.(si_up_bound)
|}.
Program Definition si_meet (x y: strided_interval) : strided_interval+⊥ :=
match congr_dec (N.gcd x.(si_stride) y.(si_stride)) x.(si_low_bound) y.(si_low_bound) return _ with
| left H ⇒
let A := Zmax x.(si_low_bound) y.(si_low_bound) in
let B := Zmin x.(si_up_bound) y.(si_up_bound) in
let m := N.lcm x.(si_stride) y.(si_stride) in
if Z_zerop m
then
if Z_le_dec A B
then NotBot {| si_stride := m; si_low_bound := A; si_up_bound := A |}
else Bot
else
let (n, K) := rem_eqn_particular x.(si_low_bound) y.(si_low_bound)
x.(si_stride) y.(si_stride) _ _ _
in
let l := A + ((n - A) mod m) in
let u := B - ((B - n) mod m) in
match Z_dec l u with
| inleft (left LT) ⇒ NotBot {| si_stride := m; si_low_bound := l; si_up_bound := u |}
| inleft (right GT) ⇒ Bot
| inright EQ ⇒ NotBot {| si_stride := 0%N; si_low_bound := l; si_up_bound := u |}
end
| right _ ⇒ Bot
end.
Lemma si_meet_valid x y :
match si_meet x y with
| NotBot z ⇒ si_valid z
| Bot ⇒ True
end.
Lemma si_meet_reduced x y :
match si_meet x y with
| NotBot z ⇒ si_reduced z
| Bot ⇒ True
end.
Definition si_size (x : strided_interval) : N :=
match Z_le_dec x.(si_low_bound) x.(si_up_bound) with
| left LE ⇒
match x.(si_stride) with
| N0 ⇒ 1%N
| Npos s ⇒ N_of_Z ((x.(si_up_bound) - x.(si_low_bound)) / (Zpos s) + 1)
end
| right GT ⇒ N0
end.
Section Gamma.
Variable interp : int → Z.
Local Coercion interp : int >-> Z.
Variables min max : Z.
Hypothesis range : ∀ i : int, min ≤ i ≤ max.
Hypothesis interpz : interp Int.zero = 0.
Hypothesis interp_inj : ∀ x y : int, x ≠ y → interp x ≠ interp y.
Definition si_top : strided_interval :=
{| si_stride := 1
; si_low_bound := min
; si_up_bound := max
|}.
Lemma si_top_reduced (H: min ≠ max) : si_reduced si_top.
Instance si_gamma : gamma_op strided_interval int := fun x ⇒
fun i ⇒ x.(si_low_bound) ≤ i ≤ x.(si_up_bound)
∧ x.(si_low_bound) ≡ i [ x.(si_stride) ].
Lemma si_gamma_monotone (x y: strided_interval) :
si_LE x y → si_gamma x ⊆ si_gamma y.
Lemma si_gamma_top (i: int) : si_gamma si_top i.
Lemma si_join_sound (x y: strided_interval) :
si_gamma x ∪ si_gamma y ⊆ si_gamma (si_join x y).
Definition si_widen (x y: strided_interval) : strided_interval :=
match Interval.widen_heuristic (Interval.ITV x.(si_low_bound) x.(si_up_bound))
(Interval.ITV y.(si_low_bound) y.(si_up_bound)) with
| Interval.ITV a b ⇒
if zeq a b
then {| si_stride := N0; si_low_bound := a; si_up_bound := b |}
else {| si_stride := 1%N; si_low_bound := a; si_up_bound := b |}
end.
Lemma si_widen_reduced x y :
si_reduced (si_widen x y).
Instance toString : ToString strided_interval :=
{ to_string i :=
if si_LE_dec si_top i
then "⊤"%string
else
match i.(si_stride) with
| N0 ⇒ string_of_z i.(si_low_bound)
| s ⇒
(string_of_z (Z_of_N s)
++ "[" ++ string_of_z i.(si_low_bound) ++ "; "
++ string_of_z i.(si_up_bound) ++ "]")%string
end
}.
Instance si_wlat : weak_lattice strided_interval :=
{| leb x y := si_LE_dec x y
; top := si_top
; join := si_join
; widen := si_widen
|}.
Lemma si_adom : adom strided_interval int si_wlat si_gamma.
Lemma si_meet_sound (x y: strided_interval) :
si_gamma x ∩ si_gamma y ⊆ match si_meet x y with NotBot z ⇒ si_gamma z | Bot ⇒ ∅ end.
Definition si_const (i: int) : strided_interval :=
{| si_stride := 0%N; si_low_bound := i; si_up_bound := i |}.
Lemma si_const_sound (i: int) : si_gamma (si_const i) i.
Lemma si_const_valid i : si_valid (si_const i).
Lemma si_const_reduced i : si_reduced (si_const i).
Definition si_add (x y: strided_interval) : strided_interval :=
let l := x.(si_low_bound) + y.(si_low_bound) in
let u := x.(si_up_bound) + y.(si_up_bound) in
if Z_le_dec min l
then
if Z_le_dec l max
then
if Z_le_dec u max
then {| si_stride := N.gcd x.(si_stride) y.(si_stride)
; si_low_bound := l
; si_up_bound := u
|}
else si_top
else
{| si_stride := N.gcd x.(si_stride) y.(si_stride)
; si_low_bound := l - Int.modulus
; si_up_bound := u - Int.modulus
|}
else
if Z_le_dec min u
then si_top
else
{| si_stride := N.gcd x.(si_stride) y.(si_stride)
; si_low_bound := l + Int.modulus
; si_up_bound := u + Int.modulus
|}.
Lemma si_add_valid x y :
si_valid x →
si_valid y →
si_valid (si_add x y).
Lemma si_add_reduced (H: min ≠ max) x y :
si_valid x →
si_valid y →
si_reduced x →
si_reduced y →
si_reduced (si_add x y).
Hint Resolve congr_plus_compat.
Definition si_is_in_itv (u v: int) (x: strided_interval) : bool :=
Z_le_dec u x.(si_low_bound) && Z_le_dec x.(si_up_bound) v.
Definition si_contains (i: int) (x: strided_interval) : bool :=
match si_meet x (si_const i) with
| Bot ⇒ false
| NotBot _ ⇒ true
end.
Function si_concretize_aux (s: positive) (base: Z) (nb: Z) (acc: list Z) {measure Zabs_nat nb} : list Z :=
let nb := nb - Zpos s in
match nb with
| Zpos _ | Z0 ⇒ si_concretize_aux s base nb (base + nb :: acc)
| Zneg _ ⇒ acc
end.
Definition si_concretize (x: strided_interval) : list Z :=
match Z_le_dec x.(si_low_bound) x.(si_up_bound) with
| left LE ⇒
match x.(si_stride) with
| N0 ⇒ x.(si_low_bound) :: nil
| Npos s ⇒
si_concretize_aux s x.(si_low_bound) ((x.(si_up_bound) - x.(si_low_bound)) / Zpos s × Zpos s + Zpos s) nil
end
| right GT ⇒ nil
end.
Lemma si_concretize_sound_aux :
∀ acc nb s base (i:int),
nb ≡ 0 [Zpos s] →
In (i:Z) (si_concretize_aux s base nb acc) ↔
In (i:Z) acc ∨ (base ≤ i ≤ base + nb - Zpos s ∧ base ≡ i [Zpos s]).
Lemma si_concretize_exact (x: strided_interval) :
∀ i : int, List.In (i:Z) (si_concretize x) ↔ γ x i.
End Gamma.
{ si_stride : N
; si_low_bound: Z
; si_up_bound : Z
}.
Definition si_valid (s: strided_interval) : Prop :=
s.(si_low_bound) ≤ s.(si_up_bound).
Definition si_reduced (s: strided_interval) : Prop :=
(s.(si_low_bound) ≡ s.(si_up_bound) [ s.(si_stride) ])
∧ (s.(si_low_bound) = s.(si_up_bound) → s.(si_stride) = N0).
Definition si_LE (x y: strided_interval) : Prop :=
y.(si_low_bound) ≤ x.(si_low_bound)
∧ x.(si_up_bound) ≤ y.(si_up_bound)
∧ ( y.(si_stride) | x.(si_stride) )
∧ ( x.(si_low_bound) ≡ y.(si_low_bound) [y.(si_stride)] ).
Definition si_LE_dec (x y: strided_interval) : { si_LE x y } + { ¬ si_LE x y }.
Definition si_join (x y: strided_interval) : strided_interval :=
{| si_stride := N.gcd (N.gcd x.(si_stride) y.(si_stride))
(Nabs_diff x.(si_low_bound) y.(si_low_bound))
; si_low_bound := Zmin x.(si_low_bound) y.(si_low_bound)
; si_up_bound := Zmax x.(si_up_bound) y.(si_up_bound)
|}.
Program Definition si_meet (x y: strided_interval) : strided_interval+⊥ :=
match congr_dec (N.gcd x.(si_stride) y.(si_stride)) x.(si_low_bound) y.(si_low_bound) return _ with
| left H ⇒
let A := Zmax x.(si_low_bound) y.(si_low_bound) in
let B := Zmin x.(si_up_bound) y.(si_up_bound) in
let m := N.lcm x.(si_stride) y.(si_stride) in
if Z_zerop m
then
if Z_le_dec A B
then NotBot {| si_stride := m; si_low_bound := A; si_up_bound := A |}
else Bot
else
let (n, K) := rem_eqn_particular x.(si_low_bound) y.(si_low_bound)
x.(si_stride) y.(si_stride) _ _ _
in
let l := A + ((n - A) mod m) in
let u := B - ((B - n) mod m) in
match Z_dec l u with
| inleft (left LT) ⇒ NotBot {| si_stride := m; si_low_bound := l; si_up_bound := u |}
| inleft (right GT) ⇒ Bot
| inright EQ ⇒ NotBot {| si_stride := 0%N; si_low_bound := l; si_up_bound := u |}
end
| right _ ⇒ Bot
end.
Lemma si_meet_valid x y :
match si_meet x y with
| NotBot z ⇒ si_valid z
| Bot ⇒ True
end.
Lemma si_meet_reduced x y :
match si_meet x y with
| NotBot z ⇒ si_reduced z
| Bot ⇒ True
end.
Definition si_size (x : strided_interval) : N :=
match Z_le_dec x.(si_low_bound) x.(si_up_bound) with
| left LE ⇒
match x.(si_stride) with
| N0 ⇒ 1%N
| Npos s ⇒ N_of_Z ((x.(si_up_bound) - x.(si_low_bound)) / (Zpos s) + 1)
end
| right GT ⇒ N0
end.
Section Gamma.
Variable interp : int → Z.
Local Coercion interp : int >-> Z.
Variables min max : Z.
Hypothesis range : ∀ i : int, min ≤ i ≤ max.
Hypothesis interpz : interp Int.zero = 0.
Hypothesis interp_inj : ∀ x y : int, x ≠ y → interp x ≠ interp y.
Definition si_top : strided_interval :=
{| si_stride := 1
; si_low_bound := min
; si_up_bound := max
|}.
Lemma si_top_reduced (H: min ≠ max) : si_reduced si_top.
Instance si_gamma : gamma_op strided_interval int := fun x ⇒
fun i ⇒ x.(si_low_bound) ≤ i ≤ x.(si_up_bound)
∧ x.(si_low_bound) ≡ i [ x.(si_stride) ].
Lemma si_gamma_monotone (x y: strided_interval) :
si_LE x y → si_gamma x ⊆ si_gamma y.
Lemma si_gamma_top (i: int) : si_gamma si_top i.
Lemma si_join_sound (x y: strided_interval) :
si_gamma x ∪ si_gamma y ⊆ si_gamma (si_join x y).
Definition si_widen (x y: strided_interval) : strided_interval :=
match Interval.widen_heuristic (Interval.ITV x.(si_low_bound) x.(si_up_bound))
(Interval.ITV y.(si_low_bound) y.(si_up_bound)) with
| Interval.ITV a b ⇒
if zeq a b
then {| si_stride := N0; si_low_bound := a; si_up_bound := b |}
else {| si_stride := 1%N; si_low_bound := a; si_up_bound := b |}
end.
Lemma si_widen_reduced x y :
si_reduced (si_widen x y).
Instance toString : ToString strided_interval :=
{ to_string i :=
if si_LE_dec si_top i
then "⊤"%string
else
match i.(si_stride) with
| N0 ⇒ string_of_z i.(si_low_bound)
| s ⇒
(string_of_z (Z_of_N s)
++ "[" ++ string_of_z i.(si_low_bound) ++ "; "
++ string_of_z i.(si_up_bound) ++ "]")%string
end
}.
Instance si_wlat : weak_lattice strided_interval :=
{| leb x y := si_LE_dec x y
; top := si_top
; join := si_join
; widen := si_widen
|}.
Lemma si_adom : adom strided_interval int si_wlat si_gamma.
Lemma si_meet_sound (x y: strided_interval) :
si_gamma x ∩ si_gamma y ⊆ match si_meet x y with NotBot z ⇒ si_gamma z | Bot ⇒ ∅ end.
Definition si_const (i: int) : strided_interval :=
{| si_stride := 0%N; si_low_bound := i; si_up_bound := i |}.
Lemma si_const_sound (i: int) : si_gamma (si_const i) i.
Lemma si_const_valid i : si_valid (si_const i).
Lemma si_const_reduced i : si_reduced (si_const i).
Definition si_add (x y: strided_interval) : strided_interval :=
let l := x.(si_low_bound) + y.(si_low_bound) in
let u := x.(si_up_bound) + y.(si_up_bound) in
if Z_le_dec min l
then
if Z_le_dec l max
then
if Z_le_dec u max
then {| si_stride := N.gcd x.(si_stride) y.(si_stride)
; si_low_bound := l
; si_up_bound := u
|}
else si_top
else
{| si_stride := N.gcd x.(si_stride) y.(si_stride)
; si_low_bound := l - Int.modulus
; si_up_bound := u - Int.modulus
|}
else
if Z_le_dec min u
then si_top
else
{| si_stride := N.gcd x.(si_stride) y.(si_stride)
; si_low_bound := l + Int.modulus
; si_up_bound := u + Int.modulus
|}.
Lemma si_add_valid x y :
si_valid x →
si_valid y →
si_valid (si_add x y).
Lemma si_add_reduced (H: min ≠ max) x y :
si_valid x →
si_valid y →
si_reduced x →
si_reduced y →
si_reduced (si_add x y).
Hint Resolve congr_plus_compat.
Definition si_is_in_itv (u v: int) (x: strided_interval) : bool :=
Z_le_dec u x.(si_low_bound) && Z_le_dec x.(si_up_bound) v.
Definition si_contains (i: int) (x: strided_interval) : bool :=
match si_meet x (si_const i) with
| Bot ⇒ false
| NotBot _ ⇒ true
end.
Function si_concretize_aux (s: positive) (base: Z) (nb: Z) (acc: list Z) {measure Zabs_nat nb} : list Z :=
let nb := nb - Zpos s in
match nb with
| Zpos _ | Z0 ⇒ si_concretize_aux s base nb (base + nb :: acc)
| Zneg _ ⇒ acc
end.
Definition si_concretize (x: strided_interval) : list Z :=
match Z_le_dec x.(si_low_bound) x.(si_up_bound) with
| left LE ⇒
match x.(si_stride) with
| N0 ⇒ x.(si_low_bound) :: nil
| Npos s ⇒
si_concretize_aux s x.(si_low_bound) ((x.(si_up_bound) - x.(si_low_bound)) / Zpos s × Zpos s + Zpos s) nil
end
| right GT ⇒ nil
end.
Lemma si_concretize_sound_aux :
∀ acc nb s base (i:int),
nb ≡ 0 [Zpos s] →
In (i:Z) (si_concretize_aux s base nb acc) ↔
In (i:Z) acc ∨ (base ≤ i ≤ base + nb - Zpos s ∧ base ≡ i [Zpos s]).
Lemma si_concretize_exact (x: strided_interval) :
∀ i : int, List.In (i:Z) (si_concretize x) ↔ γ x i.
End Gamma.
Signed SI
Instance ssi_wlat : weak_lattice strided_interval :=
si_wlat Int.min_signed Int.max_signed.
Instance ssi_gamma : gamma_op strided_interval int :=
si_gamma Int.signed.
Lemma ssi_adom : adom strided_interval int ssi_wlat ssi_gamma.
Definition ssi_top : strided_interval := si_top Int.min_signed Int.max_signed.
Definition ssi_neg (x: strided_interval) : strided_interval :=
if zle x.(si_low_bound) Int.min_signed
then if zeq x.(si_up_bound) Int.min_signed
then si_const Int.signed (Int.repr Int.min_signed)
else ssi_top
else
if congr_dec x.(si_stride) x.(si_low_bound) x.(si_up_bound)
then {| si_stride := x.(si_stride)
; si_low_bound := - x.(si_up_bound)
; si_up_bound := - x.(si_low_bound)
|}
else ssi_top.
Lemma ssi_neg_sound (x: strided_interval) :
lift_unop Int.neg (γ x) ⊆ γ (ssi_neg x).
Lemma ssi_neg_valid x :
si_valid x →
si_valid (ssi_neg x).
Lemma ssi_neg_reduced x :
si_reduced x →
si_reduced (ssi_neg x).
Definition ssi_not (i: strided_interval) : strided_interval :=
si_add Int.min_signed Int.max_signed (ssi_neg i) (si_const Int.signed Int.mone).
Lemma ssi_not_valid x :
si_valid x → si_valid (ssi_not x).
Lemma ssi_not_reduced x :
si_valid x →
si_reduced x →
si_reduced (ssi_not x).
Definition ssi_sub (x y: strided_interval) : strided_interval :=
si_add Int.min_signed Int.max_signed x (ssi_neg y).
Lemma ssi_sub_valid x y :
si_valid x → si_valid y → si_valid (ssi_sub x y).
Lemma ssi_sub_reduced x y :
si_valid x → si_reduced x →
si_valid y → si_reduced y →
si_reduced (ssi_sub x y).
Definition ssi_mul_l (x y: strided_interval) : strided_interval :=
match x.(si_stride) with
| N0 ⇒
let k : Z := x.(si_low_bound) in
match k with
| Z0 ⇒ si_const Int.signed Int.zero
| Zpos k' ⇒
let l : Z := k × y.(si_low_bound) in
if Z_le_dec Int.min_signed l
then let u : Z := k × y.(si_up_bound) in
if Z_le_dec u Int.max_signed
then {| si_stride := Npos k' × y.(si_stride)
; si_low_bound := l
; si_up_bound := u
|}
else ssi_top
else ssi_top
| Zneg k' ⇒
let l : Z := k × y.(si_up_bound) in
if Z_le_dec Int.min_signed l
then let u : Z := k × y.(si_low_bound) in
if Z_le_dec u Int.max_signed
then
if congr_dec y.(si_stride) y.(si_low_bound) y.(si_up_bound)
then {| si_stride := Npos k' × y.(si_stride)
; si_low_bound := l
; si_up_bound := u
|}
else ssi_top
else ssi_top
else ssi_top
end
| _ ⇒ ssi_top
end.
Lemma ssi_mul_l_sound : ∀ x y,
Eval_int_binop OpMul (γ x) (γ y) ⊆ γ (ssi_mul_l x y).
Lemma ssi_mul_l_valid x y:
si_valid y →
si_valid (ssi_mul_l x y).
Lemma ssi_mul_l_reduced x y:
si_reduced y →
si_reduced (ssi_mul_l x y).
Definition ssi_mul x y :=
match x.(si_stride) with
| N0 ⇒ ssi_mul_l x y
| _ ⇒ ssi_mul_l y x
end.
Lemma ssi_mul_valid x y :
si_valid x →
si_valid y →
si_valid (ssi_mul x y).
Lemma ssi_mul_reduced x y :
si_reduced x →
si_reduced y →
si_reduced (ssi_mul x y).
Lemma ssi_mul_sound x y :
Eval_int_binop OpMul (γ x) (γ y) ⊆ γ (ssi_mul x y).
Definition ssi_shl (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒
let y' := Int.shl Int.one (Int.repr y.(si_low_bound)) in
ssi_mul_l (si_const Int.signed y') x
| _ ⇒
print
"Warning ssi: shl"
(⊤)
end.
Lemma ssi_shl_sound x y :
Eval_int_binop OpShl (γ x) (γ y) ⊆ γ (ssi_shl x y).
Definition ssi_divs_r (x: strided_interval) (y: positive) : strided_interval :=
let xs := Z.of_N x.(si_stride) in
let y' := Z.pos y in
{| si_stride := if Zdivides_dec y' xs
&& (zeq (Z.sgn x.(si_low_bound)) (Z.sgn x.(si_up_bound))
|| Zdivides_dec y' x.(si_low_bound))
then N.div x.(si_stride) (N.pos y)
else 1%N
; si_low_bound := x.(si_low_bound) ÷ y'
; si_up_bound := x.(si_up_bound) ÷ y'
|}.
Lemma ssi_divs_r_valid x y :
si_valid x →
si_valid (ssi_divs_r x y).
Lemma ssi_divs_r_sound x y i j :
γ x i →
Int.signed j = Z.pos y →
γ (ssi_divs_r x y) (Int.divs i j).
Definition ssi_divs (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒
match y.(si_low_bound) with
| Z.pos p ⇒ ssi_divs_r x p
| _ ⇒ (⊤)
end
| _ ⇒ (⊤)
end.
Lemma ssi_divs_valid x y : si_valid x → si_valid (ssi_divs x y).
Lemma ssi_divs_sound x y : lift_binop Int.divs (γ x) (γ y) ⊆ γ (ssi_divs x y).
Definition ssi_shr_l (x: strided_interval) (y: Z) : strided_interval :=
let m := Z.shiftr x.(si_low_bound) y in
let M := Z.shiftr x.(si_up_bound) y in
{| si_stride := if zeq m M then 0 else 1
; si_low_bound := m
; si_up_bound := M
|}.
Lemma ssi_shr_l_sound x y i :
0 ≤ y < Int.modulus →
γ x i →
γ (ssi_shr_l x y) (Int.shr i (Int.repr y)).
Definition ssi_shr (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒ ssi_shr_l x (Int.unsigned (Int.repr y.(si_low_bound)))
| _ ⇒ (⊤)
end.
Lemma ssi_shr_sound x y i j :
γ x i → γ y j →
γ (ssi_shr x y) (Int.shr i j).
Definition ssi_shru (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒
let y' := Int.unsigned (Int.repr y.(si_low_bound)) in
if Z_zerop y'
then x
else if znegb x.(si_low_bound)
then let (m, M) := Interval.shru_top y' in
{| si_stride := 1%N; si_low_bound := m; si_up_bound := M |}
else ssi_shr_l x y'
| _ ⇒ (⊤)
end.
Lemma ssi_shru_sound x y i j :
γ x i → γ y j →
γ (ssi_shru x y) (Int.shru i j).
Opaque Interval.shru_top.
Transparent Interval.shru_top.
Definition ssi_mods_r (x: strided_interval) (y: positive) : strided_interval :=
if x.(si_stride)
then
let r := Z.rem x.(si_low_bound) (Zpos y) in
{| si_stride := N0; si_low_bound := r; si_up_bound := r |}
else
if zle 0 x.(si_low_bound)
then {| si_stride := 1%N; si_low_bound := 0; si_up_bound := Zpos y - 1 |}
else print "Warning ssi: mods" ssi_top.
Lemma ssi_mods_r_sound x y i j:
i ∈ γ(x) →
Int.signed j = Z.pos y →
γ (ssi_mods_r x y) (Int.mods i j).
Definition ssi_mods (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒
match y.(si_low_bound) with
| Z.pos p ⇒ ssi_mods_r x p
| _ ⇒ (⊤)
end
| _ ⇒ (⊤)
end.
Lemma ssi_mods_sound x y : lift_binop Int.mods (γ x) (γ y) ⊆ γ (ssi_mods x y).
Definition ssi_and (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒
match x.(si_stride) with
| N0 ⇒ si_const Int.signed (Int.and (Int.repr x.(si_low_bound)) (Int.repr (y.(si_low_bound))))
| _ ⇒
match y.(si_low_bound) with
| Zneg _ ⇒ (⊤)
| Z0 ⇒ si_const Int.signed Int.zero
| Zpos p ⇒
{| si_stride := 1; si_low_bound := 0
; si_up_bound := two_power_pos (Pos.size p) - 1 |}
end
end
| _ ⇒
print
"Warning ssi: and"
(⊤)
end.
Lemma ssi_and_valid (x y: strided_interval) :
si_valid (ssi_and x y).
Lemma ssi_and_reduced (x y: strided_interval) :
si_reduced (ssi_and x y).
Notation todo2 := (fun s _ _ ⇒ print ("TODO ssi: " ++ s)%string (NotBot top)).
Notation todobw1 := (fun s x _ ⇒ print ("TODO ssi: " ++ s)%string (NotBot x)).
Notation todobw2 := (fun s x y _ ⇒ print ("TODO ssi bw2:" ++ s)%string (NotBot x, NotBot y)).
Definition ssi_backward_add (x y res: strided_interval) :=
(si_meet x (ssi_sub res y),
si_meet y (ssi_sub res x)).
Definition ssi_backward_le (x y: strided_interval) :=
(si_meet x {| si_stride := 1; si_low_bound := Int.min_signed; si_up_bound := y.(si_up_bound) |},
si_meet {| si_stride := 1; si_low_bound := x.(si_low_bound); si_up_bound := Int.max_signed |} y).
Definition cast_usi (x: strided_interval) : bool :=
match x.(si_low_bound) with
| Zneg _ ⇒ false
| _ ⇒ zle x.(si_up_bound) Int.max_unsigned
end.
Lemma cast_usi_true x :
cast_usi x = true →
0 ≤ x.(si_low_bound) ∧ x.(si_up_bound) ≤ Int.max_unsigned.
Lemma cast_usi_gamma x i :
cast_usi x = true →
γ x i →
Int.signed i = Int.unsigned i.
Definition ssi_backward_leu (x y: strided_interval) :=
if cast_usi x && cast_usi y
then ssi_backward_le x y
else (NotBot x, NotBot y).
Lemma ssi_backward_le_sound x y i j :
si_gamma Int.signed x i →
si_gamma Int.signed y j →
Int.lt j i = false →
let '(u,v) := ssi_backward_le x y in
γ u i ∧ γ v j.
Lemma ssi_backward_leu_sound x y i j :
si_gamma Int.signed x i →
si_gamma Int.signed y j →
Int.ltu j i = false →
let '(u,v) := ssi_backward_leu x y in
γ u i ∧ γ v j.
si_wlat Int.min_signed Int.max_signed.
Instance ssi_gamma : gamma_op strided_interval int :=
si_gamma Int.signed.
Lemma ssi_adom : adom strided_interval int ssi_wlat ssi_gamma.
Definition ssi_top : strided_interval := si_top Int.min_signed Int.max_signed.
Definition ssi_neg (x: strided_interval) : strided_interval :=
if zle x.(si_low_bound) Int.min_signed
then if zeq x.(si_up_bound) Int.min_signed
then si_const Int.signed (Int.repr Int.min_signed)
else ssi_top
else
if congr_dec x.(si_stride) x.(si_low_bound) x.(si_up_bound)
then {| si_stride := x.(si_stride)
; si_low_bound := - x.(si_up_bound)
; si_up_bound := - x.(si_low_bound)
|}
else ssi_top.
Lemma ssi_neg_sound (x: strided_interval) :
lift_unop Int.neg (γ x) ⊆ γ (ssi_neg x).
Lemma ssi_neg_valid x :
si_valid x →
si_valid (ssi_neg x).
Lemma ssi_neg_reduced x :
si_reduced x →
si_reduced (ssi_neg x).
Definition ssi_not (i: strided_interval) : strided_interval :=
si_add Int.min_signed Int.max_signed (ssi_neg i) (si_const Int.signed Int.mone).
Lemma ssi_not_valid x :
si_valid x → si_valid (ssi_not x).
Lemma ssi_not_reduced x :
si_valid x →
si_reduced x →
si_reduced (ssi_not x).
Definition ssi_sub (x y: strided_interval) : strided_interval :=
si_add Int.min_signed Int.max_signed x (ssi_neg y).
Lemma ssi_sub_valid x y :
si_valid x → si_valid y → si_valid (ssi_sub x y).
Lemma ssi_sub_reduced x y :
si_valid x → si_reduced x →
si_valid y → si_reduced y →
si_reduced (ssi_sub x y).
Definition ssi_mul_l (x y: strided_interval) : strided_interval :=
match x.(si_stride) with
| N0 ⇒
let k : Z := x.(si_low_bound) in
match k with
| Z0 ⇒ si_const Int.signed Int.zero
| Zpos k' ⇒
let l : Z := k × y.(si_low_bound) in
if Z_le_dec Int.min_signed l
then let u : Z := k × y.(si_up_bound) in
if Z_le_dec u Int.max_signed
then {| si_stride := Npos k' × y.(si_stride)
; si_low_bound := l
; si_up_bound := u
|}
else ssi_top
else ssi_top
| Zneg k' ⇒
let l : Z := k × y.(si_up_bound) in
if Z_le_dec Int.min_signed l
then let u : Z := k × y.(si_low_bound) in
if Z_le_dec u Int.max_signed
then
if congr_dec y.(si_stride) y.(si_low_bound) y.(si_up_bound)
then {| si_stride := Npos k' × y.(si_stride)
; si_low_bound := l
; si_up_bound := u
|}
else ssi_top
else ssi_top
else ssi_top
end
| _ ⇒ ssi_top
end.
Lemma ssi_mul_l_sound : ∀ x y,
Eval_int_binop OpMul (γ x) (γ y) ⊆ γ (ssi_mul_l x y).
Lemma ssi_mul_l_valid x y:
si_valid y →
si_valid (ssi_mul_l x y).
Lemma ssi_mul_l_reduced x y:
si_reduced y →
si_reduced (ssi_mul_l x y).
Definition ssi_mul x y :=
match x.(si_stride) with
| N0 ⇒ ssi_mul_l x y
| _ ⇒ ssi_mul_l y x
end.
Lemma ssi_mul_valid x y :
si_valid x →
si_valid y →
si_valid (ssi_mul x y).
Lemma ssi_mul_reduced x y :
si_reduced x →
si_reduced y →
si_reduced (ssi_mul x y).
Lemma ssi_mul_sound x y :
Eval_int_binop OpMul (γ x) (γ y) ⊆ γ (ssi_mul x y).
Definition ssi_shl (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒
let y' := Int.shl Int.one (Int.repr y.(si_low_bound)) in
ssi_mul_l (si_const Int.signed y') x
| _ ⇒
"Warning ssi: shl"
(⊤)
end.
Lemma ssi_shl_sound x y :
Eval_int_binop OpShl (γ x) (γ y) ⊆ γ (ssi_shl x y).
Definition ssi_divs_r (x: strided_interval) (y: positive) : strided_interval :=
let xs := Z.of_N x.(si_stride) in
let y' := Z.pos y in
{| si_stride := if Zdivides_dec y' xs
&& (zeq (Z.sgn x.(si_low_bound)) (Z.sgn x.(si_up_bound))
|| Zdivides_dec y' x.(si_low_bound))
then N.div x.(si_stride) (N.pos y)
else 1%N
; si_low_bound := x.(si_low_bound) ÷ y'
; si_up_bound := x.(si_up_bound) ÷ y'
|}.
Lemma ssi_divs_r_valid x y :
si_valid x →
si_valid (ssi_divs_r x y).
Lemma ssi_divs_r_sound x y i j :
γ x i →
Int.signed j = Z.pos y →
γ (ssi_divs_r x y) (Int.divs i j).
Definition ssi_divs (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒
match y.(si_low_bound) with
| Z.pos p ⇒ ssi_divs_r x p
| _ ⇒ (⊤)
end
| _ ⇒ (⊤)
end.
Lemma ssi_divs_valid x y : si_valid x → si_valid (ssi_divs x y).
Lemma ssi_divs_sound x y : lift_binop Int.divs (γ x) (γ y) ⊆ γ (ssi_divs x y).
Definition ssi_shr_l (x: strided_interval) (y: Z) : strided_interval :=
let m := Z.shiftr x.(si_low_bound) y in
let M := Z.shiftr x.(si_up_bound) y in
{| si_stride := if zeq m M then 0 else 1
; si_low_bound := m
; si_up_bound := M
|}.
Lemma ssi_shr_l_sound x y i :
0 ≤ y < Int.modulus →
γ x i →
γ (ssi_shr_l x y) (Int.shr i (Int.repr y)).
Definition ssi_shr (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒ ssi_shr_l x (Int.unsigned (Int.repr y.(si_low_bound)))
| _ ⇒ (⊤)
end.
Lemma ssi_shr_sound x y i j :
γ x i → γ y j →
γ (ssi_shr x y) (Int.shr i j).
Definition ssi_shru (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒
let y' := Int.unsigned (Int.repr y.(si_low_bound)) in
if Z_zerop y'
then x
else if znegb x.(si_low_bound)
then let (m, M) := Interval.shru_top y' in
{| si_stride := 1%N; si_low_bound := m; si_up_bound := M |}
else ssi_shr_l x y'
| _ ⇒ (⊤)
end.
Lemma ssi_shru_sound x y i j :
γ x i → γ y j →
γ (ssi_shru x y) (Int.shru i j).
Opaque Interval.shru_top.
Transparent Interval.shru_top.
Definition ssi_mods_r (x: strided_interval) (y: positive) : strided_interval :=
if x.(si_stride)
then
let r := Z.rem x.(si_low_bound) (Zpos y) in
{| si_stride := N0; si_low_bound := r; si_up_bound := r |}
else
if zle 0 x.(si_low_bound)
then {| si_stride := 1%N; si_low_bound := 0; si_up_bound := Zpos y - 1 |}
else print "Warning ssi: mods" ssi_top.
Lemma ssi_mods_r_sound x y i j:
i ∈ γ(x) →
Int.signed j = Z.pos y →
γ (ssi_mods_r x y) (Int.mods i j).
Definition ssi_mods (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒
match y.(si_low_bound) with
| Z.pos p ⇒ ssi_mods_r x p
| _ ⇒ (⊤)
end
| _ ⇒ (⊤)
end.
Lemma ssi_mods_sound x y : lift_binop Int.mods (γ x) (γ y) ⊆ γ (ssi_mods x y).
Definition ssi_and (x y: strided_interval) : strided_interval :=
match y.(si_stride) with
| N0 ⇒
match x.(si_stride) with
| N0 ⇒ si_const Int.signed (Int.and (Int.repr x.(si_low_bound)) (Int.repr (y.(si_low_bound))))
| _ ⇒
match y.(si_low_bound) with
| Zneg _ ⇒ (⊤)
| Z0 ⇒ si_const Int.signed Int.zero
| Zpos p ⇒
{| si_stride := 1; si_low_bound := 0
; si_up_bound := two_power_pos (Pos.size p) - 1 |}
end
end
| _ ⇒
"Warning ssi: and"
(⊤)
end.
Lemma ssi_and_valid (x y: strided_interval) :
si_valid (ssi_and x y).
Lemma ssi_and_reduced (x y: strided_interval) :
si_reduced (ssi_and x y).
Notation todo2 := (fun s _ _ ⇒ print ("TODO ssi: " ++ s)%string (NotBot top)).
Notation todobw1 := (fun s x _ ⇒ print ("TODO ssi: " ++ s)%string (NotBot x)).
Notation todobw2 := (fun s x y _ ⇒ print ("TODO ssi bw2:" ++ s)%string (NotBot x, NotBot y)).
Definition ssi_backward_add (x y res: strided_interval) :=
(si_meet x (ssi_sub res y),
si_meet y (ssi_sub res x)).
Definition ssi_backward_le (x y: strided_interval) :=
(si_meet x {| si_stride := 1; si_low_bound := Int.min_signed; si_up_bound := y.(si_up_bound) |},
si_meet {| si_stride := 1; si_low_bound := x.(si_low_bound); si_up_bound := Int.max_signed |} y).
Definition cast_usi (x: strided_interval) : bool :=
match x.(si_low_bound) with
| Zneg _ ⇒ false
| _ ⇒ zle x.(si_up_bound) Int.max_unsigned
end.
Lemma cast_usi_true x :
cast_usi x = true →
0 ≤ x.(si_low_bound) ∧ x.(si_up_bound) ≤ Int.max_unsigned.
Lemma cast_usi_gamma x i :
cast_usi x = true →
γ x i →
Int.signed i = Int.unsigned i.
Definition ssi_backward_leu (x y: strided_interval) :=
if cast_usi x && cast_usi y
then ssi_backward_le x y
else (NotBot x, NotBot y).
Lemma ssi_backward_le_sound x y i j :
si_gamma Int.signed x i →
si_gamma Int.signed y j →
Int.lt j i = false →
let '(u,v) := ssi_backward_le x y in
γ u i ∧ γ v j.
Lemma ssi_backward_leu_sound x y i j :
si_gamma Int.signed x i →
si_gamma Int.signed y j →
Int.ltu j i = false →
let '(u,v) := ssi_backward_leu x y in
γ u i ∧ γ v j.
Reduced valid interval as a strided interval with stride 1.
Definition si_interval (l u: Z) : strided_interval+⊥ :=
match Z_dec l u with
| inleft (left LT) ⇒ NotBot {| si_stride := 1; si_low_bound := l; si_up_bound := u |}
| inleft (right GT) ⇒ Bot
| inright EQ ⇒ NotBot {| si_stride := 0; si_low_bound := l; si_up_bound := l |}
end.
Definition ssi_backward_lt (x y: strided_interval) :=
(botbind (si_meet x) (si_interval Int.min_signed (y.(si_up_bound) - 1)),
botbind (si_meet y) (si_interval (x.(si_low_bound) + 1) Int.max_signed)).
Definition ssi_backward_ltu (x y: strided_interval) :=
if cast_usi x && cast_usi y
then ssi_backward_lt x y
else (NotBot x, NotBot y).
Lemma ssi_backward_lt_sound x y i j :
γ x i → γ y j →
Int.lt i j = true →
let '(u,v) := ssi_backward_lt x y in
γ u i ∧ γ v j.
Lemma ssi_backward_ltu_sound x y i j :
γ x i → γ y j →
Int.ltu i j = true →
let '(u,v) := ssi_backward_ltu x y in
γ u i ∧ γ v j.
Definition ssi_backward_ne (x y: strided_interval) :=
let (x1, y1) := ssi_backward_lt x y in
let (y2, x2) := ssi_backward_lt y x in
(x1 ⊔ x2, y1 ⊔ y2).
Lemma ssi_backward_ne_sound x y i j :
γ x i → γ y j →
Int.eq i j = false →
let '(u, v) := ssi_backward_ne x y in
γ u i ∧ γ v j.
Hint Resolve ssi_adom lift_bot.
Definition ssi_backward_cmp (c:comparison) (x y res: strided_interval) :=
match res.(si_stride) with
| N0 ⇒
if Z_zerop res.(si_low_bound)
then
match c with
| Cne ⇒ let ab := si_meet x y in (ab, ab)
| Cgt ⇒ ssi_backward_le x y
| Clt ⇒ Interval.swap (ssi_backward_le y x)
| Cge ⇒ ssi_backward_lt x y
| Cle ⇒ Interval.swap (ssi_backward_lt y x)
| Ceq ⇒ ssi_backward_ne x y
end
else
if Z_eq_dec res.(si_low_bound) 1
then
match c with
| Ceq ⇒ let ab := si_meet x y in (ab, ab)
| Cle ⇒ ssi_backward_le x y
| Cge ⇒ Interval.swap (ssi_backward_le y x)
| Clt ⇒ ssi_backward_lt x y
| Cgt ⇒ Interval.swap (ssi_backward_lt y x)
| Cne ⇒ ssi_backward_ne x y
end
else (NotBot x, NotBot y)
| _ ⇒ (NotBot x, NotBot y)
end.
Definition ssi_backward_cmpu (c:comparison) (x y res: strided_interval) :=
match res.(si_stride) with
| N0 ⇒
if Z_zerop res.(si_low_bound)
then
match c with
| Cne ⇒ let ab := si_meet x y in (ab, ab)
| Cgt ⇒ ssi_backward_leu x y
| Clt ⇒ Interval.swap (ssi_backward_leu y x)
| Cge ⇒ ssi_backward_ltu x y
| Cle ⇒ Interval.swap (ssi_backward_ltu y x)
| Ceq ⇒ ssi_backward_ne x y
end
else
if Z_eq_dec res.(si_low_bound) 1
then
match c with
| Ceq ⇒ let ab := si_meet x y in (ab, ab)
| Cle ⇒ ssi_backward_leu x y
| Cge ⇒ Interval.swap (ssi_backward_leu y x)
| Clt ⇒ ssi_backward_ltu x y
| Cgt ⇒ Interval.swap (ssi_backward_ltu y x)
| Cne ⇒ ssi_backward_ne x y
end
else (NotBot x, NotBot y)
| _ ⇒ (NotBot x, NotBot y)
end.
Lemma ssi_backward_cmp_sound c :
∀ x y z, ∀ i j,
γ x i → γ y j → γ z (eval_int_binop (OpCmp c) i j) →
let '(u,v) := ssi_backward_cmp c x y z in
γ u i ∧ γ v j.
Lemma ssi_backward_cmpu_sound c :
∀ x y z, ∀ i j,
γ x i → γ y j → γ z (eval_int_binop (OpCmpu c) i j) →
let '(u,v) := ssi_backward_cmpu c x y z in
γ u i ∧ γ v j.
Instance ssiToString : ToString strided_interval := toString Int.min_signed Int.max_signed.
Instance ssi_dom : ab_machine_int strided_interval :=
{| as_int_adom := ssi_adom
; meet_int := si_meet
; size x := Just (si_size x)
; concretize x := Just (IntSet.of_list (List.map Int.repr (si_concretize x)))
; const_int := si_const Int.signed
; booleans := {| si_stride := 1%N; si_low_bound := 0; si_up_bound := 1 |}
; range_int x f := match f with
| Signed ⇒ NotBot (Interval.ITV x.(si_low_bound) x.(si_up_bound))
| Unsigned ⇒ top
end
; forward_int_unop op x :=
match op with
| OpNeg ⇒ NotBot (ssi_neg x)
| OpNot ⇒ NotBot (ssi_not x)
end
; forward_int_binop op x y :=
match op with
| OpAdd ⇒ NotBot (si_add Int.min_signed Int.max_signed x y)
| OpSub ⇒ NotBot (ssi_sub x y)
| OpMul ⇒ NotBot (ssi_mul x y)
| OpAnd ⇒ NotBot (ssi_and x y)
| OpDivs ⇒ NotBot (ssi_divs x y)
| OpMods ⇒ NotBot (ssi_mods x y)
| OpShl ⇒ NotBot (ssi_shl x y)
| OpShr ⇒ NotBot (ssi_shr x y)
| OpShru ⇒ NotBot (ssi_shru x y)
| _ ⇒ todo2 (to_string x ++ " " ++ to_string op ++ " " ++ to_string y)%string x y
end
; is_in_itv := si_is_in_itv Int.signed
; backward_int_unop op :=
match op with
| _ ⇒ todobw1 (to_string op)
end
; backward_int_binop op :=
match op with
| OpCmp c ⇒ ssi_backward_cmp c
| OpCmpu c ⇒ ssi_backward_cmpu c
| OpAdd ⇒ ssi_backward_add
| _ ⇒ todobw2 (to_string op)
end
|}.
Lemma ssi_is_in_itv_sound (u v: int) (x: strided_interval) :
si_is_in_itv Int.signed u v x = true →
∀ i, si_gamma Int.signed x i → Int.lt v i = false ∧ Int.lt i u = false.
Lemma ssi_add_sound (x y: strided_interval) :
lift_binop Int.add (γ x) (γ y) ⊆ γ (si_add Int.min_signed Int.max_signed x y).
Lemma ssi_not_sound x : lift_unop Int.not (si_gamma Int.signed x) ⊆ (si_gamma Int.signed (ssi_not x)).
Lemma ssi_sub_sound x y : lift_binop Int.sub (γ x) (γ y) ⊆ γ (ssi_sub x y).
Lemma ssi_and_sound x y : lift_binop Int.and (γ x) (γ y) ⊆ γ (ssi_and x y).
Lemma ssi_backward_add_sound :
∀ x y z i j,
γ x i →
γ y j →
γ z (Int.add i j) →
let (u, v) := ssi_backward_add x y z in
γ u i ∧ γ v j.
Instance ssi_num_dom_correct : ab_machine_int_correct ssi_dom.
match Z_dec l u with
| inleft (left LT) ⇒ NotBot {| si_stride := 1; si_low_bound := l; si_up_bound := u |}
| inleft (right GT) ⇒ Bot
| inright EQ ⇒ NotBot {| si_stride := 0; si_low_bound := l; si_up_bound := l |}
end.
Definition ssi_backward_lt (x y: strided_interval) :=
(botbind (si_meet x) (si_interval Int.min_signed (y.(si_up_bound) - 1)),
botbind (si_meet y) (si_interval (x.(si_low_bound) + 1) Int.max_signed)).
Definition ssi_backward_ltu (x y: strided_interval) :=
if cast_usi x && cast_usi y
then ssi_backward_lt x y
else (NotBot x, NotBot y).
Lemma ssi_backward_lt_sound x y i j :
γ x i → γ y j →
Int.lt i j = true →
let '(u,v) := ssi_backward_lt x y in
γ u i ∧ γ v j.
Lemma ssi_backward_ltu_sound x y i j :
γ x i → γ y j →
Int.ltu i j = true →
let '(u,v) := ssi_backward_ltu x y in
γ u i ∧ γ v j.
Definition ssi_backward_ne (x y: strided_interval) :=
let (x1, y1) := ssi_backward_lt x y in
let (y2, x2) := ssi_backward_lt y x in
(x1 ⊔ x2, y1 ⊔ y2).
Lemma ssi_backward_ne_sound x y i j :
γ x i → γ y j →
Int.eq i j = false →
let '(u, v) := ssi_backward_ne x y in
γ u i ∧ γ v j.
Hint Resolve ssi_adom lift_bot.
Definition ssi_backward_cmp (c:comparison) (x y res: strided_interval) :=
match res.(si_stride) with
| N0 ⇒
if Z_zerop res.(si_low_bound)
then
match c with
| Cne ⇒ let ab := si_meet x y in (ab, ab)
| Cgt ⇒ ssi_backward_le x y
| Clt ⇒ Interval.swap (ssi_backward_le y x)
| Cge ⇒ ssi_backward_lt x y
| Cle ⇒ Interval.swap (ssi_backward_lt y x)
| Ceq ⇒ ssi_backward_ne x y
end
else
if Z_eq_dec res.(si_low_bound) 1
then
match c with
| Ceq ⇒ let ab := si_meet x y in (ab, ab)
| Cle ⇒ ssi_backward_le x y
| Cge ⇒ Interval.swap (ssi_backward_le y x)
| Clt ⇒ ssi_backward_lt x y
| Cgt ⇒ Interval.swap (ssi_backward_lt y x)
| Cne ⇒ ssi_backward_ne x y
end
else (NotBot x, NotBot y)
| _ ⇒ (NotBot x, NotBot y)
end.
Definition ssi_backward_cmpu (c:comparison) (x y res: strided_interval) :=
match res.(si_stride) with
| N0 ⇒
if Z_zerop res.(si_low_bound)
then
match c with
| Cne ⇒ let ab := si_meet x y in (ab, ab)
| Cgt ⇒ ssi_backward_leu x y
| Clt ⇒ Interval.swap (ssi_backward_leu y x)
| Cge ⇒ ssi_backward_ltu x y
| Cle ⇒ Interval.swap (ssi_backward_ltu y x)
| Ceq ⇒ ssi_backward_ne x y
end
else
if Z_eq_dec res.(si_low_bound) 1
then
match c with
| Ceq ⇒ let ab := si_meet x y in (ab, ab)
| Cle ⇒ ssi_backward_leu x y
| Cge ⇒ Interval.swap (ssi_backward_leu y x)
| Clt ⇒ ssi_backward_ltu x y
| Cgt ⇒ Interval.swap (ssi_backward_ltu y x)
| Cne ⇒ ssi_backward_ne x y
end
else (NotBot x, NotBot y)
| _ ⇒ (NotBot x, NotBot y)
end.
Lemma ssi_backward_cmp_sound c :
∀ x y z, ∀ i j,
γ x i → γ y j → γ z (eval_int_binop (OpCmp c) i j) →
let '(u,v) := ssi_backward_cmp c x y z in
γ u i ∧ γ v j.
Lemma ssi_backward_cmpu_sound c :
∀ x y z, ∀ i j,
γ x i → γ y j → γ z (eval_int_binop (OpCmpu c) i j) →
let '(u,v) := ssi_backward_cmpu c x y z in
γ u i ∧ γ v j.
Instance ssiToString : ToString strided_interval := toString Int.min_signed Int.max_signed.
Instance ssi_dom : ab_machine_int strided_interval :=
{| as_int_adom := ssi_adom
; meet_int := si_meet
; size x := Just (si_size x)
; concretize x := Just (IntSet.of_list (List.map Int.repr (si_concretize x)))
; const_int := si_const Int.signed
; booleans := {| si_stride := 1%N; si_low_bound := 0; si_up_bound := 1 |}
; range_int x f := match f with
| Signed ⇒ NotBot (Interval.ITV x.(si_low_bound) x.(si_up_bound))
| Unsigned ⇒ top
end
; forward_int_unop op x :=
match op with
| OpNeg ⇒ NotBot (ssi_neg x)
| OpNot ⇒ NotBot (ssi_not x)
end
; forward_int_binop op x y :=
match op with
| OpAdd ⇒ NotBot (si_add Int.min_signed Int.max_signed x y)
| OpSub ⇒ NotBot (ssi_sub x y)
| OpMul ⇒ NotBot (ssi_mul x y)
| OpAnd ⇒ NotBot (ssi_and x y)
| OpDivs ⇒ NotBot (ssi_divs x y)
| OpMods ⇒ NotBot (ssi_mods x y)
| OpShl ⇒ NotBot (ssi_shl x y)
| OpShr ⇒ NotBot (ssi_shr x y)
| OpShru ⇒ NotBot (ssi_shru x y)
| _ ⇒ todo2 (to_string x ++ " " ++ to_string op ++ " " ++ to_string y)%string x y
end
; is_in_itv := si_is_in_itv Int.signed
; backward_int_unop op :=
match op with
| _ ⇒ todobw1 (to_string op)
end
; backward_int_binop op :=
match op with
| OpCmp c ⇒ ssi_backward_cmp c
| OpCmpu c ⇒ ssi_backward_cmpu c
| OpAdd ⇒ ssi_backward_add
| _ ⇒ todobw2 (to_string op)
end
|}.
Lemma ssi_is_in_itv_sound (u v: int) (x: strided_interval) :
si_is_in_itv Int.signed u v x = true →
∀ i, si_gamma Int.signed x i → Int.lt v i = false ∧ Int.lt i u = false.
Lemma ssi_add_sound (x y: strided_interval) :
lift_binop Int.add (γ x) (γ y) ⊆ γ (si_add Int.min_signed Int.max_signed x y).
Lemma ssi_not_sound x : lift_unop Int.not (si_gamma Int.signed x) ⊆ (si_gamma Int.signed (ssi_not x)).
Lemma ssi_sub_sound x y : lift_binop Int.sub (γ x) (γ y) ⊆ γ (ssi_sub x y).
Lemma ssi_and_sound x y : lift_binop Int.and (γ x) (γ y) ⊆ γ (ssi_and x y).
Lemma ssi_backward_add_sound :
∀ x y z i j,
γ x i →
γ y j →
γ z (Int.add i j) →
let (u, v) := ssi_backward_add x y z in
γ u i ∧ γ v j.
Instance ssi_num_dom_correct : ab_machine_int_correct ssi_dom.
Product of strided signed intervals and unsigned (non-strided) intervals.
Section SSIU.
Require Import Intervals.
Import DLib Interval.
Definition reduc2unsigned (i: strided_interval) : itv :=
let m := i.(si_low_bound) in
let M := i.(si_up_bound) in
if zle 0 m
then ITV m M
else if zlt M 0
then ITV (m + Int.modulus) (M + Int.modulus)
else utop.
Definition reduc2signed (i: itv) : strided_interval :=
match reduc2signed i with
| ITV m M ⇒ {| si_stride := 1%N; si_low_bound := m; si_up_bound := M |}
end.
Lemma reduc2unsigned_correct: ∀ i v,
si_gamma Int.signed i v →
ugamma (reduc2unsigned i) v.
Lemma reduc2signed_correct: ∀ i v,
ugamma i v →
si_gamma Int.signed (reduc2signed i) v.
Instance ssiu_red : reduction strided_interval itv :=
{| ρ := botbind2 (fun s u ⇒
let s' := reduc2signed u in
let u' := reduc2unsigned s in
match si_meet s s', u ⊓ u' with
| Bot, _ | _, Bot ⇒ Bot
| NotBot a, NotBot b ⇒ NotBot (a,b)
end)
|}.
Lemma ssiu_red_correct : reduction_correct ssi_adom unsigned_itv_adom.
Hint Resolve reduc2unsigned_correct reduc2signed_correct.
Instance ssiu_dom : ab_machine_int _ :=
@reduced_product_int _ _ ssi_dom UInterval.itvu_num ssiu_red.
Instance ssiu_dom_correct : ab_machine_int_correct ssiu_dom :=
reduced_product_int_correct ssi_num_dom_correct UInterval.itvu_num_correct ssiu_red_correct.
End SSIU.
Require Import Intervals.
Import DLib Interval.
Definition reduc2unsigned (i: strided_interval) : itv :=
let m := i.(si_low_bound) in
let M := i.(si_up_bound) in
if zle 0 m
then ITV m M
else if zlt M 0
then ITV (m + Int.modulus) (M + Int.modulus)
else utop.
Definition reduc2signed (i: itv) : strided_interval :=
match reduc2signed i with
| ITV m M ⇒ {| si_stride := 1%N; si_low_bound := m; si_up_bound := M |}
end.
Lemma reduc2unsigned_correct: ∀ i v,
si_gamma Int.signed i v →
ugamma (reduc2unsigned i) v.
Lemma reduc2signed_correct: ∀ i v,
ugamma i v →
si_gamma Int.signed (reduc2signed i) v.
Instance ssiu_red : reduction strided_interval itv :=
{| ρ := botbind2 (fun s u ⇒
let s' := reduc2signed u in
let u' := reduc2unsigned s in
match si_meet s s', u ⊓ u' with
| Bot, _ | _, Bot ⇒ Bot
| NotBot a, NotBot b ⇒ NotBot (a,b)
end)
|}.
Lemma ssiu_red_correct : reduction_correct ssi_adom unsigned_itv_adom.
Hint Resolve reduc2unsigned_correct reduc2signed_correct.
Instance ssiu_dom : ab_machine_int _ :=
@reduced_product_int _ _ ssi_dom UInterval.itvu_num ssiu_red.
Instance ssiu_dom_correct : ab_machine_int_correct ssiu_dom :=
reduced_product_int_correct ssi_num_dom_correct UInterval.itvu_num_correct ssiu_red_correct.
End SSIU.