- 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

3 files changed, 8 insertions, 8 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 4499f01..7a75d8f 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -676,9 +676,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Plbzx rd r1 r2 =>
       load2 Mint8unsigned rd r1 r2 rs m
   | Plfd rd cst r1 =>
-      load1 Mfloat64al32 rd cst r1 rs m
+      load1 Mfloat64 rd cst r1 rs m
   | Plfdx rd r1 r2 =>
-      load2 Mfloat64al32 rd r1 r2 rs m
+      load2 Mfloat64 rd r1 r2 rs m
   | Plfs rd cst r1 =>
       load1 Mfloat32 rd cst r1 rs m
   | Plfsx rd r1 r2 =>
@@ -745,9 +745,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pstbx rd r1 r2 =>
       store2 Mint8unsigned rd r1 r2 rs m
   | Pstfd rd cst r1 =>
-      store1 Mfloat64al32 rd cst r1 rs m
+      store1 Mfloat64 rd cst r1 rs m
   | Pstfdx rd r1 r2 =>
-      store2 Mfloat64al32 rd r1 r2 rs m
+      store2 Mfloat64 rd r1 r2 rs m
   | Pstfs rd cst r1 =>
       match store1 Mfloat32 rd cst r1 rs m with
       | Next rs' m' => Next (rs'#FPR13 <- Vundef) m'
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 39c0d1b..6b66686 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -563,7 +563,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
   | Mfloat32 =>
       do r <- freg_of dst;
       transl_memory_access (Plfs r) (Plfsx r) addr args GPR12 k
-  | Mfloat64 | Mfloat64al32 =>
+  | Mfloat64 =>
       do r <- freg_of dst;
       transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k
   | Mint64 =>
@@ -586,7 +586,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
   | Mfloat32 =>
       do r <- freg_of src;
       transl_memory_access (Pstfs r) (Pstfsx r) addr args temp k
-  | Mfloat64 | Mfloat64al32 =>
+  | Mfloat64 =>
       do r <- freg_of src;
       transl_memory_access (Pstfd r) (Pstfdx r) addr args temp k
   | Mint64 =>
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 6d0b52c..b9778c4 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -399,7 +399,7 @@ let print_builtin_vload_common oc chunk base offset res =
       fprintf oc "	lwz	%a, %a(%a)\n" ireg res constant offset ireg base
   | Mfloat32, FR res ->
       fprintf oc "	lfs	%a, %a(%a)\n" freg res constant offset ireg base
-  | (Mfloat64 | Mfloat64al32), FR res ->
+  | Mfloat64, FR res ->
       fprintf oc "	lfd	%a, %a(%a)\n" freg res constant offset ireg base
   (* Mint64 is special-cased below *)
   | _ ->
@@ -456,7 +456,7 @@ let print_builtin_vstore_common oc chunk base offset src =
   | Mfloat32, FR src ->
       fprintf oc "	frsp	%a, %a\n" freg FPR13 freg src;
       fprintf oc "	stfs	%a, %a(%a)\n" freg FPR13 constant offset ireg base
-  | (Mfloat64 | Mfloat64al32), FR src ->
+  | Mfloat64, FR src ->
       fprintf oc "	stfd	%a, %a(%a)\n" freg src constant offset ireg base
   (* Mint64 is special-cased below *)
   | _ ->