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/ValueAOp.v | 3 --- 1 file changed, 3 deletions(-) (limited to 'powerpc/ValueAOp.v') diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index a270d857..c81f1a6c 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -133,9 +133,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoffloat, v1::nil => singleoffloat v1 | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 - | Ointuoffloat, v1::nil => intuoffloat v1 - | Ofloatofint, v1::nil => floatofint v1 - | Ofloatofintu, v1::nil => floatofintu v1 | Ofloatofwords, v1::v2::nil => floatofwords v1 v2 | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 -- cgit