diff options
Diffstat (limited to 'backend/Main.v')
| -rw-r--r-- | backend/Main.v | 307 |
1 files changed, 307 insertions, 0 deletions
diff --git a/backend/Main.v b/backend/Main.v new file mode 100644 index 0000000..6647e26 --- /dev/null +++ b/backend/Main.v @@ -0,0 +1,307 @@ +(** The compiler back-end and its proof of semantic preservation *) + +(** Libraries. *) +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Values. +(** Languages (syntax and semantics). *) +Require Csharpminor. +Require Cminor. +Require RTL. +Require LTL. +Require Linear. +Require Mach. +Require PPC. +(** Translation passes. *) +Require Cminorgen. +Require RTLgen. +Require Constprop. +Require CSE. +Require Allocation. +Require Tunneling. +Require Linearize. +Require Stacking. +Require PPCgen. +(** Type systems. *) +Require RTLtyping. +Require LTLtyping. +Require Lineartyping. +Require Machtyping. +(** Proofs of semantic preservation and typing preservation. *) +Require Cminorgenproof. +Require RTLgenproof. +Require Constpropproof. +Require CSEproof. +Require Allocproof. +Require Alloctyping. +Require Tunnelingproof. +Require Tunnelingtyping. +Require Linearizeproof. +Require Linearizetyping. +Require Stackingproof. +Require Stackingtyping. +Require Machabstr2mach. +Require PPCgenproof. + +(** * Composing the translation passes *) + +(** We first define useful monadic composition operators, + along with funny (but convenient) notations. *) + +Definition apply_total (A B: Set) (x: option A) (f: A -> B) : option B := + match x with None => None | Some x1 => Some (f x1) end. + +Definition apply_partial (A B: Set) + (x: option A) (f: A -> option B) : option B := + match x with None => None | Some 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). + +(** We define two translation functions for whole programs: one starting with + a Csharpminor program, the other with a Cminor program. Both + translations produce PPC programs ready for pretty-printing and + assembling. Some front-ends will prefer to generate Csharpminor + (e.g. a C front-end) while some others (e.g. an ML compiler) might + find it more convenient to generate Cminor directly, bypassing + Csharpminor. + + There are two ways to compose the compiler passes. The first translates + every function from the Cminor program from Cminor to RTL, then to LTL, etc, + all the way to PPC, and iterates this transformation for every function. + The second translates the whole Cminor program to a RTL program, then to + an LTL program, etc. We follow the first approach because it has lower + memory requirements. + + The translation of a Cminor function to a PPC function is as follows. *) + +Definition transf_cminor_function (f: Cminor.function) : option PPC.code := + Some f + @@@ RTLgen.transl_function + @@ Constprop.transf_function + @@ CSE.transf_function + @@@ Allocation.transf_function + @@ Tunneling.tunnel_function + @@ Linearize.transf_function + @@@ Stacking.transf_function + @@@ PPCgen.transf_function. + +(** And here is the translation for Csharpminor functions. *) + +Definition transf_csharpminor_function (f: Csharpminor.function) : option PPC.code := + Some f + @@@ Cminorgen.transl_function + @@@ transf_cminor_function. + +(** The corresponding translations for whole program follow. *) + +Definition transf_cminor_program (p: Cminor.program) : option PPC.program := + transform_partial_program transf_cminor_function p. + +Definition transf_csharpminor_program (p: Csharpminor.program) : option PPC.program := + transform_partial_program transf_csharpminor_function p. + +(** * Equivalence with whole program transformations *) + +(** To prove semantic preservation for the whole compiler, it is easier to reason + over the second way to compose the compiler pass: the one that translate + whole programs through each compiler pass. We now define this second translation + and prove that it produces the same PPC programs as the first translation. *) + +Definition transf_cminor_program2 (p: Cminor.program) : option PPC.program := + Some p + @@@ RTLgen.transl_program + @@ Constprop.transf_program + @@ CSE.transf_program + @@@ Allocation.transf_program + @@ Tunneling.tunnel_program + @@ Linearize.transf_program + @@@ Stacking.transf_program + @@@ PPCgen.transf_program. + +Definition transf_csharpminor_program2 (p: Csharpminor.program) : option PPC.program := + Some p + @@@ Cminorgen.transl_program + @@@ transf_cminor_program2. + +Lemma transf_partial_program_compose: + forall (A B C: Set) + (f1: A -> option B) (f2: B -> option C) + (p: list (ident * A)), + transf_partial_program f1 p @@@ transf_partial_program f2 = + transf_partial_program (fun f => f1 f @@@ f2) p. +Proof. + induction p. simpl. auto. + simpl. destruct a. destruct (f1 a). + simpl. simpl in IHp. destruct (transf_partial_program f1 p). + simpl. simpl in IHp. destruct (f2 b). + destruct (transf_partial_program f2 l). + rewrite <- IHp. auto. + rewrite <- IHp. auto. + auto. + simpl. rewrite <- IHp. simpl. destruct (f2 b); auto. + simpl. auto. +Qed. + +Lemma transform_partial_program_compose: + forall (A B C: Set) + (f1: A -> option B) (f2: B -> option C) + (p: program A), + transform_partial_program f1 p @@@ + (fun p' => transform_partial_program f2 p') = + transform_partial_program (fun f => f1 f @@@ f2) p. +Proof. + unfold transform_partial_program; intros. + rewrite <- transf_partial_program_compose. simpl. + destruct (transf_partial_program f1 (prog_funct p)); simpl. + auto. auto. +Qed. + +Lemma transf_program_partial_total: + forall (A B: Set) (f: A -> B) (l: list (ident * A)), + Some (AST.transf_program f l) = + AST.transf_partial_program (fun x => Some (f x)) l. +Proof. + induction l. simpl. auto. + simpl. destruct a. rewrite <- IHl. auto. +Qed. + +Lemma transform_program_partial_total: + forall (A B: Set) (f: A -> B) (p: program A), + Some (transform_program f p) = + transform_partial_program (fun x => Some (f x)) p. +Proof. + intros. unfold transform_program, transform_partial_program. + rewrite <- transf_program_partial_total. auto. +Qed. + +Lemma apply_total_transf_program: + forall (A B: Set) (f: A -> B) (x: option (program A)), + x @@ (fun p => transform_program f p) = + x @@@ (fun p => transform_partial_program (fun x => Some (f x)) p). +Proof. + intros. unfold apply_total, apply_partial. + destruct x. apply transform_program_partial_total. auto. +Qed. + +Lemma transf_cminor_program_equiv: + forall p, transf_cminor_program2 p = transf_cminor_program p. +Proof. + intro. unfold transf_cminor_program, transf_cminor_program2, transf_cminor_function. + simpl. + unfold RTLgen.transl_program, + Constprop.transf_program, RTL.program. + rewrite apply_total_transf_program. + rewrite transform_partial_program_compose. + unfold CSE.transf_program, RTL.program. + rewrite apply_total_transf_program. + rewrite transform_partial_program_compose. + unfold Allocation.transf_program, + LTL.program, RTL.program. + rewrite transform_partial_program_compose. + unfold Tunneling.tunnel_program, LTL.program. + rewrite apply_total_transf_program. + rewrite transform_partial_program_compose. + unfold Linearize.transf_program, LTL.program, Linear.program. + rewrite apply_total_transf_program. + rewrite transform_partial_program_compose. + unfold Stacking.transf_program, Linear.program, Mach.program. + rewrite transform_partial_program_compose. + unfold PPCgen.transf_program, Mach.program, PPC.program. + rewrite transform_partial_program_compose. + reflexivity. +Qed. + +Lemma transf_csharpminor_program_equiv: + forall p, transf_csharpminor_program2 p = transf_csharpminor_program p. +Proof. + intros. + unfold transf_csharpminor_program2, transf_csharpminor_program, transf_csharpminor_function. + simpl. + replace transf_cminor_program2 with transf_cminor_program. + unfold transf_cminor_program, Cminorgen.transl_program, Cminor.program, PPC.program. + apply transform_partial_program_compose. + symmetry. apply extensionality. exact transf_cminor_program_equiv. +Qed. + +(** * Semantic preservation *) + +(** We prove that the [transf_program2] translations preserve semantics. The proof + composes the semantic preservation results for each pass. *) + +Lemma transf_cminor_program2_correct: + forall p tp n, + transf_cminor_program2 p = Some tp -> + Cminor.exec_program p (Vint n) -> + PPC.exec_program tp (Vint n). +Proof. + intros until n. + unfold transf_cminor_program2. + simpl. caseEq (RTLgen.transl_program p). intros p1 EQ1. + simpl. set (p2 := CSE.transf_program (Constprop.transf_program p1)). + caseEq (Allocation.transf_program p2). intros p3 EQ3. + simpl. set (p4 := Tunneling.tunnel_program p3). + set (p5 := Linearize.transf_program p4). + caseEq (Stacking.transf_program p5). intros p6 EQ6. + simpl. intros EQTP EXEC. + assert (WT3 : LTLtyping.wt_program p3). + apply Alloctyping.program_typing_preserved with p2. auto. + assert (WT4 : LTLtyping.wt_program p4). + unfold p4. apply Tunnelingtyping.program_typing_preserved. auto. + assert (WT5 : Lineartyping.wt_program p5). + unfold p5. apply Linearizetyping.program_typing_preserved. auto. + assert (WT6: Machtyping.wt_program p6). + apply Stackingtyping.program_typing_preserved with p5. auto. auto. + apply PPCgenproof.transf_program_correct with p6; auto. + apply Machabstr2mach.exec_program_equiv; auto. + apply Stackingproof.transl_program_correct with p5; auto. + unfold p5; apply Linearizeproof.transf_program_correct. + unfold p4; apply Tunnelingproof.transf_program_correct. + apply Allocproof.transl_program_correct with p2; auto. + unfold p2; apply CSEproof.transf_program_correct; + apply Constpropproof.transf_program_correct. + apply RTLgenproof.transl_program_correct with p; auto. + simpl; intros; discriminate. + simpl; intros; discriminate. + simpl; intros; discriminate. +Qed. + +Lemma transf_csharpminor_program2_correct: + forall p tp n, + transf_csharpminor_program2 p = Some tp -> + Csharpminor.exec_program p (Vint n) -> + PPC.exec_program tp (Vint n). +Proof. + intros until n; unfold transf_csharpminor_program2; simpl. + caseEq (Cminorgen.transl_program p). + simpl; intros p1 EQ1 EQ2 EXEC. + apply transf_cminor_program2_correct with p1. auto. + apply Cminorgenproof.transl_program_correct with p. auto. + assumption. + simpl; intros; discriminate. +Qed. + +(** It follows that the whole compiler is semantic-preserving. *) + +Theorem transf_cminor_program_correct: + forall p tp n, + transf_cminor_program p = Some tp -> + Cminor.exec_program p (Vint n) -> + PPC.exec_program tp (Vint n). +Proof. + intros. apply transf_cminor_program2_correct with p. + rewrite transf_cminor_program_equiv. assumption. assumption. +Qed. + +Theorem transf_csharpminor_program_correct: + forall p tp n, + transf_csharpminor_program p = Some tp -> + Csharpminor.exec_program p (Vint n) -> + PPC.exec_program tp (Vint n). +Proof. + intros. apply transf_csharpminor_program2_correct with p. + rewrite transf_csharpminor_program_equiv. assumption. assumption. +Qed. |