Lvc.Compiler
Require Import List CSet.
Require Import Util AllInRel MapDefined IL Rename RenameApart Sim Status Annotation.
Require CMap.
Require Liveness LivenessValidators ParallelMove ILN ILN_IL.
Require TrueLiveness LivenessAnalysis LivenessAnalysisCorrect.
Require Coherence Invariance.
Require Delocation DelocationAlgo DelocationCorrect DelocationValidator.
Require Allocation AllocationAlgo AllocationAlgoCorrect.
Require UCE DVE EAE Alpha.
Require ReachabilityAnalysis ReachabilityAnalysisCorrect.
Require Import String.
Set Implicit Arguments.
Section Compiler.
Hypothesis ssa_construction : stmt → ann (option (set var)) × ann (list var).
Hypothesis parallel_move : var → list var → list var → (list(list var × list var)).
Hypothesis first : ∀ (A:Type), A → ( A → status (A × bool)) → status A.
Arguments first {A} _ _.
Definition additionalArguments s lv :=
fst (DelocationAlgo.computeParameters nil nil nil s lv).
Class ToString (T:Type) := toString : T → string.
Hypothesis OutputStream : Type.
Hypothesis print_string : OutputStream → string → OutputStream.
Hypothesis toString_nstmt : ILN.nstmt → string.
Instance ToString_nstmt : ToString ILN.nstmt := toString_nstmt.
Hypothesis toString_stmt : stmt → string.
Instance ToString_stmt : ToString stmt := toString_stmt.
Hypothesis toString_ann : ∀ A, (A → string) → ann A → string.
Instance ToString_ann {A} `{ToString A} : ToString (ann A) :=
toString_ann (@toString A _).
Hypothesis toString_live : set var → string.
Instance ToString_live : ToString (set var) := toString_live.
Hypothesis toString_list : list var → string.
Instance ToString_list : ToString (list var) := toString_list.
Notation "S '<<' x '<<' y ';' s" := (let S := print_string S (x ++ "\n" ++ toString y ++ "\n\n") in s) (at level 1, left associativity).
Definition ensure_f P `{Computable P} (s: string) {A} (cont:status A) : status A :=
if [P] then cont else Error s.
Arguments ensure_f P [H] s {A} cont.
Notation "'ensure' P s ; cont " := (ensure_f P s cont)
(at level 20, P at level 0, s at level 0, cont at level 200, left associativity).
Definition toDeBruijn (ilin:ILN.nstmt) : status IL.stmt :=
ILN_IL.labIndices nil ilin.
Lemma toDeBruijn_correct (ilin:ILN.nstmt) s (E:onv val)
: toDeBruijn ilin = Success s
→ @sim _ ILN.statetype_I _ _ bot3 Bisim
(ILN.I.labenv_empty, E, ilin)
(nil:list I.block, E, s).
Proof.
intros. unfold toDeBruijn in H. simpl in ×.
eapply ILN_IL.labIndicesSim_sim.
econstructor; eauto; isabsurd. econstructor; isabsurd. constructor.
Qed.
Arguments sim S {H} S' {H0} r t _ _.
Definition DCVE (s:IL.stmt) : stmt × ann (set var) :=
let uc := ReachabilityAnalysis.reachabilityAnalysis s in
let s_uce := UCE.compile nil s uc in
let tlv := LivenessAnalysis.livenessAnalysis s_uce in
let s_dve := DVE.compile nil s_uce tlv in
(s_dve, DVE.compile_live s_uce tlv ∅).
Lemma DCVE_live (ili:IL.stmt) (PM:LabelsDefined.paramsMatch ili nil)
: Liveness.live_sound Liveness.Imperative nil nil (fst (DCVE ili)) (snd (DCVE ili)).
Proof.
unfold DCVE. simpl.
eapply (@DVE.dve_live _ nil nil).
eapply @LivenessAnalysisCorrect.correct; eauto.
eapply (@UCE.UCE_paramsMatch nil nil); eauto.
eapply Reachability.reachability_SC_S, ReachabilityAnalysisCorrect.correct; eauto.
eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
Qed.
Lemma DCVE_noUC ili (PM:LabelsDefined.paramsMatch ili nil)
: LabelsDefined.noUnreachableCode LabelsDefined.isCalled (fst (DCVE ili)).
Proof.
intros. subst. simpl.
eapply LabelsDefined.noUnreachableCode_mono.
- eapply (@DVE.DVE_noUnreachableCode _ nil nil).
+ eapply @LivenessAnalysisCorrect.correct; eauto.
eapply (@UCE.UCE_paramsMatch nil nil); eauto.
× eapply Reachability.reachability_SC_S, ReachabilityAnalysisCorrect.correct; eauto.
× eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
+ eapply UCE.UCE_noUnreachableCode.
× eapply ReachabilityAnalysisCorrect.correct; eauto.
× eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
- eapply LabelsDefined.trueIsCalled_isCalled.
Qed.
Lemma DCVE_occurVars s (PM:LabelsDefined.paramsMatch s nil)
: getAnn (snd (DCVE s)) ⊆ occurVars s.
Proof.
simpl.
rewrite DVE.compile_live_incl_empty; eauto.
rewrite LivenessAnalysisCorrect.livenessAnalysis_getAnn.
eapply UCE.compile_occurVars.
eapply @LivenessAnalysisCorrect.correct; eauto.
eapply (@UCE.UCE_paramsMatch nil nil); eauto.
× eapply Reachability.reachability_SC_S, ReachabilityAnalysisCorrect.correct; eauto.
× eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
Qed.
Lemma DCVE_correct (ili:IL.stmt) (E:onv val)
(PM:LabelsDefined.paramsMatch ili nil)
: defined_on (IL.occurVars ili) E
→ sim I.state I.state bot3 Sim (nil, E, ili) (nil, E, fst (DCVE ili)).
Proof.
intros. subst. unfold DCVE.
simpl in *; unfold ensure_f, additionalArguments in ×.
assert (Reachability.reachability Reachability.SoundAndComplete nil ili
(ReachabilityAnalysis.reachabilityAnalysis ili)). {
eapply ReachabilityAnalysisCorrect.correct; eauto.
}
assert (getAnn (ReachabilityAnalysis.reachabilityAnalysis ili)). {
eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
}
assert (LabelsDefined.paramsMatch
(UCE.compile nil ili (ReachabilityAnalysis.reachabilityAnalysis ili)) nil). {
eapply (@UCE.UCE_paramsMatch nil nil); eauto.
}
assert (TrueLiveness.true_live_sound Liveness.Imperative nil nil
(UCE.compile nil ili (ReachabilityAnalysis.reachabilityAnalysis ili))
(LivenessAnalysis.livenessAnalysis
(UCE.compile nil ili (ReachabilityAnalysis.reachabilityAnalysis ili)))). {
eapply @LivenessAnalysisCorrect.correct; eauto.
}
eapply sim_trans with (S2:=I.state).
eapply bisim_sim.
eapply UCE.I.sim_UCE.
eapply Reachability.reachability_SC_S, ReachabilityAnalysisCorrect.correct; eauto.
eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
eapply DVE.I.sim_DVE; [ reflexivity | eapply LivenessAnalysisCorrect.correct; eauto ].
Qed.
Definition addParams (s:IL.stmt) (lv:ann (set var)) : IL.stmt :=
let additional_params := additionalArguments s lv in
Delocation.compile nil s additional_params.
Lemma addParams_correct (E:onv val) (ili:IL.stmt) lv
: defined_on (getAnn lv) E
→ Liveness.live_sound Liveness.Imperative nil nil ili lv
→ LabelsDefined.noUnreachableCode LabelsDefined.isCalled ili
→ sim I.state F.state bot3 Sim (nil, E, ili) (nil:list F.block, E, addParams ili lv).
Proof with eauto using DCVE_live, DCVE_noUC.
intros. subst. unfold addParams.
eapply sim_trans with (S2:=I.state).
- eapply bisim_sim.
eapply DelocationCorrect.correct; eauto.
+ eapply DelocationAlgo.is_trs; eauto...
+ eapply (@Delocation.live_sound_compile nil)...
eapply DelocationAlgo.is_trs...
eapply DelocationAlgo.is_live...
- eapply bisim_sim.
eapply bisim_sym.
eapply (@Invariance.srdSim_sim nil nil nil nil nil);
[ | isabsurd | econstructor | reflexivity | | econstructor ].
+ eapply Delocation.trs_srd; eauto.
eapply DelocationAlgo.is_trs...
+ eapply (@Delocation.live_sound_compile nil nil nil)...
eapply DelocationAlgo.is_trs...
eapply DelocationAlgo.is_live...
Qed.
Definition toILF (s:IL.stmt) : IL.stmt :=
let (s_dcve, lv) := DCVE s in
addParams s_dcve lv.
Lemma toILF_correct (ili:IL.stmt) (E:onv val)
(PM:LabelsDefined.paramsMatch ili nil)
: defined_on (IL.occurVars ili) E
→ sim I.state F.state bot3 Sim (nil, E, ili) (nil:list F.block, E, toILF ili).
Proof with eauto using DCVE_live, DCVE_noUC.
intros. subst. unfold toILF.
eapply sim_trans with (S2:=I.state).
eapply DCVE_correct; eauto. let_pair_case_eq; simpl_pair_eqs; subst.
unfold fst at 1.
eapply addParams_correct...
eauto using defined_on_incl, DCVE_occurVars.
Qed.
End Compiler.
Print Assumptions toDeBruijn_correct.
Print Assumptions toILF_correct.
Require Import Util AllInRel MapDefined IL Rename RenameApart Sim Status Annotation.
Require CMap.
Require Liveness LivenessValidators ParallelMove ILN ILN_IL.
Require TrueLiveness LivenessAnalysis LivenessAnalysisCorrect.
Require Coherence Invariance.
Require Delocation DelocationAlgo DelocationCorrect DelocationValidator.
Require Allocation AllocationAlgo AllocationAlgoCorrect.
Require UCE DVE EAE Alpha.
Require ReachabilityAnalysis ReachabilityAnalysisCorrect.
Require Import String.
Set Implicit Arguments.
Section Compiler.
Hypothesis ssa_construction : stmt → ann (option (set var)) × ann (list var).
Hypothesis parallel_move : var → list var → list var → (list(list var × list var)).
Hypothesis first : ∀ (A:Type), A → ( A → status (A × bool)) → status A.
Arguments first {A} _ _.
Definition additionalArguments s lv :=
fst (DelocationAlgo.computeParameters nil nil nil s lv).
Class ToString (T:Type) := toString : T → string.
Hypothesis OutputStream : Type.
Hypothesis print_string : OutputStream → string → OutputStream.
Hypothesis toString_nstmt : ILN.nstmt → string.
Instance ToString_nstmt : ToString ILN.nstmt := toString_nstmt.
Hypothesis toString_stmt : stmt → string.
Instance ToString_stmt : ToString stmt := toString_stmt.
Hypothesis toString_ann : ∀ A, (A → string) → ann A → string.
Instance ToString_ann {A} `{ToString A} : ToString (ann A) :=
toString_ann (@toString A _).
Hypothesis toString_live : set var → string.
Instance ToString_live : ToString (set var) := toString_live.
Hypothesis toString_list : list var → string.
Instance ToString_list : ToString (list var) := toString_list.
Notation "S '<<' x '<<' y ';' s" := (let S := print_string S (x ++ "\n" ++ toString y ++ "\n\n") in s) (at level 1, left associativity).
Definition ensure_f P `{Computable P} (s: string) {A} (cont:status A) : status A :=
if [P] then cont else Error s.
Arguments ensure_f P [H] s {A} cont.
Notation "'ensure' P s ; cont " := (ensure_f P s cont)
(at level 20, P at level 0, s at level 0, cont at level 200, left associativity).
Definition toDeBruijn (ilin:ILN.nstmt) : status IL.stmt :=
ILN_IL.labIndices nil ilin.
Lemma toDeBruijn_correct (ilin:ILN.nstmt) s (E:onv val)
: toDeBruijn ilin = Success s
→ @sim _ ILN.statetype_I _ _ bot3 Bisim
(ILN.I.labenv_empty, E, ilin)
(nil:list I.block, E, s).
Proof.
intros. unfold toDeBruijn in H. simpl in ×.
eapply ILN_IL.labIndicesSim_sim.
econstructor; eauto; isabsurd. econstructor; isabsurd. constructor.
Qed.
Arguments sim S {H} S' {H0} r t _ _.
Definition DCVE (s:IL.stmt) : stmt × ann (set var) :=
let uc := ReachabilityAnalysis.reachabilityAnalysis s in
let s_uce := UCE.compile nil s uc in
let tlv := LivenessAnalysis.livenessAnalysis s_uce in
let s_dve := DVE.compile nil s_uce tlv in
(s_dve, DVE.compile_live s_uce tlv ∅).
Lemma DCVE_live (ili:IL.stmt) (PM:LabelsDefined.paramsMatch ili nil)
: Liveness.live_sound Liveness.Imperative nil nil (fst (DCVE ili)) (snd (DCVE ili)).
Proof.
unfold DCVE. simpl.
eapply (@DVE.dve_live _ nil nil).
eapply @LivenessAnalysisCorrect.correct; eauto.
eapply (@UCE.UCE_paramsMatch nil nil); eauto.
eapply Reachability.reachability_SC_S, ReachabilityAnalysisCorrect.correct; eauto.
eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
Qed.
Lemma DCVE_noUC ili (PM:LabelsDefined.paramsMatch ili nil)
: LabelsDefined.noUnreachableCode LabelsDefined.isCalled (fst (DCVE ili)).
Proof.
intros. subst. simpl.
eapply LabelsDefined.noUnreachableCode_mono.
- eapply (@DVE.DVE_noUnreachableCode _ nil nil).
+ eapply @LivenessAnalysisCorrect.correct; eauto.
eapply (@UCE.UCE_paramsMatch nil nil); eauto.
× eapply Reachability.reachability_SC_S, ReachabilityAnalysisCorrect.correct; eauto.
× eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
+ eapply UCE.UCE_noUnreachableCode.
× eapply ReachabilityAnalysisCorrect.correct; eauto.
× eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
- eapply LabelsDefined.trueIsCalled_isCalled.
Qed.
Lemma DCVE_occurVars s (PM:LabelsDefined.paramsMatch s nil)
: getAnn (snd (DCVE s)) ⊆ occurVars s.
Proof.
simpl.
rewrite DVE.compile_live_incl_empty; eauto.
rewrite LivenessAnalysisCorrect.livenessAnalysis_getAnn.
eapply UCE.compile_occurVars.
eapply @LivenessAnalysisCorrect.correct; eauto.
eapply (@UCE.UCE_paramsMatch nil nil); eauto.
× eapply Reachability.reachability_SC_S, ReachabilityAnalysisCorrect.correct; eauto.
× eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
Qed.
Lemma DCVE_correct (ili:IL.stmt) (E:onv val)
(PM:LabelsDefined.paramsMatch ili nil)
: defined_on (IL.occurVars ili) E
→ sim I.state I.state bot3 Sim (nil, E, ili) (nil, E, fst (DCVE ili)).
Proof.
intros. subst. unfold DCVE.
simpl in *; unfold ensure_f, additionalArguments in ×.
assert (Reachability.reachability Reachability.SoundAndComplete nil ili
(ReachabilityAnalysis.reachabilityAnalysis ili)). {
eapply ReachabilityAnalysisCorrect.correct; eauto.
}
assert (getAnn (ReachabilityAnalysis.reachabilityAnalysis ili)). {
eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
}
assert (LabelsDefined.paramsMatch
(UCE.compile nil ili (ReachabilityAnalysis.reachabilityAnalysis ili)) nil). {
eapply (@UCE.UCE_paramsMatch nil nil); eauto.
}
assert (TrueLiveness.true_live_sound Liveness.Imperative nil nil
(UCE.compile nil ili (ReachabilityAnalysis.reachabilityAnalysis ili))
(LivenessAnalysis.livenessAnalysis
(UCE.compile nil ili (ReachabilityAnalysis.reachabilityAnalysis ili)))). {
eapply @LivenessAnalysisCorrect.correct; eauto.
}
eapply sim_trans with (S2:=I.state).
eapply bisim_sim.
eapply UCE.I.sim_UCE.
eapply Reachability.reachability_SC_S, ReachabilityAnalysisCorrect.correct; eauto.
eapply ReachabilityAnalysisCorrect.reachabilityAnalysis_getAnn.
eapply DVE.I.sim_DVE; [ reflexivity | eapply LivenessAnalysisCorrect.correct; eauto ].
Qed.
Definition addParams (s:IL.stmt) (lv:ann (set var)) : IL.stmt :=
let additional_params := additionalArguments s lv in
Delocation.compile nil s additional_params.
Lemma addParams_correct (E:onv val) (ili:IL.stmt) lv
: defined_on (getAnn lv) E
→ Liveness.live_sound Liveness.Imperative nil nil ili lv
→ LabelsDefined.noUnreachableCode LabelsDefined.isCalled ili
→ sim I.state F.state bot3 Sim (nil, E, ili) (nil:list F.block, E, addParams ili lv).
Proof with eauto using DCVE_live, DCVE_noUC.
intros. subst. unfold addParams.
eapply sim_trans with (S2:=I.state).
- eapply bisim_sim.
eapply DelocationCorrect.correct; eauto.
+ eapply DelocationAlgo.is_trs; eauto...
+ eapply (@Delocation.live_sound_compile nil)...
eapply DelocationAlgo.is_trs...
eapply DelocationAlgo.is_live...
- eapply bisim_sim.
eapply bisim_sym.
eapply (@Invariance.srdSim_sim nil nil nil nil nil);
[ | isabsurd | econstructor | reflexivity | | econstructor ].
+ eapply Delocation.trs_srd; eauto.
eapply DelocationAlgo.is_trs...
+ eapply (@Delocation.live_sound_compile nil nil nil)...
eapply DelocationAlgo.is_trs...
eapply DelocationAlgo.is_live...
Qed.
Definition toILF (s:IL.stmt) : IL.stmt :=
let (s_dcve, lv) := DCVE s in
addParams s_dcve lv.
Lemma toILF_correct (ili:IL.stmt) (E:onv val)
(PM:LabelsDefined.paramsMatch ili nil)
: defined_on (IL.occurVars ili) E
→ sim I.state F.state bot3 Sim (nil, E, ili) (nil:list F.block, E, toILF ili).
Proof with eauto using DCVE_live, DCVE_noUC.
intros. subst. unfold toILF.
eapply sim_trans with (S2:=I.state).
eapply DCVE_correct; eauto. let_pair_case_eq; simpl_pair_eqs; subst.
unfold fst at 1.
eapply addParams_correct...
eauto using defined_on_incl, DCVE_occurVars.
Qed.
End Compiler.
Print Assumptions toDeBruijn_correct.
Print Assumptions toILF_correct.