From 56579f8ade21cb0a880ffbd6d5e28f152e951be8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 6 Apr 2014 07:11:12 +0000 Subject: Merge of branch linear-typing: 1) Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of locations that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c). This corresponds to commits 2435+2436 plus improvements in Lineartyping. 2) Add -dtimings option to measure compilation times. Moved call to C parser from Elab to Parse, to make it easier to measure parsing time independently of elaboration time. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Compiler.v | 47 +++++++++++++++++++++++++---------------------- 1 file changed, 25 insertions(+), 22 deletions(-) (limited to 'driver/Compiler.v') diff --git a/driver/Compiler.v b/driver/Compiler.v index d3628b51..ae54f487 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. -- cgit