diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asm.v | 8 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 16 |
2 files changed, 24 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 354840d4..e07b1190 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -143,6 +143,8 @@ Inductive instruction : Type := | Pnorw (rd rs1 rs2: ireg) (**r nor word *)
| Pxorw (rd rs1 rs2: ireg) (**r xor word *)
| Pnxorw (rd rs1 rs2: ireg) (**r xor word *)
+ | Pandnw (rd rs1 rs2: ireg) (**r andn word *)
+ | Pornw (rd rs1 rs2: ireg) (**r orn word *)
| Psraw (rd rs1 rs2: ireg) (**r shift right arithmetic word *)
| Psrlw (rd rs1 rs2: ireg) (**r shift right logical word *)
| Psllw (rd rs1 rs2: ireg) (**r shift left logical word *)
@@ -155,6 +157,8 @@ Inductive instruction : Type := | Pnorl (rd rs1 rs2: ireg) (**r nor long *)
| Pxorl (rd rs1 rs2: ireg) (**r xor long *)
| Pnxorl (rd rs1 rs2: ireg) (**r nxor long *)
+ | Pandnl (rd rs1 rs2: ireg) (**r andn long *)
+ | Pornl (rd rs1 rs2: ireg) (**r orn long *)
| Pmull (rd rs1 rs2: ireg) (**r mul long (low part) *)
| Pslll (rd rs1 rs2: ireg) (**r shift left logical long *)
| Psrll (rd rs1 rs2: ireg) (**r shift right logical long *)
@@ -177,6 +181,8 @@ Inductive instruction : Type := | Pnoriw (rd rs: ireg) (imm: int) (**r nor imm word *)
| Pxoriw (rd rs: ireg) (imm: int) (**r xor imm word *)
| Pnxoriw (rd rs: ireg) (imm: int) (**r nxor imm word *)
+ | Pandniw (rd rs: ireg) (imm: int) (**r andn imm word *)
+ | Porniw (rd rs: ireg) (imm: int) (**r orn imm word *)
| Psraiw (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word *)
| Psrliw (rd rs: ireg) (imm: int) (**r shift right logical imm word *)
| Pslliw (rd rs: ireg) (imm: int) (**r shift left logical imm word *)
@@ -194,6 +200,8 @@ Inductive instruction : Type := | Pnoril (rd rs: ireg) (imm: int64) (**r and immediate long *)
| Pxoril (rd rs: ireg) (imm: int64) (**r xor immediate long *)
| Pnxoril (rd rs: ireg) (imm: int64) (**r xor immediate long *)
+ | Pandnil (rd rs: ireg) (imm: int64) (**r andn long *)
+ | Pornil (rd rs: ireg) (imm: int64) (**r orn long *)
.
(** Correspondance between Asmblock and Asm *)
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index d30d62a2..c3de5206 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -380,6 +380,10 @@ module Target (*: TARGET*) = fprintf oc " xorw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pnxorw (rd, rs1, rs2) -> fprintf oc " nxorw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pandnw (rd, rs1, rs2) -> + fprintf oc " andnw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pornw (rd, rs1, rs2) -> + fprintf oc " ornw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psraw (rd, rs1, rs2) -> fprintf oc " sraw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psrlw (rd, rs1, rs2) -> @@ -403,6 +407,10 @@ module Target (*: TARGET*) = fprintf oc " xord %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pnxorl (rd, rs1, rs2) -> assert Archi.ptr64; fprintf oc " nxord %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pandnl (rd, rs1, rs2) -> + fprintf oc " andnd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pornl (rd, rs1, rs2) -> + fprintf oc " ornd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pmull (rd, rs1, rs2) -> fprintf oc " muld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pslll (rd, rs1, rs2) -> @@ -442,6 +450,10 @@ module Target (*: TARGET*) = fprintf oc " xorw %a = %a, %a\n" ireg rd ireg rs coqint imm | Pnxoriw (rd, rs, imm) -> fprintf oc " nxorw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Pandniw (rd, rs, imm) -> + fprintf oc " andnw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Porniw (rd, rs, imm) -> + fprintf oc " ornw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psraiw (rd, rs, imm) -> fprintf oc " sraw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psrliw (rd, rs, imm) -> @@ -475,6 +487,10 @@ module Target (*: TARGET*) = fprintf oc " xord %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pnxoril (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " nxord %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pandnil (rd, rs, imm) -> + fprintf oc " andnd %a = %a, %a\n" ireg rd ireg rs coqint imm + | Pornil (rd, rs, imm) -> + fprintf oc " ornd %a = %a, %a\n" ireg rd ireg rs coqint imm let get_section_names name = let (text, lit) = |