Require Import Linking Errors Globalenvs Smallstep.
Require Import Coqlib RTL Maps Compopts.
Require Import RTLtoBTL RTLtoBTLproof.
Require Import BTLtoRTL BTLtoRTLproof.
Require Import BTL_Invariants BTL_SEsimuref.
Require Import BTL_BlockSimulation BTL_BlockSimulationproof.
RTL to BTL passes
Translate from RTL to BTL with basic-blocks
Module RTLtoBTL_BBlocksOracle <:
RTLtoBTL_TranslationOracle.
Axiom rtl2btl:
RTL.function ->
BTL.code *
node *
function_info * (
PTree.t node).
Extract Constant rtl2btl => "
RTLtoBTLaux.rtl2btl_BB".
End RTLtoBTL_BBlocksOracle.
Module RTLtoBTL_BBlocksproof :=
RTLtoBTL_Translationproof RTLtoBTL_BBlocksOracle.
Module RTLtoBTL_BBlocks :=
RTLtoBTL_BBlocksproof.
Translate from RTL to BTL with basic-blocks *and* synthetic nodes insertion
Module RTLtoBTL_BBlocksSNodesOracle <:
RTLtoBTL_TranslationOracle.
Axiom rtl2btl:
RTL.function ->
BTL.code *
node *
function_info * (
PTree.t node).
Extract Constant rtl2btl => "
RTLtoBTLaux.rtl2btl_BBSN".
End RTLtoBTL_BBlocksSNodesOracle.
Module RTLtoBTL_BBlocksSNodesproof :=
RTLtoBTL_Translationproof RTLtoBTL_BBlocksSNodesOracle.
Module RTLtoBTL_BBlocksSNodes :=
RTLtoBTL_BBlocksSNodesproof.
Translate from RTL to BTL with superblocks
Module RTLtoBTL_SuperBlocksOracle <:
RTLtoBTL_TranslationOracle.
Axiom rtl2btl:
RTL.function ->
BTL.code *
node *
function_info * (
PTree.t node).
Extract Constant rtl2btl => "
RTLtoBTLaux.rtl2btl_SB".
End RTLtoBTL_SuperBlocksOracle.
Module RTLtoBTL_SuperBlocksproof :=
RTLtoBTL_Translationproof RTLtoBTL_SuperBlocksOracle.
Module RTLtoBTL_SuperBlocks :=
RTLtoBTL_SuperBlocksproof.
BTL to RTL passes
Translate from BTL to RTL
Module BTLtoRTL_ClassicOracle <:
BTLtoRTL_TranslationOracle.
Axiom btl2rtl:
BTL.function ->
RTL.code *
node * (
PTree.t node).
Extract Constant btl2rtl => "
BTLtoRTLaux.btl2rtl".
End BTLtoRTL_ClassicOracle.
Module BTLtoRTL_Classicproof :=
BTLtoRTL_Translationproof BTLtoRTL_ClassicOracle.
Module BTLtoRTL_Classic :=
BTLtoRTL_Classicproof.
BTL Block Simulation passes
Expansions (unfolding RTL pseudo-instructions) pass
(can operates on any kind of btl block)
Module BTL_ExpansionsOracle <:
BTL_BlockSimulationConfig.
Axiom btl_optim_oracle:
ValueDomain.romem ->
BTL.function ->
BTL.code *
function_info *
gluemap.
Extract Constant btl_optim_oracle => "
fun _ ->
BTL_BlockOptimizer.btl_expansions_oracle".
Axiom btl_rrules:
unit ->
rrules_set.
Extract Constant btl_rrules => "
BTL_BlockOptimizer.btl_expansions_rrules".
Axiom btl_value_analysis:
unit ->
bool.
Extract Constant btl_value_analysis => "
BTL_BlockOptimizer.btl_expansions_value_analysis".
End BTL_ExpansionsOracle.
Module BTL_Expansionsproof :=
BTL_BlockSimulationCompproof BTL_ExpansionsOracle.
Module BTL_Expansions :=
BTL_Expansionsproof.
Lazy Code Transformations pass
(operates over basic-blocks + synthetic nodes)
Module BTL_LazyCodeOracle <:
BTL_BlockSimulationConfig.
Axiom btl_optim_oracle:
ValueDomain.romem ->
BTL.function ->
BTL.code *
function_info *
gluemap.
Extract Constant btl_optim_oracle => "
fun _ ->
BTL_BlockOptimizer.btl_lazy_code_oracle".
Axiom btl_rrules:
unit ->
rrules_set.
Extract Constant btl_rrules => "
BTL_BlockOptimizer.btl_lazy_code_rrules".
Axiom btl_value_analysis:
unit ->
bool.
Extract Constant btl_value_analysis => "
BTL_BlockOptimizer.btl_lazy_code_value_analysis".
End BTL_LazyCodeOracle.
Module BTL_LazyCodeproof :=
BTL_BlockSimulationCompproof BTL_LazyCodeOracle.
Module BTL_LazyCode :=
BTL_LazyCodeproof.
Superblocks scheduling pass
Module BTL_SchedulingOracle <:
BTL_BlockSimulationConfig.
Axiom btl_optim_oracle:
ValueDomain.romem ->
BTL.function ->
BTL.code *
function_info *
gluemap.
Extract Constant btl_optim_oracle => "
BTL_BlockOptimizer.btl_scheduling_oracle".
Axiom btl_rrules:
unit ->
rrules_set.
Extract Constant btl_rrules => "
BTL_BlockOptimizer.btl_scheduling_rrules".
Axiom btl_value_analysis:
unit ->
bool.
Extract Constant btl_value_analysis => "
BTL_BlockOptimizer.btl_scheduling_value_analysis".
End BTL_SchedulingOracle.
Module BTL_Schedulingproof :=
BTL_BlockSimulationCompproof BTL_SchedulingOracle.
Module BTL_Scheduling :=
BTL_Schedulingproof.
BTL composed passes (to have a single RTL to RTL pass in the end)
Local Open Scope linking_scope.
Local Open Scope error_monad_scope.
Definition match_if {
A:
Type} (
flag:
unit ->
bool) (
R:
A ->
A ->
Prop):
A ->
A ->
Prop :=
if flag tt then R else eq.
Global Instance TransfIfLink {
A:
Type} {
LA:
Linker A}
(
flag:
unit ->
bool) (
transf:
A ->
A ->
Prop) (
TL:
TransfLink transf)
:
TransfLink (
match_if flag transf).
Proof.
unfold match_if.
destruct (
flag tt).
-
auto.
-
red;
intros.
subst tp1 tp2.
exists p;
auto.
Qed.
Definition pass_if {
L :
Language} (
flag :
unit ->
bool) (
p :
Pass L L) :
Pass L L :=
if flag tt then p else pass_identity L.
Basic-blocks transformations composed passes:
If Compopts.btl_bb is false, the pass is not called;
Activated if either expansions or lct are on;
Convert into BTL with basic-blocks, and with synthetic nodes
only in the lct case;
Expansions are applied after lct, and verified separately
(not using the same set of rewriting rules);
Code is translated back to RTL using the classical way.
RTL -> BTL (BB \/ BBSN) -> BTL (Lazy code optim) + BTL (Expansed) -> RTL
Module BTL_BBpasses.
Definition bb_passes :=
(
if negb (
Compopts.optim_lct tt)
then
mkpass RTLtoBTL_BBlocks.match_prog
else mkpass RTLtoBTL_BBlocksSNodes.match_prog)
:::
pass_if Compopts.optim_lct BTL_LazyCode.pass
:::
pass_if Compopts.optims_expanse BTL_Expansions.pass
:::
mkpass BTLtoRTL_Classic.match_prog
:::
pass_nil _.
Definition transf_program (
p:
RTL.program) :
res RTL.program :=
assertion (
Compopts.btl_bb tt);
do btlp <-
if negb (
Compopts.optim_lct tt)
then
RTLtoBTL_BBlocks.transf_program p
else RTLtoBTL_BBlocksSNodes.transf_program p;
do p1 <-
if Compopts.optim_lct tt then
BTL_LazyCode.transf_program btlp else OK btlp;
do p2 <-
if Compopts.optims_expanse tt then
BTL_Expansions.transf_program p1 else OK p1;
BTLtoRTL_Classic.transf_program p2.
End BTL_BBpasses.
Module BTL_BBpassesproof.
Include BTL_BBpasses.
Definition match_prog :=
pass_match (
compose_passes bb_passes).
Lemma transf_program_match:
forall p tp,
transf_program p =
OK tp ->
match_prog p tp.
Proof.
intros p tp H.
unfold transf_program in H;
unfold match_prog,
bb_passes,
pass_if.
destruct btl_bb;
simpl; [|
inv H;
auto ].
apply bind_inversion in H.
destruct H.
inversion_clear H.
destruct optim_lct;
simpl in *;
apply bind_inversion in H1;
destruct H1;
inversion_clear H;
exists x;
split.
1:
apply RTLtoBTL_BBlocksSNodes.transf_program_match;
auto.
2:
apply RTLtoBTL_BBlocks.transf_program_match;
auto.
all:
destruct optims_expanse;
inv H1;
subst.
1,2:
apply bind_inversion in H2;
destruct H2;
inversion_clear H.
3:
exists x;
split;
auto.
1,2,4:
exists x0;
split;
auto.
1,3:
apply BTL_LazyCode.transf_program_match;
auto.
1:
exists x1;
split;
auto.
3,4,5:
exists x0;
split;
auto;
try reflexivity.
1,5:
apply BTL_Expansions.transf_program_match;
auto.
2:
inv H1.
1,2,3,4:
exists tp;
split;
auto;
apply BTLtoRTL_Classic.transf_program_match;
auto.
Qed.
Section PRESERVATION.
Variable prog:
RTL.program.
Variable tprog:
RTL.program.
Hypothesis TRANSF:
match_prog prog tprog.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Theorem transf_program_correct:
forward_simulation (
RTL.semantics prog) (
RTL.semantics tprog).
Proof.
End PRESERVATION.
Global Instance TransfBTL_BBpasses:
TransfLink match_prog :=
pass_match_link (
compose_passes bb_passes).
End BTL_BBpassesproof.
Superblocks scheduling composed passes:
RTL -> BTL (superblocks) -> BTL (scheduled) -> RTL
Module BTL_SBpasses.
Definition sbscheduling_passes :=
mkpass RTLtoBTL_SuperBlocks.match_prog
:::
BTL_Scheduling.pass
:::
mkpass BTLtoRTL_Classic.match_prog
:::
pass_nil _.
Definition transf_program (
p:
RTL.program) :
res RTL.program :=
do btlp <-
RTLtoBTL_SuperBlocks.transf_program p;
do optp <-
BTL_Scheduling.transf_program btlp;
BTLtoRTL_Classic.transf_program optp.
End BTL_SBpasses.
Module BTL_SBpassesproof.
Include BTL_SBpasses.
Definition match_prog :=
pass_match (
compose_passes sbscheduling_passes).
Lemma transf_program_match:
forall p tp,
transf_program p =
OK tp ->
match_prog p tp.
Proof.
Section PRESERVATION.
Variable prog:
RTL.program.
Variable tprog:
RTL.program.
Hypothesis TRANSF:
match_prog prog tprog.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Theorem transf_program_correct:
forward_simulation (
RTL.semantics prog) (
RTL.semantics tprog).
Proof.
End PRESERVATION.
Global Instance TransfBTL_SBpasses:
TransfLink match_prog :=
pass_match_link (
compose_passes sbscheduling_passes).
End BTL_SBpassesproof.