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, 1 insertions, 1 deletions

diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v
index 5ea09bd8..74ee6b85 100644
--- a/powerpc/NeedOp.v
+++ b/powerpc/NeedOp.v
@@ -61,7 +61,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Onegfs | Oabsfs => op1 (default nv)
   | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
   | Osingleoffloat | Ofloatofsingle => op1 (default nv)
-  | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv)
+  | Ointoffloat => op1 (default nv)
   | Ofloatofwords | Omakelong => op2 (default nv)
   | Olowlong | Ohighlong => op1 (default nv)
   | Ocmp c => needs_of_condition c