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

3 files changed, 78 insertions, 22 deletions

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 <dir>  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);