From a7c6cf8d4d59e29ed73f9eb8bfc015b0384672a1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:33:05 +0000 Subject: Revu la repartition des sources Coq en sous-repertoires git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Main.v | 311 --------------------------------------------------------- 1 file changed, 311 deletions(-) delete mode 100644 backend/Main.v (limited to 'backend/Main.v') diff --git a/backend/Main.v b/backend/Main.v deleted file mode 100644 index 95dc4e6c..00000000 --- a/backend/Main.v +++ /dev/null @@ -1,311 +0,0 @@ -(** 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_fundef (f: Cminor.fundef) : option PPC.fundef := - Some f - @@@ RTLgen.transl_fundef - @@ Constprop.transf_fundef - @@ CSE.transf_fundef - @@@ Allocation.transf_fundef - @@ Tunneling.tunnel_fundef - @@ Linearize.transf_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). - -(** * 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_fundef. - 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_fundef. - 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 t n, - transf_cminor_program2 p = Some tp -> - Cminor.exec_program p t (Vint n) -> - PPC.exec_program tp t (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 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: - forall p tp t n, - transf_csharpminor_program p = Some tp -> - Csharpminor.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. -Qed. -- cgit