From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Compiler.v | 305 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 305 insertions(+) create mode 100644 driver/Compiler.v (limited to 'driver/Compiler.v') diff --git a/driver/Compiler.v b/driver/Compiler.v new file mode 100644 index 00000000..219fcae3 --- /dev/null +++ b/driver/Compiler.v @@ -0,0 +1,305 @@ +(* *********************************************************************) +(* *) +(* 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 Coqlib. +Require Import Maps. +Require Import Errors. +Require Import AST. +Require Import Values. +Require Import Smallstep. +(** Languages (syntax and semantics). *) +Require Csyntax. +Require Csem. +Require Csharpminor. +Require Cminor. +Require CminorSel. +Require RTL. +Require LTL. +Require LTLin. +Require Linear. +Require Mach. +Require Asm. +(** Translation passes. *) +Require Cshmgen. +Require Cminorgen. +Require Selection. +Require RTLgen. +Require Constprop. +Require CSE. +Require Allocation. +Require Tunneling. +Require Linearize. +Require Reload. +Require Stacking. +Require Asmgen. +(** Type systems. *) +Require Ctyping. +Require RTLtyping. +Require LTLtyping. +Require LTLintyping. +Require Lineartyping. +Require Machtyping. +(** Proofs of semantic preservation and typing preservation. *) +Require Cshmgenproof3. +Require Cminorgenproof. +Require Selectionproof. +Require RTLgenproof. +Require Constpropproof. +Require CSEproof. +Require Allocproof. +Require Alloctyping. +Require Tunnelingproof. +Require Tunnelingtyping. +Require Linearizeproof. +Require Linearizetyping. +Require Reloadproof. +Require Reloadtyping. +Require Stackingproof. +Require Stackingtyping. +Require Machabstr2concr. +Require Asmgenproof. + +Open Local 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: Set) (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: Set) + (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). + +(** 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. + + 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 Asm, and iterates this + transformation for every function. The second translates the whole + Cminor program to a RTL program, then to an LTL program, etc. + Between Cminor and Asm, we follow the first approach because it has + lower memory requirements. The translation from Clight to Asm + follows the second approach. + + The translation of an RTL function to an Asm function is as follows. *) + +Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := + OK f + @@ Constprop.transf_fundef + @@ CSE.transf_fundef + @@@ Allocation.transf_fundef + @@ Tunneling.tunnel_fundef + @@@ Linearize.transf_fundef + @@ Reload.transf_fundef + @@@ Stacking.transf_fundef + @@@ Asmgen.transf_fundef. + +(* Here is the translation of a Cminor function to an Asm function. *) + +Definition transf_cminor_fundef (f: Cminor.fundef) : res Asm.fundef := + OK f + @@ Selection.sel_fundef + @@@ RTLgen.transl_fundef + @@@ transf_rtl_fundef. + +(** The corresponding translations for whole program follow. *) + +Definition transf_rtl_program (p: RTL.program) : res Asm.program := + transform_partial_program transf_rtl_fundef p. + +Definition transf_cminor_program (p: Cminor.program) : res Asm.program := + transform_partial_program transf_cminor_fundef p. + +Definition transf_c_program (p: Csyntax.program) : res Asm.program := + match Ctyping.typecheck_program p with + | false => + Error (msg "Ctyping: type error") + | true => + OK p + @@@ Cshmgen.transl_program + @@@ Cminorgen.transl_program + @@@ transf_cminor_program + end. + +(** The following lemmas help reason over compositions of passes. *) + +Lemma map_partial_compose: + forall (X A B C: Set) + (ctx: X -> errmsg) + (f1: A -> res B) (f2: B -> res C) + (pa: list (X * A)) (pc: list (X * C)), + map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc -> + exists pb, map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc. +Proof. + induction pa; simpl. + intros. inv H. econstructor; eauto. + intro pc. destruct a as [x a]. + caseEq (f1 a); simpl; try congruence. intros b F1. + caseEq (f2 b); simpl; try congruence. intros c F2 EQ. + monadInv EQ. exploit IHpa; eauto. intros [pb [P Q]]. + rewrite P; simpl. + exists ((x, b) :: pb); split. auto. simpl. rewrite F2. rewrite Q. auto. +Qed. + +Lemma transform_partial_program_compose: + forall (A B C V: Set) + (f1: A -> res B) (f2: B -> res C) + (pa: program A V) (pc: program C V), + transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc -> + exists pb, transform_partial_program f1 pa = OK pb /\ + transform_partial_program f2 pb = OK pc. +Proof. + intros. monadInv H. + exploit map_partial_compose; eauto. intros [xb [P Q]]. + exists (mkprogram xb (prog_main pa) (prog_vars pa)); split. + unfold transform_partial_program. rewrite P; auto. + unfold transform_partial_program. simpl. rewrite Q; auto. +Qed. + +Lemma transform_program_partial_program: + forall (A B V: Set) (f: A -> B) (p: program A V) (tp: program B V), + transform_partial_program (fun x => OK (f x)) p = OK tp -> + transform_program f p = tp. +Proof. + intros until tp. unfold transform_partial_program. + rewrite map_partial_total. simpl. intros. inv H. auto. +Qed. + +Lemma transform_program_compose: + forall (A B C V: Set) + (f1: A -> res B) (f2: B -> C) + (pa: program A V) (pc: program C V), + transform_partial_program (fun f => f1 f @@ f2) pa = OK pc -> + exists pb, transform_partial_program f1 pa = OK pb /\ + transform_program f2 pb = pc. +Proof. + intros. + replace (fun f : A => f1 f @@ f2) + with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H. + exploit transform_partial_program_compose; eauto. + intros [pb [X Y]]. exists pb; split. auto. + apply transform_program_partial_program. auto. + apply extensionality; intro. destruct(f1 x); auto. +Qed. + +Lemma transform_partial_program_identity: + forall (A V: Set) (pa pb: program A V), + transform_partial_program (@OK A) pa = OK pb -> + pa = pb. +Proof. + intros until pb. unfold transform_partial_program. + replace (@OK A) with (fun b => @OK A b). + rewrite map_partial_identity. simpl. destruct pa; simpl; congruence. + apply extensionality; auto. +Qed. + +(** * Semantic preservation *) + +(** 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! *) + +Theorem transf_rtl_program_correct: + forall p tp beh, + transf_rtl_program p = OK tp -> + RTL.exec_program p beh -> + Asm.exec_program tp beh. +Proof. + intros. unfold transf_rtl_program, transf_rtl_fundef in H. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p7 [H7 P7]]. + clear H. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H7) as [p6 [H6 P6]]. + clear H7. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H6) as [p5 [H5 P5]]. + clear H6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H5) as [p4 [H4 P4]]. + clear H5. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H4) as [p3 [H3 P3]]. + clear H4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]]. + clear H3. + destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]]. + clear H2. + destruct (transform_program_compose _ _ _ _ _ _ _ _ H1) as [p0 [H00 P0]]. + clear H1. + generalize (transform_partial_program_identity _ _ _ _ H00). clear H00. intro. subst p0. + + assert (WT3 : LTLtyping.wt_program p3). + apply Alloctyping.program_typing_preserved with p2. auto. + assert (WT4 : LTLtyping.wt_program p4). + subst p4. apply Tunnelingtyping.program_typing_preserved. auto. + assert (WT5 : LTLintyping.wt_program p5). + apply Linearizetyping.program_typing_preserved with p4. auto. auto. + assert (WT6 : Lineartyping.wt_program p6). + subst p6. apply Reloadtyping.program_typing_preserved. auto. + assert (WT7: Machtyping.wt_program p7). + apply Stackingtyping.program_typing_preserved with p6. auto. auto. + + apply Asmgenproof.transf_program_correct with p7; auto. + apply Machabstr2concr.exec_program_equiv; auto. + apply Stackingproof.transf_program_correct with p6; auto. + subst p6; apply Reloadproof.transf_program_correct; auto. + apply Linearizeproof.transf_program_correct with p4; auto. + subst p4; apply Tunnelingproof.transf_program_correct. + apply Allocproof.transf_program_correct with p2; auto. + subst p2; apply CSEproof.transf_program_correct. + subst p1; apply Constpropproof.transf_program_correct. auto. +Qed. + +Theorem transf_cminor_program_correct: + forall p tp beh, + transf_cminor_program p = OK tp -> + Cminor.exec_program p beh -> + Asm.exec_program tp beh. +Proof. + intros. unfold transf_cminor_program, transf_cminor_fundef in H. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [H3 P3]]. + clear H. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]]. + clear H3. + destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]]. + generalize (transform_partial_program_identity _ _ _ _ H1). clear H1. intro. subst p1. + apply transf_rtl_program_correct with p3. auto. + apply RTLgenproof.transf_program_correct with p2; auto. + rewrite <- P1. apply Selectionproof.transf_program_correct; auto. +Qed. + +Theorem transf_c_program_correct: + forall p tp beh, + transf_c_program p = OK tp -> + Csem.exec_program p beh -> + Asm.exec_program tp beh. +Proof. + intros until beh; 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. -- cgit