diff options
Diffstat (limited to 'driver/Compiler.v')
| -rw-r--r-- | driver/Compiler.v | 47 |
1 files changed, 25 insertions, 22 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index d3628b5..ae54f48 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -13,6 +13,7 @@ (** The whole compiler and its proof of semantic preservation *) (** Libraries. *) +Require Import String. Require Import Coqlib. Require Import Errors. Require Import AST. @@ -100,6 +101,8 @@ Notation "a @@ b" := Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. + (** 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 @@ -108,47 +111,47 @@ Definition print {A: Type} (printer: A -> unit) (prog: A) : A := Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print (print_RTL 0) - @@ Tailcall.transf_program + @@ time "Tail calls" Tailcall.transf_program @@ print (print_RTL 1) - @@@ Inlining.transf_program + @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) - @@ Renumber.transf_program + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@ Constprop.transf_program + @@ time "Constant propagation" Constprop.transf_program @@ print (print_RTL 4) - @@ Renumber.transf_program + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 5) - @@@ CSE.transf_program + @@@ time "CSE" CSE.transf_program @@ print (print_RTL 6) - @@@ Deadcode.transf_program + @@@ time "Dead code" Deadcode.transf_program @@ print (print_RTL 7) - @@@ Allocation.transf_program + @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL - @@ Tunneling.tunnel_program + @@ time "Branch tunneling" Tunneling.tunnel_program @@@ Linearize.transf_program - @@ CleanupLabels.transf_program - @@@ Stacking.transf_program + @@ time "Label cleanup" CleanupLabels.transf_program + @@@ time "Mach generation" Stacking.transf_program @@ print print_Mach - @@@ Asmgen.transf_program. + @@@ time "Asm generation" Asmgen.transf_program. Definition transf_cminor_program (p: Cminor.program) : res Asm.program := OK p @@ print print_Cminor - @@@ Selection.sel_program - @@@ RTLgen.transl_program + @@@ time "Instruction selection" Selection.sel_program + @@@ time "RTL generation" RTLgen.transl_program @@@ transf_rtl_program. Definition transf_clight_program (p: Clight.program) : res Asm.program := OK p @@ print print_Clight - @@@ SimplLocals.transf_program - @@@ Cshmgen.transl_program - @@@ Cminorgen.transl_program + @@@ time "Simplification of locals" SimplLocals.transf_program + @@@ time "C#minor generation" Cshmgen.transl_program + @@@ time "Cminor generation" Cminorgen.transl_program @@@ transf_cminor_program. Definition transf_c_program (p: Csyntax.program) : res Asm.program := OK p - @@@ SimplExpr.transl_program + @@@ time "Clight generation" SimplExpr.transl_program @@@ transf_clight_program. (** Force [Initializers] and [Cexec] to be extracted as well. *) @@ -194,7 +197,7 @@ Theorem transf_rtl_program_correct: Proof. intros. assert (F: forward_simulation (RTL.semantics p) (Asm.semantics tp)). - unfold transf_rtl_program in H. + unfold transf_rtl_program, time in H. repeat rewrite compose_print_identity in H. simpl in H. set (p1 := Tailcall.transf_program p) in *. @@ -237,7 +240,7 @@ Theorem transf_cminor_program_correct: Proof. intros. assert (F: forward_simulation (Cminor.semantics p) (Asm.semantics tp)). - unfold transf_cminor_program in H. + 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. @@ -260,7 +263,7 @@ Theorem transf_clight_program_correct: Proof. intros. assert (F: forward_simulation (Clight.semantics1 p) (Asm.semantics tp)). - revert H; unfold transf_clight_program; simpl. + 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. @@ -285,7 +288,7 @@ Theorem transf_cstrategy_program_correct: Proof. intros. assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)). - revert H; unfold transf_c_program; simpl. + 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. |