Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructions

Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat
PowerPC operations.

The pseudoinstructions were used to implement these operations,
as follows:

Pfcfi  : Ofloatofint   i.e. the conversion signed int32 -> float64
Pfcfiu : Ofloatofintu  i.e. the conversion unsigned int32 -> float64
Pfctiu : Ointuoffloat  i.e. the conversion float64 -> unsigned int32

These pseudoinstructions were expanded (in Asmexpand.ml) in terms of

Pfcfid  : signed int64 -> float64
Pfctidz : float64 -> signed int64

and int32/int64 conversions.

This commit performs this expansion during instruction selection
(SelectOp.vp):

floatofint(n)  becomes floatoflong(longofint(n))
floatofintu(n) becomes floatoflong(longuofint(n))
intuoffloat(n) becomes cast32unsigned(longoffloat(n))

Then there is no need for the 3 removed operations and the 3 removed
pseudoinstructions.

More importantly, the correctness of these expansions is now proved as
part of instruction selection, using the corresponding results from
Floats.v.

1 files changed, 0 insertions, 26 deletions

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index d8cbd94e..cb6a659f 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -875,15 +875,6 @@ let expand_instruction instr =
         emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz)))
       else
         emit (Plwz(GPR1, Cint ofs, GPR1))
-  | Pfcfi(r1, r2) ->
-      assert (Archi.ppc64);
-      emit (Pextsw(GPR0, r2));
-      emit (Pstdu(GPR0, Cint _m8, GPR1));
-      emit (Pcfi_adjust _8);
-      emit (Plfd(r1, Cint _0, GPR1));
-      emit (Pfcfid(r1, r1));
-      emit (Paddi(GPR1, GPR1, Cint _8));
-      emit (Pcfi_adjust _m8)
   | Pfcfl(r1, r2) ->
       assert (Archi.ppc64);
       emit (Pstdu(r2, Cint _m8, GPR1));
@@ -892,15 +883,6 @@ let expand_instruction instr =
       emit (Pfcfid(r1, r1));
       emit (Paddi(GPR1, GPR1, Cint _8));
       emit (Pcfi_adjust _m8)
-  | Pfcfiu(r1, r2) ->
-      assert (Archi.ppc64);
-      emit (Prldicl(GPR0, r2, _0, _32));
-      emit (Pstdu(GPR0, Cint _m8, GPR1));
-      emit (Pcfi_adjust _8);
-      emit (Plfd(r1, Cint _0, GPR1));
-      emit (Pfcfid(r1, r1));
-      emit (Paddi(GPR1, GPR1, Cint _8));
-      emit (Pcfi_adjust _m8)
   | Pfcti(r1, r2) ->
       emit (Pfctiwz(FPR13, r2));
       emit (Pstfdu(FPR13, Cint _m8, GPR1));
@@ -908,14 +890,6 @@ let expand_instruction instr =
       emit (Plwz(r1, Cint _4, GPR1));
       emit (Paddi(GPR1, GPR1, Cint _8));
       emit (Pcfi_adjust _m8)
-  | Pfctiu(r1, r2) ->
-      assert (Archi.ppc64);
-      emit (Pfctidz(FPR13, r2));
-      emit (Pstfdu(FPR13, Cint _m8, GPR1));
-      emit (Pcfi_adjust _8);
-      emit (Plwz(r1, Cint _4, GPR1));
-      emit (Paddi(GPR1, GPR1, Cint _8));
-      emit (Pcfi_adjust _m8)
   | Pfctid(r1, r2) ->
       assert (Archi.ppc64);
       emit (Pfctidz(FPR13, r2));