Module Asmgenproof
Composing all passes from Mach to KVX Asm
Require
Import
Coqlib
Errors
.
Require
Import
Integers
Floats
AST
Linking
.
Require
Import
Values
Memory
Events
Globalenvs
Smallstep
.
Require
Import
Op
Locations
Mach
Conventions
Asm
Asmgen
Machblockgen
Asmblockgen
.
Require
Import
Machblockgenproof
Asmblockgenproof
PostpassSchedulingproof
.
Local
Open
Scope
linking_scope
.
Definition
block_passes
:=
mkpass
Machblockgenproof.match_prog
:::
mkpass
Asmblockgenproof.match_prog
:::
mkpass
PostpassSchedulingproof.match_prog
:::
mkpass
Asm.match_prog
:::
pass_nil
_.
Definition
match_prog
:=
pass_match
(
compose_passes
block_passes
).
Lemma
transf_program_match
:
forall
p
tp
,
Asmgen.transf_program
p
=
OK
tp
->
match_prog
p
tp
.
Proof.
intros
p
tp
H
.
unfold
Asmgen.transf_program
in
H
.
apply
bind_inversion
in
H
.
destruct
H
.
inversion_clear
H
.
apply
bind_inversion
in
H1
.
destruct
H1
.
inversion_clear
H
.
inversion
H2
.
unfold
time
,
Compopts.time
in
*.
remember
(
Machblockgen.transf_program
p
)
as
mbp
.
unfold
match_prog
;
cbn
.
exists
mbp
;
split
.
apply
Machblockgenproof.transf_program_match
;
auto
.
exists
x
;
split
.
apply
Asmblockgenproof.transf_program_match
;
auto
.
exists
x0
;
split
.
apply
PostpassSchedulingproof.transf_program_match
;
auto
.
exists
tp
;
split
.
apply
Asm.transf_program_match
;
auto
.
auto
.
Qed.
Return Address Offset for Mach
Definition
return_address_offset
:
Mach.function
->
Mach.code
->
ptrofs
->
Prop
:=
Mach_return_address_offset
Asmblockgenproof.return_address_offset
.
Lemma
return_address_exists
:
forall
f
sg
ros
c
,
is_tail
(
Mcall
sg
ros
::
c
)
f
.(
Mach.fn_code
) ->
exists
ra
,
return_address_offset
f
c
ra
.
Proof.
intros
;
unfold
return_address_offset
;
eapply
Mach_return_address_exists
;
eauto
.
intros
;
eapply
Asmblockgenproof.return_address_exists
;
eauto
.
Qed.
Main preservation theorem: from Mach to KVX Asm
Section
PRESERVATION
.
Variable
prog
:
Mach.program
.
Variable
tprog
:
program
.
Hypothesis
TRANSF
:
match_prog
prog
tprog
.
Let
ge
:=
Genv.globalenv
prog
.
Let
tge
:=
Genv.globalenv
tprog
.
Theorem
transf_program_correct
:
forward_simulation
(
Mach.semantics
return_address_offset
prog
) (
Asm.semantics
tprog
).
Proof.
unfold
match_prog
in
TRANSF
.
cbn
in
TRANSF
.
inv
TRANSF
.
inv
H
.
inv
H1
.
inv
H
.
inv
H2
.
inv
H
.
inv
H3
.
inv
H
.
eapply
compose_forward_simulations
.
exploit
Machblockgenproof.transf_program_correct
;
eauto
.
unfold
Machblockgenproof.inv_trans_rao
.
eapply
compose_forward_simulations
.
apply
Asmblockgenproof.transf_program_correct
;
eauto
.
eapply
compose_forward_simulations
.
apply
PostpassSchedulingproof.transf_program_correct
;
eauto
.
apply
Asm.transf_program_correct
.
eauto
.
Qed.
End
PRESERVATION
.
#[
global
]
Instance
TransfAsm
:
TransfLink
match_prog
:=
pass_match_link
(
compose_passes
block_passes
).
Stub actually needed by driver/Compiler
Module
Asmgenproof0
.
Definition
return_address_offset
:=
return_address_offset
.
End
Asmgenproof0
.