- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.

- Revised printing of intermediate RTL code.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

7 files changed, 9 insertions, 34 deletions

diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index c400c5e..fb9173d 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -65,7 +65,6 @@ rule token = parse
   | "float"    { FLOAT }
   | "float32"    { FLOAT32 }
   | "float64"    { FLOAT64 }
-  | "float64al32" { FLOAT64AL32 }
   | "floatofint"    { FLOATOFINT }
   | "floatofintu"    { FLOATOFINTU }
   | "floatoflong"  { FLOATOFLONG }
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 5d93b84..f0f92f2 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -277,7 +277,6 @@ let mkmatch expr cases =
 %token FLOAT
 %token FLOAT32
 %token FLOAT64
-%token FLOAT64AL32
 %token <float> FLOATLIT
 %token FLOATOFINT
 %token FLOATOFINTU
@@ -687,7 +686,6 @@ memory_chunk:
   | INT                                         { Mint32 }
   | FLOAT32                                     { Mfloat32 }
   | FLOAT64                                     { Mfloat64 }
-  | FLOAT64AL32                                 { Mfloat64al32 }
   | FLOAT                                       { Mfloat64 }
 ;
 
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index d0bccca..5e46d76 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -168,7 +168,6 @@ let type_chunk = function
   | Mint64 -> tlong
   | Mfloat32 -> tfloat
   | Mfloat64 -> tfloat
-  | Mfloat64al32 -> tfloat
 
 let name_of_chunk = PrintAST.name_of_chunk
 
diff --git a/backend/Cminor.v b/backend/Cminor.v
index c12c6fc..aaf7510 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -103,9 +103,8 @@ Inductive binary_operation : Type :=
   | Ocmpl: comparison -> binary_operation  (**r long signed comparison *)
   | Ocmplu: comparison -> binary_operation. (**r long unsigned comparison *)
 
-(** Expressions include reading local variables, constants and
-  arithmetic operations, reading store locations, and conditional
-  expressions (similar to [e1 ? e2 : e3] in C). *)
+(** Expressions include reading local variables, constants,
+  arithmetic operations, and memory loads. *)
 
 Inductive expr : Type :=
   | Evar : ident -> expr
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 47f6975..f050c72 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -786,7 +786,6 @@ Proof.
   rewrite <- (Float.bits_of_singleoffloat f0).
   congruence. 
 - apply encode_val_inject. rewrite val_inject_id; auto.
-- apply encode_val_inject. rewrite val_inject_id; auto.
 Qed.
 
 Lemma store_argument_load_result:
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 137f65b..5c8347c 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -110,29 +110,13 @@ let print_globdef pp (id, gd) =
 let print_program pp (prog: RTL.program) =
   List.iter (print_globdef pp) prog.prog_defs
 
-let print_if optdest prog =
-  match !optdest with
+let destination : string option ref = ref None
+
+let print_if passno prog =
+  match !destination with
   | None -> ()
   | Some f ->
-      let oc = open_out f in
+      let oc = open_out (f ^ "." ^ Z.to_string passno) in
       print_program oc prog;
       close_out oc
 
-let destination_rtl : string option ref = ref None
-let print_rtl = print_if destination_rtl
-
-let destination_tailcall : string option ref = ref None
-let print_tailcall = print_if destination_tailcall
-
-let destination_inlining : string option ref = ref None
-let print_inlining = print_if destination_inlining
-
-let destination_constprop : string option ref = ref None
-let print_constprop = print_if destination_constprop
-
-let destination_cse : string option ref = ref None
-let print_cse = print_if destination_cse
-
-let destination_deadcode : string option ref = ref None
-let print_deadcode = print_if destination_deadcode
-
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index f11cd52..eee4762 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1933,7 +1933,7 @@ Definition vnormalize (chunk: memory_chunk) (v: aval) :=
   | Mint64, L _ => v
   | Mfloat32, F f => F (Float.singleoffloat f)
   | Mfloat32, _ => Fsingle
-  | (Mfloat64 | Mfloat64al32), F f => v
+  | Mfloat64, F f => v
   | _, _ => Ifptr Pbot
   end.
 
@@ -1987,8 +1987,6 @@ Proof.
   rewrite H2. destruct v; simpl; constructor. apply Float.singleoffloat_is_single. 
 - (* float64 *)
   destruct v; try contradiction; constructor.
-- (* float64 *)
-  destruct v; try contradiction; constructor.
 Qed.
 
 Lemma vnormalize_monotone:
@@ -2057,8 +2055,7 @@ Definition chunk_compat (chunk chunk': memory_chunk) : bool :=
   | Mint32, Mint32 => true
   | Mfloat32, Mfloat32 => true
   | Mint64, Mint64 => true
-  | (Mfloat64 | Mfloat64al32), Mfloat64 => true
-  | Mfloat64al32, Mfloat64al32 => true
+  | Mfloat64, Mfloat64 => true
   | _, _ => false
   end.