The whole compiler and its proof of semantic preservation
Libraries.
Require Import String.
Require Import Coqlib Errors.
Require Import AST Linking Smallstep.
Languages (syntax and semantics).
Require Ctypes Csyntax Csem Cstrategy Cexec.
Require Clight.
Require Csharpminor.
Require Cminor.
Require CminorSel.
Require RTL.
Require LTL.
Require Linear.
Require Mach.
Require Asm.
Require RawAsm RealAsm.
Translation passes.
Require SimplExpr.
Require SimplLocals.
Require Cshmgen.
Require Cminorgen.
Require Selection.
Require RTLgen.
Require Tailcall.
Require Inlining.
Require Renumber.
Require Constprop.
Require CSE.
Require Deadcode.
Require Unusedglob.
Require Allocation.
Require Tunneling.
Require Linearize.
Require CleanupLabels.
Require Debugvar.
Require Stacking.
Require Mach2Mach2.
Require Asmgen.
Require PseudoInstructions.
Require FlatAsmgen.
Require MCgen.
Require RockSaltAsmGen.
Proofs of semantic preservation.
Require SimplExprproof.
Require SimplLocalsproof.
Require Cshmgenproof.
Require Cminorgenproof.
Require Selectionproof.
Require RTLgenproof.
Require Tailcallproof.
Require Inliningproof.
Require Renumberproof.
Require Constpropproof.
Require CSEproof.
Require Deadcodeproof.
Require Unusedglobproof.
Require Allocproof.
Require Tunnelingproof.
Require Linearizeproof.
Require CleanupLabelsproof.
Require Debugvarproof.
Require Stackingproof.
Require Asmgenproof.
Require RawAsmproof.
Require RealAsmproof2.
Require PseudoInstructionsproof.
Require FlatAsmgenproof.
Require FlatAsmGlobenv.
Require FlatAsmProgram.
Require FlatAsmgen.
Require FlatAsmSep.
Require MCgenproof.
Require MCSep.
Command-line flags.
Require Import Compopts.
Pretty-printers (defined in Caml).
Parameter print_Clight:
Clight.program ->
unit.
Parameter print_Cminor:
Cminor.program ->
unit.
Parameter print_RTL:
Z ->
RTL.program ->
unit.
Parameter print_LTL:
LTL.program ->
unit.
Parameter print_Mach:
Mach.program ->
unit.
Local Open Scope string_scope.
Composing the translation passes
We first define useful monadic composition operators,
along with funny (but convenient) notations.
Definition apply_total (
A B:
Type) (
x:
res A) (
f:
A ->
B) :
res B :=
match x with Error msg =>
Error msg |
OK x1 =>
OK (
f x1)
end.
Definition apply_partial (
A B:
Type)
(
x:
res A) (
f:
A ->
res B) :
res B :=
match x with Error msg =>
Error msg |
OK x1 =>
f x1 end.
Notation "
a @@@
b" :=
(
apply_partial _ _ a b) (
at level 50,
left associativity).
Notation "
a @@
b" :=
(
apply_total _ _ a b) (
at level 50,
left associativity).
Definition print {
A:
Type} (
printer:
A ->
unit) (
prog:
A) :
A :=
let unused :=
printer prog in prog.
Definition time {
A B:
Type} (
name:
string) (
f:
A ->
B) :
A ->
B :=
f.
Definition total_if {
A:
Type}
(
flag:
unit ->
bool) (
f:
A ->
A) (
prog:
A) :
A :=
if flag tt then f prog else prog.
Definition partial_if {
A:
Type}
(
flag:
unit ->
bool) (
f:
A ->
res A) (
prog:
A) :
res A :=
if flag tt then f prog else OK prog.
We define three translation functions for whole programs: one
starting with a C program, one with a Cminor program, one with an
RTL program. The three translations produce Asm programs ready for
pretty-printing and assembling.
Local Existing Instance ValueAnalysis.romem_for_wp_instance.
Definition transf_rtl_program (
f:
RTL.program) :
res Asm.program :=
OK f
@@
print (
print_RTL 0)
@@
total_if Compopts.optim_tailcalls (
time "
Tail calls"
Tailcall.transf_program)
@@
print (
print_RTL 1)
@@@
partial_if Compopts.optim_inlining (
time "
Inlining"
Inlining.transf_program)
@@
print (
print_RTL 2)
@@
time "
Renumbering"
Renumber.transf_program
@@
print (
print_RTL 3)
@@
total_if Compopts.optim_constprop (
time "
Constant propagation"
Constprop.transf_program)
@@
print (
print_RTL 4)
@@
total_if Compopts.optim_constprop (
time "
Renumbering"
Renumber.transf_program)
@@
print (
print_RTL 5)
@@@
partial_if Compopts.optim_CSE (
time "
CSE"
CSE.transf_program)
@@
print (
print_RTL 6)
@@@
partial_if Compopts.optim_redundancy (
time "
Redundancy elimination"
Deadcode.transf_program)
@@
print (
print_RTL 7)
@@@
time "
Unused globals"
Unusedglob.transform_program
@@
print (
print_RTL 8)
@@@
time "
Register allocation"
Allocation.transf_program
@@
print print_LTL
@@
time "
Branch tunneling"
Tunneling.tunnel_program
@@@
time "
CFG linearization"
Linearize.transf_program
@@
time "
Label cleanup"
CleanupLabels.transf_program
@@@
partial_if Compopts.debug (
time "
Debugging info for local variables"
Debugvar.transf_program)
@@@
time "
Mach generation"
Stacking.transf_program
@@
print print_Mach
@@@
time "
Asm generation"
Asmgen.transf_program.
Definition transf_cminor_program (
p:
Cminor.program) :
res Asm.program :=
OK p
@@
print print_Cminor
@@@
time "
Instruction selection"
Selection.sel_program
@@@
time "
RTL generation"
RTLgen.transl_program
@@@
transf_rtl_program.
Definition transf_cminor_program_rs (
p:
Cminor.program) :
res RockSaltAsm.program :=
OK p
@@@
transf_cminor_program
@@@
PseudoInstructions.check_program
@@
time "
Elimination of pseudo instruction"
PseudoInstructions.transf_program
@@@
time "
Generation of FlatAsm"
FlatAsmgen.transf_program
@@@
time "
Generation of MC"
MCgen.transf_program
@@@
time "
Generation of RockSalt program"
RockSaltAsmGen.transf_program.
Definition transf_clight_program (
p:
Clight.program) :
res Asm.program :=
OK p
@@
print print_Clight
@@@
time "
Simplification of locals"
SimplLocals.transf_program
@@@
time "
C#
minor generation"
Cshmgen.transl_program
@@@
time "
Cminor generation"
Cminorgen.transl_program
@@@
transf_cminor_program.
Definition transf_c_program (
p:
Csyntax.program) :
res Asm.program :=
OK p
@@@
time "
Clight generation"
SimplExpr.transl_program
@@@
transf_clight_program.
Definition transf_c_program_real p :
res Asm.program :=
transf_c_program p
@@@
PseudoInstructions.check_program
@@
time "
Elimination of pseudo instruction"
PseudoInstructions.transf_program.
Definition transf_c_program_flatasm p :
res FlatAsm.program :=
transf_c_program_real p
@@@
time "
Generation of FlatAsm"
FlatAsmgen.transf_program.
Definition transf_c_program_mc p :
res MC.program :=
transf_c_program_flatasm p
@@@
time "
Generation of MC"
MCgen.transf_program.
Definition transf_c_program_rs p :
res RockSaltAsm.program :=
transf_c_program_mc p
@@@
time "
Generation of RockSalt program"
RockSaltAsmGen.transf_program.
The following lemmas help reason over compositions of passes.
Lemma print_identity:
forall (
A:
Type) (
printer:
A ->
unit) (
prog:
A),
print printer prog =
prog.
Proof.
intros;
unfold print.
destruct (
printer prog);
auto.
Qed.
Lemma compose_print_identity:
forall (
A:
Type) (
x:
res A) (
f:
A ->
unit),
x @@
print f =
x.
Proof.
Relational specification of compilation
Definition match_if {
A:
Type} (
flag:
unit ->
bool) (
R:
A ->
A ->
Prop):
A ->
A ->
Prop :=
if flag tt then R else eq.
Lemma total_if_match:
forall (
A:
Type) (
flag:
unit ->
bool) (
f:
A ->
A) (
rel:
A ->
A ->
Prop) (
prog:
A),
(
forall p,
rel p (
f p)) ->
match_if flag rel prog (
total_if flag f prog).
Proof.
Lemma partial_if_match:
forall (
A:
Type) (
flag:
unit ->
bool) (
f:
A ->
res A) (
rel:
A ->
A ->
Prop) (
prog tprog:
A),
(
forall p tp,
f p =
OK tp ->
rel p tp) ->
partial_if flag f prog =
OK tprog ->
match_if flag rel prog tprog.
Proof.
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.
This is the list of compilation passes of CompCert in relational style.
Each pass is characterized by a match_prog relation between its
input code and its output code. The mkpass and ::: combinators,
defined in module Linking, ensure that the passes are composable
(the output language of a pass is the input language of the next pass)
and that they commute with linking (property TransfLink, inferred
by the type class mechanism of Coq).
Local Open Scope linking_scope.
Definition CompCert'
s_passes :=
mkpass SimplExprproof.match_prog
:::
mkpass SimplLocalsproof.match_prog
:::
mkpass Cshmgenproof.match_prog
:::
mkpass Cminorgenproof.match_prog
:::
mkpass Selectionproof.match_prog
:::
mkpass RTLgenproof.match_prog
:::
mkpass (
match_if Compopts.optim_tailcalls Tailcallproof.match_prog)
:::
mkpass (
match_if Compopts.optim_inlining Inliningproof.match_prog)
:::
mkpass Renumberproof.match_prog
:::
mkpass (
match_if Compopts.optim_constprop Constpropproof.match_prog)
:::
mkpass (
match_if Compopts.optim_constprop Renumberproof.match_prog)
:::
mkpass (
match_if Compopts.optim_CSE CSEproof.match_prog)
:::
mkpass (
match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
:::
mkpass Unusedglobproof.match_prog
:::
mkpass Allocproof.match_prog
:::
mkpass Tunnelingproof.match_prog
:::
mkpass Linearizeproof.match_prog
:::
mkpass CleanupLabelsproof.match_prog
:::
mkpass (
match_if Compopts.debug Debugvarproof.match_prog)
:::
mkpass Stackingproof.match_prog
:::
mkpass Asmgenproof.match_prog
:::
pass_nil _.
Composing the match_prog relations above, we obtain the relation
between CompCert C sources and Asm code that characterize CompCert's
compilation.
Definition match_prog:
Csyntax.program ->
Asm.program ->
Prop :=
pass_match (
compose_passes CompCert'
s_passes).
Fixpoint passes_app {
A B C} (
l1:
Passes A B) (
l2:
Passes B C) :
Passes A C :=
match l1 in (
Passes AA BB)
return (
Passes BB C ->
Passes AA C)
with
|
pass_nil _ =>
fun l3 =>
l3
|
pass_cons _ _ _ P1 l1 =>
fun l2 =>
P1 :::
passes_app l1 l2
end l2.
Definition real_asm_passes :=
mkpass PseudoInstructions.match_check_prog
:::
mkpass PseudoInstructionsproof.match_prog
:::
pass_nil _.
Definition match_prog_real :=
pass_match (
compose_passes (
passes_app CompCert'
s_passes real_asm_passes)).
Definition flat_asm_passes :=
passes_app real_asm_passes
(
mkpass FlatAsmgenproof.match_prog :::
pass_nil _).
Definition match_prog_flat :=
pass_match (
compose_passes (
passes_app CompCert'
s_passes flat_asm_passes)).
Definition mc_passes :=
passes_app flat_asm_passes
(
mkpass MCgenproof.match_prog :::
pass_nil _).
Definition match_prog_mc :=
pass_match (
compose_passes (
passes_app CompCert'
s_passes mc_passes)).
The transf_c_program function, when successful, produces
assembly code that is in the match_prog relation with the source C program.
Theorem transf_c_program_match:
forall p tp,
transf_c_program p =
OK tp ->
match_prog p tp.
Proof.
Lemma compose_passes_app:
forall {
l1 l2} (
A:
Passes l1 l2) {
l3} (
B:
Passes l2 l3)
p tp,
compose_passes (
passes_app A B)
p tp <->
exists pi,
compose_passes A p pi /\
compose_passes B pi tp.
Proof.
induction A;
simpl;
intros.
split.
eexists;
split;
eauto.
intros (
pi &
EQ &
CP);
inv EQ;
auto.
setoid_rewrite IHA.
split;
intro H;
decompose [
ex and]
H;
eauto.
Qed.
Theorem transf_c_program_real_match:
forall p tp,
transf_c_program_real p =
OK tp ->
match_prog_real p tp.
Proof.
Theorem transf_c_program_flat_match:
forall p tp,
transf_c_program_flatasm p =
OK tp ->
match_prog_flat p tp.
Proof.
Theorem transf_c_program_mc_match:
forall p tp,
transf_c_program_mc p =
OK tp ->
match_prog_mc p tp.
Proof.
Semantic preservation
We now prove that the whole CompCert compiler (as characterized by the
match_prog relation) preserves semantics by constructing
the following simulations:
-
Forward simulations from Cstrategy to Asm
(composition of the forward simulations for each pass).
-
Backward simulations for the same languages
(derived from the forward simulation, using receptiveness of the source
language and determinacy of Asm).
-
Backward simulation from Csem to Asm
(composition of two backward simulations).
:
forall {
RETVAL:
Type},
forall sem:
_ RETVAL,
forward_simulation sem sem.
Proof.
intros.
apply forward_simulation_step with (
fun s1 s2 =>
s2 =
s1);
intros.
-
auto.
-
exists s1;
auto.
-
subst s2;
auto.
-
subst s2.
exists s1';
auto.
Qed.
Lemma match_if_simulation:
forall {
RETVAL:
Type},
forall (
A:
Type) (
sem:
A ->
semantics RETVAL) (
flag:
unit ->
bool) (
transf:
A ->
A ->
Prop) (
prog tprog:
A),
match_if flag transf prog tprog ->
(
forall p tp,
transf p tp ->
forward_simulation (
sem p) (
sem tp)) ->
forward_simulation (
sem prog) (
sem tprog).
Proof.
Section WITHEXTERNALCALLS.
Local Existing Instance Events.symbols_inject_instance.
Local Existing Instance StackADT.inject_perm_all.
Context `{
external_calls_prf:
Events.ExternalCalls
(
symbols_inject_instance :=
Events.symbols_inject_instance) }.
Context {
i64_helpers_correct_prf:
SplitLongproof.I64HelpersCorrect mem}.
Context `{
memory_model_x_prf: !
Unusedglobproof.Mem.MemoryModelX mem}.
Definition fn_stack_requirements (
tp:
Asm.program) (
id:
ident) :
Z :=
match Globalenvs.Genv.find_symbol (
Globalenvs.Genv.globalenv tp)
id with
|
Some b =>
match Globalenvs.Genv.find_funct_ptr (
Globalenvs.Genv.globalenv tp)
b with
|
Some (
Internal f) =>
Asm.fn_stacksize f
|
_ => 0
end
|
None => 0
end.
Definition flat_fn_stack_requirements (
tp:
FlatAsm.program) (
id:
ident) :
Z :=
match List.find (
fun '(
id',
_,
_) =>
ident_eq id id') (
FlatAsmProgram.prog_defs tp)
with
|
None => 0
|
Some (
_,
def,
_) =>
match def with
|
Some (
Gfun (
Internal f)) =>
FlatAsmProgram.fn_stacksize f
|
_ => 0
end
end.
Definition mc_fn_stack_requirements (
tp:
MC.program) (
id:
ident) :
Z :=
match List.find (
fun '(
id',
_,
_) =>
ident_eq id id') (
FlatAsmProgram.prog_defs tp)
with
|
None => 0
|
Some (
_,
def,
_) =>
match def with
|
Some (
Gfun (
Internal f)) =>
FlatAsmProgram.fn_stacksize f
|
_ => 0
end
end.
Definition printable_oracle (
tp:
Asm.program) :
list (
ident *
Z) :=
fold_left (
fun acc gd =>
match gd with
(
id,
Some (
Gfun (
Internal f))) => (
id,
fn_stack_requirements tp id)::
acc
|
_ =>
acc
end) (
prog_defs tp)
nil.
Lemma match_program_no_more_functions:
forall {
F1 V1 F2 V2}
`{
Linker F1} `{
Linker V1}
Mf Mv
(
p1:
program F1 V1) (
p2:
program F2 V2),
match_program Mf Mv p1 p2 ->
forall b,
Globalenvs.Genv.find_funct_ptr (
Globalenvs.Genv.globalenv p1)
b =
None ->
Globalenvs.Genv.find_funct_ptr (
Globalenvs.Genv.globalenv p2)
b =
None.
Proof.
Lemma fn_stack_requirements_pos:
forall ps p i,
Asmgenproof.match_prog ps p ->
0 <=
fn_stack_requirements p i.
Proof.
Definition mk_init_stk {
F V} (
p:
AST.program F V) :
StackADT.stack :=
(
Some (
StackADT.make_singleton_frame_adt
(
Globalenvs.Genv.genv_next (
Globalenvs.Genv.globalenv p)) 0 0),
nil) ::
nil .
Definition mk_init_stk_flat {
I} (
p: @
FlatAsmProgram.program I) :
StackADT.stack :=
(
Some (
StackADT.make_singleton_frame_adt
(
FlatAsmGlobenv.Genv.genv_next (
FlatAsmProgram.globalenv p)) 0 0),
nil) ::
nil .
Theorem cstrategy_semantic_preservation:
forall p tp,
match_prog p tp ->
let init_stk :=
mk_init_stk tp in
forward_simulation (
Cstrategy.semantics (
fn_stack_requirements tp)
p) (
Asm.semantics tp init_stk)
/\
backward_simulation (
atomic (
Cstrategy.semantics (
fn_stack_requirements tp)
p)) (
Asm.semantics tp init_stk).
Proof.
Theorem cstrategy_semantic_preservation_raw:
forall p tp,
match_prog p tp ->
forall (
NORSP:
RawAsmproof.asm_prog_no_rsp (
Globalenvs.Genv.globalenv tp)),
forward_simulation (
Cstrategy.semantics (
fn_stack_requirements tp)
p) (
RawAsm.semantics tp (
Asm.Pregmap.init Values.Vundef))
/\
backward_simulation (
atomic (
Cstrategy.semantics (
fn_stack_requirements tp)
p)) (
RawAsm.semantics tp (
Asm.Pregmap.init Values.Vundef)).
Proof.
Theorem cstrategy_semantic_preservation_raw':
forall p tp,
match_prog p tp ->
forward_simulation (
Cstrategy.semantics (
fn_stack_requirements tp)
p) (
RawAsm.semantics tp (
Asm.Pregmap.init Values.Vundef))
/\
backward_simulation (
atomic (
Cstrategy.semantics (
fn_stack_requirements tp)
p)) (
RawAsm.semantics tp (
Asm.Pregmap.init Values.Vundef)).
Proof.
Theorem c_semantic_preservation:
forall p tp,
match_prog p tp ->
let init_stk :=
mk_init_stk tp in
backward_simulation (
Csem.semantics (
fn_stack_requirements tp)
p) (
Asm.semantics tp init_stk).
Proof.
Theorem c_semantic_preservation_raw:
forall p tp,
match_prog p tp ->
backward_simulation (
Csem.semantics (
fn_stack_requirements tp)
p) (
RawAsm.semantics tp (
Asm.Pregmap.init Values.Vundef)).
Proof.
Theorem c_semantic_preservation_real:
forall p tp,
match_prog_real p tp ->
backward_simulation (
Csem.semantics (
fn_stack_requirements tp)
p) (
RealAsm.semantics tp (
Asm.Pregmap.init Values.Vundef)).
Proof.
Lemma find_unique:
forall {
A B:
Type} (
l:
list (
ident *
A *
B))
i def sb
(
IN:
In (
i,
def,
sb)
l)
(
NPT:
list_norepet (
map (
fun '(
i,
_,
_) =>
i)
l)),
find (
fun '(
i',
_,
_) =>
ident_eq i i')
l =
Some (
i,
def,
sb).
Proof.
induction l;
simpl;
intros.
contradiction.
inv IN.
-
destruct peq;
try contradiction.
simpl.
auto.
-
destruct a.
destruct p.
inv NPT.
destruct (
ident_eq i i0).
subst.
generalize (
in_map (
fun '(
i,
_,
_) =>
i)
l (
i0,
def,
sb)
H).
congruence.
exploit IHl;
eauto.
Qed.
Lemma flat_fn_stack_requirements_match:
forall p tp
(
FM:
FlatAsmgenproof.match_prog p tp),
fn_stack_requirements p =
flat_fn_stack_requirements tp.
Proof.
Theorem c_semantic_preservation_flat:
forall p tp,
match_prog_flat p tp ->
backward_simulation (
Csem.semantics (
flat_fn_stack_requirements tp)
p) (
FlatAsm.semantics tp (
Asm.Pregmap.init Values.Vundef)).
Proof.
Lemma mc_fn_stack_requirements_match:
forall p tp
(
FM:
MCgenproof.match_prog p tp),
flat_fn_stack_requirements p =
mc_fn_stack_requirements tp.
Proof.
Lemma flatasmgen_update_maps_lmap_code:
forall defs g l d c g'
l'
d'
c',
FlatAsmgen.update_maps g l d c defs = (
g',
l',
d',
c') ->
(
forall i lb sb o,
l i lb =
Some (
sb,
o) ->
sb =
FlatAsmProgram.code_segid) ->
forall i lb sb o,
l'
i lb =
Some (
sb,
o) ->
sb =
FlatAsmProgram.code_segid.
Proof.
Lemma flatasmgen_make_maps_code:
forall p g l d c,
FlatAsmgen.make_maps p = (
g,
l,
d,
c) ->
forall i lb sb o,
l i lb =
Some (
sb,
o) ->
sb =
FlatAsmProgram.code_segid.
Proof.
Theorem c_semantic_preservation_mc:
forall p tp,
match_prog_mc p tp ->
backward_simulation (
Csem.semantics (
mc_fn_stack_requirements tp)
p) (
MC.semantics tp (
Asm.Pregmap.init Values.Vundef)).
Proof.
Correctness of the CompCert compiler
Combining the results above, we obtain semantic preservation for two
usage scenarios of CompCert: compilation of a single monolithic program,
and separate compilation of multiple source files followed by linking.
In the monolithic case, we have a whole C program p that is
compiled in one run of CompCert to a whole Asm program tp.
Then, tp preserves the semantics of p, in the sense that there
exists a backward simulation of the dynamic semantics of p
by the dynamic semantics of tp.
Theorem transf_c_program_correct:
forall p tp,
transf_c_program p =
OK tp ->
let init_stk :=
mk_init_stk tp in
backward_simulation (
Csem.semantics (
fn_stack_requirements tp)
p) (
Asm.semantics tp init_stk).
Proof.
Theorem transf_c_program_correct_raw:
forall p tp,
transf_c_program p =
OK tp ->
backward_simulation (
Csem.semantics (
fn_stack_requirements tp)
p) (
RawAsm.semantics tp (
Asm.Pregmap.init Values.Vundef)).
Proof.
Theorem transf_c_program_correct_real:
forall p tp,
transf_c_program_real p =
OK tp ->
backward_simulation (
Csem.semantics (
fn_stack_requirements tp)
p) (
RealAsm.semantics tp (
Asm.Pregmap.init Values.Vundef)).
Proof.
Theorem transf_c_program_correct_flat:
forall p tp,
transf_c_program_flatasm p =
OK tp ->
backward_simulation (
Csem.semantics (
flat_fn_stack_requirements tp)
p) (
FlatAsm.semantics tp (
Asm.Pregmap.init Values.Vundef)).
Proof.
Theorem transf_c_program_correct_mc:
forall p tp,
transf_c_program_mc p =
OK tp ->
backward_simulation (
Csem.semantics (
mc_fn_stack_requirements tp)
p) (
MC.semantics tp (
Asm.Pregmap.init Values.Vundef)).
Proof.
Here is the separate compilation case. Consider a nonempty list c_units
of C source files (compilation units), C1 ,,, Cn. Assume that every
C compilation unit Ci is successfully compiled by CompCert, obtaining
an Asm compilation unit Ai. Let asm_unit be the nonempty list
A1 ... An. Further assume that the C units C1 ... Cn can be linked
together to produce a whole C program c_program. Then, the generated
Asm units can be linked together, producing a whole Asm program
asm_program. Moreover, asm_program preserves the semantics of
c_program, in the sense that there exists a backward simulation of
the dynamic semantics of asm_program by the dynamic semantics of c_program.
Theorem separate_transf_c_program_correct:
forall c_units asm_units c_program,
nlist_forall2 (
fun cu tcu =>
transf_c_program cu =
OK tcu)
c_units asm_units ->
link_list c_units =
Some c_program ->
exists asm_program,
link_list asm_units =
Some asm_program
/\
let init_stk :=
mk_init_stk asm_program in
backward_simulation (
Csem.semantics (
fn_stack_requirements asm_program)
c_program) (
Asm.semantics asm_program init_stk).
Proof.
Theorem separate_transf_c_program_correct_raw:
forall c_units asm_units c_program,
nlist_forall2 (
fun cu tcu =>
transf_c_program cu =
OK tcu)
c_units asm_units ->
link_list c_units =
Some c_program ->
exists asm_program,
link_list asm_units =
Some asm_program
/\
let init_stk :=
mk_init_stk asm_program in
backward_simulation (
Csem.semantics (
fn_stack_requirements asm_program)
c_program) (
RawAsm.semantics asm_program
(
Asm.Pregmap.init Values.Vundef)
).
Proof.
Theorem separate_transf_c_program_correct_real:
forall c_units asm_units c_program,
nlist_forall2 (
fun cu tcu =>
transf_c_program_real cu =
OK tcu)
c_units asm_units ->
link_list c_units =
Some c_program ->
exists asm_program,
link_list asm_units =
Some asm_program
/\
let init_stk :=
mk_init_stk asm_program in
backward_simulation (
Csem.semantics (
fn_stack_requirements asm_program)
c_program) (
RealAsm.semantics asm_program
(
Asm.Pregmap.init Values.Vundef)
).
Proof.
Theorem separate_transf_c_program_correct_flat:
forall c_units asm_units c_program,
nlist_forall2 (
fun cu tcu =>
transf_c_program_flatasm cu =
OK tcu)
c_units asm_units ->
link_list c_units =
Some c_program ->
exists asm_program,
link_list asm_units =
Some asm_program
/\
let init_stk :=
mk_init_stk_flat asm_program in
backward_simulation (
Csem.semantics (
flat_fn_stack_requirements asm_program)
c_program) (
FlatAsm.semantics asm_program
(
Asm.Pregmap.init Values.Vundef)
).
Proof.
Theorem separate_transf_c_program_correct_mc:
forall c_units asm_units c_program,
nlist_forall2 (
fun cu tcu =>
transf_c_program_mc cu =
OK tcu)
c_units asm_units ->
link_list c_units =
Some c_program ->
exists asm_program,
link_list asm_units =
Some asm_program
/\
let init_stk :=
mk_init_stk_flat asm_program in
backward_simulation (
Csem.semantics (
mc_fn_stack_requirements asm_program)
c_program) (
MC.semantics asm_program
(
Asm.Pregmap.init Values.Vundef)
).
Proof.
End WITHEXTERNALCALLS.