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

2 files changed, 34 insertions, 1 deletions

diff --git a/test/regression/Makefile b/test/regression/Makefile
index 57d5db3..22e5433 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -30,7 +30,8 @@ TESTS_DIFF=NaNs
 
 EXTRAS=annot1 commaprec expr2 expr3 expr4 extern1 funct2 funptr1 \
   pragmas ptrs1 ptrs2 struct1 struct2 struct3 \
-  struct4 struct5 struct6 struct9 struct10 types1 seqops
+  struct4 struct5 struct6 struct9 struct10 types1 seqops \
+  singlefloats
 
 # Test known to fail
 FAILURES=funct1
diff --git a/test/regression/singlefloats.c b/test/regression/singlefloats.c
new file mode 100644
index 0000000..9e3c582
--- /dev/null
+++ b/test/regression/singlefloats.c
@@ -0,0 +1,32 @@
+/* This caused an internal compiler error in CompCert 2.2.
+   (RTLtyping failure, because y is used both as a float32 and a float64). */
+
+typedef union
+{
+  float value;
+  unsigned int word;
+} shape;
+
+float
+expf(float x)
+{
+        float y,hi;
+
+        y = 1/hi;
+
+        shape A;
+        A.value = y;
+
+        shape B;
+        B.word = A.word;
+        y = B.value;
+
+        return y;
+}
+
+/* Another internal compiler error in CompCert 2.2.  */
+
+void store(volatile float * p, double x)
+{
+  *p = x + 1.0;
+}