From ef5477a47b49c405744319fbdef0a689b1bf03d4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Dec 2020 10:30:51 +0100 Subject: 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. --- powerpc/Op.v | 18 +----------------- 1 file changed, 1 insertion(+), 17 deletions(-) (limited to 'powerpc/Op.v') diff --git a/powerpc/Op.v b/powerpc/Op.v index 0f082c1f..a96a0439 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -105,7 +105,7 @@ Inductive operation : Type := | Osubl: operation (**r [rd = r1 - r2] *) | Onegl: operation (**r [rd = - r1] *) | Omull: operation (**r [rd = r1 * r2] *) - | Omullhs: operation (**r [rd = high part of r1 * r2, signed] *) + | Omullhs: operation (**r [rd = high part of r1 * r2, signed] *) | Omullhu: operation (**r [rd = high part of r1 * r2, unsigned] *) | Odivl: operation (**r [rd = r1 / r2] (signed) *) | Odivlu: operation (**r [rd = r1 / r2] (unsigned) *) @@ -141,9 +141,6 @@ Inductive operation : Type := | Ofloatofsingle: operation (**r [rd] is [r1] extended to double-precision float *) (*c Conversions between int and float: *) | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *) - | Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] (PPC64 only) *) - | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] (PPC64 only) *) - | Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] (PPC64 only *) | Ofloatofwords: operation (**r [rd = float_of_words(r1,r2)] *) (*c Manipulating 64-bit integers: *) | Omakelong: operation (**r [rd = r1 << 32 | r2] *) @@ -299,9 +296,6 @@ Definition eval_operation | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1) | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1) | Ointoffloat, v1::nil => Val.intoffloat v1 - | Ointuoffloat, v1::nil => Val.intuoffloat v1 - | Ofloatofint, v1::nil => Val.floatofint v1 - | Ofloatofintu, v1::nil => Val.floatofintu v1 | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2) | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2) | Olowlong, v1::nil => Some(Val.loword v1) @@ -449,9 +443,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoffloat => (Tfloat :: nil, Tsingle) | Ofloatofsingle => (Tsingle :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) - | Ointuoffloat => (Tfloat :: nil, Tint) - | Ofloatofint => (Tint :: nil, Tfloat) - | Ofloatofintu => (Tint :: nil, Tfloat) | Ofloatofwords => (Tint :: Tint :: nil, Tfloat) | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) @@ -570,9 +561,6 @@ Proof with (try exact I; try reflexivity). destruct v0... destruct v0... destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2... - destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2... - destruct v0; simpl in H0; inv H0... - destruct v0; simpl in H0; inv H0... destruct v0; destruct v1... destruct v0; destruct v1... destruct v0... @@ -999,10 +987,6 @@ Proof. inv H4; simpl; auto. inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2. exists (Vint i); auto. - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2. - exists (Vint i); auto. - inv H4; simpl in H1; inv H1; simpl. TrivialExists. - inv H4; simpl in H1; inv H1; simpl. TrivialExists. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. -- cgit