diff options
Diffstat (limited to 'driver/Compiler.vexpand')
-rw-r--r-- | driver/Compiler.vexpand | 533 |
1 files changed, 533 insertions, 0 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand new file mode 100644 index 00000000..4c7c963a --- /dev/null +++ b/driver/Compiler.vexpand @@ -0,0 +1,533 @@ +(* *********************************************************************) +(* *) +(* 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 Tailcall. +Require Inlining. +Require Profiling. +Require ProfilingExploit. +Require FirstNop. +Require Renumber. +Require Duplicate. +Require Constprop. +Require LICM. +Require CSE. +Require ForwardMoves. +Require CSE2. +Require CSE3. +Require Deadcode. +Require Unusedglob. +Require Allnontrap. +Require Allocation. +Require Tunneling. +Require Linearize. +Require CleanupLabels. +Require Debugvar. +Require Stacking. +Require Asmgen. +(** Proofs of semantic preservation. *) +Require SimplExprproof. +Require SimplLocalsproof. +Require Cshmgenproof. +Require Cminorgenproof. +Require Selectionproof. +Require RTLgenproof. +Require Tailcallproof. +Require Inliningproof. +Require Profilingproof. +Require ProfilingExploitproof. +Require FirstNopproof. +Require Renumberproof. +Require Duplicateproof. +Require Constpropproof. +Require LICMproof. +Require CSEproof. +Require ForwardMovesproof. +Require CSE2proof. +Require CSE3proof. +Require Deadcodeproof. +Require Unusedglobproof. +Require Allnontrapproof. +Require Allocproof. +Require Tunnelingproof. +Require Linearizeproof. +Require CleanupLabelsproof. +Require Debugvarproof. +Require Stackingproof. +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: 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_TRANSF_PROGRAM + @@@ 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 "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. + +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 Inliningproof.match_prog + ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) + ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) + ::: mkpass Renumberproof.match_prog + ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) + ::: mkpass Renumberproof.match_prog + ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) + ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) + ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) + ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.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). + +(** 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. simpl in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. + unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. + unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. + unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. + destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. + set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. + set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. + set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *. + set (p9bis := Renumber.transf_program p9) in *. + destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := Renumber.transf_program p10) in *. + set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. + destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. + set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. + destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. + set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. + destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. + set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. + destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. + destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + set (p17 := Tunneling.tunnel_program p16) in *. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + set (p19 := CleanupLabels.transf_program p18) in *. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. + 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. + exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. + exists p8; split. apply Inliningproof.transf_program_match; auto. + exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. + exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. + exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. + exists p9bis; split. apply Renumberproof.transf_program_match. + exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. + exists p11; split. apply Renumberproof.transf_program_match. + exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. + exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. + exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. + exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. + exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. + exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. + exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. + exists p15; split. apply Unusedglobproof.transf_program_match; auto. + exists p16; split. apply Allocproof.transf_program_match; auto. + exists p17; split. apply Tunnelingproof.transf_program_match. + exists p18; split. apply Linearizeproof.transf_program_match; auto. + exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. + exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. + exists p21; split. apply Stackingproof.transf_program_match; auto. + 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) (Asm.semantics p31)). + { + 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. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. + eapply compose_forward_simulations. + eapply Inliningproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. + eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. + eapply compose_forward_simulations. + eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. + eapply compose_forward_simulations. + eapply Unusedglobproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Allocproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Tunnelingproof.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. |