Commit ef5477a4 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

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.
parent e6e036b3
......@@ -200,12 +200,9 @@ Inductive instruction : Type :=
| Pfadd: freg -> freg -> freg -> instruction (**r float addition *)
| Pfadds: freg -> freg -> freg -> instruction (**r float addition *)
| Pfcmpu: freg -> freg -> instruction (**r float comparison *)
| Pfcfi: freg -> ireg -> instruction (**r signed-int-to-float conversion (pseudo, PPC64) *)
| Pfcfl: freg -> ireg -> instruction (**r signed-long-to-float conversion (pseudo, PPC64) *)
| Pfcfiu: freg -> ireg -> instruction (**r unsigned-int-to-float conversion (pseudo, PPC64) *)
| Pfcfid: freg -> freg -> instruction (**r signed-long-to-float conversion (PPC64) *)
| Pfcti: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo) *)
| Pfctiu: ireg -> freg -> instruction (**r float-to-unsigned-int conversion, round towards 0 (pseudo, PPC64) *)
| Pfctid: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo, PPC64) *)
| Pfctidz: freg -> freg -> instruction (**r float-to-signed-long conversion, round towards 0 (PPC64) *)
| Pfctiw: freg -> freg -> instruction (**r float-to-signed-int conversion, round by default *)
......@@ -825,16 +822,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m
| Pfcmpu r1 r2 =>
Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
| Pfcfi rd r1 =>
Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m
| Pfcfl rd r1 =>
Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong rs#r1)))) m
| Pfcfiu rd r1 =>
Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m
| Pfcti rd r1 =>
Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m
| Pfctiu rd r1 =>
Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m
| Pfctid rd r1 =>
Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m
| Pfdiv rd r1 r2 =>
......
......@@ -198,12 +198,9 @@ let pp_instructions pp ic =
| Pfadd (fr1,fr2,fr3) -> instruction pp "Pfadd" [Freg fr1; Freg fr2; Freg fr3]
| Pfadds (fr1,fr2,fr3) -> instruction pp "Pfadds" [Freg fr1; Freg fr2; Freg fr3]
| Pfcmpu (fr1,fr2) -> instruction pp "Pfcmpu" [Freg fr1; Freg fr2]
| Pfcfi (ir,fr)
| Pfcfl (ir,fr) -> assert false (* Should not occur *)
| Pfcfid (fr1,fr2) -> instruction pp "Pfcfid" [Freg fr1; Freg fr2]
| Pfcfiu _ (* Should not occur *)
| Pfcti _ (* Should not occur *)
| Pfctiu _ (* Should not occur *)
| Pfctid _ -> assert false (* Should not occur *)
| Pfctidz (fr1,fr2) -> instruction pp "Pfctidz" [Freg fr1; Freg fr2]
| Pfctiw (fr1,fr2) -> instruction pp "Pfctiw" [Freg fr1; Freg fr2]
......
......@@ -875,15 +875,6 @@ let expand_instruction instr =
emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz)))
else
emit (Plwz(GPR1, Cint ofs, GPR1))
| Pfcfi(r1, r2) ->
assert (Archi.ppc64);
emit (Pextsw(GPR0, r2));
emit (Pstdu(GPR0, Cint _m8, GPR1));
emit (Pcfi_adjust _8);
emit (Plfd(r1, Cint _0, GPR1));
emit (Pfcfid(r1, r1));
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
| Pfcfl(r1, r2) ->
assert (Archi.ppc64);
emit (Pstdu(r2, Cint _m8, GPR1));
......@@ -892,15 +883,6 @@ let expand_instruction instr =
emit (Pfcfid(r1, r1));
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
| Pfcfiu(r1, r2) ->
assert (Archi.ppc64);
emit (Prldicl(GPR0, r2, _0, _32));
emit (Pstdu(GPR0, Cint _m8, GPR1));
emit (Pcfi_adjust _8);
emit (Plfd(r1, Cint _0, GPR1));
emit (Pfcfid(r1, r1));
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
| Pfcti(r1, r2) ->
emit (Pfctiwz(FPR13, r2));
emit (Pstfdu(FPR13, Cint _m8, GPR1));
......@@ -908,14 +890,6 @@ let expand_instruction instr =
emit (Plwz(r1, Cint _4, GPR1));
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
| Pfctiu(r1, r2) ->
assert (Archi.ppc64);
emit (Pfctidz(FPR13, r2));
emit (Pstfdu(FPR13, Cint _m8, GPR1));
emit (Pcfi_adjust _8);
emit (Plwz(r1, Cint _4, GPR1));
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
| Pfctid(r1, r2) ->
assert (Archi.ppc64);
emit (Pfctidz(FPR13, r2));
......
......@@ -611,15 +611,6 @@ Definition transl_op
| Ointoffloat, a1 :: nil =>
do r1 <- freg_of a1; do r <- ireg_of res;
OK (Pfcti r r1 :: k)
| Ointuoffloat, a1 :: nil =>
do r1 <- freg_of a1; do r <- ireg_of res;
OK (Pfctiu r r1 :: k)
| Ofloatofint, a1 :: nil =>
do r1 <- ireg_of a1; do r <- freg_of res;
OK (Pfcfi r r1 :: k)
| Ofloatofintu, a1 :: nil =>
do r1 <- ireg_of a1; do r <- freg_of res;
OK (Pfcfiu r r1 :: k)
| Ofloatofwords, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res;
OK (Pfmake r r1 r2 :: k)
......
......@@ -1498,18 +1498,6 @@ Opaque Val.add.
rewrite H1; auto.
(* Ointoffloat *)
- 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 *)
......
......@@ -166,7 +166,7 @@ Definition destroyed_by_op (op: operation): list mreg :=
| Ofloatconst _ => R12 :: nil
| Osingleconst _ => R12 :: nil
| Olongconst _ => R12 :: nil
| Ointoffloat | Ointuoffloat => F13 :: nil
| Ointoffloat => F13 :: nil
| Olongoffloat => F13 :: nil
| Oaddlimm _ => R12 :: nil
| Oandlimm _ => R12 :: nil
......
......@@ -61,7 +61,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Onegfs | Oabsfs => op1 (default nv)
| Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
| Osingleoffloat | Ofloatofsingle => op1 (default nv)
| Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv)
| Ointoffloat => op1 (default nv)
| Ofloatofwords | Omakelong => op2 (default nv)
| Olowlong | Ohighlong => op1 (default nv)
| Ocmp c => needs_of_condition c
......
......@@ -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.
......
......@@ -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)
......
......@@ -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.
......
......@@ -553,22 +553,16 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3
| Pfcmpu(r1, r2) ->
fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2
| Pfcfi(r1, r2) ->
assert false
| Pfcfl(r1, r2) ->
assert false
| Pfcfid(r1, r2) ->
fprintf oc " fcfid %a, %a\n" freg r1 freg r2
| Pfcfiu(r1, r2) ->
assert false
| Pfcti(r1, r2) ->
assert false
| Pfctid(r1, r2) ->
assert false
| Pfctidz(r1, r2) ->
fprintf oc " fctidz %a, %a\n" freg r1 freg r2
| Pfctiu(r1, r2) ->
assert false
| Pfctiw(r1, r2) ->
fprintf oc " fctiw %a, %a\n" freg r1 freg r2
| Pfctiwz(r1, r2) ->
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment