Require Import Classical.
Require Import Relation_Operators.
Require Import List.
Import ListNotations.
Require Import Sorted.
Require Import Coqlib.
Require Import Maps.
Require Import Dom.
Require Import Utils.
Require Import SSA.
Require Import SSAutils.
Require Import SSAlive.
Require Import SSAfastliveutils.
Require Import SSAfastliveprecomputeRTthm.
Require Import SSAfastliveprecomputeTTthm.
Require Import SSAfastliveprecompute.
Require Import SSAfastliveprecomputethm.
Require Import SSAfastlive.
Lemma successors_not_nil :
forall f pc,
f.(
fn_code) !
pc <>
None <-> (
successors f) !
pc <>
None.
Proof.
Lemma succs_successors_instr :
forall f pc pc'
succs,
(
successors f) !
pc =
Some succs ->
In pc'
succs ->
exists instr, (
fn_code f) !
pc =
Some instr /\
In pc' (
successors_instr instr).
Proof.
intros.
unfold successors in H.
rewrite PTree.gmap1 in H.
unfold option_map in H.
destruct (
f.(
fn_code) !
pc)
as [
instr|]; [|
discriminate].
inv H.
eexists;
split; [
reflexivity|
eassumption].
Qed.
Lemma path_cfg :
forall f p s1 s2,
SSApath f s1 p s2 ->
match s1,
s2 with
| (
PState pc1), (
PState pc2) => (
cfg f **)
pc1 pc2
|
_,
_ =>
True
end.
Proof.
clear.
induction 1 ;
intros.
destruct s;
auto.
destruct s1;
destruct s3;
auto.
destruct s2.
apply rt_trans with pc2;
eauto.
apply rt_step.
inv STEP.
auto.
econstructor ;
eauto.
exploit (@
path_from_ret_nil node) ;
eauto.
intro Heq.
inv Heq.
inv H.
Qed.
Lemma path_reached :
forall f p pc,
SSApath f (
PState (
entry f))
p (
PState pc) ->
reached f pc.
Proof.
intros.
simpl in H.
eapply path_cfg in H ;
eauto.
Qed.
Lemma dom_intermediate :
forall f d i j,
reached f i ->
sdom f d j ->
forall p,
SSApath f (
PState i)
p (
PState j) ->
~
In d p ->
Forall (
sdom f d) (
p ++ [
j]).
Proof.
intros f d i j REACHED SDOM.
intros.
rewrite Forall_forall.
intros.
rewrite in_app_iff in H1.
destruct H1 as [
H1|[
H1|[]]]; [|
congruence].
inv SDOM.
inv DOM; [
contradiction|].
constructor;
try congruence.
By contradiction *)
destruct (
classic (
dom f d x)); [
assumption|].
exploit (
not_dom_path_wo peq);
eauto.
-
destruct (
reached_path (
cfg f) (
exit f) (
entry f)
_ REACHED)
as (
p1 &
H3).
destruct (
in_path_split peq (
cfg f) (
exit f) (
entry f)
_ _ _ _ H H1)
as (
p' &
_ &
HH1 &
_).
apply (
path_reached f (
p1 ++
p')).
eapply path_app;
eassumption.
-
intros (
p1 &
H4 &
H5).
destruct (
in_path_split'
peq _ _ _ _ _ _ _ H H1)
as (
p' &
p'' &
_ &
_ &
HH1 &
HH2).
assert (~
In d (
p1 ++
x ::
p''))
as Ha.
{
intros contra.
rewrite in_app_iff in contra.
destruct contra as [
contra|
contra]; [
contradiction|].
contradiction H0.
rewrite HH2.
rewrite in_app_iff.
right;
assumption.
}
contradiction Ha.
apply PATH.
eapply path_app;
eassumption.
Qed.
Section CORRECTNESS.
Variable f :
function.
Variable wf :
wf_ssa_function f.
Notation reachable := (
reachable (
successors f)).
Notation reduced_reachable := (
reduced_reachable (
successors f)).
Lemma reduced_reachable_exists_path :
forall back u v,
reached f u ->
reduced_reachable back u v ->
exists p,
SSApath f (
PState u)
p (
PState v)
/\
Sorted (
fun u v => ~
In (
u,
v)
back) (
p++[
v]).
Proof.
intros.
apply reduced_reachable_equiv in H0.
induction H0.
-
exists [].
split;
repeat constructor.
-
destruct (
succs_successors_instr _ _ _ _ H0 H1)
as (
instr &
H41 &
H42).
destruct IHreduced_reachable_bis as (
p &
IH1 &
IH2).
econstructor 3.
apply H.
constructor 1.
econstructor;
eassumption.
exists (
root::
p).
split.
+
econstructor.
*
constructor.
eassumption.
econstructor;
eassumption.
*
assumption.
+
simpl.
constructor.
assumption.
inv IH1.
*
constructor.
assumption.
*
inv STEP; [|
inv PATH;
inv STEP].
constructor.
assumption.
Qed.
Lemma exists_path_reduced_reachable :
forall back u p v,
SSApath f (
PState u)
p (
PState v) ->
Sorted (
fun u v => ~
In (
u,
v)
back) (
p++[
v]) ->
reduced_reachable back u v.
Proof.
intros back u p.
revert u.
induction p;
intros.
-
inv H.
constructor.
-
inv H.
inv STEP; [|
inv PATH;
inv STEP].
inv STEP0.
apply reduced_reachable_equiv.
destruct (
successors_instr_succs _ _ _ _ HCFG_ins HCFG_in)
as (
instr &
H11 &
H12).
econstructor;
try eassumption.
+
inv PATH.
*
inv H0.
inv H3.
assumption.
*
inv STEP; [|
inv PATH0;
inv STEP].
inv H0.
inv H3.
assumption.
+
apply reduced_reachable_equiv.
apply IHp.
assumption.
inv H0.
assumption.
Qed.
Lemma reachable_reached :
forall u v,
reachable u v ->
(
cfg f **)
u v.
Proof.
intros.
induction H.
-
constructor 2.
-
econstructor 3.
apply IHreachable.
constructor 1.
destruct (
succs_successors_instr _ _ _ _ H0 H1)
as (
instr &
H21 &
H22).
econstructor;
eassumption.
Qed.
Lemma reached_reachable :
forall u v,
(
cfg f **)
u v ->
reachable u v.
Proof.
Lemma reachable_exists_path :
forall u v,
reached f u ->
reachable u v ->
exists p,
SSApath f (
PState u)
p (
PState v).
Proof.
intros.
induction H0.
-
eexists;
constructor.
-
destruct (
succs_successors_instr _ _ _ _ H1 H2)
as (
instr &
H31 &
H32).
destruct IHreachable as (
p' &
H4).
exists (
p' ++
x ::
nil).
eapply path_app.
eassumption.
econstructor.
+
constructor.
*
econstructor 3.
apply H.
apply reachable_reached.
assumption.
*
econstructor;
eassumption.
+
constructor.
Qed.
Lemma exists_path_reachable :
forall u p v,
SSApath f (
PState u)
p (
PState v) ->
reachable u v.
Proof.
Lemma Sorted_app_l :
forall {
A} (
R :
A ->
A ->
Prop)
l1 l2,
Sorted R (
l1 ++
l2) ->
Sorted R l1.
Proof.
intros. induction l1.
- constructor.
- inv H. constructor.
+ auto.
+ destruct l1.
* constructor.
* inv H3. constructor; assumption.
Qed.
Lemma Sorted_app_r :
forall {
A} (
R :
A ->
A ->
Prop)
l1 l2,
Sorted R (
l1 ++
l2) ->
Sorted R l2.
Proof.
intros. induction l1.
- assumption.
- inv H. auto.
Qed.
Lemma ssa_reached_closed :
forall pc,
reached f pc ->
f.(
fn_code) !
pc <>
None.
Proof.
Lemma dom_reduced_reachable :
forall dom_pre,
let '(
r,
c,
t,
back) :=
precompute_r_t (
successors f)
f.(
fn_entrypoint)
dom_pre in
forall d u,
dom f d u ->
reduced_reachable back d u.
Proof.
Lemma corollary1 :
forall dom_pre,
let '(
r,
c,
t,
back) :=
precompute_r_t (
successors f)
f.(
fn_entrypoint)
dom_pre in
forall d u p v,
sdom f d u ->
sdom f d v ->
SSApath f (
PState u)
p (
PState v) ->
Sorted (
fun u v => ~
In (
u,
v)
back) (
p++[
v]) ->
Forall (
sdom f d) (
p++[
v]).
Proof.
Lemma Exists_first :
forall {
A} (
P :
A ->
Prop) (
P_dec :
forall x, {
P x} + {~
P x})
l,
Exists P l ->
exists l1 x l2,
l =
l1 ++
x ::
l2 /\
P x /\
Forall (
fun x => ~
P x)
l1.
Proof.
intros. induction l.
- inversion H.
- destruct (P_dec a).
+ exists [], a, l. split; [reflexivity|]. split; [assumption|constructor].
+ inv H; [contradiction|].
destruct (IHl H1) as (l1 & x & l2 & H21 & H22 & H23).
exists (a::l1), x, l2.
split; [|split].
* simpl. rewrite <- H21. reflexivity.
* assumption.
* constructor; assumption.
Qed.
Lemma Exists_last :
forall {
A} (
P :
A ->
Prop) (
P_dec :
forall x, {
P x} + {~
P x})
l,
Exists P l ->
exists l1 x l2,
l =
l1 ++
x ::
l2 /\
P x /\
Forall (
fun x => ~
P x)
l2.
Proof.
intros.
induction l.
-
inversion H.
-
destruct (
Exists_dec _ l P_dec).
+
apply IHl in e.
destruct e as (
l1 &
x &
l2 &
e1 &
e2 &
e3).
exists (
a::
l1),
x,
l2.
split; [|
split;
assumption].
simpl.
rewrite <-
e1.
reflexivity.
+
exists [],
a,
l.
split; [
reflexivity|].
split.
*
inv H; [|
contradiction].
assumption.
*
apply Forall_Exists_neg.
assumption.
Qed.
Lemma last_indep :
forall {
A} (
l :
list A)
d d',
l <> [] ->
last l d =
last l d'.
Proof.
intros. induction l.
- contradiction.
- destruct l.
+ reflexivity.
+ simpl. apply IHl. discriminate.
Qed.
Lemma last_cons :
forall {
A}
x (
l :
list A)
d,
last (
x::
l)
d =
last l x.
Proof.
intros. induction l.
- reflexivity.
- simpl. simpl in IHl.
destruct l; [reflexivity|assumption].
Qed.
Lemma last_app :
forall {
A} (
l1 l2 :
list A)
d,
l2 <> [] ->
last (
l1 ++
l2)
d =
last l2 d.
Proof.
induction l1; intros.
- reflexivity.
- simpl. destruct (l1 ++ l2) eqn:Hl1l2.
+ destruct l1; simpl in Hl1l2; congruence.
+ rewrite <- Hl1l2. apply IHl1. assumption.
Qed.
Lemma last_in :
forall {
A} (
l :
list A)
d,
In (
last l d) (
d ::
l).
Proof.
intros A l.
induction l;
intros.
-
left;
reflexivity.
-
rewrite last_cons.
right.
apply IHl.
Qed.
Lemma last_not_nil_in :
forall {
A} (
l :
list A)
d,
l <> [] ->
In (
last l d)
l.
Proof.
intros A l.
induction l;
intros.
-
contradiction.
-
destruct l.
+
left;
reflexivity.
+
rewrite last_cons.
right.
apply IHl.
discriminate.
Qed.
Lemma clos_refl_trans_list :
forall {
A} (
R :
A ->
A ->
Prop)
x y,
clos_refl_trans _ R x y <->
exists l,
Sorted R (
x::
l) /\
List.last l x =
y.
Proof.
split;
intros.
{
apply Operators_Properties.clos_rt_rt1n_iff in H.
induction H.
-
exists [].
split; [|
reflexivity].
repeat constructor.
-
destruct IHclos_refl_trans_1n as (
l &
IH1 &
IH2).
exists (
y::
l).
split.
+
constructor; [
assumption|].
constructor.
assumption.
+
rewrite last_cons.
assumption.
}
{
destruct H as (
l &
H1 &
H2).
revert x y H1 H2.
induction l;
intros.
-
simpl in H2.
subst.
constructor 2.
-
inversion H1.
subst a0 l0.
inversion H4.
subst b l0.
econstructor 3.
+
constructor 1.
eassumption.
+
apply IHl.
assumption.
rewrite last_cons in H2.
assumption.
}
Qed.
Lemma directly_included_dec :
forall r u v,
{
directly_included r u v} + {~
directly_included r u v}.
Proof.
intros.
destruct (
r !
u)
as [(
n1,
n2)|]
eqn:
Hru.
-
destruct (
r !
v)
as [(
m1,
m2)|]
eqn:
Hrv.
+
destruct (
Pos.leb_spec0 n1 m1).
*
destruct (
Pos.leb_spec0 m2 n2).
--
left.
exists n1,
n2,
m1,
m2.
repeat split;
assumption.
--
right.
intros (
n1' &
n2' &
m1' &
m2' &
contra1 &
contra2 & (
contra31 &
contra32)).
rewrite contra1 in Hru.
inv Hru.
rewrite contra2 in Hrv.
inv Hrv.
contradiction.
*
right.
intros (
n1' &
n2' &
m1' &
m2' &
contra1 &
contra2 & (
contra31 &
contra32)).
rewrite contra1 in Hru.
inv Hru.
rewrite contra2 in Hrv.
inv Hrv.
contradiction.
+
right.
intros (
_ &
_ &
m1 &
m2 &
_ &
contra &
_).
congruence.
-
right.
intros (
n1 &
n2 &
_ &
_ &
contra &
_).
congruence.
Qed.
Lemma cross_included_dec :
forall r c u v,
{
cross_included r c u v} + {~
cross_included r c u v}.
Proof.
Lemma is_in_t_sdom_1 :
forall dom_pre,
let '(
r,
c,
t,
back) :=
precompute_r_t (
successors f)
f.(
fn_entrypoint)
dom_pre in
forall d u p v,
SSApath f (
PState u)
p (
PState v) ->
Forall (
sdom f d) (
p ++ [
v]) ->
exists t',
is_in_t (
successors f)
back u t' /\
sdom f d t' /\
reduced_reachable back t'
v.
Proof.
intros.
destruct (
precompute_r_t (
successors f)
f.(
fn_entrypoint)
dom_pre)
as (((
r,
c),
t),
back)
eqn:
Hprecompute_r_t.
intros.
exploit precompute_r_t_r_c_correct.
rewrite Hprecompute_r_t.
intros R_C_correct.
remember (
PState u)
as U.
remember (
PState v)
as V.
revert dependent v.
revert dependent u.
induction H;
intros.
-
inv HeqU.
inv H.
exists u.
split; [|
split].
+
apply rt_refl.
+
inv H0.
assumption.
+
constructor.
-
inv STEP; [|
inv H;
inv STEP].
inv H1.
inv H0.
destruct (
cross_included_dec r c u v).
+
exists u.
split; [
constructor 2|].
split; [
assumption|].
apply R_C_correct;
assumption.
+
destruct IHpath with (
u:=
pc') (
v0:=
v)
as (
t' &
IH1 &
IH2 &
IH3).
reflexivity.
reflexivity.
assumption.
destruct (
proj1 (
clos_refl_trans_list _ _ _)
IH1)
as (
l &
H31 &
H32).
destruct (
Exists_first (
fun x => ~
cross_included r c u x))
with (
l:=
pc'::
l++[
v])
as (
l1 &
x &
l2 &
H41 &
H42 &
H43).
simpl.
intros x.
destruct (
cross_included_dec r c u x).
right.
intros contra.
contradiction.
left.
assumption.
apply Exists_exists.
exists v.
split; [|
assumption].
right.
rewrite in_app_iff.
right;
left;
reflexivity.
exists t'.
split; [|
split;
assumption].
assert (
l2 = [] \/
l2 <> [])
as Ha
by (
destruct l2; [
left|
right];
congruence).
destruct Ha as [
Ha|
Ha].
*
subst l2.
rewrite app_comm_cons in H41.
apply app_inj_tail in H41.
destruct H41 as [
H41 H41'].
subst x l1.
rewrite Forall_forall in H43.
contradiction (
H43 t').
rewrite <-
H32.
apply last_in.
intros contra.
apply n.
apply R_C_correct.
split; [
apply reached_reachable;
assumption|].
split.
destruct STEP0.
apply successors_not_nil.
congruence.
eapply reduced_reachable_trans; [|
eassumption].
apply R_C_correct.
assumption.
*
destruct (
exists_last Ha)
as (
l2' &
v' &
Ha').
subst l2.
rewrite 2!
app_comm_cons in H41.
rewrite app_assoc in H41.
apply app_inj_tail in H41.
destruct H41 as [
H41 H41'].
subst v'.
apply clos_refl_trans_list.
exists (
x::
l2').
split.
--
constructor.
rewrite H41 in H31.
apply Sorted_app_r in H31.
assumption.
constructor.
split.
intros contra.
apply H42.
apply R_C_correct.
split; [
apply reached_reachable;
assumption|].
split; [|
assumption].
destruct STEP0.
apply successors_not_nil.
congruence.
s is obtained from the last element of [l1] or is [u] if [l1] is nil *)
assert (
l1 = [] \/
l1 <> [])
as Hb
by (
destruct l1; [
left|
right];
congruence).
destruct Hb as [
Hb|
Hb].
++
subst l1.
inversion H41.
subst x l2'.
exists u.
split; [|
constructor].
destruct (
in_dec p2eq (
u,
pc')
back); [
assumption|].
contradiction H42.
apply R_C_correct.
split; [
apply reached_reachable;
assumption|].
destruct STEP0.
split.
apply successors_not_nil.
congruence.
econstructor;
try eassumption.
constructor.
unfold successors.
rewrite PTree.gmap1.
unfold option_map.
rewrite HCFG_ins.
reflexivity.
++
destruct (
exists_last Hb)
as (
l1' &
y &
Hb').
subst l1.
rewrite H41 in H31.
rewrite app_assoc_reverse in H31.
apply Sorted_app_r in H31.
inversion H31.
subst a l0.
inversion H5.
subst b l0.
destruct H1 as (
H11 &
s &
H12 &
H13).
exists s.
split; [
assumption|].
eapply reduced_reachable_trans; [|
eassumption].
destruct (
cross_included_dec r c u y).
**
apply R_C_correct.
assumption.
**
rewrite Forall_forall in H43.
contradiction (
H43 y).
rewrite in_app_iff.
right;
left;
reflexivity.
--
erewrite <-
last_cons in H32.
rewrite H41 in H32.
rewrite last_app in H32 by discriminate.
eassumption.
Qed.
Lemma is_in_t_sdom_2 :
forall dom_pre,
let '(
r,
c,
t,
back) :=
precompute_r_t (
successors f)
f.(
fn_entrypoint)
dom_pre in
forall d u t'
v,
reached f u ->
is_in_t (
successors f)
back u t' ->
sdom f d t' ->
reduced_reachable back t'
v ->
sdom f d v ->
exists p,
SSApath f (
PState u)
p (
PState v)
/\
Forall (
sdom f d) (
p ++ [
v]).
Proof.
Section QUERIES.
Variable a :
reg.
Variable d :
node.
Hypothesis d_def :
def f a d.
Variable q :
node.
Let live1 :=
fst (
analyze f).
Let live2 :=
snd (
analyze f).
Lemma lemma2 :
live_spec f a q <->
exists p u,
SSApath f (
PState q)
p (
PState u)
/\
Forall (
sdom f d) (
p ++ [
u])
/\
use f a u.
Proof.
split;
intros.
-
apply (
live_spec_reached _ wf)
in H as REACHED.
apply (
live_spec_exists_path _ wf)
in H.
destruct H as (
d' &
u &
p &
H &
H0 &
H1 &
H2).
assert (
d' =
d)
by (
eapply ssa_def_unique;
eauto);
subst.
exploit (
wf.(
fn_strict _));
try eassumption.
intros DOM.
exists p,
u.
split; [
assumption|].
split.
+
eapply dom_intermediate;
try eassumption.
*
constructor.
assumption.
intros contra.
apply H2.
rewrite in_app_iff.
right;
left;
congruence.
*
intros contra.
apply H2.
rewrite in_app_iff.
left;
congruence.
+
assumption.
-
destruct H as (
p &
u &
H &
H0 &
H1).
rewrite Forall_forall in H0.
eapply (
exists_path_live_spec _ wf);
try eassumption.
intros contra.
apply H0 in contra.
inv contra.
contradiction.
Qed.
Theorem analyze_1_complete :
live_spec f a q ->
live1 a q =
true.
Proof.
Theorem analyze_1_sound :
live1 a q =
true ->
live_spec f a q.
Proof.
Theorem analyze_2_complete :
live_spec f a q ->
live2 a q =
true.
Proof.
intros.
unfold analyze in live2.
unfold Time.time in live2.
set (
dom_pre :=
fun u =>
match f.(
fn_dom) !
u with
|
Some num =>
num.(
pre)
|
None => 0
end)
in live2.
destruct (
precompute_r_t (
successors f)
f.(
fn_entrypoint)
dom_pre)
as (((
r,
c),
t),
back)
eqn:
Hprecompute_r_t.
simpl in live2.
unfold live2.
assert (
forall u,
reachable (
fn_entrypoint f)
u -> (
successors f) !
u <>
None)
as g_reachable_closed.
{
intros.
apply successors_not_nil.
apply ssa_reached_closed.
apply reachable_reached.
assumption.
}
assert (
forall u v,
reachable (
fn_entrypoint f)
u ->
reachable (
fn_entrypoint f)
v ->
dom_pre u =
dom_pre v ->
u =
v)
as dom_pre_inj.
{
intros.
unfold dom_pre in H2.
destruct (
f.(
fn_dom) !
u)
eqn:
Hu.
-
destruct (
f.(
fn_dom) !
v)
eqn:
Hv.
+
eapply wf.(
fn_dom_wf _).(
dom_pre_inj _);
eassumption.
+
contradiction (
wf.(
fn_dom_wf _).(
dom_defined _)
v).
apply reachable_reached;
assumption.
-
contradiction (
wf.(
fn_dom_wf _).(
dom_defined _)
u).
apply reachable_reached;
assumption.
}
apply lemma2 in H as H0.
destruct H0 as (
p &
u &
H01 &
H02 &
H03).
exploit is_in_t_sdom_1.
rewrite Hprecompute_r_t.
intros H1.
edestruct H1 as (
t' &
H11 &
H12 &
H13);
try eassumption.
apply (
live_spec_reached _ wf)
in H as Hreached.
unfold is_live_in.
erewrite (
compute_def_correct _ wf);
try eassumption.
assert (
exists i_d,
f.(
fn_dom) !
d =
Some i_d)
as (
i_d &
Hi_d).
{
destruct (
f.(
fn_dom) !
d)
as [
i_d|]
eqn:
Hi_d.
-
eexists;
reflexivity.
-
contradiction (
wf.(
fn_dom_wf _).(
dom_defined _)
d).
inv H12.
inv DOM; [
contradiction|].
destruct (
reached_path (
cfg f) (
exit f) (
entry f)
_ RPC')
as (
p1 &
H2).
destruct (
in_path_split peq (
cfg f) (
exit f) (
entry f)
_ _ _ _ H2 (
PATH _ H2))
as (
p2 &
_ &
H3 &
_).
eapply path_reached.
eassumption.
}
assert (
exists i_q,
f.(
fn_dom) !
q =
Some i_q)
as (
i_q &
Hi_q).
{
destruct (
f.(
fn_dom) !
q)
as [
i_q|]
eqn:
Hi_q.
-
eexists;
reflexivity.
-
contradiction (
wf.(
fn_dom_wf _).(
dom_defined _)
q).
}
rewrite Hi_d,
Hi_q.
apply andb_true_iff.
split.
-
eapply (
live_spec_strict _ wf)
in H as Hsdom;
try eassumption.
apply (
sdom_test_correct _ wf)
in Hsdom;
try assumption.
unfold sdom_test,
is_strict_ancestor in Hsdom.
rewrite Hi_d,
Hi_q in Hsdom.
apply itv_strict_incl_spec in Hsdom.
destruct Hsdom as (
Hsdom1 &
Hsdom2).
apply andb_true_iff.
split; [
apply Z.ltb_lt|
apply Z.leb_le];
assumption.
-
exploit precompute_r_t_t_correct;
try eassumption.
rewrite Hprecompute_r_t.
intros.
exploit (
proj2 (
H0 q t')).
split; [
apply reached_reachable;
assumption|
assumption].
intros.
destruct H2 as (
set &
H21 &
H22).
change SSAfastliveprecomputeRT.node with node in H21.
rewrite H21.
assert (
reached f t')
as t'
_reached.
{
inv H12.
inv DOM; [
contradiction|].
assumption. }
assert (
r !
t' <>
None)
as t'
_black.
{
exploit precompute_r_t_r_in_g.
rewrite Hprecompute_r_t.
intros.
eapply H2.
split.
-
apply reached_reachable.
assumption.
-
apply successors_not_nil.
apply ssa_reached_closed.
assumption.
}
assert (
exists i_t',
f.(
fn_dom) !
t' =
Some i_t')
as (
i_t' &
Hi_t').
{
destruct (
f.(
fn_dom) !
t')
as [
i_t'|]
eqn:
Hi_t'.
-
eexists;
reflexivity.
-
contradiction (
wf.(
fn_dom_wf _).(
dom_defined _)
t').
}
eapply (
sdom_test_correct _ wf)
in H12 as Hsdom;
try eassumption.
unfold sdom_test,
is_strict_ancestor in Hsdom.
rewrite Hi_d,
Hi_t'
in Hsdom.
apply itv_strict_incl_spec in Hsdom.
destruct Hsdom as (
Hsdom1 &
Hsdom2).
unfold DomTest.Z.int_lt in Hsdom1.
unfold DomTest.Z.int_le in Hsdom2.
apply wf.(
fn_dom_wf _).(
dom_pre_le_post _)
in Hi_t'
as Hwf_i_t';
try assumption.
assert (
Sorted (
fun u v =>
dom_pre u <
dom_pre v)
set)
as set_sorted.
{
exploit precompute_r_t_t_sorted;
try eassumption.
rewrite Hprecompute_r_t.
eauto.
}
apply Sorted_StronglySorted in set_sorted;
[|
intros n1 n2 n3;
apply Z.lt_trans].
assert (
forall t'',
In t''
set ->
t_linked t q t'')
as Ha
by (
intros;
eexists;
split;
eassumption).
clear H21.
assert (
i_d.(
pre) <=
i_d.(
pre))
as Hmin1 by reflexivity.
assert (
i_d.(
pre) <
i_t'.(
pre))
as Hmin2 by assumption.
revert Hmin1 Hmin2.
generalize i_d.(
pre)
at 2 3 4
as min.
induction set as [|
t''
set].
+
contradiction H22.
+
intros.
simpl.
destruct H22 as [
H22|
H22].
*
subst t''.
rewrite Hi_t'.
destruct (
Z.ltb_spec i_d.(
post)
i_t'.(
pre)); [
xomega|].
destruct (
Z.leb_spec i_t'.(
pre)
min); [
xomega|].
apply orb_true_iff.
left.
apply existsb_exists.
exists u.
split; [
apply (
make_du_chain_correct _ wf);
assumption|].
apply can_reach_spec;
try assumption.
exploit precompute_r_t_r_c_correct.
rewrite Hprecompute_r_t.
intros.
apply H4.
split; [|
split].
--
apply reached_reachable;
assumption.
--
apply successors_not_nil.
apply ssa_reached_closed.
assumption.
--
assumption.
*
assert (
r !
t'' <>
None)
as t''
_black.
{
exploit precompute_r_t_t_target_black;
try eassumption.
rewrite Hprecompute_r_t.
intros.
eapply H2.
apply Ha.
left;
reflexivity.
}
assert (
reached f t'')
as t''
_reached.
{
exploit precompute_r_t_r_in_g.
rewrite Hprecompute_r_t.
intros.
apply reachable_reached,
H2.
assumption.
}
assert (
exists i_t'',
f.(
fn_dom) !
t'' =
Some i_t'')
as (
i_t'' &
Hi_t'').
{
destruct (
f.(
fn_dom) !
t'')
as [
i_t''|]
eqn:
Hi_t''.
-
eexists;
reflexivity.
-
contradiction (
wf.(
fn_dom_wf _).(
dom_defined _)
t'').
}
rewrite Hi_t''.
inv set_sorted.
rewrite Forall_forall in H5.
apply H5 in H22 as H6.
unfold dom_pre in H6.
rewrite Hi_t'',
Hi_t'
in H6.
destruct (
Z.ltb_spec i_d.(
post)
i_t''.(
pre)); [
xomega|].
destruct (
Z.leb_spec i_t''.(
pre)
min).
--
apply IHset;
try assumption.
intros t'''.
intros.
apply Ha.
right;
assumption.
--
rewrite orb_true_iff.
destruct (
Z.le_gt_cases i_t'.(
pre)
i_t''.(
post)).
++
left.
apply existsb_exists.
exists u.
split; [
apply (
make_du_chain_correct _ wf);
assumption|].
apply can_reach_spec;
try assumption.
exploit precompute_r_t_r_c_correct.
rewrite Hprecompute_r_t.
intros.
apply H8.
split; [|
split].
**
apply reached_reachable;
assumption.
**
apply successors_not_nil.
apply ssa_reached_closed.
assumption.
**
eapply reduced_reachable_trans; [|
eassumption].
exploit dom_reduced_reachable.
rewrite Hprecompute_r_t.
intros.
apply H9.
eapply wf.(
fn_dom_wf _).(
dom_test_correct _);
try eassumption.
unfold dom_test,
is_ancestor.
rewrite Hi_t'',
Hi_t'.
apply itv_incl_spec.
split;
unfold DomTest.Z.int_le; [
xomega|].
pre i_t'' < pre i_t' <= post i_t''
Since the intervals i_t' and i_t'' are disjoint or included,
this means that i_t' is included in i_t'', hence the result.
*)
edestruct wf.(
fn_dom_wf _).(
dom_cases _)
with (
u:=
t') (
v:=
t'')
as [
H10|[
H10|[
H10|
H10]]];
try eassumption;
[| |
destruct H10 as (
H101 &
H102);
unfold DomTest.Z.int_le in H101,
H102..];
xomega.
++
right.
apply IHset;
try assumption.
intros t'''.
intros.
apply Ha.
right;
assumption.
apply wf.(
fn_dom_wf _).(
dom_pre_le_post _)
in Hi_t'';
try assumption.
xomega.
Qed.
Theorem analyze_2_sound :
live2 a q =
true ->
live_spec f a q.
Proof.
intros.
unfold analyze in live2.
unfold Time.time in live2.
set (
dom_pre :=
fun u =>
match f.(
fn_dom) !
u with
|
Some num =>
num.(
pre)
|
None => 0
end)
in live2.
destruct (
precompute_r_t (
successors f)
f.(
fn_entrypoint)
dom_pre)
as (((
r,
c),
t),
back)
eqn:
Hprecompute_r_t.
change (
SSAfastliveprecomputeRT.node)
with node in *.
simpl in live2.
unfold live2 in H.
assert (
forall u,
reachable (
fn_entrypoint f)
u -> (
successors f) !
u <>
None)
as g_reachable_closed.
{
intros.
apply successors_not_nil.
apply ssa_reached_closed.
apply reachable_reached.
assumption.
}
assert (
forall u v,
reachable (
fn_entrypoint f)
u ->
reachable (
fn_entrypoint f)
v ->
dom_pre u =
dom_pre v ->
u =
v)
as dom_pre_inj.
{
intros.
unfold dom_pre in H2.
destruct (
f.(
fn_dom) !
u)
eqn:
Hu.
-
destruct (
f.(
fn_dom) !
v)
eqn:
Hv.
+
eapply wf.(
fn_dom_wf _).(
dom_pre_inj _);
eassumption.
+
contradiction (
wf.(
fn_dom_wf _).(
dom_defined _)
v).
apply reachable_reached;
assumption.
-
contradiction (
wf.(
fn_dom_wf _).(
dom_defined _)
u).
apply reachable_reached;
assumption.
}
unfold is_live_in in H.
erewrite (
compute_def_correct _ wf)
in H;
try eassumption.
destruct (
f.(
fn_dom) !
d)
as [
i_d|]
eqn:
Hi_d; [|
discriminate].
destruct (
f.(
fn_dom) !
q)
as [
i_q|]
eqn:
Hi_q; [|
discriminate].
apply andb_true_iff in H.
destruct H as (
HH1 &
HH2).
apply andb_true_iff in HH1.
destruct HH1 as (
HH11 &
HH12).
apply Z.ltb_lt in HH11.
apply Z.leb_le in HH12.
destruct (
t !
q)
as [
set|]
eqn:
Htq; [|
discriminate].
assert (
forall t',
In t'
set ->
t_linked t q t')
as Ha
by (
intros;
eexists;
split;
eassumption).
clear Htq.
assert (
i_d.(
pre) <=
i_d.(
pre))
as Hmin1 by reflexivity.
revert Hmin1 HH2.
generalize i_d.(
pre)
at 2 3
as min.
induction set as [|
t'
set];
intros.
-
simpl in HH2.
discriminate.
-
simpl in HH2.
destruct (
f.(
fn_dom) !
t')
as [
i_t'|]
eqn:
Hi_t'; [|
discriminate].
destruct (
Z.ltb_spec i_d.(
post)
i_t'.(
pre)); [
discriminate|].
destruct (
Z.leb_spec i_t'.(
pre)
min).
+
eapply IHset;
try eassumption.
intros t''.
intros.
apply Ha.
right;
assumption.
+
apply orb_true_iff in HH2.
destruct HH2 as [
HH2|
HH2].
*
apply existsb_exists in HH2.
destruct HH2 as (
u &
HH21 &
HH22).
apply (
make_du_chain_complete _ wf)
in HH21.
assert (
r !
t' <>
None)
as t'
_black.
{
exploit precompute_r_t_t_target_black;
try eassumption.
rewrite Hprecompute_r_t.
intros.
eapply H1.
apply Ha.
left;
reflexivity.
}
apply can_reach_spec in HH22;
try assumption.
exploit precompute_r_t_r_c_correct.
rewrite Hprecompute_r_t.
intros.
apply H1 in HH22.
destruct HH22 as (
HH221 &
HH222 &
HH223).
exploit (
proj1 (
sdom_test_correct _ wf t'
d (
reachable_reached _ _ HH221))).
{
unfold sdom_test,
is_strict_ancestor.
rewrite Hi_d,
Hi_t'.
apply itv_strict_incl_spec.
split; [
unfold DomTest.Z.int_lt;
xomega|].
unfold DomTest.Z.int_le.
pre i_d < pre i_t' <= post i_d
Since the intervals i_d and i_t' are disjoint or included,
this means that i_t' is included in i_d, hence the result.
*)
edestruct wf.(
fn_dom_wf _).(
dom_cases _)
with (
u:=
d) (
v:=
t')
as [
H6|[
H6|[
H6|
H6]]];
try eassumption;
[| |
destruct H6 as (
H61 &
H62);
unfold DomTest.Z.int_le in H61,
H62..];
xomega.
}
intros Hsdom.
exploit precompute_r_t_t_correct;
try eassumption.
rewrite Hprecompute_r_t.
intros.
exploit (
proj1 (
H2 q t')).
apply Ha.
left;
reflexivity.
intros (
H3 &
H4).
exploit is_in_t_sdom_2.
rewrite Hprecompute_r_t.
intros.
eapply H5 in H4;
try eassumption.
--
destruct H4 as (
p &
H41 &
H42).
apply lemma2.
exists p,
u.
split; [|
split];
assumption.
--
apply reachable_reached.
assumption.
--
constructor; [
eapply wf.(
fn_strict _);
eassumption|].
intros contra.
subst.
inv Hsdom.
exploit dom_reduced_reachable.
rewrite Hprecompute_r_t.
intros.
apply H6 in DOM.
exploit reduced_reachable_antisym.
rewrite Hprecompute_r_t.
intros.
contradiction NEQ.
symmetry.
eapply H7;
eassumption.
*
apply IHset with (
min:=
i_t'.(
post));
try assumption.
intros t''.
intros.
apply Ha.
right;
assumption.
apply wf.(
fn_dom_wf _).(
dom_pre_le_post _)
in Hi_t';
try assumption.
xomega.
Qed.
End QUERIES.
Lemma analyze_1_use :
let live1 :=
fst (
analyze f)
in
forall a q,
live1 a q =
true ->
exists pc,
use f a pc.
Proof.
Theorem analyze_1_correct :
let live1 :=
fst (
analyze f)
in
forall a q,
live1 a q =
true <->
live_spec f a q.
Proof.
Lemma analyze_2_use :
let live2 :=
snd (
analyze f)
in
forall a q,
live2 a q =
true ->
exists pc,
use f a pc.
Proof.
Theorem analyze_2_correct :
let live2 :=
snd (
analyze f)
in
forall a q,
live2 a q =
true <->
live_spec f a q.
Proof.
End CORRECTNESS.