diff options
Diffstat (limited to 'common/Main.v')
| -rw-r--r-- | common/Main.v | 174 |
1 files changed, 90 insertions, 84 deletions
diff --git a/common/Main.v b/common/Main.v index 95dc4e6c..f472ec3a 100644 --- a/common/Main.v +++ b/common/Main.v @@ -6,6 +6,8 @@ Require Import Maps. Require Import AST. Require Import Values. (** Languages (syntax and semantics). *) +Require Csyntax. +Require Csem. Require Csharpminor. Require Cminor. Require RTL. @@ -14,6 +16,7 @@ Require Linear. Require Mach. Require PPC. (** Translation passes. *) +Require Cshmgen. Require Cminorgen. Require RTLgen. Require Constprop. @@ -24,11 +27,13 @@ Require Linearize. Require Stacking. Require PPCgen. (** Type systems. *) +Require Ctyping. Require RTLtyping. Require LTLtyping. Require Lineartyping. Require Machtyping. (** Proofs of semantic preservation and typing preservation. *) +Require Cshmgenproof3. Require Cminorgenproof. Require RTLgenproof. Require Constpropproof. @@ -62,12 +67,9 @@ 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 + a C 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. + assembling. 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, @@ -89,24 +91,20 @@ Definition transf_cminor_fundef (f: Cminor.fundef) : option PPC.fundef := @@@ Stacking.transf_fundef @@@ PPCgen.transf_fundef. -(** And here is the translation for Csharpminor functions. *) - -Definition transf_csharpminor_fundef - (gce: Cminorgen.compilenv) (f: Csharpminor.fundef) : option PPC.fundef := - Some f - @@@ Cminorgen.transl_fundef gce - @@@ transf_cminor_fundef. - (** The corresponding translations for whole program follow. *) Definition transf_cminor_program (p: Cminor.program) : option PPC.program := transform_partial_program transf_cminor_fundef p. -Definition transf_csharpminor_program (p: Csharpminor.program) : option PPC.program := - let gce := Cminorgen.build_global_compilenv p in - transform_partial_program - (transf_csharpminor_fundef gce) - (Csharpminor.program_of_program p). +Definition transf_c_program (p: Csyntax.program) : option PPC.program := + match Ctyping.typecheck_program p with + | false => None + | true => + Some p + @@@ Cshmgen.transl_program + @@@ Cminorgen.transl_program + @@@ transf_cminor_program + end. (** * Equivalence with whole program transformations *) @@ -126,23 +124,18 @@ Definition transf_cminor_program2 (p: Cminor.program) : option PPC.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) +Lemma map_partial_compose: + forall (X 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. + (p: list (X * A)), + map_partial f1 p @@@ map_partial f2 = + map_partial (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 (map_partial f1 p). simpl. simpl in IHp. destruct (f2 b). - destruct (transf_partial_program f2 l). + destruct (map_partial f2 l). rewrite <- IHp. auto. rewrite <- IHp. auto. auto. @@ -150,40 +143,67 @@ Proof. simpl. auto. Qed. +(* +Lemma transform_partial_program2_compose: + forall (A B C V W X: Set) + (f1: A -> option B) (g1: V -> option W) + (f2: B -> option C) (g2: W -> option X) + (p: program A V), + transform_partial_program2 f1 g1 p @@@ + (fun p' => transform_partial_program2 f2 g2 p') = + transform_partial_program2 (fun x => f1 x @@@ f2) (fun x => g1 x @@@ g2) p. +Proof. + unfold transform_partial_program2; intros. + rewrite <- map_partial_compose; simpl. + rewrite <- map_partial_compose; simpl. + destruct (map_partial f1 (prog_funct p)); simpl; auto. + destruct (map_partial g1 (prog_vars p)); simpl; auto. + destruct (map_partial f2 l); auto. +Qed. + +Lemma transform_program_partial2_partial: + forall (A B V: Set) (f: A -> option B) (p: program A V), + transform_partial_program f p = + transform_partial_program2 f (fun x => Some x) p. +Proof. + intros. unfold transform_partial_program, transform_partial_program2. + rewrite map_partial_identity. auto. +Qed. + +Lemma apply_partial_transf_program: + forall (A B V: Set) (f: A -> option B) (x: option (program A V)), + x @@@ (fun p => transform_partial_program f p) = + x @@@ (fun p => transform_partial_program2 f (fun x => Some x) p). +Proof. + intros. unfold apply_partial. + destruct x. apply transform_program_partial2_partial. auto. +Qed. +*) Lemma transform_partial_program_compose: - forall (A B C: Set) + forall (A B C V: Set) (f1: A -> option B) (f2: B -> option C) - (p: program A), + (p: program A V), transform_partial_program f1 p @@@ - (fun p' => transform_partial_program f2 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. + rewrite <- map_partial_compose. simpl. + destruct (map_partial 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), + forall (A B V: Set) (f: A -> B) (p: program A V), 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. + rewrite map_partial_total. auto. Qed. Lemma apply_total_transf_program: - forall (A B: Set) (f: A -> B) (x: option (program A)), + forall (A B V: Set) (f: A -> B) (x: option (program A V)), x @@ (fun p => transform_program f p) = x @@@ (fun p => transform_partial_program (fun x => Some (f x)) p). Proof. @@ -219,6 +239,7 @@ Proof. reflexivity. Qed. +(* Lemma transf_csharpminor_program_equiv: forall p, transf_csharpminor_program2 p = transf_csharpminor_program p. Proof. @@ -227,22 +248,27 @@ Proof. 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. + rewrite apply_partial_transf_program. + rewrite transform_partial_program2_compose. + reflexivity. 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. *) +(** We prove that the [transf_program] translations preserve semantics. The proof + composes the semantic preservation results for each pass. + This establishes the correctness of the whole compiler! *) -Lemma transf_cminor_program2_correct: +Theorem transf_cminor_program_correct: forall p tp t n, - transf_cminor_program2 p = Some tp -> + transf_cminor_program p = Some tp -> Cminor.exec_program p t (Vint n) -> PPC.exec_program tp t (Vint n). Proof. intros until n. + rewrite <- transf_cminor_program_equiv. unfold transf_cminor_program2. simpl. caseEq (RTLgen.transl_program p). intros p1 EQ1. simpl. set (p2 := CSE.transf_program (Constprop.transf_program p1)). @@ -273,39 +299,19 @@ Proof. simpl; intros; discriminate. Qed. -Lemma transf_csharpminor_program2_correct: - forall p tp t n, - transf_csharpminor_program2 p = Some tp -> - Csharpminor.exec_program p t (Vint n) -> - PPC.exec_program tp t (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 t n, - transf_cminor_program p = Some tp -> - Cminor.exec_program p t (Vint n) -> - PPC.exec_program tp t (Vint n). -Proof. - intros. apply transf_cminor_program2_correct with p. - rewrite transf_cminor_program_equiv. assumption. assumption. -Qed. - -Theorem transf_csharpminor_program_correct: +Theorem transf_c_program_correct: forall p tp t n, - transf_csharpminor_program p = Some tp -> - Csharpminor.exec_program p t (Vint n) -> + transf_c_program p = Some tp -> + Csem.exec_program p t (Vint n) -> PPC.exec_program tp t (Vint n). Proof. - intros. apply transf_csharpminor_program2_correct with p. - rewrite transf_csharpminor_program_equiv. assumption. assumption. + intros until n; unfold transf_c_program; simpl. + caseEq (Ctyping.typecheck_program p); try congruence; intro. + caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1. + caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. + intros EQ3 SEM. + eapply transf_cminor_program_correct; eauto. + eapply Cminorgenproof.transl_program_correct; eauto. + eapply Cshmgenproof3.transl_program_correct; eauto. + apply Ctyping.typecheck_program_correct; auto. Qed. |