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, 12 deletions

diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 20cf9c1d..0442f7e8 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1500,18 +1500,6 @@ Opaque Val.add.
 - replace v with (Val.maketotal (Val.intoffloat (rs x))).
   TranslOpSimpl.
   rewrite H1; auto.
-  (* Ointuoffloat *)
-- replace v with (Val.maketotal (Val.intuoffloat (rs x))).
-  TranslOpSimpl.
-  rewrite H1; auto.
-  (* Ofloatofint *)
-- replace v with (Val.maketotal (Val.floatofint (rs x))).
-  TranslOpSimpl.
-  rewrite H1; auto.
-  (* Ofloatofintu *)
-- replace v with (Val.maketotal (Val.floatofintu (rs x))).
-  TranslOpSimpl.
-  rewrite H1; auto.
   (* Ocmp *)
 - destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto.
   exists rs'; auto with asmgen.