From 862e6d00d0ee5d3a534ab111790d19823a73efa2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:34:58 +0100 Subject: Strengthen the main compiler correctness results to account for separate compilation and linking Define a "match_prog" relation corresponding to the composition of CompCert's passes. Use it to show semantic preservation (backward/forward simulations) not just for the compilation of whole programs, but also for the separate compilation of multiple units followed by linking. --- driver/Compiler.v | 399 ++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 250 insertions(+), 149 deletions(-) (limited to 'driver/Compiler.v') diff --git a/driver/Compiler.v b/driver/Compiler.v index ea5849ec..dd752aca 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -14,15 +14,10 @@ (** Libraries. *) Require Import String. -Require Import Coqlib. -Require Import Errors. -Require Import AST. -Require Import Smallstep. +Require Import Coqlib Errors. +Require Import AST Linking Smallstep. (** Languages (syntax and semantics). *) -Require Csyntax. -Require Csem. -Require Cstrategy. -Require Cexec. +Require Ctypes Csyntax Csem Cstrategy Cexec. Require Clight. Require Csharpminor. Require Cminor. @@ -192,171 +187,228 @@ Proof. intros. destruct x; simpl. rewrite print_identity. auto. auto. Qed. -Remark forward_simulation_identity: - forall sem, forward_simulation sem sem. +(** * 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. apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros. -- auto. -- exists s1; auto. -- subst s2; auto. -- subst s2. exists s1'; auto. + intros. unfold match_if, total_if. destruct (flag tt); auto. Qed. -Lemma total_if_simulation: - forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> A) (prog: A), - (forall p, forward_simulation (sem p) (sem (f p))) -> - forward_simulation (sem prog) (sem (total_if flag f prog)). +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 total_if. destruct (flag tt). auto. apply forward_simulation_identity. + intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence. Qed. -Lemma partial_if_simulation: - forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> res A) (prog tprog: A), - partial_if flag f prog = OK tprog -> - (forall p tp, f p = OK tp -> forward_simulation (sem p) (sem tp)) -> - forward_simulation (sem prog) (sem tprog). +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 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). + +(** 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. unfold partial_if in *. destruct (flag tt). eauto. inv H. apply forward_simulation_identity. + 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 (p9 := Renumber.transf_program p8) in *. + set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. + set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. + destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. + destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. + set (p16 := Tunneling.tunnel_program p15) in *. + destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. + set (p18 := CleanupLabels.transf_program p17) in *. + destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate. + destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; 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 p9; split. apply Renumberproof.transf_program_match; auto. + exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. + exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. + exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p14; split. apply Unusedglobproof.transf_program_match; auto. + exists p15; split. apply Allocproof.transf_program_match; auto. + exists p16; split. apply Tunnelingproof.transf_program_match. + exists p17; split. apply Linearizeproof.transf_program_match; auto. + exists p18; split. apply CleanupLabelsproof.transf_program_match; auto. + exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. + exists p20; split. apply Stackingproof.transf_program_match; auto. + exists tp; split. apply Asmgenproof.transf_program_match; auto. + reflexivity. Qed. (** * Semantic preservation *) -(** We prove that the [transf_program] translations preserve semantics - by constructing the following simulations: -- Forward simulations from [Cstrategy] / [Cminor] / [RTL] to [Asm] +(** 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). +*) -These results establish the correctness of the whole compiler! *) - -Theorem transf_rtl_program_correct: - forall p tp, - transf_rtl_program p = OK tp -> - forward_simulation (RTL.semantics p) (Asm.semantics tp) - * backward_simulation (RTL.semantics p) (Asm.semantics tp). -Proof. - intros. - assert (F: forward_simulation (RTL.semantics p) (Asm.semantics tp)). - unfold transf_rtl_program, time in H. - repeat rewrite compose_print_identity in H. - simpl in H. - set (p1 := total_if optim_tailcalls Tailcall.transf_program p) in *. - destruct (Inlining.transf_program p1) as [p11|] eqn:?; simpl in H; try discriminate. - set (p12 := Renumber.transf_program p11) in *. - set (p2 := total_if optim_constprop Constprop.transf_program p12) in *. - set (p21 := total_if optim_constprop Renumber.transf_program p2) in *. - destruct (partial_if optim_CSE CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p3) as [p31|] eqn:?; simpl in H; try discriminate. - destruct (Unusedglob.transform_program p31) as [p32|] eqn:?; simpl in H; try discriminate. - destruct (Allocation.transf_program p32) as [p4|] eqn:?; simpl in H; try discriminate. - set (p5 := Tunneling.tunnel_program p4) in *. - destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate. - set (p7 := CleanupLabels.transf_program p6) in *. - destruct (partial_if debug Debugvar.transf_program p7) as [p71|] eqn:?; simpl in H; try discriminate. - destruct (Stacking.transf_program p71) as [p8|] eqn:?; simpl in H; try discriminate. - apply compose_forward_simulation with (RTL.semantics p1). - apply total_if_simulation. apply Tailcallproof.transf_program_correct. - apply compose_forward_simulation with (RTL.semantics p11). - apply Inliningproof.transf_program_correct; auto. - apply compose_forward_simulation with (RTL.semantics p12). - apply Renumberproof.transf_program_correct. - apply compose_forward_simulation with (RTL.semantics p2). - apply total_if_simulation. apply Constpropproof.transf_program_correct. - apply compose_forward_simulation with (RTL.semantics p21). - apply total_if_simulation. apply Renumberproof.transf_program_correct. - apply compose_forward_simulation with (RTL.semantics p3). - eapply partial_if_simulation; eauto. apply CSEproof.transf_program_correct. - apply compose_forward_simulation with (RTL.semantics p31). - eapply partial_if_simulation; eauto. apply Deadcodeproof.transf_program_correct. - apply compose_forward_simulation with (RTL.semantics p32). - apply Unusedglobproof.transf_program_correct; auto. - apply compose_forward_simulation with (LTL.semantics p4). - apply Allocproof.transf_program_correct; auto. - apply compose_forward_simulation with (LTL.semantics p5). - apply Tunnelingproof.transf_program_correct. - apply compose_forward_simulation with (Linear.semantics p6). - apply Linearizeproof.transf_program_correct; auto. - apply compose_forward_simulation with (Linear.semantics p7). - apply CleanupLabelsproof.transf_program_correct. - apply compose_forward_simulation with (Linear.semantics p71). - eapply partial_if_simulation; eauto. apply Debugvarproof.transf_program_correct. - apply compose_forward_simulation with (Mach.semantics Asmgenproof0.return_address_offset p8). - apply Stackingproof.transf_program_correct. - exact Asmgenproof.return_address_exists. - auto. - apply Asmgenproof.transf_program_correct; eauto. - split. auto. - apply forward_to_backward_simulation. auto. - apply RTL.semantics_receptive. - apply Asm.semantics_determinate. -Qed. - -Theorem transf_cminor_program_correct: - forall p tp, - transf_cminor_program p = OK tp -> - forward_simulation (Cminor.semantics p) (Asm.semantics tp) - * backward_simulation (Cminor.semantics p) (Asm.semantics tp). +Remark forward_simulation_identity: + forall sem, forward_simulation sem sem. Proof. - intros. - assert (F: forward_simulation (Cminor.semantics p) (Asm.semantics tp)). - unfold transf_cminor_program, time in H. - repeat rewrite compose_print_identity in H. - simpl in H. - destruct (Selection.sel_program p) as [p1|] eqn:?; simpl in H; try discriminate. - destruct (RTLgen.transl_program p1) as [p2|] eqn:?; simpl in H; try discriminate. - eapply compose_forward_simulation. apply Selectionproof.transf_program_correct. eauto. - eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption. - exact (fst (transf_rtl_program_correct _ _ H)). - - split. auto. - apply forward_to_backward_simulation. auto. - apply Cminor.semantics_receptive. - apply Asm.semantics_determinate. + 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. -Theorem transf_clight_program_correct: - forall p tp, - transf_clight_program p = OK tp -> - forward_simulation (Clight.semantics1 p) (Asm.semantics tp) - * backward_simulation (Clight.semantics1 p) (Asm.semantics tp). +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. - assert (F: forward_simulation (Clight.semantics1 p) (Asm.semantics tp)). - revert H; unfold transf_clight_program, time; simpl. - rewrite print_identity. - caseEq (SimplLocals.transf_program p); simpl; try congruence; intros p0 EQ0. - caseEq (Cshmgen.transl_program p0); simpl; try congruence; intros p1 EQ1. - caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. - intros EQ3. - eapply compose_forward_simulation. apply SimplLocalsproof.transf_program_correct. eauto. - eapply compose_forward_simulation. apply Cshmgenproof.transl_program_correct. eauto. - eapply compose_forward_simulation. apply Cminorgenproof.transl_program_correct. eauto. - exact (fst (transf_cminor_program_correct _ _ EQ3)). - - split. auto. - apply forward_to_backward_simulation. auto. - apply Clight.semantics_receptive. - apply Asm.semantics_determinate. + intros. unfold match_if in *. destruct (flag tt). eauto. subst. apply forward_simulation_identity. Qed. -Theorem transf_cstrategy_program_correct: +Theorem cstrategy_semantic_preservation: forall p tp, - transf_c_program p = OK tp -> + match_prog p tp -> forward_simulation (Cstrategy.semantics p) (Asm.semantics tp) - * backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp). + /\ backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp). Proof. - intros. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)). - revert H; unfold transf_c_program, time; simpl. - caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0. - intros EQ1. - eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto. - exact (fst (transf_clight_program_correct _ _ EQ1)). - + 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 p21)). + { + 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 Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. + 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 Deadcodeproof.transf_program_correct; eassumption. + 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. @@ -364,9 +416,9 @@ Proof. apply Asm.semantics_determinate. Qed. -Theorem transf_c_program_correct: +Theorem c_semantic_preservation: forall p tp, - transf_c_program p = OK tp -> + match_prog p tp -> backward_simulation (Csem.semantics p) (Asm.semantics tp). Proof. intros. @@ -376,5 +428,54 @@ Proof. apply Cstrategy.strategy_simulation. apply Csem.semantics_single_events. eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive. - exact (snd (transf_cstrategy_program_correct _ _ H)). + 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. -- cgit