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, 15 insertions, 9 deletions

diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index c3eda068..7b34ea89 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -851,8 +851,13 @@ Proof.
   destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0.
   exists (Vint n); split; auto. unfold intuoffloat.
   destruct Archi.ppc64.
-  econstructor. constructor; eauto. constructor. simpl; rewrite Heqo; auto.
-  set (im := Int.repr Int.half_modulus).
+- apply Float.to_intu_to_long in Heqo.
+  econstructor. constructor. econstructor. econstructor; eauto. constructor.
+  simpl; rewrite Heqo; simpl; eauto. constructor.
+  simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned. auto.
+  assert (Int.modulus < Int64.max_unsigned) by (compute; auto).
+  generalize (Int.unsigned_range n). omega.  
+- set (im := Int.repr Int.half_modulus).
   set (fm := Float.of_intu im).
   assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)).
     constructor. auto.
@@ -889,11 +894,12 @@ Theorem eval_floatofint:
 Proof.
   intros until y. unfold floatofint. destruct (floatofint_match a); intros.
   InvEval. TrivialExists.
-  destruct Archi.ppc64.
-  TrivialExists.
   rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.of_int i)); split; auto.
-  set (t1 := addimm Float.ox8000_0000 a).
+  destruct Archi.ppc64.
+- rewrite Float.of_int_of_long.
+  EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto.
+- set (t1 := addimm Float.ox8000_0000 a).
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
   exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1.
@@ -913,12 +919,12 @@ Theorem eval_floatofintu:
 Proof.
   intros until y. unfold floatofintu. destruct (floatofintu_match a); intros.
   InvEval. TrivialExists.
-  destruct Archi.ppc64.
-  TrivialExists.
   rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.of_intu i)); split; auto.
-  unfold floatofintu.
-  set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
+  destruct Archi.ppc64.
+- rewrite Float.of_intu_of_long.
+  EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto.
+- set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
   exploit (eval_subf le t2).
   unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor.