- 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

5 files changed, 9 insertions, 17 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 7bd1755..08a1ef4 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -486,17 +486,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pmovsd_fi rd n =>
       Next (nextinstr (rs#rd <- (Vfloat n))) m
   | Pmovsd_fm rd a =>
-      exec_load Mfloat64al32 m a rs rd
+      exec_load Mfloat64 m a rs rd
   | Pmovsd_mf a r1 =>
-      exec_store Mfloat64al32 m a rs r1 nil
+      exec_store Mfloat64 m a rs r1 nil
   | Pfld_f r1 =>
       Next (nextinstr (rs#ST0 <- (rs r1))) m
   | Pfld_m a =>
-      exec_load Mfloat64al32 m a rs ST0
+      exec_load Mfloat64 m a rs ST0
   | Pfstp_f rd =>
       Next (nextinstr (rs#rd <- (rs ST0) #ST0 <- Vundef)) m
   | Pfstp_m a =>
-      exec_store Mfloat64al32 m a rs ST0 (ST0 :: nil)
+      exec_store Mfloat64 m a rs ST0 (ST0 :: nil)
   | Pxchg_rr r1 r2 =>
       Next (nextinstr (rs#r1 <- (rs r2) #r2 <- (rs r1))) m
   (** Moves with conversion *)
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 740dff8..fa4112d 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -441,7 +441,7 @@ Definition transl_load (chunk: memory_chunk)
       do r <- ireg_of dest; OK(Pmov_rm r am :: k)
   | Mfloat32 =>
       do r <- freg_of dest; OK(Pcvtss2sd_fm r am :: k)
-  | Mfloat64 | Mfloat64al32 =>
+  | Mfloat64 =>
       do r <- freg_of dest; OK(Pmovsd_fm r am :: k)
   | Mint64 =>
       Error (msg "Asmgen.transl_load")
@@ -460,7 +460,7 @@ Definition transl_store (chunk: memory_chunk)
       do r <- ireg_of src; OK(Pmov_mr am r :: k)
   | Mfloat32 =>
       do r <- freg_of src; OK(Pcvtsd2ss_mf am r :: k)
-  | Mfloat64 | Mfloat64al32 =>
+  | Mfloat64 =>
       do r <- freg_of src; OK(Pmovsd_mf am r :: k)
   | Mint64 =>
       Error (msg "Asmgen.transl_store")
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 5d3df67..6f2aee5 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -997,10 +997,6 @@ Proof.
     auto. decEq. apply Pregmap.gso; auto with asmgen.
   exists rs2. split. 
   destruct chunk; ArgsInv; apply exec_straight_one; auto.
-  (* Mfloat64 -> Mfloat64al32 *)
-  rewrite <- H. simpl. unfold exec_load. rewrite H1.
-  destruct (eval_addrmode ge x rs); simpl in *; try discriminate.
-  erewrite Mem.load_float64al32; eauto. 
   split. unfold rs2. rewrite nextinstr_nf_inv1. Simplifs. apply preg_of_data.
   intros. unfold rs2. Simplifs. 
 Qed.
@@ -1047,10 +1043,6 @@ Proof.
   intros. Transparent destroyed_by_store. simpl in H2. simpl. Simplifs.
 (* float64 *)
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store. erewrite Mem.storev_float64al32; eauto. auto.
-  intros. Simplifs.
-(* float64al32 *)
-  econstructor; split.
   apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto.
   intros. Simplifs.
 Qed.
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index 826dadf..47340ec 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -94,7 +94,7 @@ Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mre
   | Mint8signed | Mint8unsigned => AX :: CX :: nil
   | Mint16signed | Mint16unsigned | Mint32 | Mint64 => nil
   | Mfloat32 => X7 :: nil
-  | Mfloat64 | Mfloat64al32 => FP0 :: nil
+  | Mfloat64 => FP0 :: nil
   end.
 
 Definition destroyed_by_cond (cond: condition): list mreg :=
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 0a666cb..01034f1 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -354,7 +354,7 @@ let print_builtin_vload_common oc chunk addr res =
       end
   | Mfloat32, [FR res] ->
       fprintf oc "	cvtss2sd %a, %a\n" addressing addr freg res
-  | (Mfloat64 | Mfloat64al32), [FR res] ->
+  | Mfloat64, [FR res] ->
       fprintf oc "	movsd	%a, %a\n" addressing addr freg res
   | _ ->
       assert false
@@ -396,7 +396,7 @@ let print_builtin_vstore_common oc chunk addr src tmp =
   | Mfloat32, [FR src] ->
       fprintf oc "	cvtsd2ss %a, %%xmm7\n" freg src;
       fprintf oc "	movss	%%xmm7, %a\n" addressing addr
-  | (Mfloat64 | Mfloat64al32), [FR src] ->
+  | Mfloat64, [FR src] ->
       fprintf oc "	movsd	%a, %a\n" freg src addressing addr
   | _ ->
       assert false