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, 13 insertions, 12 deletions

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index e468ab2..0d2cb89 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2081,11 +2081,8 @@ let _ = elab_funbody_f := elab_funbody
 
 (** * Entry point *)
 
-let elab_preprocessed_file name ic =
-  let lb = Lexer.init name ic in
+let elab_file prog =
   reset();
-  ignore (elab_definitions false (Builtins.environment())
-                                 (Parser.file Lexer.initial lb));
-  Lexer.finish();
+  ignore (elab_definitions false (Builtins.environment()) prog);
   elaborated_program()
 
diff --git a/cparser/Elab.mli b/cparser/Elab.mli
index 007e3d4..7eee4a0 100644
--- a/cparser/Elab.mli
+++ b/cparser/Elab.mli
@@ -13,4 +13,4 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-val elab_preprocessed_file : string -> in_channel -> C.program
+val elab_file : Cabs.definition list -> C.program
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 2a144e2..4a2ced2 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -40,14 +40,18 @@ let parse_transformations s =
 
 let preprocessed_file transfs name sourcefile =
   Cerrors.reset();
-  let t = parse_transformations transfs in
   let ic = open_in sourcefile in
   let p =
     try
-      transform_program t (Elab.elab_preprocessed_file name ic)
-    with Parsing.Parse_error ->
-           Cerrors.error "Error during parsing"; []
-       | Cerrors.Abort ->
-           [] in
+      let t = parse_transformations transfs in
+      let lb = Lexer.init name ic in
+      let parse = Clflags.time2 "Parsing" Parser.file Lexer.initial lb in
+      let p1 = Clflags.time "Elaboration" Elab.elab_file parse in
+      Clflags.time2 "Emulations" transform_program t p1
+    with
+    | Parsing.Parse_error ->
+        Cerrors.error "Error during parsing"; []
+    | Cerrors.Abort ->
+        [] in
   close_in ic;
   if Cerrors.check_errors() then None else Some p