Proof of CSSApargen transformation
Require Recdef.
Require Import FSets.
Require Import Coqlib.
Require Import Ordered.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Smallstep.
Require Import CSSApar.
Require Import SSA.
Require Import SSAutils.
Require Import CSSApargen.
Require Import Kildall.
Require Import Conventions.
Require Import Utils.
Require Import NArith.
Require Import Events.
Require Import Bijection.
Require Import Permutation.
Require Import Utilsvalidproof.
Require Import KildallComp.
Require Import DLib.
Require Import CSSApargenspec.
Require Import CSSAutils.
Ltac sz :=
unfold Plt,
Ple in * ; (
zify;
omega).
Reasoning about monadic computations
Remark bind_inversion:
forall (
A B:
Type) (
f:
mon A) (
g:
A ->
mon B)
(
y:
B) (
s1 s3:
state) (
i:
state_incr s1 s3),
bind f g s1 =
OK y s3 i ->
exists x,
exists s2,
exists i1,
exists i2,
f s1 =
OK x s2 i1 /\
g x s2 =
OK y s3 i2.
Proof.
intros until i. unfold bind. destruct (f s1); intros.
discriminate.
exists a; exists s'; exists s.
destruct (g a s'); inv H.
exists s0; auto.
Qed.
Remark bind2_inversion:
forall (
A B C:
Type) (
f:
mon (
A*
B)) (
g:
A ->
B ->
mon C)
(
z:
C) (
s1 s3:
state) (
i:
state_incr s1 s3),
bind2 f g s1 =
OK z s3 i ->
exists x,
exists y,
exists s2,
exists i1,
exists i2,
f s1 =
OK (
x,
y)
s2 i1 /\
g x y s2 =
OK z s3 i2.
Proof.
unfold bind2; intros.
exploit bind_inversion; eauto.
intros [[x y] [s2 [i1 [i2 [P Q]]]]]. simpl in Q.
exists x; exists y; exists s2; exists i1; exists i2; auto.
Qed.
Ltac monadInv1 H :=
match type of H with
| (
OK _ _ _ =
OK _ _ _) =>
inversion H;
clear H;
try subst
| (
Error _ _ =
OK _ _ _) =>
discriminate
| (
ret _ _ =
OK _ _ _) =>
inversion H;
clear H;
try subst
| (
error _ _ =
OK _ _ _) =>
discriminate
| (
bind ?
F ?
G ?
S =
OK ?
X ?
S' ?
I) =>
let x :=
fresh "
x"
in (
let s :=
fresh "
s"
in (
let i1 :=
fresh "
INCR"
in (
let i2 :=
fresh "
INCR"
in (
let EQ1 :=
fresh "
EQ"
in (
let EQ2 :=
fresh "
EQ"
in (
destruct (
bind_inversion _ _ F G X S S'
I H)
as [
x [
s [
i1 [
i2 [
EQ1 EQ2]]]]];
clear H;
try (
monadInv1 EQ2)))))))
| (
bind2 ?
F ?
G ?
S =
OK ?
X ?
S' ?
I) =>
let x1 :=
fresh "
x"
in (
let x2 :=
fresh "
x"
in (
let s :=
fresh "
s"
in (
let i1 :=
fresh "
INCR"
in (
let i2 :=
fresh "
INCR"
in (
let EQ1 :=
fresh "
EQ"
in (
let EQ2 :=
fresh "
EQ"
in (
destruct (
bind2_inversion _ _ _ F G X S S'
I H)
as [
x1 [
x2 [
s [
i1 [
i2 [
EQ1 EQ2]]]]]];
clear H;
try (
monadInv1 EQ2))))))))
end.
Ltac monadInv H :=
match type of H with
| (
ret _ _ =
OK _ _ _) =>
monadInv1 H
| (
error _ _ =
OK _ _ _) =>
monadInv1 H
| (
bind ?
F ?
G ?
S =
OK ?
X ?
S' ?
I) =>
monadInv1 H
| (
bind2 ?
F ?
G ?
S =
OK ?
X ?
S' ?
I) =>
monadInv1 H
| (?
F _ _ _ _ _ _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
try monadInv1 H
| (?
F _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
end.
Utility lemmas
Lemma Plt_neq :
forall (
r1 r2 :
reg),
Plt (
fst r1) (
fst r2) ->
r1 <>
r2.
Proof.
intros.
assert (fst r1 <> fst r2) by auto.
congruence.
Qed.
Hint Resolve Plt_neq.
Lemma nth_error_nil_notSome_node :
forall k,
nth_error (
nil:
list node)
k =
None.
Proof.
induction k; auto.
Qed.
Lemma nth_error_nil_notSome_reg :
forall k,
nth_error (
nil:
list reg)
k =
None.
Proof.
induction k; auto.
Qed.
Hint Resolve nth_error_nil_notSome_node
nth_error_nil_notSome_reg.
Lemma notIn_notnth:
forall k (
nodes:
list node)
pc,
~
In pc nodes ->
nth_error nodes k <>
Some pc.
Proof.
induction k; intros.
+ simpl. flatten.
unfold Specif.error. congruence.
unfold value. unfold not in *; intros.
apply H. constructor. congruence.
+ simpl. flatten.
unfold Specif.error. congruence.
apply IHk.
unfold not in *; intros.
apply H. constructor 2. auto.
Qed.
Lemma nth_In_reg:
forall k (
regs:
list reg)
r,
nth_error regs k =
Some r ->
In r regs.
Proof.
induction k; intros; simpl in *;
flatten regs; unfold Specif.error in H;
unfold value in H; go.
Qed.
Hint Resolve nth_In_reg.
Lemma nth_In_node:
forall k (
nodes:
list node)
pc,
nth_error nodes k =
Some pc ->
In pc nodes.
Proof.
induction k; intros; simpl in *;
flatten regs; unfold Specif.error in H;
unfold value in H; go.
Qed.
Hint Resolve nth_In_node.
Kildall lemmas
Lemma add_successors_other :
forall l pred from pc,
~
In pc l ->
pred !!!
pc = (
add_successors pred from l) !!!
pc.
Proof.
induction l; intros.
+ simpl in *. congruence.
+ simpl in *.
case_eq (peq a pc); intros.
- rewrite e in *.
intuition.
- assert (~ In pc l) by intuition.
replace (pred !!! pc) with
((PTree.set a (from :: pred !!! a) pred)
!!! pc).
eapply IHl; eauto.
unfold successors_list in *.
rewrite PTree.gso; auto.
Qed.
Lemma add_successors_notfrom :
forall l pred from pc pc',
~
In pc' (
pred !!!
pc) ->
pc' <>
from ->
~
In pc' ((
add_successors pred from l) !!!
pc).
Proof.
induction l; intros.
+ simpl in *. congruence.
+ simpl in *.
unfold successors_list.
flatten; go.
flatten Eq; go.
assert(Eqsuccs:
(add_successors (PTree.set a (from :: l1) pred)
from l) !!! pc = l0).
{ unfold successors_list; go. }
rewrite <- Eqsuccs.
apply IHl; auto.
{ case_eq (peq a pc); intros.
- rewrite e in *.
unfold successors_list.
rewrite PTree.gss.
unfold not; intros HIn.
inv HIn; auto.
apply H.
unfold successors_list.
go.
- unfold successors_list.
rewrite PTree.gso; auto.
}
assert(Eqsuccs:
(add_successors (PTree.set a (from :: nil) pred)
from l) !!! pc = l0).
{ unfold successors_list; go. }
rewrite <- Eqsuccs.
apply IHl; auto.
{ case_eq (peq a pc); intros.
- rewrite e in *.
unfold successors_list.
rewrite PTree.gss.
unfold not; intros HIn.
inv HIn; auto.
- unfold successors_list.
rewrite PTree.gso; auto.
}
Qed.
Lemma not_in_foldelems :
forall pc pc'
elems predinit,
~
In pc' (
map fst elems) ->
~
In pc' (
predinit !!!
pc) ->
~
In pc' (
fold_right
(
fun pcins pred =>
add_successors pred (
fst pcins)
(
successors_instr (
snd pcins)))
predinit elems) !!!
pc.
Proof.
intro pc.
induction elems; intros.
+ simpl. auto.
+ simpl in *.
apply add_successors_notfrom; go.
eapply IHelems; eauto.
Qed.
Lemma nodups_in_preds_aux :
forall pc elems predinit,
(
forall pcins,
In pcins elems ->
In pc (
successors_instr (
snd pcins)) ->
(
successors_instr (
snd pcins)) =
pc ::
nil) ->
(
forall elt,
In elt elems ->
~
In (
fst elt) (
predinit !!!
pc)) ->
NoDup (
map fst elems) ->
NoDup (
predinit !!!
pc) ->
NoDup
(
List.fold_right
(
fun pcins pred =>
add_successors pred (
fst pcins)
(
successors_instr (
snd pcins)))
predinit elems) !!!
pc.
Proof.
intro pc.
induction elems; intros.
+ simpl. auto.
+ simpl.
case_eq (in_dec peq pc (successors_instr (snd a)));
intros.
- assert (Succs: successors_instr (snd a) = pc :: nil)
by auto.
rewrite Succs.
simpl.
unfold successors_list.
rewrite PTree.gss.
simpl in H1.
constructor.
inv H1.
apply not_in_foldelems; eauto.
apply IHelems; auto.
inv H1; auto.
- rewrite <- add_successors_other; go.
apply IHelems; go.
inv H1; auto.
Qed.
Lemma nodups_in_preds :
forall l f preds pc,
wf_ssa_function f ->
preds =
make_predecessors (
fn_code f)
successors_instr ->
(
fn_phicode f) !
pc <>
None ->
preds !
pc =
Some (
l :
list node) ->
~
In pc l ->
NoDup (
pc ::
l).
Proof.
intros.
constructor; auto.
assert(EQ: preds !!! pc = l).
unfold successors_list; go.
rewrite <- EQ.
rewrite H0.
unfold make_predecessors.
rewrite PTree.fold_spec.
rewrite <- List.fold_left_rev_right.
apply nodups_in_preds_aux; intros.
{ rewrite <- in_rev in H4.
destruct pcins.
simpl in *.
assert ((fn_code f) ! p = Some i).
apply PTree.elements_complete. auto.
assert (JP: join_point pc f).
induction H. apply fn_phicode_inv. auto.
assert (Insuccs: In pc (succs f p)).
unfold successors.
unfold successors_list. flatten.
{ rewrite PTree.gmap1 in Eq.
rewrite H6 in Eq.
simpl in *. go. }
{ rewrite PTree.gmap1 in Eq.
rewrite H6 in Eq.
simpl in *. congruence. }
assert ((fn_code f) ! p = Some (Inop pc)).
induction H.
apply fn_normalized; auto.
assert(RW: i = Inop pc).
congruence.
rewrite RW. auto.
}
{ unfold successors_list. flatten ; auto.
assert((PTree.empty (list positive)) ! pc = None).
apply PTree.gempty. congruence. }
{ rewrite map_rev.
cut (NoDup (rev (rev (map fst
(PTree.elements (fn_code f))))));
intros.
apply nodups_rev.
auto.
rewrite rev_involutive.
assert (list_norepet
(map fst (PTree.elements (fn_code f)))).
apply PTree.elements_keys_norepet.
apply list_norepet_NoDup; auto. }
{ unfold successors_list; flatten.
assert ((PTree.empty (list positive)) ! pc = None).
apply PTree.gempty. congruence.
constructor. }
Qed.
Lemma in_successors_if_succofpred :
forall f pc l k n i,
(
fn_code f) !
n =
Some i ->
(
make_predecessors (
fn_code f)
successors_instr)
!
pc =
Some l ->
nth_error l k =
Some n ->
In pc ((
successors f) !!!
n).
Proof.
intros.
unfold successors_list.
unfold successors.
rewrite PTree.gmap1.
unfold option_map.
rewrite H.
apply make_predecessors_correct2
with (code := (fn_code f)) (n0 := n).
auto.
assert((make_predecessors (fn_code f) successors_instr)
!!! pc = l).
unfold successors_list. flatten.
unfold make_preds.
rewrite H2.
eapply nth_In_node; eauto.
Qed.
Lemma inop_is_not_in_two_preds :
forall f l pred pc pc',
(
make_predecessors (
fn_code f)
successors_instr)
!
pc' =
Some l ->
pc <>
pc' ->
(
fn_code f) !
pred =
Some (
Inop pc) ->
~
In pred l.
Proof.
intros.
assert(preds: (make_predecessors (fn_code f) successors_instr)
!!! pc' = l).
unfold successors_list. flatten.
rewrite <- preds.
apply make_predecessors_correct2_aux
with (i := Inop pc).
auto.
simpl. intuition.
Qed.
get_maxreg correctness
Lemma ple_foldmaxreg_init :
forall l m n,
Ple m n ->
Ple
m
(
List.fold_left (
fun m r' =>
Pmax m (
fst (
r' :
reg)))
l n).
Proof.
induction l; intros.
simpl. auto.
simpl.
apply Ple_trans with
(Pos.max m (fst a)); auto.
apply Pos.le_max_l.
apply IHl.
apply Pos.max_le_compat.
auto. apply Ple_refl.
Qed.
Lemma max_reg_in_list_correct_aux :
forall l (
r :
reg)
m,
In r l ->
Ple (
fst r)
(
List.fold_left (
fun m r' =>
Pmax m (
fst r'))
l m).
Proof.
induction l; intros.
inv H.
simpl in *.
destruct H.
+ rewrite H in *.
eapply ple_foldmaxreg_init; eauto.
apply Pos.le_max_r.
+ auto.
Qed.
Lemma max_reg_in_list_correct :
forall l r,
In r l ->
Ple (
fst r) (
max_reg_in_list l).
Proof.
unfold max_reg_in_list.
intros.
apply max_reg_in_list_correct_aux.
auto.
Qed.
Lemma max_reg_in_Icall_inl (
ins :
SSA.instruction) :
forall r args res x y,
Ple (
fst r)
(
get_max_reg_in_ins (
Icall x (
inl r)
args res y)).
Proof.
intros.
unfold get_max_reg_in_ins.
apply max_reg_in_list_correct.
constructor. auto.
Qed.
Lemma max_reg_in_Itailcall_inl (
ins :
SSA.instruction) :
forall r args sig,
Ple (
fst r)
(
get_max_reg_in_ins (
Itailcall sig (
inl r)
args)).
Proof.
intros.
unfold get_max_reg_in_ins.
apply max_reg_in_list_correct.
constructor. auto.
Qed.
Lemma max_reg_in_Icall_args (
ins :
SSA.instruction) :
forall ros args arg res sig y,
In arg args ->
Ple (
fst arg)
(
get_max_reg_in_ins (
Icall sig ros args res y)).
Proof.
intros.
unfold get_max_reg_in_ins.
flatten; apply max_reg_in_list_correct.
+ constructor 2.
constructor 2.
auto.
+ constructor 2.
auto.
Qed.
Lemma max_reg_in_Itailcall_args (
ins :
SSA.instruction) :
forall ros args arg sig,
In arg args ->
Ple (
fst arg)
(
get_max_reg_in_ins (
Itailcall sig ros args)).
Proof.
intros.
unfold get_max_reg_in_ins.
flatten; apply max_reg_in_list_correct.
+ constructor 2.
auto.
+ auto.
Qed.
Lemma max_reg_in_Iop_args (
ins :
SSA.instruction) :
forall op args arg res pc,
In arg args ->
Ple (
fst arg)
(
get_max_reg_in_ins (
Iop op args res pc)).
Proof.
intros.
unfold get_max_reg_in_ins.
flatten; apply max_reg_in_list_correct.
constructor 2. auto.
Qed.
Lemma max_reg_in_Iload_args (
ins :
SSA.instruction) :
forall chunk addr args arg dst pc,
In arg args ->
Ple (
fst arg)
(
get_max_reg_in_ins (
Iload chunk addr args dst pc)).
Proof.
intros.
unfold get_max_reg_in_ins.
flatten; apply max_reg_in_list_correct.
constructor 2. auto.
Qed.
Lemma max_reg_in_Istore_args (
ins :
SSA.instruction) :
forall chunk addr args arg src pc,
In arg args ->
Ple (
fst arg)
(
get_max_reg_in_ins (
Istore chunk addr args src pc)).
Proof.
intros.
unfold get_max_reg_in_ins.
flatten; apply max_reg_in_list_correct.
constructor 2. auto.
Qed.
Lemma max_reg_in_Istore_src (
ins :
SSA.instruction) :
forall chunk addr args src pc,
Ple (
fst src)
(
get_max_reg_in_ins (
Istore chunk addr args src pc)).
Proof.
intros.
unfold get_max_reg_in_ins.
flatten; apply max_reg_in_list_correct.
constructor. auto.
Qed.
Lemma max_reg_in_Ibuiltin_args (
ins :
SSA.instruction) :
forall ef args arg res pc,
In arg args ->
Ple (
fst arg)
(
get_max_reg_in_ins (
Ibuiltin ef args res pc)).
Proof.
intros.
unfold get_max_reg_in_ins.
flatten; apply max_reg_in_list_correct.
constructor 2. auto.
Qed.
Lemma max_reg_in_Icond_args (
ins :
SSA.instruction) :
forall cond args arg ifso ifnot,
In arg args ->
Ple (
fst arg)
(
get_max_reg_in_ins (
Icond cond args ifso ifnot)).
Proof.
intros.
unfold get_max_reg_in_ins.
flatten; apply max_reg_in_list_correct.
auto.
Qed.
Lemma max_reg_in_Ijumptable_arg (
ins :
SSA.instruction) :
forall arg tbl,
Ple (
fst arg)
(
get_max_reg_in_ins (
Ijumptable arg tbl)).
Proof.
intros.
unfold get_max_reg_in_ins.
flatten; apply max_reg_in_list_correct.
constructor. auto.
Qed.
Lemma max_reg_in_Ireturn_r (
ins :
SSA.instruction) :
forall r,
Ple (
fst r)
(
get_max_reg_in_ins (
Ireturn (
Some r))).
Proof.
intros.
unfold get_max_reg_in_ins.
flatten; apply max_reg_in_list_correct.
constructor. auto.
Qed.
Lemma max_reg_in_phi_dst :
forall dst args,
Ple (
fst dst) (
get_max_reg_in_phiins (
Iphi args dst)).
Proof.
intros.
unfold get_max_reg_in_phiins.
apply max_reg_in_list_correct.
simpl. auto.
Qed.
Lemma max_reg_in_phi_arg :
forall dst args arg,
In arg args ->
Ple (
fst arg) (
get_max_reg_in_phiins (
Iphi args dst)).
Proof.
intros.
unfold get_max_reg_in_phiins.
apply max_reg_in_list_correct.
simpl. auto.
Qed.
Lemma ple_foldmaxpos_init :
forall l m n,
Ple m n ->
Ple
m
(
List.fold_left (
fun m p =>
Pmax m p)
l n).
Proof.
induction l; intros.
simpl. auto.
simpl.
apply Ple_trans with
(Pos.max m a); auto.
apply Pos.le_max_l.
apply IHl.
apply Pos.max_le_compat.
auto. apply Ple_refl.
Qed.
Lemma ple_foldmaxphi_init :
forall l m n,
Ple m n ->
Ple
m
(
List.fold_left (
fun m phi =>
Pmax m
(
get_max_reg_in_phiins phi))
l n).
Proof.
induction l; intros.
simpl. auto.
simpl.
apply Ple_trans with
(Pos.max m (get_max_reg_in_phiins a)); auto.
apply Pos.le_max_l.
apply IHl.
apply Pos.max_le_compat.
auto. apply Ple_refl.
Qed.
Lemma max_reg_in_phib_dst_aux :
forall phib dst args init,
In (
Iphi args dst)
phib ->
Ple (
get_max_reg_in_phiins (
Iphi args dst))
(
List.fold_left (
fun m phiins =>
Pmax m
(
get_max_reg_in_phiins phiins))
phib init).
Proof.
induction phib; intros.
+ inv H.
+ simpl in *.
destruct H.
- rewrite H in *.
simpl in *.
apply ple_foldmaxphi_init.
apply Pos.le_max_r.
- auto.
Qed.
Lemma max_reg_in_phib_dst :
forall phib dst args,
In (
Iphi args dst)
phib ->
Ple (
get_max_reg_in_phiins (
Iphi args dst))
(
get_max_reg_in_phib phib).
Proof.
intros.
unfold get_max_reg_in_phib.
apply max_reg_in_phib_dst_aux.
auto.
Qed.
Lemma ple_foldmaxphib_init :
forall l m n,
Ple m n ->
Ple
m
(
List.fold_left
(
fun m (
pphib :
positive *
phiblock) =>
Pmax m
(
get_max_reg_in_phib (
snd pphib)))
l n).
Proof.
induction l; intros.
simpl. auto.
simpl.
apply Ple_trans with
(Pos.max m (get_max_reg_in_phib (snd a))); auto.
apply Pos.le_max_l.
apply IHl.
apply Pos.max_le_compat.
auto. apply Ple_refl.
Qed.
Lemma ple_foldmaxins_init :
forall l m n,
Ple m n ->
Ple
m
(
List.fold_left
(
fun m (
pcins :
positive *
instruction) =>
Pmax m
(
get_max_reg_in_ins (
snd pcins)))
l n).
Proof.
induction l; intros.
simpl. auto.
simpl.
apply Ple_trans with
(Pos.max m (get_max_reg_in_ins (snd a))); auto.
apply Pos.le_max_l.
apply IHl.
apply Pos.max_le_compat.
auto. apply Ple_refl.
Qed.
Lemma max_reg_in_phicode_aux :
forall elems init pphib (
pc:
positive)
phib,
In pphib elems ->
pphib = (
pc,
phib) ->
Ple (
get_max_reg_in_phib phib)
(
fold_left
(
fun m p =>
Pos.max m (
get_max_reg_in_phib (
snd p)))
elems init).
Proof.
induction elems; intros.
+ inv H.
+ simpl in *.
destruct H.
- rewrite H in *.
simpl in *.
apply ple_foldmaxphib_init.
destruct pphib. simpl.
assert (p0 = phib) by congruence.
rewrite H1 in *.
apply Pos.le_max_r.
- eauto.
Qed.
Lemma max_reg_in_code_aux :
forall elems pcins (
pc:
positive)
ins init,
In pcins elems ->
pcins = (
pc,
ins) ->
Ple (
get_max_reg_in_ins ins)
(
fold_left
(
fun m p =>
Pmax m (
get_max_reg_in_ins (
snd p)))
elems init).
Proof.
induction elems; intros.
+ inv H.
+ simpl in *.
destruct H.
- rewrite H in *.
simpl in *.
apply ple_foldmaxins_init.
destruct pcins. simpl.
assert (i = ins) by congruence.
rewrite H1 in *.
apply Pos.le_max_r.
- eauto.
Qed.
Lemma max_reg_in_phicode :
forall phicode pc phib,
phicode !
pc =
Some phib ->
Ple (
get_max_reg_in_phib phib)
(
get_max_reg_in_phicode phicode).
Proof.
intros.
unfold get_max_reg_in_phicode.
rewrite PTree.fold_spec.
eapply max_reg_in_phicode_aux; eauto.
apply PTree.elements_correct; eauto.
Qed.
Lemma max_reg_in_code :
forall code pc ins,
code !
pc =
Some ins ->
Ple (
get_max_reg_in_ins ins)
(
get_max_reg_in_code code).
Proof.
intros.
unfold get_max_reg_in_code.
rewrite PTree.fold_spec.
eapply max_reg_in_code_aux; eauto.
apply PTree.elements_correct; eauto.
Qed.
Lemma max_reg_correct_phicode :
forall f,
Ple (
get_max_reg_in_phicode (
fn_phicode f))
(
get_maxreg f).
Proof.
intros.
unfold get_maxreg.
apply Ple_trans with
(Pos.max (get_max_reg_in_phicode (fn_phicode f))
(max_reg_in_list (fn_params f))).
apply Pos.le_max_l.
apply Pos.le_max_r.
Qed.
Lemma max_reg_correct_code :
forall f,
Ple (
get_max_reg_in_code (
fn_code f))
(
get_maxreg f).
Proof.
intros.
unfold get_maxreg.
apply Pos.le_max_l.
Qed.
wf_ssa lemmas for transformation
Lemma wf_unique_def_phib_aux :
forall phib,
NoDup phib ->
(
forall (
r :
reg) (
args0 args' :
list reg),
In (
Iphi args0 r)
phib ->
In (
Iphi args'
r)
phib ->
args0 =
args') ->
unique_def_phib_spec phib.
Proof.
induction phib; go; intros.
destruct a.
constructor; intros.
+ simpl in *.
unfold not; intros.
rewrite H2 in *.
inv H.
assert (l = args').
eapply H0; eauto.
congruence.
+ inv H.
eapply IHphib; eauto.
Qed.
Lemma wf_unique_def_phib :
forall phib f pc,
SSA.wf_ssa_function f ->
(
fn_phicode f) !
pc =
Some phib ->
unique_def_phib_spec phib.
Proof.
intros.
induction H.
unfold unique_def_spec in *.
repeat destruct fn_ssa as [_ fn_ssa].
assert (Hwf: NoDup phib
/\ (forall r args0 args',
In (Iphi args0 r) phib ->
In (Iphi args' r) phib ->
args0 = args')).
eauto.
destruct Hwf.
apply wf_unique_def_phib_aux; auto.
Qed.
Lemma notinpredspc :
forall f pc preds phib,
normalized_jp f ->
(
fn_phicode f) !
pc =
Some phib ->
(
make_predecessors (
fn_code f)
successors_instr)
!
pc =
Some preds ->
~
In pc preds.
Proof.
intros.
unfold not; intros.
assert ((fn_phicode f) ! pc = None).
unfold normalized_jp in H.
eapply H; eauto.
congruence. congruence.
Qed.
The transformation verifies the specification
Lemma initialize_phi_block_correct :
forall x pc s s'
INCR,
initialize_phi_block pc s =
OK x s'
INCR ->
(
st_phicode s') !
pc =
Some nil.
Proof.
intros. unfold initialize_phi_block in H.
flatten H.
simpl. apply PTree.gss.
Qed.
Lemma initialize_parcopy_block_correct :
forall x pc s s'
INCR,
initialize_parcopy_block pc s =
OK x s'
INCR ->
(
st_parcopycode s') !
pc =
Some nil.
Proof.
intros. unfold initialize_parcopy_block in H.
flatten H.
simpl. apply PTree.gss.
Qed.
Lemma initialize_parcopy_block_correct2 :
forall pc'
x pc s s'
INCR,
initialize_parcopy_block pc'
s =
OK x s'
INCR ->
(
st_parcopycode s) !
pc =
Some nil ->
(
st_parcopycode s') !
pc =
Some nil.
Proof.
intros.
case_eq (peq pc pc'); intros.
+ unfold initialize_parcopy_block in H.
flatten H. simpl.
apply PTree.gss.
+ unfold initialize_parcopy_block in H.
flatten H. simpl.
rewrite PTree.gso; auto.
Qed.
Lemma initialize_parcopy_blocks_correct_aux :
forall l x pc s s'
INCR,
initialize_parcopy_blocks l s =
OK x s'
INCR ->
(
st_parcopycode s) !
pc =
Some nil ->
(
st_parcopycode s') !
pc =
Some nil.
Proof.
induction l; intros; simpl in *.
inv H. auto.
simpl in H.
monadInv H.
assert ((st_parcopycode s0) ! pc = Some nil).
eapply initialize_parcopy_block_correct2; eauto.
eauto.
Qed.
Lemma initialize_parcopy_blocks_correct :
forall l x pc s s'
INCR,
initialize_parcopy_blocks l s =
OK x s'
INCR ->
In pc l ->
(
st_parcopycode s') !
pc =
Some nil.
Proof.
induction l; intros.
go.
simpl in *.
monadInv H.
destruct H0; go.
rewrite H in *.
assert ((st_parcopycode s0) ! pc = Some nil).
eapply initialize_parcopy_block_correct; eauto.
eapply initialize_parcopy_blocks_correct_aux; eauto.
Qed.
Hint Resolve initialize_parcopy_blocks_correct.
Lemma initialize_parcopy_blocks_correct_parcother :
forall l x pc s s'
INCR,
initialize_parcopy_blocks l s =
OK x s'
INCR ->
~
In pc l ->
(
st_parcopycode s) !
pc = (
st_parcopycode s') !
pc.
Proof.
induction l; intros.
+ simpl in H. unfold ret in H.
assert (s = s') by congruence.
congruence.
+ simpl in *.
monadInv H.
replace ((st_parcopycode s') ! pc)
with ((st_parcopycode s0) ! pc).
unfold initialize_parcopy_block in EQ.
replace (st_parcopycode s0)
with (PTree.set a nil (st_parcopycode s)).
rewrite PTree.gso. auto. auto.
destruct s0; simpl; congruence.
eapply IHl; eauto.
Qed.
Lemma initialize_parcopy_blocks_correct_other :
forall l u s s'
INCR,
initialize_parcopy_blocks l s =
OK u s'
INCR ->
st_phicode s =
st_phicode s'.
Proof.
induction l; intros.
+ unfold initialize_parcopy_blocks in H.
unfold ret in H. congruence.
+ simpl in *.
monadInv H.
replace (st_phicode s) with (st_phicode s0).
eauto.
unfold initialize_parcopy_block in EQ.
destruct s0; simpl; congruence.
Qed.
Inductive gen_new_regs_spec (
maxreg :
positive)
(
fs_init :
positive)
:
positive ->
list reg ->
list reg ->
Prop :=
|
gen_new_regs_spec_nil:
forall (
GNRSPECinitnil:
Plt maxreg fs_init),
gen_new_regs_spec maxreg fs_init fs_init
nil nil
|
gen_new_regs_spec_cons:
forall arg args arg'
args'
fs_max
(
GNRSPECinit: (
fst arg') =
fs_init)
(
GNRSPECold:
Ple (
fst arg)
maxreg)
(
GNRSPECfresh:
Plt maxreg (
fst arg'))
(
GNRSPECrec:
gen_new_regs_spec maxreg (
Pos.succ fs_init)
fs_max
args args'),
gen_new_regs_spec maxreg fs_init fs_max
(
arg ::
args) (
arg' ::
args').
Lemma gen_new_regs_spec_incr :
forall maxreg fs_init fs_max args args',
gen_new_regs_spec maxreg fs_init fs_max
args args' ->
Ple fs_init fs_max.
Proof.
intros.
induction H; intros.
apply Ple_refl.
apply Ple_trans with (Pos.succ fs_init).
apply Ple_succ.
assumption.
Qed.
Hint Resolve gen_new_regs_spec_incr.
Lemma gen_new_regs_spec_ple_arg_maxreg :
forall maxreg fs_init fs_max args args',
gen_new_regs_spec maxreg fs_init fs_max
args args' ->
forall k arg,
nth_error args k =
Some arg ->
Ple (
fst arg)
maxreg.
Proof.
intros until args'.
intro H. induction H; intros.
+ destruct k; simpl in *; unfold Specif.error in *;
congruence.
+ destruct k; simpl in *; unfold value in *; go.
Qed.
Lemma gen_new_regs_spec_plt_maxreg_arg' :
forall maxreg fs_init fs_max args args',
gen_new_regs_spec maxreg fs_init fs_max
args args' ->
forall k arg',
nth_error args'
k =
Some arg' ->
Plt maxreg (
fst arg').
Proof.
intros until args'.
intro H. induction H; intros.
+ destruct k; simpl in *; unfold Specif.error in *;
congruence.
+ destruct k; simpl in *; unfold value in *; go.
Qed.
Lemma gen_new_regs_spec_max_in :
forall maxreg fs_init fs_max args args',
gen_new_regs_spec maxreg fs_init fs_max
args args' ->
(
forall arg',
In arg'
args' ->
Plt (
fst arg')
fs_max).
Proof.
intros until args'.
intro H.
induction H; intros arg0' Inargs'. inv Inargs'.
simpl in *.
destruct Inargs' as [EQ | Inargs'].
+ rewrite <- EQ.
assert (Plt (fst arg') fs_max).
rewrite GNRSPECinit.
apply Plt_Ple_trans with (Pos.succ fs_init).
apply Plt_succ.
eapply gen_new_regs_spec_incr; eauto.
auto.
+ eauto.
Qed.
Lemma gen_new_regs_spec_plt_maxreg_fs_init :
forall maxreg fs_init fs_max args args',
gen_new_regs_spec maxreg fs_init fs_max
args args' ->
Plt maxreg fs_init.
Proof.
intros.
induction H; intros.
auto.
rewrite GNRSPECinit in GNRSPECfresh.
auto.
Qed.
Hint Resolve gen_new_regs_spec_plt_maxreg_fs_init.
Lemma gen_new_regs_spec_min_in :
forall maxreg fs_init fs_max args args',
gen_new_regs_spec maxreg fs_init fs_max
args args' ->
(
forall arg',
In arg'
args' ->
Ple fs_init (
fst arg')).
Proof.
intros until args'.
intro H.
induction H; intros arg0' Inargs'. inv Inargs'.
simpl in *.
destruct Inargs' as [EQ | Inargs'].
+ rewrite <- EQ.
assert (Ple fs_init (fst arg')).
rewrite GNRSPECinit.
apply Ple_refl.
auto.
+ assert (Ple (Pos.succ fs_init) (fst arg0')) by eauto.
apply Ple_trans with (Pos.succ fs_init).
apply Ple_succ.
auto.
Qed.
Hint Resolve gen_new_regs_spec_min_in.
Lemma gen_new_regs_spec_nthNotNonefromNotNone :
forall maxreg fs_init fs_max args args',
gen_new_regs_spec maxreg fs_init fs_max
args args' ->
forall k,
nth_error args k <>
None
->
nth_error args'
k <>
None.
Proof.
intros until args'. intro H. induction H.
+ intros. auto.
+ intros.
destruct k; simpl in *.
- unfold value in *. congruence.
- eauto.
Qed.
Hint Resolve gen_new_regs_spec_nthNotNonefromNotNone.
Lemma gen_new_regs_spec_nthNotNonetoNotNone :
forall maxreg fs_init fs_max args args',
gen_new_regs_spec maxreg fs_init fs_max
args args' ->
forall k,
nth_error args'
k <>
None
->
nth_error args k <>
None.
Proof.
intros until args'. intro H. induction H.
+ intros. auto.
+ intros.
destruct k; simpl in *.
- unfold value in *. congruence.
- eauto.
Qed.
Hint Resolve gen_new_regs_spec_nthNotNonetoNotNone.
Lemma gen_new_regs_correct :
forall args s s'
args'
INCR maxreg,
(
Plt maxreg (
fst (
next_fresh_reg s))) ->
(
forall arg,
In arg args ->
Ple (
fst arg)
maxreg) ->
gen_new_regs args s =
OK args'
s'
INCR ->
gen_new_regs_spec maxreg (
fst (
next_fresh_reg s))
(
fst (
next_fresh_reg s'))
args args'.
Proof.
induction args; intros.
+ simpl in *.
unfold ret in *.
assert (RW: args' = nil) by congruence.
rewrite RW in *.
assert (RW2: s = s') by congruence.
rewrite RW2 in *.
apply gen_new_regs_spec_nil.
auto.
+ simpl in *.
monadInv H1.
assert (EQfs: fst x = fst (next_fresh_reg s)).
{ unfold gen_newreg in EQ. go. }
apply gen_new_regs_spec_cons; auto.
- assert (Plt maxreg (fst x)).
rewrite EQfs. auto.
auto.
- assert (NextFs: Pos.succ (fst (next_fresh_reg s)) =
fst (next_fresh_reg s0)).
unfold gen_newreg in EQ. go.
rewrite NextFs.
apply IHargs with (INCR := INCR2); auto.
rewrite <- NextFs.
apply Plt_Ple_trans with (fst (next_fresh_reg s));
auto.
apply Ple_succ.
Qed.
Hint Resolve gen_new_regs_correct.
Lemma gen_new_regs_correct_parcode :
forall args s args'
s'
INCR,
gen_new_regs args s =
OK args'
s'
INCR ->
st_parcopycode s =
st_parcopycode s'.
Proof.
induction args; intros.
+ unfold gen_new_regs in *.
unfold ret in *.
congruence.
+ simpl in *.
monadInv H.
unfold gen_newreg in *.
replace (st_parcopycode s) with (st_parcopycode s0).
eapply IHargs; eauto.
go.
Qed.
Hint Resolve gen_new_regs_correct_parcode.
Lemma gen_new_regs_correct_phicode :
forall args s args'
s'
INCR,
gen_new_regs args s =
OK args'
s'
INCR ->
st_phicode s =
st_phicode s'.
Proof.
induction args; intros.
+ unfold gen_new_regs in *.
unfold ret in *.
congruence.
+ simpl in *.
monadInv H.
unfold gen_newreg in *.
replace (st_phicode s) with (st_phicode s0).
eapply IHargs; eauto.
go.
Qed.
Hint Resolve gen_new_regs_correct_phicode.
Lemma add_parcopies_correct_fresh :
forall parcopies copy_nodes s u s'
INCR,
add_parcopies parcopies copy_nodes s =
OK u s'
INCR ->
fst (
next_fresh_reg s) =
fst (
next_fresh_reg s').
Proof.
induction parcopies; intros.
+ simpl in *. destruct copy_nodes; unfold ret in *;
unfold error in *; congruence.
+ simpl in *.
destruct copy_nodes; unfold error in *; try congruence.
monadInv H.
replace (next_fresh_reg s') with (next_fresh_reg s0).
eapply IHparcopies; eauto.
unfold add_parcopy in EQ0.
flatten EQ0. auto.
Qed.
Hint Resolve add_parcopies_correct_fresh.
Lemma add_parcopies_correct_phicode :
forall parcopies copy_nodes s u s'
INCR,
add_parcopies parcopies copy_nodes s =
OK u s'
INCR ->
st_phicode s =
st_phicode s'.
Proof.
induction parcopies; intros.
+ simpl in *. destruct copy_nodes; unfold ret in *;
unfold error in *; congruence.
+ simpl in *.
destruct copy_nodes; unfold error in *; try congruence.
monadInv H.
replace (st_phicode s') with (st_phicode s0).
eapply IHparcopies; eauto.
unfold add_parcopy in EQ0.
flatten EQ0. auto.
Qed.
Hint Resolve add_parcopies_correct_phicode.
Inductive add_parcopies_spec (
pcode1 :
parcopycode) :
list parcopy ->
list node
->
parcopycode ->
Prop :=
|
add_parcopies_spec_nil:
add_parcopies_spec pcode1 nil nil pcode1
|
add_parcopies_spec_cons:
forall pc parcb pcode2 parcopy copy_nodes
parcopies
(
APSPECparcb:
pcode2 !
pc =
Some parcb)
(
APSPECnodup: ~
In pc copy_nodes)
(
APSPECrec:
add_parcopies_spec pcode1 parcopies copy_nodes
pcode2),
add_parcopies_spec pcode1 (
parcopy ::
parcopies)
(
pc ::
copy_nodes)
(
PTree.set pc (
parcopy ::
parcb)
pcode2).
Lemma add_parcopies_spec_correct_other :
forall pcode1 parcopies copy_nodes pcode2,
add_parcopies_spec pcode1 parcopies copy_nodes pcode2 ->
forall pc,
~
In pc copy_nodes ->
pcode1 !
pc =
pcode2 !
pc.
Proof.
intros until pcode2.
intro H. induction H; auto; intros.
simpl in *.
assert (pc <> pc0).
auto.
rewrite PTree.gso.
auto. auto.
Qed.
Hint Resolve add_parcopies_spec_correct_other.
Lemma add_parcopies_k_notSomefromNone :
forall parcode1 parcopies copy_nodes parcode2,
add_parcopies_spec parcode1 parcopies
copy_nodes parcode2 ->
forall pc,
parcode2 !
pc <>
None ->
parcode1 !
pc <>
None.
Proof.
intros until parcode2. intro H. induction H; intros.
auto.
case_eq (peq pc pc0); intros.
+ rewrite e in *.
rewrite PTree.gss in H0.
apply IHadd_parcopies_spec. congruence.
+ rewrite PTree.gso in H0; auto.
Qed.
Lemma add_parcopies_k :
forall pcode1 parcopies copy_nodes pcode2,
add_parcopies_spec pcode1 parcopies copy_nodes pcode2 ->
forall k pred parcopy parcb,
nth_error copy_nodes k =
Some pred ->
nth_error parcopies k =
Some parcopy ->
pcode1 !
pred =
Some parcb ->
pcode2 !
pred =
Some (
parcopy ::
parcb).
Proof.
intros until pcode2.
intro H.
induction H; intros.
generalize nth_error_nil_notSome_node; intros; congruence.
case_eq (peq pc pred); intros.
+ rewrite e in *.
rewrite PTree.gss.
destruct k.
- simpl in *. unfold value in *.
replace (pcode1 ! pred) with (pcode2 ! pred) in H2.
congruence.
symmetry. eauto.
- simpl in *.
assert (nth_error copy_nodes k <> Some pred).
apply notIn_notnth; auto.
assert (nth_error copy_nodes k = Some pred)
by auto.
congruence.
+ rewrite PTree.gso; auto.
destruct k.
- simpl in *. unfold value in *. congruence.
- simpl in *.
apply IHadd_parcopies_spec with (k := k); auto.
Qed.
Lemma add_parcopies_pred_exist_parcb :
forall pcode1 parcopies copy_nodes pcode2,
add_parcopies_spec pcode1 parcopies copy_nodes pcode2 ->
forall pred (
parcb parcb0 :
parcopyblock),
In pred copy_nodes ->
pcode1 !
pred =
Some parcb0 ->
exists parcb,
pcode2 !
pred =
Some parcb.
Proof.
intros until pcode2. intro H. induction H; intros.
exists parcb0; auto.
case_eq (peq pred pc); intros.
+ rewrite e in *.
rewrite PTree.gss.
exists (parcopy :: parcb). auto.
+ inv H0. congruence.
rewrite PTree.gso; auto.
eauto.
Qed.
Lemma add_parcopies_nth_notNonetonotNone :
forall pcode1 parcopies copy_nodes pcode2,
add_parcopies_spec pcode1 parcopies copy_nodes pcode2 ->
forall k,
nth_error copy_nodes k <>
None ->
nth_error parcopies k <>
None.
Proof.
intros until pcode2. intro H. induction H; intros.
+ destruct k; simpl in *; intros;
unfold Specif.error in H; congruence.
+ destruct k; simpl in *; intros.
- unfold value in *; congruence.
- auto.
Qed.
Hint Resolve add_parcopies_nth_notNonetonotNone.
Lemma add_parcopies_correct :
forall copy_nodes s parcopies u s'
INCR,
NoDup copy_nodes ->
add_parcopies parcopies copy_nodes s =
OK u s'
INCR ->
add_parcopies_spec (
st_parcopycode s)
parcopies copy_nodes
(
st_parcopycode s').
Proof.
induction copy_nodes; intros s parcopies u s' INCR HNoDups H.
+ simpl in H.
destruct parcopies.
unfold add_parcopies in H; unfold ret in H.
assert (RW: s = s') by congruence.
rewrite RW.
constructor.
unfold add_parcopies in H; unfold error in H; congruence.
+ simpl in H.
destruct parcopies.
unfold add_parcopies in H; unfold error in H; try congruence.
monadInv H.
assert ((st_parcopycode s0) ! a <> None).
unfold add_parcopy in EQ0.
flatten EQ0.
case_eq ((st_parcopycode s0) ! a); intros; try congruence.
replace (st_parcopycode s') with
(PTree.set a (p :: p0) (st_parcopycode s0)).
eapply add_parcopies_spec_cons; eauto.
inv HNoDups. auto.
eapply IHcopy_nodes; eauto.
inv HNoDups. auto.
unfold add_parcopy in EQ0.
flatten EQ0. simpl. congruence.
Qed.
Hint Resolve add_parcopies_correct.
Inductive build_parcopies_spec :
list reg ->
list reg ->
list parcopy ->
Prop :=
|
build_parcopies_spec_nil:
build_parcopies_spec nil nil nil
|
build_parcopies_spec_cons:
forall arg arg'
args args'
parcopies,
build_parcopies_spec args args'
parcopies ->
build_parcopies_spec (
arg ::
args) (
arg' ::
args')
(
Iparcopy arg arg' ::
parcopies).
Lemma build_parcopies_correct:
forall args args'
s parcopies s'
INCR,
build_parcopies args args'
s =
OK parcopies s'
INCR ->
build_parcopies_spec args args'
parcopies.
Proof.
induction args; intros; simpl in *; flatten H;
unfold error in H; try congruence.
+ unfold ret in H. go.
+ monadInv H. go.
Qed.
Hint Resolve build_parcopies_correct.
Lemma build_parcopies_nth:
forall args args'
parcopies,
build_parcopies_spec args args'
parcopies ->
forall k arg arg',
nth_error args k =
Some arg ->
nth_error args'
k =
Some arg' ->
nth_error parcopies k =
Some (
Iparcopy arg arg').
Proof.
intros until parcopies. intro H. induction H; intros.
+ assert (nth_error (nil:list reg) (k:nat) = None).
auto. congruence.
+ destruct k; simpl in *.
- unfold value in *. congruence.
- eauto.
Qed.
Hint Resolve build_parcopies_nth.
Lemma build_parcopies_nth_revargs:
forall args args'
parcopies,
build_parcopies_spec args args'
parcopies ->
forall k,
nth_error parcopies k <>
None ->
nth_error args k <>
None.
Proof.
intros until parcopies. intro H. induction H; intros.
+ destruct k; simpl in *; unfold Specif.error in H;
congruence.
+ destruct k; simpl in *.
- unfold value in *. congruence.
- eauto.
Qed.
Hint Resolve build_parcopies_nth_revargs.
Lemma build_parcopies_correct_phicode:
forall args args'
s parcopies s'
INCR,
build_parcopies args args'
s =
OK parcopies s'
INCR ->
st_phicode s =
st_phicode s'.
Proof.
induction args; intros.
+ unfold build_parcopies in H.
flatten H. unfold ret in H.
congruence. unfold error in H. congruence.
+ simpl in *. flatten H.
unfold error in H. congruence.
monadInv H. eauto.
Qed.
Hint Resolve build_parcopies_correct_phicode.
Lemma build_parcopies_correct_fresh:
forall args args'
s parcopies s'
INCR,
build_parcopies args args'
s =
OK parcopies s'
INCR ->
fst (
next_fresh_reg s) =
fst (
next_fresh_reg s').
Proof.
induction args; intros.
+ unfold build_parcopies in H.
flatten H. unfold ret in H.
congruence. unfold error in H. congruence.
+ simpl in *. flatten H.
unfold error in H. congruence.
monadInv H. eauto.
Qed.
Hint Resolve build_parcopies_correct_fresh.
Lemma build_parcopies_correct_parcopycode:
forall args args'
s parcopies s'
INCR,
build_parcopies args args'
s =
OK parcopies s'
INCR ->
st_parcopycode s =
st_parcopycode s'.
Proof.
induction args; intros.
+ unfold build_parcopies in H.
flatten H. unfold ret in H.
congruence. unfold error in H. congruence.
+ simpl in *. flatten H.
unfold error in H. congruence.
monadInv H. eauto.
Qed.
Hint Resolve build_parcopies_correct_parcopycode.
Inductive add_parcopy_spec (
pc :
node):
reg ->
reg ->
parcopycode ->
parcopycode ->
Prop :=
|
add_parcopy_spec_intro:
forall dst'
dst parcode parcb,
parcode !
pc =
Some parcb ->
add_parcopy_spec pc dst'
dst
parcode (
PTree.set pc
((
Iparcopy dst'
dst) ::
parcb)
parcode).
Lemma add_parcopy_correct:
forall dst'
dst pc s u s'
INCR,
add_parcopy (
Iparcopy dst'
dst)
pc s =
OK u s'
INCR ->
add_parcopy_spec pc dst'
dst
(
st_parcopycode s) (
st_parcopycode s').
Proof.
intros.
unfold add_parcopy in H.
flatten H; go.
Qed.
Hint Resolve add_parcopy_correct.
Lemma add_parcopy_correct_phicode:
forall dst'
dst pc s u s'
INCR,
add_parcopy (
Iparcopy dst'
dst)
pc s =
OK u s'
INCR ->
st_phicode s =
st_phicode s'.
Proof.
intros. unfold add_parcopy in H. flatten H. auto.
Qed.
Hint Resolve add_parcopy_correct_phicode.
Lemma add_parcopy_correct_fresh:
forall dst'
dst pc s u s'
INCR,
add_parcopy (
Iparcopy dst'
dst)
pc s =
OK u s'
INCR ->
fst (
next_fresh_reg s) =
fst (
next_fresh_reg s').
Proof.
intros. unfold add_parcopy in H. flatten H. auto.
Qed.
Hint Resolve add_parcopy_correct_fresh.
Lemma add_new_phi_correct_fresh:
forall dst'
args'
pc s u s'
INCR,
add_new_phi dst'
args'
pc s =
OK u s'
INCR ->
fst (
next_fresh_reg s) =
fst (
next_fresh_reg s').
Proof.
intros.
unfold add_new_phi in H.
flatten H. auto.
Qed.
Hint Resolve add_new_phi_correct_fresh.
Lemma add_new_phi_correct_parcode:
forall dst'
args'
pc s u s'
INCR,
add_new_phi dst'
args'
pc s =
OK u s'
INCR ->
st_parcopycode s =
st_parcopycode s'.
Proof.
intros.
unfold add_new_phi in H.
flatten H. auto.
Qed.
Hint Resolve add_new_phi_correct_parcode.
Lemma add_new_phi_correct_phicodeNotNone:
forall dst'
args'
pc s u s'
INCR,
add_new_phi dst'
args'
pc s =
OK u s'
INCR ->
(
st_phicode s) !
pc <>
None.
Proof.
intros.
unfold add_new_phi in H.
flatten H.
Qed.
Hint Resolve add_new_phi_correct_phicodeNotNone.
Inductive add_new_phi_spec (
pc :
node) :
reg ->
list reg ->
phicode ->
phicode ->
Prop :=
|
add_new_phi_spec_intro:
forall dst'
args'
phicode phib',
phicode !
pc =
Some phib' ->
add_new_phi_spec pc dst'
args'
phicode
(
PTree.set pc (
Iphi args'
dst' ::
phib')
phicode).
Lemma add_new_phi_correct:
forall dst'
args'
pc s u s'
INCR,
add_new_phi dst'
args'
pc s =
OK u s'
INCR ->
add_new_phi_spec pc dst'
args'
(
st_phicode s) (
st_phicode s').
Proof.
intros.
unfold add_new_phi in H.
flatten H; go.
Qed.
Hint Resolve add_new_phi_correct.
Inductive handle_phi_block_spec (
maxreg:
positive)
(
preds :
list node) (
pc :
node)
:
phiblock ->
positive ->
positive ->
phicode ->
phicode ->
parcopycode ->
parcopycode ->
Prop :=
|
handle_phi_block_spec_nil:
forall phicode parcode fs_init,
handle_phi_block_spec maxreg preds pc
nil fs_init fs_init
phicode phicode
parcode parcode
|
handle_phi_block_spec_cons:
forall args dst args'
dst'
block
fs_init fs_next fs_last
parcopies
parcode1 parcode2 parcode3 parcode4
phicode1 phicode2 phicode3
(
PBSPECargsfresh:
(
forall arg,
In arg args ->
Ple (
fst arg)
maxreg))
(
PBSPECdst_old:
Ple (
fst dst)
maxreg)
(
PBSPECfs_init_fresh:
Plt maxreg fs_init)
(
PBSPECnewreg: (
fst dst') =
fs_init)
(
PBSPECgen_new_regs:
gen_new_regs_spec maxreg (
Pos.succ fs_init)
fs_next
args args')
(
PBSPECrec:
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2)
(
PBSPECparcopies:
build_parcopies_spec args args'
parcopies)
(
PBSPECadd_parcopy:
add_parcopy_spec pc dst'
dst parcode2 parcode3)
(
PBSPECadd_parcopies:
add_parcopies_spec parcode3 parcopies preds parcode4)
(
PBSPECnew_phi:
add_new_phi_spec pc dst'
args'
phicode2 phicode3),
handle_phi_block_spec maxreg preds pc
(
Iphi args dst ::
block)
fs_init fs_last
phicode1 phicode3
parcode1 parcode4.
Lemma handle_phi_block_spec_incr :
forall maxreg preds pc block fs_init fs_last
phicode1 phicode2 parcode1 parcode2,
handle_phi_block_spec maxreg preds pc
block fs_init fs_last phicode1 phicode2
parcode1 parcode2 ->
Ple fs_init fs_last.
Proof.
intros. induction H.
apply Ple_refl.
apply Ple_trans with fs_next; auto.
apply Ple_trans with (Pos.succ fs_init); eauto.
apply Ple_succ.
Qed.
Hint Resolve handle_phi_block_spec_incr.
Lemma handle_phi_block_spec_ple_init_arg :
forall maxreg preds pc block fs_init fs_last
phicode1 phicode2 parcode1 parcode2,
handle_phi_block_spec maxreg preds pc
block fs_init fs_last
phicode1 phicode2 parcode1 parcode2 ->
forall arg'
args'
dst'
phib',
phicode1 !
pc =
Some nil ->
phicode2 !
pc =
Some phib' ->
In (
Iphi args'
dst')
phib' ->
In arg'
args' ->
Ple fs_init (
fst arg').
Proof.
intros until parcode2.
intro H; induction H; intros.
+ assert (RW: phib' = nil) by congruence.
rewrite RW in *.
inv H1.
+ apply Ple_trans with (Pos.succ fs_init).
apply Ple_succ.
inv PBSPECnew_phi.
rewrite PTree.gss in H1.
assert (RW: Iphi args' dst' :: phib'0 = phib')
by congruence.
rewrite <- RW in *.
inv H2; go.
apply Ple_trans with fs_next; eauto.
Qed.
Lemma handle_phi_block_spec_ple_init_dst :
forall maxreg preds pc block fs_init fs_last
phicode1 phicode2 parcode1 parcode2,
handle_phi_block_spec maxreg preds pc
block fs_init fs_last
phicode1 phicode2 parcode1 parcode2 ->
forall args'
dst'
phib',
phicode1 !
pc =
Some nil ->
phicode2 !
pc =
Some phib' ->
In (
Iphi args'
dst')
phib' ->
Ple fs_init (
fst dst').
Proof.
intros until parcode2.
intro H; induction H; intros.
+ assert (RW: phib' = nil) by congruence.
rewrite RW in *.
inv H1.
+ inv PBSPECnew_phi.
rewrite PTree.gss in H1.
assert (RW: Iphi args' dst' :: phib'0 = phib')
by congruence.
rewrite <- RW in *.
inv H2; go.
assert (EQdst: dst' = dst'0) by congruence.
rewrite EQdst.
apply Ple_refl.
apply Ple_trans with fs_next; eauto.
apply Ple_trans with (Pos.succ (fst dst')).
apply Ple_succ.
eauto.
Qed.
Ltac normalize_new_phi :=
match goal with
| [
H: ((
PTree.set ?
pc (
Iphi ?
args'0 ?
dst'0 :: ?
phib'0)
?
phicode) ! ?
pc =
Some (
Iphi ?
args' ?
dst' :: ?
phib'))
|-
_ ] =>
rewrite PTree.gss in H;
assert (
EQ1:
args' =
args'0)
by congruence;
assert (
EQ2:
dst' =
dst'0)
by congruence;
assert (
EQ3:
phib' =
phib'0)
by congruence;
rewrite EQ1 in *;
rewrite EQ2 in *;
rewrite EQ3 in *
|
_ =>
idtac
end.
Lemma handle_phi_block_spec_plt_arg :
forall maxreg preds pc block fs_next fs_last
phicode1 phicode2 parcode1 parcode2,
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 ->
phicode1 !
pc =
Some nil ->
forall phib'
dst'
args' (
arg':
reg)
args''
arg''
arg'
dst'',
phicode2 !
pc =
Some (
Iphi args'
dst' ::
phib') ->
In (
Iphi args''
dst'')
phib' ->
In arg'
args' ->
In arg''
args'' ->
Plt (
fst arg') (
fst arg'').
Proof.
intros.
induction H; try congruence.
apply Plt_Ple_trans with fs_next;
inv PBSPECnew_phi; normalize_new_phi.
eapply gen_new_regs_spec_max_in; eauto.
eapply handle_phi_block_spec_ple_init_arg; eauto.
Qed.
Lemma handle_phi_block_spec_plt_dst :
forall maxreg preds pc block fs_next fs_last
phicode1 phicode2 parcode1 parcode2,
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 ->
phicode1 !
pc =
Some nil ->
forall phib'
dst'
args' (
arg':
reg)
args''
dst'',
phicode2 !
pc =
Some (
Iphi args'
dst' ::
phib') ->
In (
Iphi args''
dst'')
phib' ->
Plt (
fst dst') (
fst dst'').
Proof.
intros.
induction H; try congruence.
apply Plt_Ple_trans with fs_next;
inv PBSPECnew_phi; normalize_new_phi.
apply Plt_Ple_trans with (Pos.succ (fst dst')).
apply Plt_succ.
eapply gen_new_regs_spec_incr; eauto.
eapply handle_phi_block_spec_ple_init_dst; eauto.
Qed.
Lemma handle_phi_block_spec_fresh1 :
forall maxreg preds pc block fs_next fs_last
phicode1 phicode2 parcode1 parcode2,
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 ->
forall arg'
k phib'
dst'
args',
phicode1 !
pc =
Some nil ->
phicode2 !
pc =
Some (
Iphi args'
dst' ::
phib') ->
forall (
args'' :
list reg) (
arg''
dst'' :
reg),
In (
Iphi args''
dst'')
phib' ->
nth_error args''
k =
Some arg'' ->
nth_error args'
k =
Some arg' ->
arg' <>
arg''.
Proof.
intros.
assert (Plt (fst arg') (fst arg'')).
assert (In arg'' args'').
eauto.
eapply handle_phi_block_spec_plt_arg; eauto.
auto.
Qed.
Lemma handle_phi_block_spec_fresh2 :
forall maxreg preds pc block fs_next fs_last
phicode1 phicode2 parcode1 parcode2,
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 ->
forall phib'
dst'
args',
phicode1 !
pc =
Some nil ->
phicode2 !
pc =
Some (
Iphi args'
dst' ::
phib') ->
forall (
args'' :
list reg) (
arg''
dst'' :
reg),
In (
Iphi args''
dst'')
phib' ->
dst' <>
dst''.
Proof.
intros.
assert (Plt (fst dst') (fst dst'')).
eapply handle_phi_block_spec_plt_dst; eauto.
auto.
Qed.
Lemma handle_phi_block_spec_fresh3 :
forall maxreg preds pc,
NoDup (
pc ::
preds) ->
forall block fs_next fs_last
phicode1 phicode2 parcode1 parcode2,
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 ->
forall arg'
k phib'
dst'
args',
phicode1 !
pc =
Some nil ->
phicode2 !
pc =
Some (
Iphi args'
dst' ::
phib') ->
forall args''
dst'',
In (
Iphi args''
dst'')
phib' ->
nth_error args'
k =
Some arg' ->
arg' <>
dst''.
Proof.
intros.
assert (Plt (fst arg') (fst dst'')).
inv H0; go.
inv PBSPECnew_phi; normalize_new_phi.
apply Plt_Ple_trans with fs_next0.
eapply gen_new_regs_spec_max_in; eauto.
eauto.
eapply handle_phi_block_spec_ple_init_dst; eauto.
auto.
Qed.
Lemma handle_phi_block_spec_exists_phib' :
forall maxreg preds pc block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 phib,
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 ->
phicode1 !
pc =
Some phib ->
exists phib',
phicode2 !
pc =
Some phib'.
Proof.
intros.
induction H.
exists phib; auto.
inv PBSPECnew_phi.
exists (Iphi args' dst' :: phib').
rewrite PTree.gss. auto.
Qed.
Lemma handle_phi_block_spec_exists_parcb' :
forall maxreg preds pc block fs_next fs_last
phicode1 phicode2 parcode1 parcode2,
NoDup (
pc ::
preds) ->
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 ->
parcode1 !
pc =
Some nil ->
exists parcb',
parcode2 !
pc =
Some parcb'.
Proof.
intros until parcode2. intros HNoDups H. induction H.
exists nil; auto.
intros.
exploit IHhandle_phi_block_spec; auto.
intros.
destruct H1 as [parcb' H1].
assert (EQparcother: parcode3 ! pc = parcode4 ! pc).
eapply add_parcopies_spec_correct_other; eauto.
inv HNoDups; auto.
inv PBSPECadd_parcopy.
rewrite PTree.gss in EQparcother.
exists (Iparcopy dst' dst :: parcb).
auto.
Qed.
Lemma handle_phi_block_spec_exists_parcb :
forall maxreg preds pc block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 pred,
NoDup (
pc ::
preds) ->
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 ->
In pred preds ->
parcode1 !
pred =
Some nil ->
exists parcb,
parcode2 !
pred =
Some parcb.
Proof.
intros until pred. intros HNoDups H. induction H.
exists nil; auto.
intros.
exploit IHhandle_phi_block_spec; auto.
intros.
destruct H2 as [parcb H2].
assert (EQparc: parcode2 ! pred = parcode3 ! pred).
inv PBSPECadd_parcopy. rewrite PTree.gso; auto.
inv HNoDups; auto. congruence.
rewrite EQparc in *.
eapply add_parcopies_pred_exist_parcb; eauto.
Qed.
Lemma handle_phi_block_spec_preserves_parcother :
forall maxreg preds pc block fs_next fs_last
phicode1 phicode2 parcode1 parcode2,
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 ->
forall pc',
NoDup (
pc ::
preds) ->
pc' <>
pc ->
~
In pc'
preds ->
parcode1 !
pc' =
parcode2 !
pc'.
Proof.
intros until parcode2.
intro H. induction H; intros.
+ auto.
+ replace (parcode4 ! pc') with (parcode3 ! pc').
replace (parcode3 ! pc') with (parcode2 ! pc').
auto.
inv PBSPECadd_parcopy. rewrite PTree.gso; auto.
eauto.
Qed.
Lemma handle_phi_block_spec_preserves_phibother :
forall maxreg preds pc block fs_next fs_last
phicode1 phicode2 parcode1 parcode2,
handle_phi_block_spec maxreg preds pc
block fs_next fs_last
phicode1 phicode2 parcode1 parcode2 ->
forall pc',
pc' <>
pc ->
phicode1 !
pc' =
phicode2 !
pc'.
Proof.
intros until parcode2.
intro H. induction H; intros.
+ auto.
+ replace (phicode3 ! pc') with (phicode2 ! pc').
auto.
inv PBSPECnew_phi.
rewrite PTree.gso; auto.
Qed.
Lemma handle_phi_block_correct :
forall maxreg preds pc,
NoDup (
pc ::
preds) ->
forall block s u s'
INCR,
(
forall args dst,
In (
Iphi args dst)
block
->
Ple (
fst dst)
maxreg) ->
(
forall args dst,
In (
Iphi args dst)
block ->
forall arg,
In arg args ->
Ple (
fst arg)
maxreg) ->
(
Plt maxreg (
fst (
next_fresh_reg s))) ->
handle_phi_block preds block pc s =
OK u s'
INCR ->
handle_phi_block_spec maxreg preds pc
block (
fst (
next_fresh_reg s)) (
fst (
next_fresh_reg s'))
(
st_phicode s) (
st_phicode s')
(
st_parcopycode s) (
st_parcopycode s').
Proof.
intros maxreg preds pc HNoDups.
induction block; intros s u s' INCR
Hnotfreshdst Hnotfresharg Hfresh Hphib.
+ simpl in Hphib. unfold ret in Hphib.
go.
+ unfold handle_phi_block in Hphib.
destruct a.
monadInv Hphib.
fold handle_phi_block in EQ0.
rename r into dst.
rename l into args.
rename x0 into args'.
rename x1 into u'.
rename x2 into parcopies.
rename x into dst'.
rename x3 into u''.
rename x4 into u'''.
assert (Hdst': dst' = next_fresh_reg s).
unfold gen_newreg in EQ. congruence.
assert (freshs0: Plt maxreg (fst (next_fresh_reg s0))).
apply Plt_Ple_trans with (fst (next_fresh_reg s)).
auto.
inversion INCR0; auto.
assert (Hnew_regs_spec:
gen_new_regs_spec maxreg
(fst (next_fresh_reg s0)) (fst (next_fresh_reg s1))
args args').
eapply gen_new_regs_correct; eauto.
assert (freshs1: Plt maxreg (fst (next_fresh_reg s1))).
apply Plt_Ple_trans with (fst (next_fresh_reg s0)).
auto.
inversion INCR2; auto.
assert(IHspec:
handle_phi_block_spec maxreg preds pc block
(fst (next_fresh_reg s1)) (fst (next_fresh_reg s2))
(st_phicode s1) (st_phicode s2)
(st_parcopycode s1) (st_parcopycode s2)).
eapply IHblock; eauto.
case_eq ((st_phicode s2) ! pc); intros.
assert (Hbuild_parcopies_spec:
build_parcopies_spec args args' parcopies)
by eauto.
assert (Hadd_parcopy_spec:
add_parcopy_spec pc dst' dst
(st_parcopycode s3) (st_parcopycode s4))
by eauto.
inversion HNoDups.
assert (Hadd_parcopies_spec:
add_parcopies_spec
(st_parcopycode s4)
parcopies preds
(st_parcopycode s5))
by eauto.
assert (Hadd_new_phi_spec:
add_new_phi_spec pc dst' args'
(st_phicode s5) (st_phicode s'))
by eauto.
{ apply handle_phi_block_spec_cons
with (args' := args')
(dst' := dst')
(fs_next := fst (next_fresh_reg s1))
(parcopies := parcopies)
(parcode2 := st_parcopycode s2)
(parcode3 := st_parcopycode s4)
(phicode2 := st_phicode s2); eauto.
- unfold gen_newreg in EQ. go.
- unfold gen_newreg in EQ.
assert (ss0: Pos.succ (fst (next_fresh_reg s))
= fst (next_fresh_reg s0)) by go.
rewrite ss0.
eapply gen_new_regs_correct; eauto.
- assert (s2s'fs: fst (next_fresh_reg s') =
fst (next_fresh_reg s2)).
{ symmetry.
replace (fst (next_fresh_reg s'))
with (fst (next_fresh_reg s5)).
replace (fst (next_fresh_reg s5))
with (fst (next_fresh_reg s4)).
replace (fst (next_fresh_reg s4))
with (fst (next_fresh_reg s3)).
eauto. eauto. eauto. eauto. }
rewrite s2s'fs.
assert (ss1parcode: st_parcopycode s =
st_parcopycode s1).
{ replace (st_parcopycode s1)
with (st_parcopycode s0).
eauto. unfold gen_newreg in EQ. go.
eauto. }
rewrite ss1parcode.
assert (ss1phicode: st_phicode s =
st_phicode s1).
{ replace (st_phicode s1) with (st_phicode s0).
eauto. unfold gen_newreg in EQ. go.
eauto. }
rewrite ss1phicode.
auto.
- replace (st_parcopycode s2)
with (st_parcopycode s3).
auto.
symmetry. eauto.
- replace (st_parcopycode s')
with (st_parcopycode s5); eauto.
- replace (st_phicode s2) with
(st_phicode s3).
replace (st_phicode s3) with
(st_phicode s4).
replace (st_phicode s4) with
(st_phicode s5).
auto.
symmetry. eauto.
symmetry. eauto.
symmetry. eauto. }
assert (s2s5phicode: st_phicode s2 = st_phicode s5).
{ replace (st_phicode s2) with (st_phicode s3).
replace (st_phicode s3) with (st_phicode s4).
eauto. symmetry. eauto.
symmetry.
eapply build_parcopies_correct_phicode; eauto. }
rewrite s2s5phicode in H.
assert ((st_phicode s5) ! pc <> None) by eauto.
congruence.
Qed.
Lemma handle_phi_block_spec_equiv_phib :
forall maxreg preds pc,
NoDup (
pc ::
preds) ->
forall phib fs_init fs_last
phicode1 phicode2 parcode1 parcode2
k pred,
handle_phi_block_spec maxreg preds pc
phib fs_init fs_last
phicode1 phicode2
parcode1 parcode2 ->
forall parcb parcb'
phib',
parcode1 !
pc =
Some nil ->
phicode1 !
pc =
Some nil ->
parcode2 !
pc =
Some parcb' ->
phicode2 !
pc =
Some phib' ->
nth_error preds k =
Some pred ->
parcode1 !
pred =
Some nil ->
parcode2 !
pred =
Some parcb ->
equiv_phib_spec maxreg k phib parcb phib'
parcb'.
Proof.
intros until pc. intro HNoDups.
intros until pred. intro H.
assert (Horig:
handle_phi_block_spec maxreg preds pc
phib fs_init fs_last
phicode1 phicode2 parcode1 parcode2)
by auto.
induction H; intros.
{ replace parcb with (nil:parcopyblock).
replace parcb' with (nil:parcopyblock).
replace phib' with (nil:phiblock).
apply equiv_phib_spec_nil.
congruence.
congruence.
congruence. }
case_eq (nth_error args k);
case_eq (nth_error args' k).
{
intros arg' nth_args' arg nth_args.
inv PBSPECnew_phi.
replace phib' with
(Iphi args' dst' :: phib'0) in *.
inv PBSPECadd_parcopy.
set (parcode3 := PTree.set pc
(Iparcopy dst' dst :: parcb0) parcode2) in *.
replace parcb' with
(Iparcopy dst' dst :: parcb0) in *.
{
case_eq (parcode3 ! pred); intros.
+ assert (parcode4 ! pred =
Some (Iparcopy arg arg' :: l)).
eapply add_parcopies_k; eauto.
assert (RW: parcb = Iparcopy arg arg' :: l)
by congruence.
rewrite RW.
assert (parcode2 ! pred = Some l).
{ unfold parcode3 in *. rewrite PTree.gso in H9.
auto. inv HNoDups.
assert (In pred preds) by eauto.
congruence. }
apply equiv_phib_spec_cons; auto.
- intros.
eapply handle_phi_block_spec_fresh1; eauto.
- intros.
assert (dst' <> dst'').
eapply handle_phi_block_spec_fresh2; eauto.
auto.
- intros.
eapply handle_phi_block_spec_fresh3; eauto.
- eapply gen_new_regs_spec_ple_arg_maxreg;
eauto.
- eapply gen_new_regs_spec_plt_maxreg_arg';
eauto.
+ assert (parcode3 ! pred <> None).
eapply add_parcopies_k_notSomefromNone; eauto.
assert (parcode4 ! pred = Some parcb)
by auto.
congruence.
congruence.
}
assert (parc3parc4: parcode3 ! pc = parcode4 ! pc).
inv HNoDups. eauto.
unfold parcode3 in parc3parc4.
rewrite PTree.gss in parc3parc4.
congruence.
rewrite PTree.gss in H3. congruence.
}
{ intros.
assert (nth_error args k <> None).
congruence.
assert (nth_error args' k <> None).
eauto.
congruence. }
{ intros.
assert (nth_error args' k <> None).
congruence.
assert (nth_error args k <> None).
eauto.
congruence. }
{ intros.
assert (nth_error preds k <> None) by congruence.
assert (nth_error parcopies k <> None) by eauto.
assert (nth_error args k <> None) by eauto.
congruence. }
Qed.
Lemma equiv_phib_spec_plt_maxreg_phib'
dst :
forall maxreg k phib parcb phib'
parcb',
equiv_phib_spec maxreg k phib parcb phib'
parcb' ->
forall args'
dst',
In (
Iphi args'
dst')
phib' ->
Plt maxreg (
fst dst').
Proof.
intros until parcb'.
intro H. induction H; intros args'' dst'' HIn.
+ inv HIn.
+ simpl in *.
destruct HIn; try congruence; eauto.
Qed.
Lemma equiv_phib_spec_plt_maxreg_phib'
arg :
forall maxreg k phib parcb phib'
parcb',
equiv_phib_spec maxreg k phib parcb phib'
parcb' ->
forall arg'
args'
dst',
In (
Iphi args'
dst')
phib' ->
nth_error args'
k =
Some arg' ->
Plt maxreg (
fst arg').
Proof.
intros until parcb'.
intro H. induction H;
intros arg'' args'' dst'' HIn Hnth.
+ inv HIn.
+ simpl in *.
destruct HIn; try congruence; eauto.
Qed.
Lemma equiv_phib_spec_parcbdst_inphib' :
forall maxreg k phib parcb phib'
parcb',
equiv_phib_spec maxreg k phib parcb phib'
parcb' ->
forall arg arg',
In (
Iparcopy arg arg')
parcb ->
exists args'
dst',
nth_error args'
k =
Some arg' /\
In (
Iphi args'
dst')
phib'.
Proof.
intros until parcb'.
intro H. induction H; intros arg'' arg''' HIn.
+ inv HIn.
+ simpl in *.
destruct HIn.
- go.
- assert (Hrec: exists args'0 dst'0,
nth_error args'0 k = Some arg''' /\
In (Iphi args'0 dst'0) phib').
eauto.
destruct Hrec as [args'0 [dst'0 [Hr1 Hr2]]].
exists args'0. exists dst'0.
split; auto.
Qed.
Lemma equiv_phib_spec_parcb'
src_inphib' :
forall maxreg k phib parcb phib'
parcb',
equiv_phib_spec maxreg k phib parcb phib'
parcb' ->
forall dst dst',
In (
Iparcopy dst'
dst)
parcb' ->
exists args',
In (
Iphi args'
dst')
phib'.
Proof.
intros until parcb'.
intro H. induction H; intros dst''' dst'' HIn.
+ inv HIn.
+ simpl in *.
destruct HIn.
- go.
- assert (Hrec: exists args'0,
In (Iphi args'0 dst'') phib').
eauto.
destruct Hrec as [args'0 HInphidst].
exists args'0.
auto.
Qed.
Lemma equiv_phib_spec_parcb'
dst_inphib :
forall maxreg k phib parcb phib'
parcb',
equiv_phib_spec maxreg k phib parcb phib'
parcb' ->
forall dst dst',
In (
Iparcopy dst'
dst)
parcb' ->
exists args,
In (
Iphi args dst)
phib.
Proof.
intros until parcb'.
intro H. induction H; intros dst''' dst'' HIn.
+ inv HIn.
+ simpl in *.
destruct HIn.
- go.
- assert (Hrec: exists args'0,
In (Iphi args'0 dst''') phib).
eauto.
destruct Hrec as [args'0 HInphidst].
exists args'0.
auto.
Qed.
Lemma equiv_phib_spec_ple_phibdst_maxreg :
forall maxreg k phib parcb phib'
parcb',
equiv_phib_spec maxreg k phib parcb phib'
parcb' ->
forall args dst,
In (
Iphi args dst)
phib ->
Ple (
fst dst)
maxreg.
Proof.
intros until parcb'.
intro H. induction H; intros args0 dst0 HIn.
+ inv HIn.
+ simpl in *.
destruct HIn; go.
Qed.
Lemma equiv_phib_spec_correct :
forall maxreg k phib parcb phib'
parcb',
unique_def_phib_spec phib ->
equiv_phib_spec maxreg k phib parcb phib'
parcb' ->
equiv_phib maxreg k phib parcb phib'
parcb'.
Proof.
intros until parcb'.
intros Hunique_def H.
induction H.
constructor.
constructor 2; auto; intros.
+ assert (Plt maxreg (fst dst'')).
eapply equiv_phib_spec_plt_maxreg_phib'dst; eauto.
assert (Plt (fst arg) (fst dst'')).
apply Ple_Plt_trans with maxreg; auto.
auto.
+ assert (HIn:
exists args' dst',
nth_error args' k = Some dst'' /\
In (Iphi args' dst') phib').
eapply equiv_phib_spec_parcbdst_inphib'; eauto.
destruct HIn as [args'0 [dst'0 HIn]].
destruct HIn.
assert (Plt maxreg (fst dst'')).
eapply equiv_phib_spec_plt_maxreg_phib'arg; eauto.
assert (Plt (fst arg) (fst dst'')).
apply Ple_Plt_trans with maxreg; auto.
auto.
+ assert (HIn:
exists args' dst',
nth_error args' k = Some dst'' /\
In (Iphi args' dst') phib').
eapply equiv_phib_spec_parcbdst_inphib'; eauto.
destruct HIn as [args'0 [dst'0 HIn]].
destruct HIn.
eauto.
+ assert (HIn: exists args'0,
In (Iphi args'0 arg'') phib').
eapply equiv_phib_spec_parcb'src_inphib'; eauto.
destruct HIn as [args'0 HIn].
assert (arg'' <> dst') by eauto.
auto.
+ assert (HIn: exists args'0,
In (Iphi args'0 dst'') phib).
eapply equiv_phib_spec_parcb'dst_inphib; eauto.
destruct HIn as [args'0 HIn].
assert (Plt (fst dst'') (fst dst')).
apply Ple_Plt_trans with maxreg.
eapply equiv_phib_spec_ple_phibdst_maxreg; eauto.
auto.
assert (dst'' <> dst') by eauto.
auto.
+ assert (HIn: exists args0,
In (Iphi args0 dst'') phib).
eapply equiv_phib_spec_parcb'dst_inphib; eauto.
destruct HIn as [args'0 HIn].
inv Hunique_def.
eauto.
+ inv Hunique_def.
eauto.
Qed.
Lemma nodupnth_get_index :
forall l pc k,
NoDup l ->
nth_error l k =
Some pc ->
SSA.get_index l pc =
Some k.
Proof.
induction l; intros.
+ destruct k; simpl in *.
unfold Specif.error in *; congruence.
unfold Specif.error in *; congruence.
+ destruct k; simpl in *; intros.
- unfold value in *.
assert (RW: a = pc) by congruence.
rewrite RW in *.
unfold SSA.get_index.
simpl.
flatten.
- assert (SSA.get_index l pc = Some k).
inv H. auto.
assert (HIn: In pc l) by eauto.
inv H.
unfold SSA.get_index in *.
simpl in *.
flatten.
assert (EQ1: 1 = 0 + 1) by auto.
assert (EQ2: (S k) = k + 1) by omega.
rewrite EQ1. rewrite EQ2.
apply get_index_acc_inv. auto.
Qed.
Lemma index_pred_from_nth :
forall l pc k pc'
preds,
NoDup (
pc ::
l) ->
preds !
pc =
Some l ->
nth_error l k =
Some pc' ->
index_pred preds pc'
pc =
Some k.
Proof.
intros.
unfold index_pred.
unfold successors_list.
flatten.
+ flatten Eq.
rewrite <- H2 in *.
destruct k; simpl in *; intros.
unfold Specif.error in *; congruence.
unfold Specif.error in *; congruence.
+ flatten Eq.
apply nodupnth_get_index.
rewrite <- H2 in H.
inv H. auto.
rewrite <- H2 in H1.
auto.
Qed.
Lemma handle_phi_block_spec_from_handle_phi_block :
forall f pc preds s1 s s0 s2 x x0 u
INCR INCR1 INCR2 phib,
(
make_predecessors (
fn_code f)
successors_instr) !
pc
=
Some preds ->
wf_ssa_function f ->
Plt (
get_maxreg f) (
fst (
next_fresh_reg s1)) ->
initialize_phi_block pc s1 =
OK x s INCR ->
initialize_parcopy_blocks (
pc ::
preds)
s =
OK x0 s0 INCR1 ->
normalized_jp f ->
(
fn_phicode f) !
pc =
Some phib ->
handle_phi_block preds phib pc s0 =
OK u s2 INCR2 ->
handle_phi_block_spec (
get_maxreg f)
preds pc
phib
(
fst (
next_fresh_reg s0))
(
fst (
next_fresh_reg s2))
(
st_phicode s0) (
st_phicode s2)
(
st_parcopycode s0) (
st_parcopycode s2).
Proof.
intros.
eapply handle_phi_block_correct; eauto.
+ eapply nodups_in_preds; eauto; try congruence.
eapply notinpredspc; eauto.
+ intros.
apply Ple_trans with
(get_max_reg_in_phiins (Iphi args dst)).
apply max_reg_in_phi_dst.
apply Ple_trans with
(get_max_reg_in_phib phib).
apply max_reg_in_phib_dst. auto.
apply Ple_trans with
(get_max_reg_in_phicode (fn_phicode f)).
eapply max_reg_in_phicode; eauto.
apply max_reg_correct_phicode.
+ intros.
apply Ple_trans with
(get_max_reg_in_phiins (Iphi args dst)).
apply max_reg_in_phi_arg. auto.
apply Ple_trans with
(get_max_reg_in_phib phib).
apply max_reg_in_phib_dst. auto.
apply Ple_trans with
(get_max_reg_in_phicode (fn_phicode f)).
eapply max_reg_in_phicode; eauto.
apply max_reg_correct_phicode.
+ apply Plt_Ple_trans with
(fst (next_fresh_reg s)).
apply Plt_Ple_trans with
(fst (next_fresh_reg s1)).
auto.
inversion INCR; auto.
inversion INCR1; auto.
Qed.
Lemma copy_node_cssagen_spec_parcode_other :
forall f pc s1 s2 incr pc'
phib preds,
wf_ssa_function f ->
normalized_jp f ->
copy_node
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f) (
fn_phicode f)
pc s1
=
OK tt s2 incr ->
(
fn_phicode f) !
pc =
Some phib ->
(
make_predecessors (
fn_code f)
successors_instr)
!
pc =
Some preds ->
pc' <>
pc ->
~
In pc'
preds ->
Plt (
get_maxreg f) (
fst (
next_fresh_reg s1)) ->
(
st_parcopycode s1) !
pc' = (
st_parcopycode s2) !
pc'.
Proof.
intros until preds.
intros WF Norm_jp H Hphib Hpreds Hpcpc' HnotIn Hfresh.
unfold copy_node in H.
flatten H.
+ monadInv H.
assert ((make_predecessors (fn_code f) successors_instr)
! pc = Some l) by auto.
assert (RW: l = preds) by congruence.
rewrite RW in *.
simpl. unfold not; intros.
replace ((st_parcopycode s2) ! pc')
with ((st_parcopycode s0) ! pc').
replace ((st_parcopycode s0) ! pc')
with ((st_parcopycode s) ! pc').
unfold initialize_phi_block in EQ; go.
eapply initialize_parcopy_blocks_correct_parcother;
eauto.
unfold not; intros HInpc'.
inv HInpc'; auto.
assert(Hb:
handle_phi_block_spec (get_maxreg f) preds pc
phib
(fst (next_fresh_reg s0))
(fst (next_fresh_reg s2))
(st_phicode s0) (st_phicode s2)
(st_parcopycode s0) (st_parcopycode s2)).
eapply handle_phi_block_spec_from_handle_phi_block;
eauto.
eapply handle_phi_block_spec_preserves_parcother; eauto.
eapply nodups_in_preds; eauto; try congruence.
eapply notinpredspc; eauto.
+ unfold error in H. go.
Qed.
Lemma copy_node_cssagen_spec_phicode_other :
forall f pc s1 s2 u incr pc'
phib preds,
wf_ssa_function f ->
normalized_jp f ->
copy_node
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f) (
fn_phicode f)
pc s1
=
OK u s2 incr ->
(
fn_phicode f) !
pc =
Some phib ->
(
make_predecessors (
fn_code f)
successors_instr)
!
pc =
Some preds ->
pc' <>
pc ->
Plt (
get_maxreg f) (
fst (
next_fresh_reg s1)) ->
(
st_phicode s1) !
pc' = (
st_phicode s2) !
pc'.
Proof.
intros until preds.
intros WF Norm_jp H Hphib Hpreds Hpcpc' Hfresh.
unfold copy_node in H.
flatten H.
+ monadInv H.
assert ((make_predecessors (fn_code f) successors_instr)
! pc = Some l) by auto.
assert (RW: l = preds) by congruence.
rewrite RW in *.
replace ((st_phicode s2) ! pc')
with ((st_phicode s) ! pc').
unfold initialize_phi_block in EQ.
replace (st_phicode s) with
(PTree.set pc nil (st_phicode s1)).
rewrite PTree.gso; auto.
go.
replace ((st_phicode s2) ! pc')
with ((st_phicode s0) ! pc').
replace (st_phicode s0)
with (st_phicode s).
auto.
eapply initialize_parcopy_blocks_correct_other; eauto.
assert(Hb:
handle_phi_block_spec (get_maxreg f) preds pc
phib
(fst (next_fresh_reg s0))
(fst (next_fresh_reg s2))
(st_phicode s0) (st_phicode s2)
(st_parcopycode s0) (st_parcopycode s2)).
eapply handle_phi_block_spec_from_handle_phi_block;
eauto.
eapply handle_phi_block_spec_preserves_phibother;
eauto.
+ unfold error in H. go.
Qed.
Lemma copy_node_cssagenspec_other :
forall f s1 pc k s2 pc'
incr phib,
cssa_spec
(
get_maxreg f)
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f)
(
fn_phicode f) (
st_phicode s1)
(
st_parcopycode s1)
pc k ->
wf_ssa_function f ->
normalized_jp f ->
Plt (
get_maxreg f) (
fst (
next_fresh_reg s1)) ->
copy_node
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f) (
fn_phicode f)
pc'
s1
=
OK tt s2 incr ->
(
fn_phicode f) !
pc =
Some phib ->
pc <>
pc' ->
cssa_spec
(
get_maxreg f)
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f)
(
fn_phicode f) (
st_phicode s2)
(
st_parcopycode s2)
pc k.
Proof.
intros until phib.
intros H WF Norm_jp Hfresh Hcopy_node Hpcpc'.
inv H; go.
case_eq ((fn_phicode f) ! pc'); intros.
case_eq (
(make_predecessors (fn_code f) successors_instr) ! pc');
intros.
assert (~ In pc' l).
{ unfold not; intros.
assert((fn_phicode f) ! pc' = None).
unfold normalized_jp in Norm_jp.
eapply Norm_jp; go.
congruence. congruence. }
assert (~ In pc l).
{ unfold not; intros.
assert((fn_phicode f) ! pc = None).
unfold normalized_jp in Norm_jp.
eapply Norm_jp; go.
congruence. congruence. }
assert(EQ1: (st_parcopycode s1) ! pred =
(st_parcopycode s2) ! pred).
apply copy_node_cssagen_spec_parcode_other
with (pc := pc') (f := f)
(incr := incr) (phib := p) (preds := l); go.
{ unfold not; intros EQpredpc'.
rewrite EQpredpc' in *.
assert (Nthpc': nth_error (
(make_predecessors (fn_code f)
successors_instr) !!! pc : list positive) k =
Some pc').
eapply index_pred_some_nth; eauto.
unfold successors_list in Nthpc'.
flatten Nthpc'.
assert(In pc' l0).
eapply nth_In_node; eauto.
assert ((fn_phicode f) ! pc' = None).
unfold normalized_jp in Norm_jp.
eapply Norm_jp; go.
congruence. congruence.
assert (nth_error (nil : list node) k = None).
apply nth_error_nil_notSome_node.
assert (nth_error (nil : list node) k = Some pc').
auto. congruence. }
eapply inop_is_not_in_two_preds; eauto.
assert(EQ2: (st_parcopycode s1) ! pc =
(st_parcopycode s2) ! pc).
eapply copy_node_cssagen_spec_parcode_other; eauto.
assert(EQ3: (st_phicode s1) ! pc =
(st_phicode s2) ! pc).
eapply copy_node_cssagen_spec_phicode_other; eauto.
rewrite EQ1 in *.
rewrite EQ2 in *.
rewrite EQ3 in *.
go.
{ induction WF.
assert(JP: join_point pc' f).
apply fn_phicode_inv.
congruence.
inv JP.
congruence. }
{ unfold copy_node in Hcopy_node.
flatten Hcopy_node. unfold ret in *.
assert (RW: s1 = s2) by congruence.
rewrite RW in *.
go. }
Qed.
Lemma copy_node_cssagenspec_other_mfold :
forall f,
wf_ssa_function f ->
normalized_jp f ->
forall l s1 pc k s2 u incr,
cssa_spec
(
get_maxreg f)
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f)
(
fn_phicode f) (
st_phicode s1)
(
st_parcopycode s1)
pc k ->
mfold_unit (
copy_node
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f) (
fn_phicode f))
l s1 =
OK u s2 incr ->
~
In pc l ->
Plt (
get_maxreg f) (
fst (
next_fresh_reg s1)) ->
cssa_spec
(
get_maxreg f)
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f)
(
fn_phicode f) (
st_phicode s2)
(
st_parcopycode s2)
pc k.
Proof.
intros f WF Norm_jp.
induction l; intros until incr;
intros Hspec H Hnotin Hplt.
+ simpl in *. unfold ret in *.
assert (EQ: s1 = s2) by congruence.
rewrite EQ in *. auto.
+ case_eq ((fn_phicode f) ! pc); intros.
simpl in *.
monadInv H.
assert(Hstep:
cssa_spec
(get_maxreg f)
(make_predecessors (fn_code f) successors_instr)
(fn_code f)
(fn_phicode f) (st_phicode s)
(st_parcopycode s)
pc k).
destruct x.
eapply copy_node_cssagenspec_other; eauto.
eapply IHl; eauto.
apply Plt_Ple_trans with (fst (next_fresh_reg s1)).
auto. inversion INCR; auto.
go.
Qed.
Lemma copy_node_cssagenspec :
forall f pc s1 s2 incr k,
wf_ssa_function f ->
normalized_jp f ->
Plt (
get_maxreg f) (
fst (
next_fresh_reg s1)) ->
copy_node
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f) (
fn_phicode f)
pc s1
=
OK tt s2 incr ->
cssa_spec
(
get_maxreg f)
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f)
(
fn_phicode f) (
st_phicode s2)
(
st_parcopycode s2)
pc k.
Proof.
intros until k. intros WF Norm_jp Pltmaxregfresh H.
case_eq ((fn_phicode f) ! pc); go; intro phib; intros.
unfold copy_node in H.
flatten H.
+ assert (~ In pc l).
eapply notinpredspc; eauto.
monadInv H.
set (preds :=
make_predecessors (fn_code f) successors_instr)
in *.
case_eq (nth_error l k); intros.
{
assert(Hb:
handle_phi_block_spec (get_maxreg f) l pc
phib
(fst (next_fresh_reg s0))
(fst (next_fresh_reg s2))
(st_phicode s0) (st_phicode s2)
(st_parcopycode s0) (st_parcopycode s2)).
eapply handle_phi_block_spec_from_handle_phi_block;
eauto.
assert (phib_init: (st_phicode s0) ! pc = Some nil).
replace (st_phicode s0) with (st_phicode s).
eapply initialize_phi_block_correct; eauto.
eapply initialize_parcopy_blocks_correct_other; eauto.
assert (parcb'_init:
(st_parcopycode s0) ! pc = Some nil)
by eauto.
assert (parcb_init:
(st_parcopycode s0) ! n = Some nil)
by eauto.
assert (HEphib': exists phib',
(st_phicode s2) ! pc = Some phib').
eapply handle_phi_block_spec_exists_phib'; eauto.
assert (HEparcb': exists parcb',
(st_parcopycode s2) ! pc = Some parcb').
eapply handle_phi_block_spec_exists_parcb'; eauto.
eapply nodups_in_preds; eauto. congruence.
assert (HEparcb: exists parcb,
(st_parcopycode s2) ! n = Some parcb).
eapply handle_phi_block_spec_exists_parcb; eauto.
eapply nodups_in_preds; eauto. congruence.
destruct HEphib' as [phib' Hphib'].
destruct HEparcb' as [parcb' Hparcb'].
destruct HEparcb as [parcb Hparcb].
apply cssa_spec_jp_pred_k
with (pred := n) (phib := phib) (phib' := phib')
(parcb := parcb) (parcb' := parcb'); auto.
induction WF.
apply fn_normalized. apply fn_phicode_inv. go.
assert (codepred: exists i, (fn_code f) ! n = Some i).
eapply make_predecessors_some; go.
destruct codepred as [i codepred].
eapply in_successors_if_succofpred; eauto.
eapply index_pred_from_nth; eauto.
eapply nodups_in_preds; eauto. congruence.
apply handle_phi_block_spec_equiv_phib
with (preds := l) (pc := pc)
(fs_init := fst (next_fresh_reg s0))
(fs_last := fst (next_fresh_reg s2))
(phicode1 := st_phicode s0)
(phicode2 := st_phicode s2)
(parcode1 := st_parcopycode s0)
(parcode2 := st_parcopycode s2)
(pred := n); auto.
eapply nodups_in_preds; eauto.
congruence.
}
eapply cssa_spec_jp_invalid_k; eauto.
+ unfold error in H. go.
Qed.
Lemma mfold_copy_node_correct :
forall f,
wf_ssa_function f ->
normalized_jp f ->
forall l pc
u s s'
incr k,
mfold_unit (
copy_node
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f) (
fn_phicode f))
l s =
OK u s'
incr ->
Plt (
get_maxreg f) (
fst (
next_fresh_reg s)) ->
NoDup l ->
In pc l ->
cssa_spec (
get_maxreg f)
(
make_predecessors (
fn_code f)
successors_instr)
(
fn_code f) (
fn_phicode f)
(
st_phicode s') (
st_parcopycode s')
pc k.
Proof.
intros f WF Norm_jp.
induction l; intros.
+ inv H2.
+ simpl in *.
monadInv H.
destruct H2.
- rewrite H in *.
assert (Hstep:
cssa_spec (get_maxreg f)
(make_predecessors (fn_code f) successors_instr)
(fn_code f) (fn_phicode f)
(st_phicode s0) (st_parcopycode s0) pc k).
destruct x.
apply copy_node_cssagenspec with
(s1 := s) (incr := INCR); go.
inv H1.
eapply copy_node_cssagenspec_other_mfold; eauto.
apply Plt_Ple_trans with (fst (next_fresh_reg s)).
auto. inversion INCR; auto.
- apply IHl with
(u := u) (s := s0) (incr := INCR0); auto.
apply Plt_Ple_trans with (fst (next_fresh_reg s)).
auto. inversion INCR; auto.
inv H1; auto.
Qed.
Normalisations validators proofs
Lemma inops_checker_correct :
forall f,
wf_ssa_function f ->
check_jp_inops f =
true ->
inop_in_jp f.
Proof.
intros f WF CHECK.
unfold inop_in_jp.
intros.
unfold check_jp_inops in CHECK.
rewrite forallb_forall in CHECK.
exploit (CHECK pc).
case_eq ((fn_phicode f) ! pc); try congruence; intros.
assert (In (pc, p) (PTree.elements (fn_phicode f))).
apply PTree.elements_correct; auto.
eapply In_Infst_phib; eauto.
intros.
unfold check_inop_jp in H0.
flatten H0; auto.
exists n; auto.
Qed.
Lemma normalisation_checker_correct_aux :
forall f,
check_joinpoints f =
true ->
forall pc succ,
(
fn_code f) !
pc =
Some (
Inop succ) ->
(
fn_phicode f) !
succ <>
None ->
(
fn_phicode f) !
pc =
None.
Proof.
intros f CHECK pc succ codepc phisucc.
unfold check_joinpoints in CHECK.
rewrite forallb_forall in CHECK.
exploit (CHECK pc).
assert (In (pc, Inop succ) (PTree.elements (fn_code f))).
apply PTree.elements_correct; auto.
eapply In_Infst; eauto.
intros.
unfold check_node in H.
flatten H; auto.
Qed.
Lemma In_nth_error :
forall l (
pc :
node),
In pc l ->
exists k,
nth_error l k =
Some pc.
Proof.
induction l; intros.
inv H.
simpl in *.
destruct H.
+ exists 0. simpl. unfold value. congruence.
+ cut (exists k : nat, nth_error l k = Some pc); auto.
intros HE. destruct HE as [k nthk].
exists (S k). simpl. auto.
Qed.
Lemma normalisation_checker_correct :
forall f,
wf_ssa_function f ->
check_joinpoints f =
true ->
normalized_jp f.
Proof.
intros f WF CHECK.
unfold normalized_jp.
intros pc preds phipc mkpreds pred Inpred.
eapply normalisation_checker_correct_aux; eauto.
induction WF.
apply fn_normalized.
apply fn_phicode_inv. auto.
assert (H: exists i, (fn_code f) ! pred = Some i).
eapply make_predecessors_some; eauto.
destruct H.
assert (nthk: exists k, nth_error preds k = Some pred).
apply In_nth_error; auto.
destruct nthk.
eapply in_successors_if_succofpred; eauto.
Qed.
Proof of the transformation specification
Lemma transl_function_charact:
forall f tf,
wf_ssa_function f ->
transl_function f =
Errors.OK tf ->
tr_function f tf.
Proof.
intros f tf WF H.
unfold transl_function in H.
case_eq (init_state f) ; intros.
rewrite H0 in *.
case_eq (mfold_unit
(copy_node
(make_predecessors (fn_code f) successors_instr)
(fn_code f) (fn_phicode f))
l s); intros.
{ rewrite H1 in H. congruence. }
{ rewrite H1 in H. flatten H.
repeat rewrite andb_true_iff in Eq.
destruct Eq as [[Hcheckjps Hcheckinops] Hcheckentry].
eapply tr_function_intro ; eauto.
apply normalisation_checker_correct; auto.
destruct u. eauto.
unfold entry_point_not_jp_pred in *; flatten Hcheckentry.
apply inops_checker_correct; auto.
}
Qed.
Lemma transl_function_spec_ok :
forall f tf,
normalized_jp f ->
tr_function f tf ->
transl_function_spec f tf.
Proof.
intros f tf Norm_jp H.
inv H.
econstructor; go; intros; simpl.
+ unfold init_state in H0.
assert (RW: lp = map fst (PTree.elements (fn_code f)))
by congruence.
assert (HNoDups: NoDup lp).
assert (list_norepet lp).
rewrite RW in *.
apply PTree.elements_keys_norepet.
apply list_norepet_NoDup; auto.
eapply mfold_copy_node_correct; eauto.
unfold init_state in *.
assert (RWinitreg: next_fresh_reg init =
(Pos.succ (get_maxreg f), 1%positive))
by go.
rewrite RWinitreg. simpl.
apply Plt_succ.
rewrite RW in *.
assert (In (pc, ins) (PTree.elements (fn_code f))).
apply PTree.elements_correct. auto.
eapply In_Infst; eauto.
+ eapply wf_unique_def_phib; eauto.
Qed.
Section PRESERVATION.
Variable prog:
SSA.program.
Variable tprog:
CSSApar.program.
Hypothesis TRANSF_PROG:
transl_program prog =
Errors.OK tprog.
Hypothesis WF_PROG :
wf_ssa_program prog.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof.
intro. unfold ge, tge.
apply Genv.find_symbol_transf_partial with transl_fundef.
exact TRANSF_PROG.
Qed.
Inductive match_regset (
max_reg:
positive) :
SSA.regset ->
SSA.regset ->
Prop :=
|
mrg_intro :
forall rs rs',
(
forall r, (
Ple (
fst r)
max_reg) ->
rs#2
r =
rs'#2
r) ->
match_regset max_reg rs rs'.
Inductive match_stackframes :
list stackframe ->
list CSSApar.stackframe ->
Prop :=
|
match_stackframes_nil:
match_stackframes nil nil
|
match_stackframes_cons:
forall res f sp pc rs rs'
s tf ts
(
STACK : (
match_stackframes s ts ))
(
SPEC: (
transl_function f =
Errors.OK tf))
(
WFF:
wf_ssa_function f)
(
MREG:
match_regset (
get_maxreg f)
rs rs'),
match_stackframes
((
Stackframe res f sp pc rs) ::
s)
((
CSSApar.Stackframe res tf sp pc rs') ::
ts).
Hint Constructors match_stackframes.
Set Implicit Arguments.
Inductive match_states:
SSA.state ->
CSSApar.state ->
Prop :=
|
match_states_intro:
forall s ts sp pc rs rs'
m f tf
(
SPEC:
transl_function f =
Errors.OK tf)
(
STACK:
match_stackframes s ts)
(
WFF:
wf_ssa_function f)
(
MREG:
match_regset (
get_maxreg f)
rs rs'),
match_states (
State s f sp pc rs m)
(
CSSApar.State ts tf sp pc rs'
m)
|
match_states_call:
forall s ts f tf args m
(
SPEC:
transl_fundef f =
Errors.OK tf)
(
STACK:
match_stackframes s ts)
(
WFF:
wf_ssa_fundef f),
match_states (
Callstate s f args m)
(
CSSApar.Callstate ts tf args m)
|
match_states_return:
forall s ts v m
(
STACK:
match_stackframes s ts ),
match_states (
Returnstate s v m)
(
CSSApar.Returnstate ts v m).
Hint Constructors match_states.
Lemma function_ptr_translated:
forall (
b:
Values.block) (
f:
SSA.fundef),
Genv.find_funct_ptr ge b =
Some f ->
exists tf,
Genv.find_funct_ptr tge b =
Some tf
/\
transl_fundef f =
Errors.OK tf.
Proof.
apply (Genv.find_funct_ptr_transf_partial transl_fundef).
exact TRANSF_PROG.
Qed.
Lemma sig_fundef_translated:
forall f tf,
wf_ssa_fundef f ->
transl_fundef f =
Errors.OK tf ->
CSSApar.funsig tf =
SSA.funsig f.
Proof.
intros f tf. intros.
case_eq f; intros.
- rewrite H1 in H0.
simpl in *. Errors.monadInv H0.
eapply transl_function_charact in EQ ; eauto.
inv EQ.
simpl; auto.
inv H. auto.
- rewrite H1 in H0. go.
Qed.
Lemma transf_initial_states:
forall st1,
initial_state prog st1 ->
exists st2,
CSSApar.initial_state tprog st2
/\
match_states st1 st2.
Proof.
intros.
inv H.
exploit function_ptr_translated; eauto.
intros [tf [Hfind Htrans]].
exists (CSSApar.Callstate nil tf nil m0); split.
econstructor; eauto.
eapply Genv.init_mem_transf_partial; eauto.
rewrite symbols_preserved.
rewrite (transform_partial_program_main _ _ TRANSF_PROG). auto.
rewrite <- H3. apply sig_fundef_translated; auto.
unfold wf_ssa_program in WF_PROG.
assert (ID: exists id, In (id, Gfun f) (prog_defs prog)).
eapply Genv.find_funct_ptr_inversion; eauto.
destruct ID as [id InId].
apply WF_PROG with (id := id). eauto.
eapply match_states_call ; eauto.
eapply Genv.find_funct_ptr_prop; eauto.
Qed.
Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2
->
final_state st1 r
->
CSSApar.final_state st2 r.
Proof.
intros. inv H0. inv H.
inv STACK.
constructor.
Qed.
Lemma instructions_preserved:
forall f tf,
transl_function f =
Errors.OK tf ->
CSSApar.fn_code tf =
fn_code f.
Proof.
intros.
unfold transl_function in H.
flatten H; go.
Qed.
Lemma no_new_joinpoints:
forall f tf,
transl_function f =
Errors.OK tf ->
forall pc,
CSSApar.join_point pc tf ->
join_point pc f.
Proof.
intros.
inv H0.
apply jp_cons with l; auto.
rewrite same_successors_same_predecessors
with (f2 := successors_instr)
(m2 := CSSApar.fn_code tf).
rewrite Hpreds; auto.
intros.
erewrite PTree.gmap1.
erewrite PTree.gmap1.
unfold option_map.
case_eq ((fn_code f) ! i); intros.
+ rewrite instructions_preserved with f tf.
rewrite H0; eauto.
congruence.
+ case_eq ((CSSApar.fn_code tf) ! i); intros; auto.
rewrite instructions_preserved with f tf in H1.
congruence. auto.
Qed.
Lemma join_points_preserved:
forall f tf,
transl_function f =
Errors.OK tf ->
forall pc,
join_point pc f ->
CSSApar.join_point pc tf.
Proof.
intros.
inv H0.
econstructor; go.
assert (CSSApar.fn_code tf = fn_code f).
apply instructions_preserved; auto.
go.
Qed.
Lemma registers_equal:
forall rs rs'
args max_reg,
(
forall r,
In r args ->
Ple (
fst r)
max_reg) ->
match_regset max_reg rs rs'
->
rs' ##2
args =
rs ##2
args.
Proof.
intros.
inv H0.
induction args; eauto.
simpl.
erewrite IHargs; go.
erewrite H1; go.
Qed.
Lemma functions_translated:
forall (
v:
val) (
f:
SSA.fundef),
Genv.find_funct ge v =
Some f ->
exists tf,
Genv.find_funct tge v =
Some tf
/\
transl_fundef f =
Errors.OK tf.
Proof.
apply (Genv.find_funct_transf_partial transl_fundef).
exact TRANSF_PROG.
Qed.
Lemma spec_ros_r_find_function:
forall rs rs'
f r,
rs #2
r =
rs' #2
r ->
SSA.find_function ge (
inl _ r)
rs =
Some f ->
exists tf,
CSSApar.find_function tge (
inl _ r)
rs' =
Some tf
/\
transl_fundef f =
Errors.OK tf.
Proof.
intros.
eapply functions_translated; eauto. inv H0.
rewrite H; auto.
Qed.
Lemma spec_ros_id_find_function:
forall rs rs'
f id,
SSA.find_function ge (
inr _ id)
rs =
Some f ->
exists tf,
CSSApar.find_function tge (
inr _ id)
rs' =
Some tf
/\
transl_fundef f =
Errors.OK tf.
Proof.
intros.
simpl in *.
case_eq (Genv.find_symbol ge id) ; intros.
rewrite H0 in H.
rewrite symbols_preserved in * ; eauto ; rewrite H0 in *.
exploit function_ptr_translated; eauto.
rewrite H0 in H ; inv H.
Qed.
Lemma stacksize_preserved:
forall f tf,
transl_function f =
Errors.OK tf ->
fn_stacksize f =
CSSApar.fn_stacksize tf.
Proof.
intros.
unfold transl_function in H.
flatten H; go.
Qed.
parallel block evaluation simplification lemmas
Lemma parcopy_store_other :
forall rs r parcb,
(
forall src dst,
In (
Iparcopy src dst)
parcb
->
r <>
dst) ->
rs !!2
r = (
parcopy_store parcb rs) !!2
r.
Proof.
intros rs r parcb.
induction parcb; go.
intros.
simpl. destruct a.
rewrite P2Map.gso; go.
Qed.
Lemma copy_out_of_parcb :
forall (
rs :
SSA.regset) (
parcb :
parcopyblock)
(
src dst :
SSA.reg),
(
forall src'
dst',
In (
CSSApar.Iparcopy src'
dst')
parcb
->
src <>
dst') ->
parcopy_store (
CSSApar.Iparcopy src dst ::
parcb)
rs =
(
parcopy_store parcb rs)#2
dst <-
((
parcopy_store parcb rs) #2
src).
Proof.
intros.
simpl.
assert (rs !!2 src =
(parcopy_store parcb rs) !!2 src).
eapply parcopy_store_other; go.
go.
Qed.
Lemma copy_out_of_phib :
forall (
rs :
SSA.regset) (
phib :
phiblock)
(
src dst :
SSA.reg) (
args :
list SSA.reg) (
k :
nat),
(
forall args'
dst',
In (
Iphi args'
dst')
phib
->
src <>
dst') ->
nth_error args k =
Some src ->
phi_store k (
Iphi args dst ::
phib)
rs =
(
phi_store k phib rs)#2
dst <-
((
phi_store k phib rs) #2
src).
Proof.
intros. simpl.
case_eq (nth_error args k); intros; go.
assert (EQ: r = src) by congruence.
rewrite EQ in *.
assert (rs !!2 src =
(phi_store k phib rs) !!2 src).
eapply phi_store_other; go.
go.
Qed.
equiv_phib inductive predicate consequences
Lemma equiv_phib_fresh_parcb :
forall maxreg k phib parcb phib'
parcb'
src dst
(
EQ_PHIB:
equiv_phib maxreg k phib parcb phib'
parcb')
(
IN_parcb:
In (
Iparcopy src dst)
parcb),
Plt maxreg (
fst dst).
Proof.
intros.
induction EQ_PHIB; go.
simpl in IN_parcb.
destruct IN_parcb; go.
Qed.
Lemma equiv_phib_fresh_parcb' :
forall maxreg k phib parcb phib'
parcb'
src dst
(
EQ_PHIB:
equiv_phib maxreg k phib parcb phib'
parcb')
(
IN_parcb:
In (
Iparcopy src dst)
parcb'),
Plt maxreg (
fst src).
Proof.
intros.
induction EQ_PHIB; go.
simpl in IN_parcb.
destruct IN_parcb; go.
Qed.
Lemma equiv_phib_fresh_phib'1 :
forall maxreg k phib parcb phib'
parcb'
arg args dst
(
EQ_PHIB:
equiv_phib maxreg k phib parcb phib'
parcb')
(
IN_parcb:
In (
Iphi args dst)
phib')
(
ARG:
nth_error args k =
Some arg),
Plt maxreg (
fst arg).
Proof.
intros.
induction EQ_PHIB; go.
simpl in IN_parcb.
destruct IN_parcb; go.
Qed.
Lemma equiv_phib_fresh_phib'2 :
forall maxreg k phib parcb phib'
parcb'
args dst
(
EQ_PHIB:
equiv_phib maxreg k phib parcb phib'
parcb')
(
IN_parcb:
In (
Iphi args dst)
phib'),
Plt maxreg (
fst dst).
Proof.
intros.
induction EQ_PHIB; go.
simpl in IN_parcb.
destruct IN_parcb; go.
Qed.
Lemma equiv_phib_notfresh_phib1 :
forall maxreg k phib parcb phib'
parcb'
arg args dst
(
EQ_PHIB:
equiv_phib maxreg k phib parcb phib'
parcb')
(
IN_parcb:
In (
Iphi args dst)
phib)
(
ARG:
nth_error args k =
Some arg),
Ple (
fst arg)
maxreg.
Proof.
intros.
induction EQ_PHIB; go.
simpl in IN_parcb.
destruct IN_parcb; go.
Qed.
Lemma equiv_phib_notfresh_phib2 :
forall maxreg k phib parcb phib'
parcb'
args dst
(
EQ_PHIB:
equiv_phib maxreg k phib parcb phib'
parcb')
(
IN_parcb:
In (
Iphi args dst)
phib),
Ple (
fst dst)
maxreg.
Proof.
intros.
induction EQ_PHIB; go.
simpl in IN_parcb.
destruct IN_parcb; go.
Qed.
Lemma equiv_phib_nth :
forall maxreg k phib phib'
parcb parcb',
equiv_phib maxreg k phib parcb phib'
parcb' ->
forall args dst,
In (
Iphi args dst)
phib'
->
exists arg,
nth_error args k =
Some arg.
Proof.
intros maxreg k phib phib' parcb parcb' H.
induction H.
{ intros. contradiction. }
intros args0 dst0 IH_IN.
simpl in *.
destruct IH_IN.
exists arg'. congruence.
apply IHequiv_phib with (dst := dst0).
auto.
Qed.
Lemma equiv_phib_parcsrc_phib'
dst :
forall maxreg k phib phib'
parcb parcb',
equiv_phib maxreg k phib parcb phib'
parcb' ->
forall src dst,
In (
Iparcopy src dst)
parcb' ->
exists args,
In (
Iphi args src)
phib'.
Proof.
intros maxreg k phib phib' parcb parcb' EQ_PHIB.
induction EQ_PHIB; intros src dst0 In_src; go.
simpl in *.
destruct In_src.
- go.
- assert (Exists_args:
exists args0, In (Iphi args0 src) phib') by eauto.
destruct Exists_args as [args0 In_args_phib'].
exists args0. auto.
Qed.
Lemma equiv_phib_args_k_notnone :
forall maxreg k phib parcb phib'
parcb'
args dst,
equiv_phib maxreg k phib parcb phib'
parcb' ->
In (
Iphi args dst)
phib'
->
nth_error args k <>
None.
Proof.
intros maxreg k phib parcb phib' parcb' args dst H.
induction H. auto.
intro HIn.
inv HIn; go.
Qed.
Lemma reg_Ple_Plt_not_eq :
forall maxreg (
r1 r2 :
reg),
Ple (
fst r1)
maxreg ->
Plt maxreg (
fst r2) ->
r1 <>
r2.
Proof.
intros.
destruct r1. destruct r2.
simpl in *.
assert (r <> r0); try congruence.
assert (Plt r r0); auto.
apply Ple_Plt_trans with maxreg; auto.
Qed.
Hint Resolve equiv_phib_fresh_parcb equiv_phib_fresh_parcb'
equiv_phib_fresh_phib'1
equiv_phib_fresh_phib'2
equiv_phib_notfresh_phib1 equiv_phib_notfresh_phib2
equiv_phib_nth equiv_phib_args_k_notnone
reg_Ple_Plt_not_eq.
Hint Resolve parc_dst_in.
Lemma in_parc_dst_in_not :
forall r parcb,
(
forall src, ~
In (
Iparcopy src r)
parcb) ->
~
In r (
map parc_dst parcb).
Proof.
induction parcb; auto; intros.
simpl in *. unfold not in *; intros.
destruct a.
destruct H0.
+ assert (EQ: r1 = r) by go. rewrite EQ in *.
go.
+ go.
Qed.
Hint Resolve in_parc_dst_in_not.
Definition phib_dst (
phiins :
phiinstruction) :=
match phiins with
|
Iphi args dst =>
dst
end.
Lemma in_phib_dst_exists_args :
forall dst phib,
In dst (
map phib_dst phib) ->
exists args,
In (
Iphi args dst)
phib.
Proof.
induction phib; intros.
{ simpl in H. contradiction. }
simpl in *.
destruct a.
case_eq (p2eq r dst); intros.
+ rewrite e in *. go.
+ simpl in H.
destruct H. congruence.
assert (IN_phib: exists args, In (Iphi args dst) phib).
auto. destruct IN_phib as [src IN_parcb].
eauto.
Qed.
Lemma in_phib_dst_in :
forall args dst phib,
In (
Iphi args dst)
phib ->
In dst (
map phib_dst phib).
Proof.
induction phib; auto; intros.
simpl in *.
destruct H; [left | right]; go.
Qed.
Lemma in_phib_dst_simul :
forall rs (
phib :
phiblock) (
r :
reg) (
k :
nat)
args arg,
NoDup (
map phib_dst phib) ->
In (
Iphi args r)
phib ->
(
forall args'
dst',
In (
Iphi args'
dst')
phib
->
nth_error args'
k <>
None) ->
nth_error args k =
Some arg ->
(
phi_store k phib rs) !!2
r =
rs !!2
arg.
Proof.
induction phib; intros r k args arg HNoDup H.
{ simpl in H. contradiction. }
simpl in *.
destruct a.
case_eq (nth_error l k); intros.
+ simpl in *.
case_eq (p2eq r r0); intros.
- rewrite e in *.
rewrite P2Map.gss.
destruct H; go.
inv HNoDup.
assert (In r0 (map phib_dst phib)).
eapply in_phib_dst_in; eauto.
contradiction.
- rewrite P2Map.gso; auto.
destruct H; go.
inv HNoDup.
eapply IHphib; eauto.
+ simpl in *. inv HNoDup.
destruct H. congruence. eauto.
Qed.
Lemma in_parcb_dst_simul :
forall rs (
r :
reg) (
parcb :
parcopyblock)
src,
NoDup (
map parc_dst parcb) ->
In (
Iparcopy src r)
parcb ->
(
parcopy_store parcb rs) !!2
r =
rs !!2
src.
Proof.
induction parcb; intros.
{ simpl in H. contradiction. }
simpl in *.
destruct a.
destruct H0.
+ assert (EQ1: r0 = src) by congruence.
assert (EQ2: r1 = r) by congruence.
rewrite EQ1 in *. rewrite EQ2 in *.
inv H.
apply P2Map.gss.
+ inv H.
rewrite P2Map.gso; auto.
unfold not in *; intros. go.
Qed.
Lemma equiv_phib_nodups_parcb_dst :
forall maxreg k phib parcb phib'
parcb',
equiv_phib maxreg k phib parcb phib'
parcb' ->
NoDup (
map parc_dst parcb).
Proof.
intros.
induction H; go.
simpl.
constructor; go.
unfold not; intros.
assert(Exists_src: exists src,
In (Iparcopy src arg') parcb).
apply in_parcb_dst_exists_src; auto.
destruct Exists_src as [src in_src_parcb'].
assert (arg' <> arg'); go.
Qed.
Hint Resolve equiv_phib_nodups_parcb_dst.
Lemma equiv_phib_nodups_phib'
_dst :
forall maxreg k phib parcb phib'
parcb',
equiv_phib maxreg k phib parcb phib'
parcb' ->
NoDup (
map phib_dst phib').
Proof.
intros.
induction H; go.
simpl.
constructor; go.
unfold not; intros.
assert(Exists_args': exists args',
In (Iphi args' dst') phib').
apply in_phib_dst_exists_args; auto.
destruct Exists_args' as [src in_src_parcb'].
assert (dst' <> dst'); go.
Qed.
Hint Resolve equiv_phib_nodups_phib'
_dst.
Lemma equiv_phib_spec_rev:
forall maxreg k phib parcb phib'
parcb',
equiv_phib maxreg k phib parcb phib'
parcb' ->
equiv_phib_spec maxreg k phib parcb phib'
parcb'.
Proof.
intros; induction H; go.
Qed.
Lemma equiv_phib_nodups_parcb'
_dst :
forall maxreg k phib parcb phib'
parcb',
unique_def_phib_spec phib ->
equiv_phib maxreg k phib parcb phib'
parcb' ->
NoDup (
map parc_dst parcb').
Proof.
intros until parcb'. intros Hwf H.
induction H; go.
simpl.
constructor; go.
unfold not; intros.
assert(Exists_src: exists src,
In (Iparcopy src dst) parcb').
apply in_parcb_dst_exists_src; auto.
destruct Exists_src as [src in_src_parcb'].
assert (equiv_phib_spec maxreg k phib parcb phib' parcb').
apply equiv_phib_spec_rev; auto.
assert (dst <> dst); auto.
assert (exists args0,
In (Iphi args0 dst) phib).
eapply equiv_phib_spec_parcb'dst_inphib; eauto.
eauto.
inv Hwf. auto.
Qed.
Hint Resolve equiv_phib_nodups_parcb'
_dst.
Lemma parcb_not_in :
forall r parcb,
~
In r (
map parc_dst parcb) ->
forall src dst,
In (
Iparcopy src dst)
parcb ->
r <>
dst.
Proof.
induction parcb; go; intros.
simpl in *.
destruct H0.
- rewrite H0 in *. go.
- intuition. go.
Qed.
Hint Resolve parcb_not_in.
Lemma phi_store_emulation :
forall rs rs'
k phib parcb phib'
parcb'
maxreg,
match_regset maxreg rs rs' ->
unique_def_phib_spec phib ->
equiv_phib maxreg k phib parcb phib'
parcb' ->
forall r,
Ple (
fst r)
maxreg ->
(
phi_store k phib rs) !!2
r =
(
parcopy_store parcb'
(
phi_store k phib'
(
parcopy_store parcb rs'))) !!2
r.
Proof.
intros rs rs' k phib parcb phib' parcb' maxreg MREG
WFphib EQ_PHIB.
induction EQ_PHIB.
- simpl. inv MREG. eapply H; go.
- intros. symmetry.
inv WFphib.
assert (r <> dst'). eauto.
assert (r <> arg'). eauto.
set (rec_simuled_store :=
(parcopy_store parcb'
(phi_store k phib'
(parcopy_store parcb rs')))) in *.
rewrite copy_out_of_parcb; go.
rewrite copy_out_of_phib with
(parcopy_store (Iparcopy arg arg' :: parcb) rs')
phib' arg' dst' args' k; go.
rewrite copy_out_of_parcb; go.
case_eq (p2eq r dst); intros; go.
+ rewrite e in *.
symmetry. simpl.
case_eq (nth_error args k); go; intros.
rewrite P2Map.gss.
assert (R_EQ: r0 = arg) by go.
rewrite R_EQ in *.
repeat rewrite P2Map.gss.
rewrite <- parcopy_store_other; go.
rewrite P2Map.gss.
rewrite <- phi_store_other; go.
rewrite P2Map.gss.
rewrite <- parcopy_store_other; go.
inv MREG. auto.
+ symmetry. simpl.
case_eq (nth_error args k); go; intros.
rewrite P2Map.gso; auto.
rewrite IHEQ_PHIB; auto.
unfold rec_simuled_store.
case_eq (in_dec p2eq r (map parc_dst parcb')); intros.
{
assert (Exists_src: exists src,
In (Iparcopy src r) parcb').
apply in_parcb_dst_exists_src; auto.
destruct Exists_src as [src In_src_r_parcb'].
rewrite in_parcb_dst_simul with (src := src); go.
symmetry.
rewrite P2Map.gso; go.
rewrite in_parcb_dst_simul with (src := src); go.
rewrite P2Map.gso.
assert (Exists_args'': exists args'',
In (Iphi args'' src) phib').
eapply equiv_phib_parcsrc_phib'dst; eauto.
destruct Exists_args'' as [args'' In_args''src].
assert (Exists_arg'': exists arg'',
nth_error args'' k = Some arg'').
eapply equiv_phib_nth; go.
destruct Exists_arg'' as [arg'' arg''kargs''].
rewrite in_phib_dst_simul
with (arg := arg'') (args := args''); go.
rewrite <- parcopy_store_other; go.
rewrite P2Map.gso.
symmetry.
rewrite in_phib_dst_simul
with (arg := arg'') (args := args''); go.
assert (arg' <> arg'') by go. go.
assert (dst' <> src) by go. go.
}
{
rewrite <- parcopy_store_other.
rewrite <- phi_store_other; go.
rewrite <- parcopy_store_other; go.
symmetry.
repeat rewrite P2Map.gso; auto.
rewrite <- parcopy_store_other.
rewrite P2Map.gso; auto.
rewrite <- phi_store_other; go.
rewrite P2Map.gso; auto.
rewrite <- parcopy_store_other; go.
apply parcb_not_in; auto.
apply parcb_not_in; auto.
}
Qed.
(index_preds preds pc) injectivity
Lemma get_index_acc_le_k :
forall l pc acc k,
get_index_acc l pc acc =
Some k ->
acc <=
k.
Proof.
induction l; go.
intros. simpl in *. flatten H; go.
assert (acc + 1 <= k).
eauto. omega.
Qed.
Lemma index_acc_inj :
forall l pc1 pc2 k p,
get_index_acc l pc1 p =
Some k ->
get_index_acc l pc2 p =
Some k ->
pc1 =
pc2.
Proof.
induction l; intros pc1 pc2 k p H H0.
go.
simpl in H. simpl in H0.
flatten H; flatten H0; go.
+ assert (k + 1 <= k).
eapply get_index_acc_le_k; eauto.
omega.
+ assert (k + 1 <= k).
eapply get_index_acc_le_k; eauto.
omega.
Qed.
Lemma index_preds_pc_inj :
forall f pc1 pc2 succ k preds,
preds =
make_predecessors (
fn_code f)
successors_instr ->
index_pred preds pc1 succ =
Some k ->
index_pred preds pc2 succ =
Some k ->
pc1 =
pc2.
Proof.
intros.
unfold index_pred in *.
case_eq (preds !!! succ); intros.
+ rewrite H2 in *. congruence.
+ rewrite H2 in *.
eapply index_acc_inj; eauto.
Qed.
Lemma get_preds_some :
forall preds (
pc :
node)
lpreds,
preds !
pc =
Some lpreds ->
preds !!!
pc =
lpreds.
Proof.
induction lpreds; intros;
unfold successors_list;
rewrite H; auto.
Qed.
Lemma match_regset_args :
forall args maxreg rs rs',
match_regset maxreg rs rs' ->
(
forall arg,
In arg args ->
Ple (
fst arg)
maxreg) ->
rs' ##2
args =
rs ##2
args.
Proof.
induction args; go.
intros.
simpl.
erewrite IHargs; eauto.
inv H.
rewrite H1; auto.
Qed.
Proving the transformation
Lemma transl_step_correct:
forall s1 t s2,
step ge s1 t s2 ->
forall s1' (
MS:
match_states s1 s1'),
exists s2',
CSSApar.step tge s1'
t s2' /\
match_states s2 s2'.
Proof.
induction 1; intros; inv MS; auto;
match goal with
| [H : transl_fundef (Internal ?f) = _ |- _ ] => idtac
| [H : transl_fundef (External ?f) = _ |- _ ] => idtac
| [ |- context [CSSApar.Returnstate ?ts ?vres ?m]] =>
idtac
| _ =>
(exploit transl_function_charact ; eauto; intros);
(exploit transl_function_spec_ok ; eauto; intros)
end;
match goal with
| [SPEC: transl_function_spec ?f ?tf |- _ ] =>
inv SPEC
| _ => try (generalize (wf_ssa f) ; intros HWF)
end;
match goal with
| [Htr : tr_function ?f ?tf |- normalized_jp ?f ]
=> inv Htr; auto
| _ => idtac
end.
{ exists (CSSApar.State ts tf sp pc' rs' m). split; auto.
econstructor 1 ; eauto.
- erewrite instructions_preserved; eauto.
- intuition.
apply H0.
eapply no_new_joinpoints; eauto. }
{
set (preds := make_predecessors
(fn_code f) successors_instr) in *.
assert (CSSA_SPEC: cssa_spec
(get_maxreg f)
preds
(fn_code f) (fn_phicode f)
(CSSApar.fn_phicode tf) (fn_parcopycode tf) pc' k).
assert(codepc': exists i, (fn_code f) ! pc' = Some i).
{ induction WFF.
eapply fn_code_closed; go. }
destruct codepc' as [i codepc']. eauto.
inv CSSA_SPEC; try congruence.
{
assert (nth_error (preds !!! pc' : list positive) k =
Some pc).
eapply index_pred_some_nth; eauto.
assert (preds !!! pc' = (lpreds : list positive)).
apply get_preds_some. auto.
assert (nth_error (lpreds : list positive) k = None)
by auto.
congruence.
}
exists (CSSApar.State ts tf sp pc'
(parcopy_store parcb'
(phi_store k phib'
(parcopy_store parcb rs')))
m).
split.
+ assert (EQ_PC_PRED: pc = pred).
eapply index_preds_pc_inj; eauto.
rewrite EQ_PC_PRED in *.
eapply CSSApar.exec_Inop_jp; eauto.
- erewrite instructions_preserved; eauto.
- eapply join_points_preserved; eauto.
- unfold get_preds.
unfold CSSApar.get_preds.
erewrite instructions_preserved; eauto.
+ apply match_states_intro; go.
constructor; intros.
assert (PHIBS_EQ: phib0 = phib) by congruence.
rewrite PHIBS_EQ in *.
eapply phi_store_emulation; eauto.
eapply equiv_phib_spec_correct; eauto.
}
{ exists (CSSApar.State ts tf sp pc' (rs' #2 res <- v) m).
split.
+ econstructor; eauto.
assert ((CSSApar.fn_code tf) ! pc =
Some (Iop op args res pc')).
erewrite instructions_preserved; eauto; simpl; eauto.
eauto.
assert (REGS_EQ: rs' ##2 args = rs ##2 args).
{ eapply registers_equal; intros; eauto.
apply Ple_trans with
(get_max_reg_in_ins
(Iop op args res pc')).
apply max_reg_in_Iop_args.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
}
rewrite REGS_EQ.
erewrite eval_operation_preserved; eauto.
eapply symbols_preserved.
+ constructor; eauto. constructor.
inv MREG. intros.
rewrite P2Map.gsspec. rewrite P2Map.gsspec.
destruct p2eq; eauto. }
{ exists (CSSApar.State ts tf sp pc' (rs' #2 dst <- v) m).
split.
+ eapply CSSApar.exec_Iload; eauto.
assert ((CSSApar.fn_code tf) ! pc =
Some (Iload chunk addr args dst pc')).
erewrite instructions_preserved; eauto; simpl; eauto.
eauto.
assert (REGS_EQ: rs' ##2 args = rs ##2 args).
{ eapply registers_equal; eauto; intros.
apply Ple_trans with
(get_max_reg_in_ins
(Iload chunk addr args dst pc')).
apply max_reg_in_Iload_args.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
}
rewrite REGS_EQ.
erewrite eval_addressing_preserved; eauto.
eapply symbols_preserved.
+ constructor; eauto. constructor.
inv MREG. intros.
rewrite P2Map.gsspec. rewrite P2Map.gsspec.
destruct p2eq; eauto. }
{ exists (CSSApar.State ts tf sp pc' rs' m').
split.
+ eapply CSSApar.exec_Istore; eauto.
assert ((CSSApar.fn_code tf) ! pc =
Some (Istore chunk addr args src pc')).
{ erewrite instructions_preserved; eauto; simpl; eauto. }
eauto.
assert (REGS_EQ: rs' ##2 args = rs ##2 args).
{ eapply registers_equal; eauto; intros.
apply Ple_trans with
(get_max_reg_in_ins
(Istore chunk addr args src pc')).
apply max_reg_in_Istore_args.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
}
rewrite REGS_EQ.
erewrite eval_addressing_preserved; eauto.
eapply symbols_preserved.
inv MREG. rewrite <- H3. auto.
apply Ple_trans with
(get_max_reg_in_ins
(Istore chunk addr args src pc')).
apply max_reg_in_Istore_src.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
+ constructor; eauto. }
{
assert (WFfd: wf_ssa_fundef fd).
{
unfold wf_ssa_program in WF_PROG.
assert (ID: exists id,
In (id, Gfun fd) (prog_defs prog)).
unfold find_function in H0.
unfold Genv.find_funct in H0.
flatten H0;
apply Genv.find_funct_ptr_inversion
with (b := b); auto.
destruct ID as [id Infd].
apply WF_PROG with id.
auto.
}
assert (RW: rs' ##2 args = rs ##2 args).
{ assert(Pleargs: forall arg, In arg args ->
Ple (fst arg) (get_maxreg f)); intros.
apply Ple_trans with
(get_max_reg_in_ins (Icall (funsig fd)
ros args res pc')).
apply max_reg_in_Icall_args.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
eapply match_regset_args; eauto.
}
destruct ros.
- assert(Htfd: exists tfd,
CSSApar.find_function tge (inl _ r) rs' = Some tfd
/\ transl_fundef fd = Errors.OK tfd).
apply spec_ros_r_find_function
with (rs := rs); auto.
assert (Ple (fst r) (get_maxreg f)).
{
apply Ple_trans with
(get_max_reg_in_ins (Icall (funsig fd)
(inl r) args res pc')).
apply max_reg_in_Icall_inl.
repeat constructor; auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
}
inv MREG; auto.
destruct Htfd as [tfd Hfindtfd].
exists (CSSApar.Callstate
(CSSApar.Stackframe res tf sp pc' rs' :: ts)
tfd (rs'##2 args) m).
split.
+ apply CSSApar.exec_Icall
with (sig := CSSApar.funsig tfd)
(ros := inl r); eauto.
{ erewrite instructions_preserved; eauto; simpl;
eauto.
assert (CSSApar.funsig tfd = funsig fd).
apply sig_fundef_translated.
auto.
destruct Hfindtfd. auto.
go. }
destruct Hfindtfd. auto.
+ rewrite RW in *.
apply match_states_call.
destruct Hfindtfd. auto.
go.
auto.
- assert(Htfd: exists tfd,
CSSApar.find_function tge (inr i) rs' = Some tfd
/\ transl_fundef fd = Errors.OK tfd).
apply spec_ros_id_find_function
with (rs := rs); auto.
destruct Htfd as [tfd Htfd].
exists (CSSApar.Callstate
(CSSApar.Stackframe res tf sp pc' rs' :: ts)
tfd (rs'##2 args) m).
split.
+ apply CSSApar.exec_Icall
with (sig := CSSApar.funsig tfd)
(ros := inr i); eauto.
erewrite instructions_preserved; eauto.
assert (EQfdtfd: CSSApar.funsig tfd = funsig fd).
apply sig_fundef_translated.
auto.
destruct Htfd. auto.
rewrite EQfdtfd. auto.
destruct Htfd. auto.
+ rewrite RW in *.
apply match_states_call.
destruct Htfd. auto.
go.
auto.
}
{
assert (WFfd: wf_ssa_fundef fd).
{
unfold wf_ssa_program in WF_PROG.
assert (ID: exists id,
In (id, Gfun fd) (prog_defs prog)).
unfold find_function in H0.
unfold Genv.find_funct in H0.
flatten H0;
apply Genv.find_funct_ptr_inversion
with (b := b); auto.
destruct ID as [id Infd].
apply WF_PROG with id.
auto.
}
assert (RW: rs' ##2 args = rs ##2 args).
{ assert(Pleargs: forall arg, In arg args ->
Ple (fst arg) (get_maxreg f)); intros.
apply Ple_trans with
(get_max_reg_in_ins (Itailcall (funsig fd)
ros args)).
apply max_reg_in_Itailcall_args.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
eapply match_regset_args; eauto.
}
destruct ros.
- assert(Htfd: exists tfd,
CSSApar.find_function tge (inl _ r) rs' = Some tfd
/\ transl_fundef fd = Errors.OK tfd).
apply spec_ros_r_find_function
with (rs := rs); auto.
assert (Ple (fst r) (get_maxreg f)).
{
apply Ple_trans with
(get_max_reg_in_ins (Itailcall (funsig fd)
(inl r) args)).
apply max_reg_in_Itailcall_inl.
repeat constructor; auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
}
inv MREG; auto.
destruct Htfd as [tfd Hfindtfd].
exists (CSSApar.Callstate
ts tfd rs'##2 args m').
split.
+ apply CSSApar.exec_Itailcall
with (sig := CSSApar.funsig tfd)
(ros := inl r); eauto.
{ erewrite instructions_preserved; eauto; simpl;
eauto.
assert (CSSApar.funsig tfd = funsig fd).
apply sig_fundef_translated.
auto.
destruct Hfindtfd. auto.
go. }
destruct Hfindtfd. auto.
rewrite <- stacksize_preserved with (f := f);
auto.
+ rewrite RW in *.
apply match_states_call.
destruct Hfindtfd. auto.
go.
auto.
- assert(Htfd: exists tfd,
CSSApar.find_function tge (inr i) rs' = Some tfd
/\ transl_fundef fd = Errors.OK tfd).
apply spec_ros_id_find_function
with (rs := rs); auto.
destruct Htfd as [tfd Htfd].
exists (CSSApar.Callstate
ts tfd (rs'##2 args) m').
split.
+ apply CSSApar.exec_Itailcall
with (sig := CSSApar.funsig tfd)
(ros := inr i); eauto.
erewrite instructions_preserved; eauto.
assert (EQfdtfd: CSSApar.funsig tfd = funsig fd).
apply sig_fundef_translated.
auto.
destruct Htfd. auto.
rewrite EQfdtfd. auto.
destruct Htfd. auto.
rewrite <- stacksize_preserved with (f := f);
auto.
+ rewrite RW in *.
apply match_states_call.
destruct Htfd. auto.
go.
auto.
}
{ exists (CSSApar.State ts tf sp pc' (rs'#2 res <- v) m').
split.
+ eapply CSSApar.exec_Ibuiltin; eauto.
assert ((CSSApar.fn_code tf) ! pc =
Some (Ibuiltin ef args res pc')).
{ erewrite instructions_preserved; eauto; simpl;
eauto. }
eauto.
assert (REGS_EQ: rs' ##2 args = rs ##2 args).
{ eapply registers_equal; eauto; intros.
apply Ple_trans with
(get_max_reg_in_ins
(Ibuiltin ef args res pc')).
apply max_reg_in_Ibuiltin_args.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
}
rewrite REGS_EQ.
eapply external_call_symbols_preserved; eauto.
eapply symbols_preserved.
eapply Genv.find_var_info_transf_partial; eauto.
+ constructor; eauto.
constructor. inv MREG. intros.
rewrite P2Map.gsspec. rewrite P2Map.gsspec.
destruct p2eq; eauto. }
{ exists (CSSApar.State ts tf sp ifso rs' m).
split.
+ eapply CSSApar.exec_Icond_true; eauto.
assert ((CSSApar.fn_code tf) ! pc =
Some (Icond cond args ifso ifnot)).
{ erewrite instructions_preserved; eauto; simpl;
eauto. }
eauto.
assert (REGS_EQ: rs' ##2 args = rs ##2 args).
{ eapply registers_equal; eauto; intros.
apply Ple_trans with
(get_max_reg_in_ins
(Icond cond args ifso ifnot)).
apply max_reg_in_Icond_args.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
}
rewrite REGS_EQ.
auto.
+ constructor; eauto. }
{ exists (CSSApar.State ts tf sp ifnot rs' m).
split.
+ eapply CSSApar.exec_Icond_false; eauto.
assert ((CSSApar.fn_code tf) ! pc =
Some (Icond cond args ifso ifnot)).
{ erewrite instructions_preserved; eauto; simpl;
eauto. }
eauto.
assert (REGS_EQ: rs' ##2 args = rs ##2 args).
{ eapply registers_equal; eauto; intros.
apply Ple_trans with
(get_max_reg_in_ins
(Icond cond args ifso ifnot)).
apply max_reg_in_Icond_args.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
}
rewrite REGS_EQ.
auto.
+ constructor; eauto. }
{ exists (CSSApar.State ts tf sp pc' rs' m).
split.
+ eapply CSSApar.exec_Ijumptable; eauto.
assert ((CSSApar.fn_code tf) ! pc =
Some (Ijumptable arg tbl)).
{ erewrite instructions_preserved; eauto; simpl;
eauto. }
eauto.
inv MREG. rewrite <- H3. congruence.
apply Ple_trans with
(get_max_reg_in_ins
(Ijumptable arg tbl)).
apply max_reg_in_Ijumptable_arg.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
+ constructor; eauto. }
{ exists (CSSApar.Returnstate ts
(regmap2_optget or Vundef rs') m').
split.
+ eapply CSSApar.exec_Ireturn; eauto.
assert ((CSSApar.fn_code tf) ! pc =
Some (Ireturn or)).
{ erewrite instructions_preserved; eauto; simpl; eauto. }
eauto.
erewrite <- stacksize_preserved; eauto.
+ destruct or; simpl; eauto.
inv MREG. rewrite H2. auto.
apply Ple_trans with
(get_max_reg_in_ins
(Ireturn (Some r))).
apply max_reg_in_Ireturn_r.
{ constructor. auto. } auto.
apply Ple_trans with
(get_max_reg_in_code (fn_code f)).
eapply max_reg_in_code; eauto.
apply max_reg_correct_code.
}
{
destruct tf as [tf | tf].
exists (CSSApar.State ts tf (Vptr stk Int.zero)
tf.(CSSApar.fn_entrypoint)
(init_regs args (CSSApar.fn_params tf))
m').
split.
+ eapply CSSApar.exec_function_internal.
erewrite <- stacksize_preserved; eauto.
simpl in SPEC.
unfold Errors.bind in SPEC.
flatten SPEC.
+ simpl in *.
unfold Errors.bind in SPEC.
flatten SPEC.
replace (CSSApar.fn_entrypoint tf)
with (fn_entrypoint f).
apply match_states_intro; eauto.
induction WFF. auto.
econstructor; eauto; intros.
replace (CSSApar.fn_params tf)
with (fn_params f); auto.
unfold transl_function in Eq.
flatten Eq. simpl. auto.
unfold transl_function in Eq.
flatten Eq. simpl. auto.
+ simpl in SPEC.
unfold Errors.bind in SPEC.
flatten SPEC.
}
{ inv SPEC.
exists (CSSApar.Returnstate ts res m').
split.
+ eapply CSSApar.exec_function_external.
eapply external_call_symbols_preserved; eauto.
eapply symbols_preserved.
eapply Genv.find_var_info_transf_partial; eauto.
+ econstructor; eauto. }
{
inv STACK.
exists (CSSApar.State ts0 tf sp pc
(rs' #2 res <- vres) m).
split.
+ eapply CSSApar.exec_return.
+ econstructor; eauto.
econstructor; intros.
inv MREG.
case_eq (p2eq res r); intros.
- rewrite e in *.
rewrite P2Map.gss.
rewrite P2Map.gss.
auto.
- rewrite P2Map.gso.
rewrite P2Map.gso.
auto. auto. auto.
}
Qed.
Theorem transf_program_correct:
forward_simulation (
SSA.semantics prog) (
CSSApar.semantics tprog).
Proof.
eapply forward_simulation_step with (match_states := match_states).
eexact symbols_preserved.
eexact transf_initial_states.
eexact transf_final_states.
exact transl_step_correct.
Qed.
End PRESERVATION.