aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v10
-rw-r--r--mppa_k1c/Asmblock.v8
-rw-r--r--mppa_k1c/Asmblockgen.v13
-rw-r--r--mppa_k1c/Asmblockgenproof1.v10
-rw-r--r--mppa_k1c/Asmexpand.ml4
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml13
-rw-r--r--mppa_k1c/TargetPrinter.ml8
-rw-r--r--test/mppa/instr/cast_S32_S64.c7
-rw-r--r--test/mppa/instr/cast_S64_U32.c7
-rw-r--r--test/mppa/instr/cast_U32_S64.c7
10 files changed, 51 insertions, 36 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 23b11a03..eef5f39c 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -87,16 +87,14 @@ Inductive instruction : Type :=
| Pfss (rs: freg) (ra: ireg) (ofs: offset) (**r store float *)
| Pfsd (rd: freg) (ra: ireg) (ofs: offset) (**r store 64-bit float *)
- (** Arith R *)
- | Pcvtw2l (rd: ireg) (**r Convert Word to Long *)
-
(** Arith RR *)
| Pmv (rd rs: ireg) (**r register move *)
| Pnegw (rd rs: ireg) (**r negate word *)
| Pnegl (rd rs: ireg) (**r negate long *)
| Pfnegd (rd rs: ireg) (**r float negate double *)
| Pcvtl2w (rd rs: ireg) (**r Convert Long to Word *)
- | Pmvw2l (rd rs: ireg) (**r Move Convert Word to Long *)
+ | Psxwd (rd rs: ireg) (**r Sign Extend Word to Double Word *)
+ | Pzxwd (rd rs: ireg) (**r Zero Extend Word to Double Word *)
(** Arith RI32 *)
| Pmake (rd: ireg) (imm: int) (**r load immediate *)
@@ -175,7 +173,6 @@ Definition basic_to_instruction (b: basic) :=
(** PArith basics *)
(* R *)
- | PArithR Asmblock.Pcvtw2l r => Pcvtw2l r
| PArithR (Asmblock.Ploadsymbol id ofs) r => Ploadsymbol r id ofs
(* RR *)
@@ -183,7 +180,8 @@ Definition basic_to_instruction (b: basic) :=
| PArithRR Asmblock.Pnegw rd rs => Pnegw rd rs
| PArithRR Asmblock.Pnegl rd rs => Pnegl rd rs
| PArithRR Asmblock.Pcvtl2w rd rs => Pcvtl2w rd rs
- | PArithRR Asmblock.Pmvw2l rd rs => Pmvw2l rd rs
+ | PArithRR Asmblock.Psxwd rd rs => Psxwd rd rs
+ | PArithRR Asmblock.Pzxwd rd rs => Pzxwd rd rs
| PArithRR Asmblock.Pfnegd rd rs => Pfnegd rd rs
(* RI32 *)
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index c11d043b..5d60af6b 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -269,7 +269,6 @@ Coercion PStoreRRO: store_name_rro >-> Funclass.
(** Arithmetic instructions **)
Inductive arith_name_r : Type :=
- | Pcvtw2l (**r Convert Word to Long *)
| Ploadsymbol (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)
.
@@ -279,7 +278,8 @@ Inductive arith_name_rr : Type :=
| Pnegl (**r negate long *)
| Pfnegd (**r float negate double *)
| Pcvtl2w (**r Convert Long to Word *)
- | Pmvw2l (**r Move Convert Word to Long *)
+ | Psxwd (**r Sign Extend Word to Double Word *)
+ | Pzxwd (**r Zero Extend Word to Double Word *)
.
Inductive arith_name_ri32 : Type :=
@@ -797,7 +797,6 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset
match ai with
| PArithR n d =>
match n with
- | Pcvtw2l => rs#d <- (Val.longofint rs#d)
| Ploadsymbol s ofs => rs#d <- (Genv.symbol_address ge s ofs)
end
@@ -808,7 +807,8 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset
| Pnegl => rs#d <- (Val.negl rs#s)
| Pfnegd => rs#d <- (Val.negf rs#s)
| Pcvtl2w => rs#d <- (Val.loword rs#s)
- | Pmvw2l => rs#d <- (Val.longofint rs#s)
+ | Psxwd => rs#d <- (Val.longofint rs#s)
+ | Pzxwd => rs#d <- (Val.longofintu rs#s)
end
| PArithRI32 n d i =>
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 9a564117..0d1dd49c 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -115,12 +115,6 @@ Definition sltimm64 := opimm64 Psltl Psltil.
Definition sltuimm64 := opimm64 Psltul Psltiul.
*)
-Definition cast32signed (rd rs: ireg) :=
- if (ireg_eq rd rs)
- then Pcvtw2l rd
- else Pmvw2l rd rs
- .
-
Definition addptrofs (rd rs: ireg) (n: ptrofs) :=
if Ptrofs.eq_dec n Ptrofs.zero then
Pmv rd rs
@@ -460,11 +454,12 @@ Definition transl_op
OK (Pcvtl2w rd rs ::i k)
| Ocast32signed, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
- OK (cast32signed rd rs ::i k)
+ OK (Psxwd rd rs ::i k)
| Ocast32unsigned, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
- assertion (ireg_eq rd rs);
- OK (Pcvtw2l rd ::i Psllil rd rd (Int.repr 32) ::i Psrlil rd rd (Int.repr 32) ::i k)
+ OK (Pzxwd rd rs ::i k)
+(* assertion (ireg_eq rd rs);
+ OK (Pcvtw2l rd ::i Psllil rd rd (Int.repr 32) ::i Psrlil rd rd (Int.repr 32) ::i k) *)
| Oaddl, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Paddl rd rs1 rs2 ::i k)
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 2b653236..02301161 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1068,7 +1068,7 @@ Qed.
(** Some arithmetic properties. *)
-Remark cast32unsigned_from_cast32signed:
+(* Remark cast32unsigned_from_cast32signed:
forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)).
Proof.
intros. apply Int64.same_bits_eq; intros.
@@ -1096,7 +1096,7 @@ Proof.
+ split.
* Simpl.
* intros. destruct r; Simpl.
-Qed.
+Qed. *)
(* Translation of arithmetic operations *)
@@ -1169,12 +1169,12 @@ Opaque Int.eq.
eapply exec_straight_step. simpl; reflexivity. auto.
apply exec_straight_one. simpl; reflexivity. auto.
split; intros; Simpl.
-- (* Ocast32signed *)
+(* - (* Ocast32signed *)
exploit cast32signed_correct; eauto. intros (rs' & A & B & C).
exists rs'; split; eauto. split. apply B.
intros. assert (r <> PC). { destruct r; auto; contradict H; discriminate. }
apply C; auto.
-- (* longofintu *)
+ *)(* - (* longofintu *)
econstructor; split.
eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto.
split; intros; Simpl. (* unfold Pregmap.set; Simpl. *) destruct (PregEq.eq x0 x0).
@@ -1182,7 +1182,7 @@ Opaque Int.eq.
assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal.
rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto.
- + contradict n. auto.
+ + contradict n. auto. *)
- (* Ocmp *)
exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
exists rs'; split. eexact A. eauto with asmgen.
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 265de410..de75df25 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -505,10 +505,6 @@ let expand_instruction instr =
*)| Pcvtl2w (rd, rs) ->
assert Archi.ptr64;
emit (Paddiw (rd, rs, Int.zero)) (* 32-bit sign extension *)
- | Pcvtw2l (r) -> (* Pcvtw2l *)
- assert Archi.ptr64
- (* no-operation because the 32-bit integer was kept sign extended already *)
- (* FIXME - is it really the case on the MPPA ? *)
(*| Pjal_r(r, sg) ->
fixup_call sg; emit instr
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 083decde..4d7c8636 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -27,12 +27,13 @@ type ab_inst_rec = {
exception OpaqueInstruction
let arith_rr_str = function
+ | Pcvtl2w -> "Pcvtl2w"
| Pmv -> "Pmv"
| Pnegw -> "Pnegw"
| Pnegl -> "Pnegl"
| Pfnegd -> "Pfnegd"
- | Pcvtl2w -> "Pcvtl2w"
- | Pmvw2l -> "Pmvw2l"
+ | Psxwd -> "Psxwd"
+ | Pzxwd -> "Pzxwd"
let arith_rrr_str = function
| Pcompw it -> "Pcompw"
@@ -116,7 +117,6 @@ let arith_rr_rec i rd rs = { inst = arith_rr_str i; write_locs = [Reg rd]; read_
let arith_r_rec i rd = match i with
(* FIXME - this instruction is expanded to nothing, yet it still has a semantic in Asmblock.v.
* It will introduce unneeded dependencies.. *)
- | Pcvtw2l -> { inst = "Pcvtw2l"; write_locs = [Reg rd]; read_locs = [Reg rd]; imm = None ; is_control = false}
(* For Ploadsymbol, writing the highest integer since we do not know how many bits does a symbol have *)
| Ploadsymbol (id, ofs) -> { inst = "Ploadsymbol"; write_locs = [Reg rd]; read_locs = []; imm = Some (I64 Integers.Int64.max_signed); is_control = false}
@@ -327,7 +327,7 @@ type real_instruction =
(* ALU *)
| Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw
| Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord
- | Make | Nop
+ | Make | Nop | Sxwd | Zxwd
(* LSU *)
| Lbs | Lbz | Lhs | Lhz | Lws | Ld
| Sb | Sh | Sw | Sd
@@ -359,6 +359,8 @@ let ab_inst_to_real = function
| "Pxorl" | "Pxoril" -> Xord
| "Pmake" | "Pmakel" | "Ploadsymbol" -> Make
| "Pnop" | "Pcvtw2l" -> Nop
+ | "Psxwd" -> Sxwd
+ | "Pzxwd" -> Zxwd
| "Plb" -> Lbs
| "Plbu" -> Lbz
@@ -417,6 +419,7 @@ let rec_to_usage r =
| Some E27U27L10 -> mau_y)
| Nop -> alu_nop
| Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding)
+ | Sxwd | Zxwd -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding)
| Lbs | Lbz | Lhs | Lhz | Lws | Ld ->
(match encoding with None | Some U6 | Some S10 -> lsu_data
| Some U27L5 | Some U27L10 -> lsu_data_x
@@ -433,6 +436,7 @@ let real_inst_to_latency = function
| Nop -> 0 (* Only goes through ID *)
| Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw
| Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
+ | Sxwd | Zxwd
-> 1
| Mulw | Muld -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
| Lbs | Lbz | Lhs | Lhz | Lws | Ld
@@ -582,7 +586,6 @@ let print_inst oc = function
| Asm.Pfreeframe(sz, ofs) -> fprintf oc " Pfreeframe\n"
| Asm.Pbuiltin(ef, args, res) -> fprintf oc " Pbuiltin\n"
| Asm.Pcvtl2w(rd, rs) -> fprintf oc " Pcvtl2w %a = %a\n" ireg rd ireg rs
- | Asm.Pcvtw2l rd -> fprintf oc " Pcvtw2l %a\n" ireg rd
| i -> print_instruction oc i
let print_bb oc bb =
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 098027f2..36fab151 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -268,11 +268,9 @@ module Target (*: TARGET*) =
fprintf oc " sd %a[%a] = %a\n" offset ofs ireg ra ireg rd
(* Arith R instructions *)
- | Pcvtw2l(rd) -> assert false
- (* Converted to no instruction in Asmexpand *)
(* Arith RR instructions *)
- | Pmv(rd, rs) | Pmvw2l(rd, rs) ->
+ | Pmv(rd, rs) ->
fprintf oc " addd %a = %a, 0\n" ireg rd ireg rs
| Pcvtl2w(rd, rs) -> assert false
| Pnegl(rd, rs) -> assert Archi.ptr64;
@@ -281,6 +279,10 @@ module Target (*: TARGET*) =
fprintf oc " negw %a = %a\n" ireg rd ireg rs
| Pfnegd(rd, rs) ->
fprintf oc " fnegd %a = %a\n" ireg rs ireg rd
+ | Psxwd(rd, rs) ->
+ fprintf oc " sxwd %a = %a\n" ireg rd ireg rs
+ | Pzxwd(rd, rs) ->
+ fprintf oc " zxwd %a = %a\n" ireg rd ireg rs
(* Arith RI32 instructions *)
| Pmake (rd, imm) ->
diff --git a/test/mppa/instr/cast_S32_S64.c b/test/mppa/instr/cast_S32_S64.c
new file mode 100644
index 00000000..09c97e00
--- /dev/null
+++ b/test/mppa/instr/cast_S32_S64.c
@@ -0,0 +1,7 @@
+#include "framework.h"
+
+BEGIN_TEST(int)
+{
+ c = (long long) a;
+}
+END_TEST32()
diff --git a/test/mppa/instr/cast_S64_U32.c b/test/mppa/instr/cast_S64_U32.c
new file mode 100644
index 00000000..da49b2a8
--- /dev/null
+++ b/test/mppa/instr/cast_S64_U32.c
@@ -0,0 +1,7 @@
+#include "framework.h"
+
+BEGIN_TEST(long long)
+{
+ c = (unsigned int) a;
+}
+END_TEST()
diff --git a/test/mppa/instr/cast_U32_S64.c b/test/mppa/instr/cast_U32_S64.c
new file mode 100644
index 00000000..b6bcdf6a
--- /dev/null
+++ b/test/mppa/instr/cast_U32_S64.c
@@ -0,0 +1,7 @@
+#include "framework.h"
+
+BEGIN_TEST(unsigned int)
+{
+ c = (long long) a;
+}
+END_TEST()
generated by cgit (git 2.34.1) at 2024-07-01 23:44:51 +0000