From 6acefcbbc51aa7d2edb7b2098a5b15d06e742604 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 22 Jan 2019 16:18:22 +0100 Subject: Added sxwd and zxwd support --- mppa_k1c/Asm.v | 10 ++++------ mppa_k1c/Asmblock.v | 8 ++++---- mppa_k1c/Asmblockgen.v | 13 ++++--------- mppa_k1c/Asmblockgenproof1.v | 10 +++++----- mppa_k1c/Asmexpand.ml | 4 ---- mppa_k1c/PostpassSchedulingOracle.ml | 13 ++++++++----- mppa_k1c/TargetPrinter.ml | 8 +++++--- test/mppa/instr/cast_S32_S64.c | 7 +++++++ test/mppa/instr/cast_S64_U32.c | 7 +++++++ test/mppa/instr/cast_U32_S64.c | 7 +++++++ 10 files changed, 51 insertions(+), 36 deletions(-) create mode 100644 test/mppa/instr/cast_S32_S64.c create mode 100644 test/mppa/instr/cast_S64_U32.c create mode 100644 test/mppa/instr/cast_U32_S64.c 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() -- cgit