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/Clflags.ml | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++ driver/Compiler.v | 47 +++++++++++++++++++++++++---------------------- driver/Driver.ml | 2 ++ 3 files changed, 78 insertions(+), 22 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b1f2bd8..610d807 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -52,3 +52,54 @@ let option_small_data = && Configuration.system = "diab" then 8 else 0) let option_small_const = ref (!option_small_data) +let option_timings = ref false + +(** Timing facility *) + +let timers : (string * float) list ref = ref [] + +let add_to_timer name time = + let rec add = function + | [] -> [name, time] + | (name1, time1 as nt1) :: rem -> + if name1 = name then (name1, time1 +. time) :: rem else nt1 :: add rem + in timers := add !timers + +let time name fn arg = + if not !option_timings then + fn arg + else begin + let start = Sys.time() in + try + let res = fn arg in + add_to_timer name (Sys.time() -. start); + res + with x -> + add_to_timer name (Sys.time() -. start); + raise x + end + +let time2 name fn arg1 arg2 = time name (fun () -> fn arg1 arg2) () +let time3 name fn arg1 arg2 arg3 = time name (fun () -> fn arg1 arg2 arg3) () + +let time_coq name fn arg = + if not !option_timings then + fn arg + else begin + let start = Sys.time() in + try + let res = fn arg in + add_to_timer (Camlcoq.camlstring_of_coqstring name) (Sys.time() -. start); + res + with x -> + add_to_timer (Camlcoq.camlstring_of_coqstring name) (Sys.time() -. start); + raise x + end + +let print_timers () = + if !option_timings then + List.iter + (fun (name, time) -> Printf.printf "%7.2fs %s\n" time name) + !timers + +let _ = at_exit print_timers 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. diff --git a/driver/Driver.ml b/driver/Driver.ml index 8853794..e768fa2 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -457,6 +457,7 @@ Tracing options: General options: -stdlib Set the path of the Compcert run-time library -v Print external commands before invoking them + -timings Show the time spent in various compiler passes Interpreter mode: -interp Execute given .c files using the reference interpreter -quiet Suppress diagnostic messages for the interpreter @@ -529,6 +530,7 @@ let cmdline_actions = push_linker_arg s); "-Os$", Set option_Osize; "-O$", Unset option_Osize; + "-timings$", Set option_timings; "-fsmall-data$", Integer(fun n -> option_small_data := n); "-fsmall-const$", Integer(fun n -> option_small_const := n); "-ffloat-const-prop$", Integer(fun n -> option_ffloatconstprop := n); -- cgit v1.2.3