diff options
Diffstat (limited to 'driver/Compiler.vexpand')
| -rw-r--r-- | driver/Compiler.vexpand | 391 |
1 files changed, 391 insertions, 0 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand new file mode 100644 index 00000000..7503d3ed --- /dev/null +++ b/driver/Compiler.vexpand @@ -0,0 +1,391 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** 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. +(** Translation passes. *) +Require Initializers. +Require SimplExpr. +Require SimplLocals. +Require Cshmgen. +Require Cminorgen. +Require Selection. +Require RTLgen. +Require Import Duplicatepasses. +EXPAND_RTL_REQUIRE +Require Asmgen. +(** Proofs of semantic preservation. *) +Require SimplExprproof. +Require SimplLocalsproof. +Require Cshmgenproof. +Require Cminorgenproof. +Require Selectionproof. +Require RTLgenproof. +EXPAND_RTL_REQUIRE_PROOF +Require Import Asmgenproof. +(** 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: Z -> 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. *) + +Definition transf_rtl_program (f: RTL.program) : res Asm.program := + OK f + @@ print (print_RTL 0) +EXPAND_RTL_TRANSF_PROGRAM + @@@ time "Total Mach->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_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. + +(** Force [Initializers] and [Cexec] to be extracted as well. *) + +Definition transl_init := Initializers.transl_init. +Definition cexec_do_step := Cexec.do_step. + +(** 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. + intros. destruct x; simpl. rewrite print_identity. auto. auto. +Qed. + +(** * 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. + intros. unfold match_if, total_if. destruct (flag tt); auto. +Qed. + +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. + intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence. +Qed. + +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. + +(** 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 +EXPAND_RTL_MKPASS + ::: 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). + +(** 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. + intros p tp T. + unfold transf_c_program, time in T. cbn in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; cbn in T; try discriminate. + unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; cbn in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; cbn in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; cbn in T; try discriminate. + unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; cbn in T; try discriminate. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; cbn in T; try discriminate. + unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. + cbn in T. +EXPAND_RTL_PROOF + unfold match_prog; simpl. + exists p1; split. apply SimplExprproof.transf_program_match; auto. + exists p2; split. apply SimplLocalsproof.match_transf_program; auto. + exists p3; split. apply Cshmgenproof.transf_program_match; auto. + exists p4; split. apply Cminorgenproof.transf_program_match; auto. + exists p5; split. apply Selectionproof.transf_program_match; auto. + exists p6; split. apply RTLgenproof.transf_program_match; auto. +EXPAND_RTL_PROOF2 + exists tp; split. apply Asmgenproof.transf_program_match; auto. + reflexivity. +Qed. + +(** * 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). +*) + +Remark forward_simulation_identity: + forall sem, 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 (A: Type) (sem: A -> semantics) (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. + intros. unfold match_if in *. destruct (flag tt). eauto. subst. apply forward_simulation_identity. +Qed. + +Theorem cstrategy_semantic_preservation: + forall p tp, + match_prog p tp -> + forward_simulation (Cstrategy.semantics p) (Asm.semantics tp) + /\ backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp). +Proof. + intros p tp M. unfold match_prog, pass_match in M; simpl in M. +Ltac DestructM := + match goal with + [ H: exists p, _ /\ _ |- _ ] => + let p := fresh "p" in let M := fresh "M" in let MM := fresh "MM" in + destruct H as (p & M & MM); clear H + end. + repeat DestructM. subst tp. + assert (F: forward_simulation (Cstrategy.semantics p) +EXPAND_ASM_SEMANTICS + ). + { + eapply compose_forward_simulations. + eapply SimplExprproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply SimplLocalsproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Cshmgenproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Cminorgenproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Selectionproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLgenproof.transf_program_correct; eassumption. +EXPAND_RTL_FORWARD_SIMULATIONS + eapply compose_forward_simulations. + eapply RTLtoBTLproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply BTL_Schedulerproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply BTLtoRTLproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Allocationproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply LTLTunnelingproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Linearizeproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply CleanupLabelsproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Debugvarproof.transf_program_correct. + eapply compose_forward_simulations. + eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof0.return_address_offset). + exact Asmgenproof.return_address_exists. + eassumption. + eapply Asmgenproof.transf_program_correct; eassumption. + } + split. auto. + apply forward_to_backward_simulation. + apply factor_forward_simulation. auto. eapply sd_traces. eapply Asm.semantics_determinate. + apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive. + apply Asm.semantics_determinate. +Qed. + +Theorem c_semantic_preservation: + forall p tp, + match_prog p tp -> + backward_simulation (Csem.semantics p) (Asm.semantics tp). +Proof. + intros. + apply compose_backward_simulation with (atomic (Cstrategy.semantics p)). + eapply sd_traces; eapply Asm.semantics_determinate. + apply factor_backward_simulation. + apply Cstrategy.strategy_simulation. + apply Csem.semantics_single_events. + eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive. + exact (proj2 (cstrategy_semantic_preservation _ _ H)). +Qed. + +(** * 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 -> + backward_simulation (Csem.semantics p) (Asm.semantics tp). +Proof. + intros. apply c_semantic_preservation. apply transf_c_program_match; auto. +Qed. + +(** 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 + /\ backward_simulation (Csem.semantics c_program) (Asm.semantics asm_program). +Proof. + intros. + assert (nlist_forall2 match_prog c_units asm_units). + { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_c_program_match; auto. } + assert (exists asm_program, link_list asm_units = Some asm_program /\ match_prog c_program asm_program). + { eapply link_list_compose_passes; eauto. } + destruct H2 as (asm_program & P & Q). + exists asm_program; split; auto. apply c_semantic_preservation; auto. +Qed. |