diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-10 15:18:50 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-10 15:18:50 +0200 |
commit | 67a5ffd5f8a1f2f95dc480daee9b5d927c768a2d (patch) | |
tree | 52f7fc7d4cde6c7144b789d4df730b831753337a /mppa_k1c | |
parent | e6fd7a6abcebee211acf1ef95e0779d7c8aa1325 (diff) | |
download | compcert-kvx-67a5ffd5f8a1f2f95dc480daee9b5d927c768a2d.tar.gz compcert-kvx-67a5ffd5f8a1f2f95dc480daee9b5d927c768a2d.zip |
MPPA - bunch of ops added : lowlong, and, or, shr..
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 31 | ||||
-rw-r--r-- | mppa_k1c/Asmexpand.ml | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmgen.v | 34 | ||||
-rw-r--r-- | mppa_k1c/Asmgenproof.v | 6 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 26 |
5 files changed, 80 insertions, 21 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d7959445..6fe00407 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -191,18 +191,29 @@ Inductive instruction : Type := (** 32-bit integer register-immediate instructions *) | Paddiw (rd: ireg) (rs: ireg) (imm: int) (**r add immediate *) + | Pandiw (rd: ireg) (rs: ireg) (imm: int) (**r and immediate *) + | Psrliw (rd: ireg) (rs: ireg) (imm: int) (**r shift right logical immediate *) (** 32-bit integer register-register instructions *) | Paddw (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) + | Pandw (rd: ireg) (rs1 rs2: ireg) (**r integer andition *) | Pnegw (rd: ireg) (rs: ireg) (**r negate word *) (** 64-bit integer register-immediate instructions *) | Paddil (rd: ireg) (rs: ireg) (imm: int64) (**r add immediate *) + | Pandil (rd: ireg) (rs: ireg) (imm: int64) (**r and immediate *) + | Poril (rd: ireg) (rs: ireg) (imm: int64) (**r or long immediate *) + | Psrlil (rd: ireg) (rs: ireg) (imm: int) (**r shift right logical immediate long *) | Pmake (rd: ireg) (imm: int) (**r load immediate *) | Pmakel (rd: ireg) (imm: int64) (**r load immediate long *) +(** Conversions *) + | Pcvtl2w (rd: ireg) (rs: ireg) (**r Convert Long to Word *) + (** 64-bit integer register-register instructions *) | Paddl (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) + | Pandl (rd: ireg) (rs1 rs2: ireg) (**r integer andition *) + | Porl (rd: ireg) (rs1 rs2: ireg) (**r or long *) | Pnegl (rd: ireg) (rs: ireg) (**r negate long *) (* Unconditional jumps. Links are always to X1/RA. *) @@ -713,16 +724,28 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** 32-bit integer register-immediate instructions *) | Paddiw d s i => Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m + | Pandiw d s i => + Next (nextinstr (rs#d <- (Val.and rs##s (Vint i)))) m + | Psrliw d s i => + Next (nextinstr (rs#d <- (Val.shru rs##s (Vint i)))) m (** 32-bit integer register-register instructions *) | Paddw d s1 s2 => Next (nextinstr (rs#d <- (Val.add rs##s1 rs##s2))) m + | Pandw d s1 s2 => + Next (nextinstr (rs#d <- (Val.and rs##s1 rs##s2))) m | Pnegw d s => Next (nextinstr (rs#d <- (Val.neg rs###s))) m (** 64-bit integer register-immediate instructions *) | Paddil d s i => Next (nextinstr (rs#d <- (Val.addl rs###s (Vlong i)))) m + | Pandil d s i => + Next (nextinstr (rs#d <- (Val.andl rs###s (Vlong i)))) m + | Poril d s i => + Next (nextinstr (rs#d <- (Val.orl rs###s (Vlong i)))) m + | Psrlil d s i => + Next (nextinstr (rs#d <- (Val.shrlu rs###s (Vint i)))) m | Pmakel d i => Next (nextinstr (rs#d <- (Vlong i))) m | Pmake d i => @@ -731,9 +754,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** 64-bit integer register-register instructions *) | Paddl d s1 s2 => Next (nextinstr (rs#d <- (Val.addl rs###s1 rs###s2))) m + | Pandl d s1 s2 => + Next (nextinstr (rs#d <- (Val.andl rs###s1 rs###s2))) m + | Porl d s1 s2 => + Next (nextinstr (rs#d <- (Val.orl rs###s1 rs###s2))) m | Pnegl d s => Next (nextinstr (rs#d <- (Val.negl rs###s))) m +(** Conversions *) + | Pcvtl2w d s => + Next (nextinstr (rs#d <- (Val.loword rs###s))) m + (** Unconditional jumps. *) | Pj_l l => goto_label f l rs m diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index f21ad2eb..d24383a7 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -548,10 +548,10 @@ let expand_instruction instr = end else begin emit (Pxorl(rd, rs1, rs2)); emit (Psltul(rd, X0, X rd)) end - | Pcvtl2w(rd, rs) -> +*)| Pcvtl2w(rd, rs) -> assert Archi.ptr64; emit (Paddiw(rd, rs, Int.zero)) (* 32-bit sign extension *) - | Pcvtw2l(r) -> +(*| Pcvtw2l(r) -> assert Archi.ptr64 (* no-operation because the 32-bit integer was kept sign extended already *) diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 2c99b6dc..b892cd64 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -82,8 +82,8 @@ Definition opimm32 (op: ireg -> ireg -> ireg -> instruction) end. Definition addimm32 := opimm32 Paddw Paddiw. -(* Definition andimm32 := opimm32 Pandw Pandiw. +(* Definition orimm32 := opimm32 Porw Poriw. Definition xorimm32 := opimm32 Pxorw Pxoriw. Definition sltimm32 := opimm32 Psltw Psltiw. @@ -107,10 +107,10 @@ Definition opimm64 (op: ireg -> ireg -> ireg -> instruction) end. Definition addimm64 := opimm64 Paddl Paddil. +Definition orimm64 := opimm64 Porl Poril. +Definition andimm64 := opimm64 Pandl Pandil. (* -Definition andimm64 := opimm64 Pandl Pandil. -Definition orimm64 := opimm64 Porl Poril. Definition xorimm64 := opimm64 Pxorl Pxoril. Definition sltimm64 := opimm64 Psltl Psltil. Definition sltuimm64 := opimm64 Psltul Psltiul. @@ -286,10 +286,10 @@ Definition transl_op | Oand, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandw rd rs1 rs2 :: k) - | Oandimm n, a1 :: nil => +*)| Oandimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (andimm32 rd rs n k) - | Oor, a1 :: a2 :: nil => +(*| Oor, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Porw rd rs1 rs2 :: k) | Oorimm n, a1 :: nil => @@ -316,10 +316,10 @@ Definition transl_op | Oshru, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psrlw rd rs1 rs2 :: k) - | Oshruimm n, a1 :: nil => +*)| Oshruimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Psrliw rd rs n :: k) - | Oshrximm n, a1 :: nil => +(*| Oshrximm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (if Int.eq n Int.zero then Pmv rd rs :: k else Psraiw GPR31 rs (Int.repr 31) :: @@ -328,10 +328,10 @@ Definition transl_op Psraiw rd GPR31 n :: k) (* [Omakelong], [Ohighlong] should not occur *) - | Olowlong, a1 :: nil => +*)| Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pcvtl2w rd rs :: k) - | Ocast32signed, a1 :: nil => +(*| Ocast32signed, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; assertion (ireg_eq rd rs); OK (Pcvtw2l rd :: k) @@ -375,16 +375,16 @@ Definition transl_op | Oandl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandl rd rs1 rs2 :: k) - | Oandlimm n, a1 :: nil => +*)| Oandlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (andimm64 rd rs n k) - | Oorl, a1 :: a2 :: nil => +(*| Oorl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Porl rd rs1 rs2 :: k) - | Oorlimm n, a1 :: nil => +*)| Oorlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (orimm64 rd rs n k) - | Oxorl, a1 :: a2 :: nil => +(*| Oxorl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pxorl rd rs1 rs2 :: k) | Oxorlimm n, a1 :: nil => @@ -405,10 +405,10 @@ Definition transl_op | Oshrlu, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psrll rd rs1 rs2 :: k) - | Oshrluimm n, a1 :: nil => +*)| Oshrluimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Psrlil rd rs n :: k) - | Oshrxlimm n, a1 :: nil => +(*| Oshrxlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (if Int.eq n Int.zero then Pmv rd rs :: k else Psrail GPR31 rs (Int.repr 63) :: @@ -656,9 +656,9 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) else loadind_ptr SP f.(fn_link_ofs) GPR30 c) *)| Mop op args res => transl_op op args res k -(*| Mload chunk addr args dst => + | Mload chunk addr args dst => transl_load chunk addr args dst k - | Mstore chunk addr args src => +(*| Mstore chunk addr args src => transl_store chunk addr args src k | Mcall sig (inl r) => do r1 <- ireg_of r; OK (Pjal_r r1 sig :: k) diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index a7a41f18..c8a89ef3 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -307,8 +307,14 @@ Opaque Int.eq. - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. (* Oaddimm32 *) - apply opimm32_label; intros; exact I. +(* Oandimm32 *) +- apply opimm32_label; intros; exact I. (* Oaddimm64 *) - apply opimm64_label; intros; exact I. +(* Oandimm64 *) +- apply opimm64_label; intros; exact I. +(* Oorimm64 *) +- apply opimm64_label; intros; exact I. Qed. (* diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 31a68e38..af76fdfc 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -211,12 +211,33 @@ module Target : TARGET = fprintf oc " addd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 | Paddil (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm + | Paddl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " addd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + + | Psrliw (rd, rs, imm) -> + fprintf oc " srlw %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm + | Psrlil (rd, rs, imm) -> + fprintf oc " srld %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm + + | Poril (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " ord %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm + | Porl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " ord %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + + | Pandiw (rd, rs, imm) -> + fprintf oc " andd %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm + | Pandw(rd, rs1, rs2) -> + fprintf oc " andd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + | Pandil (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " andd %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm + | Pandl(rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " andd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + | Pmake (rd, imm) -> fprintf oc " make %a, %a\n;;\n" ireg rd coqint imm | Pmakel (rd, imm) -> fprintf oc " make %a, %a\n;;\n" ireg rd coqint64 imm - | Paddl(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " addd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 + | Pnegl(rd, rs) -> assert Archi.ptr64; fprintf oc " negd %a = %a\n;;\n" ireg rd ireg rs | Pnegw(rd, rs) -> @@ -243,6 +264,7 @@ module Target : TARGET = assert false | Pfreeframe(sz, ofs) -> assert false + | Pcvtl2w _ -> assert false (* Pseudo-instructions that remain *) | Plabel lbl -> |