diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-06 10:30:51 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-06 12:18:57 +0100 |
| commit | ef5477a47b49c405744319fbdef0a689b1bf03d4 (patch) | |
| tree | 47de3060e1e67749e67ec4d7b16046cb5227b1fc /powerpc/SelectOp.vp | |
| parent | e6e036b3f285d2f3ba2a5036a413eb9c7d7534cd (diff) | |
| download | compcert-kvx-ef5477a47b49c405744319fbdef0a689b1bf03d4.tar.gz compcert-kvx-ef5477a47b49c405744319fbdef0a689b1bf03d4.zip | |
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.
Diffstat (limited to 'powerpc/SelectOp.vp')
| -rw-r--r-- | powerpc/SelectOp.vp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index ba6612e8..cd9a65df 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -468,7 +468,7 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Definition intuoffloat (e: expr) := if Archi.ppc64 then - Eop Ointuoffloat (e ::: Enil) + Eop Olowlong (Eop Olongoffloat (e ::: Enil) ::: Enil) else Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) @@ -482,7 +482,8 @@ Nondetfunction floatofintu (e: expr) := Eop (Ofloatconst (Float.of_intu n)) Enil | _ => if Archi.ppc64 then - Eop Ofloatofintu (e ::: Enil) else + Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil) + else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil) end. @@ -493,7 +494,8 @@ Nondetfunction floatofint (e: expr) := Eop (Ofloatconst (Float.of_int n)) Enil | _ => if Archi.ppc64 then - Eop Ofloatofint (e ::: Enil) else + Eop Ofloatoflong (Eop Ocast32signed (e ::: Enil) ::: Enil) + else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: addimm Float.ox8000_0000 e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil) |