diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-10 23:53:02 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-10 23:53:02 +0200 |
| commit | 295058286407ec6c4182f2b12b27608fc7d28f95 (patch) | |
| tree | 9f5583cf990eb9aaee259e13b0737cce27948fe2 /mppa_k1c/Asm.v | |
| parent | e2ea45f5ba656254fa11bf3f355da67292c11f06 (diff) | |
| download | compcert-kvx-295058286407ec6c4182f2b12b27608fc7d28f95.tar.gz compcert-kvx-295058286407ec6c4182f2b12b27608fc7d28f95.zip | |
use shift 1-4 in backend
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 6a4095da..04f6969b 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -182,9 +182,9 @@ Inductive instruction : Type := | Pfcompl (ft: ftest) (rd rs1 rs2: ireg) (**r comparison float64 *)
| Paddw (rd rs1 rs2: ireg) (**r add word *)
- | Paddxw (shift : Z) (rd rs1 rs2: ireg) (**r add word *)
+ | Paddxw (shift : shift1_4) (rd rs1 rs2: ireg) (**r add word *)
| Psubw (rd rs1 rs2: ireg) (**r sub word *)
- | Psubxw (shift : Z) (rd rs1 rs2: ireg) (**r add word *)
+ | Psubxw (shift : shift1_4) (rd rs1 rs2: ireg) (**r add word *)
| Pmulw (rd rs1 rs2: ireg) (**r mul word *)
| Pandw (rd rs1 rs2: ireg) (**r and word *)
| Pnandw (rd rs1 rs2: ireg) (**r nand word *)
@@ -202,9 +202,9 @@ Inductive instruction : Type := | Pmsubw (rd rs1 rs2: ireg) (**r multiply-add words *)
| Paddl (rd rs1 rs2: ireg) (**r add long *)
- | Paddxl (shift : Z) (rd rs1 rs2: ireg) (**r add long shift *)
+ | Paddxl (shift : shift1_4) (rd rs1 rs2: ireg) (**r add long shift *)
| Psubl (rd rs1 rs2: ireg) (**r sub long *)
- | Psubxl (shift : Z) (rd rs1 rs2: ireg) (**r sub long shift *)
+ | Psubxl (shift : shift1_4) (rd rs1 rs2: ireg) (**r sub long shift *)
| Pandl (rd rs1 rs2: ireg) (**r and long *)
| Pnandl (rd rs1 rs2: ireg) (**r nand long *)
| Porl (rd rs1 rs2: ireg) (**r or long *)
@@ -232,9 +232,9 @@ Inductive instruction : Type := | Pcompiw (it: itest) (rd rs: ireg) (imm: int) (**r comparison imm word *)
| Paddiw (rd rs: ireg) (imm: int) (**r add imm word *)
- | Paddxiw (shift : Z) (rd rs: ireg) (imm: int) (**r add imm word *)
+ | Paddxiw (shift : shift1_4) (rd rs: ireg) (imm: int) (**r add imm word *)
| Psubiw (rd rs: ireg) (imm: int) (**r subtract imm word *)
- | Psubxiw (shift : Z) (rd rs: ireg) (imm: int) (**r subtract imm word *)
+ | Psubxiw (shift : shift1_4) (rd rs: ireg) (imm: int) (**r subtract imm word *)
| Pmuliw (rd rs: ireg) (imm: int) (**r mul imm word *)
| Pandiw (rd rs: ireg) (imm: int) (**r and imm word *)
| Pnandiw (rd rs: ireg) (imm: int) (**r nand imm word *)
@@ -258,9 +258,9 @@ Inductive instruction : Type := (** Arith RRI64 *)
| Pcompil (it: itest) (rd rs: ireg) (imm: int64) (**r comparison imm long *)
| Paddil (rd rs: ireg) (imm: int64) (**r add immediate long *)
- | Paddxil (shift : Z) (rd rs: ireg) (imm: int64) (**r add immediate long *)
+ | Paddxil (shift : shift1_4) (rd rs: ireg) (imm: int64) (**r add immediate long *)
| Psubil (rd rs: ireg) (imm: int64) (**r subtract imm long *)
- | Psubxil (shift : Z) (rd rs: ireg) (imm: int64) (**r subtract imm long *)
+ | Psubxil (shift : shift1_4) (rd rs: ireg) (imm: int64) (**r subtract imm long *)
| Pmulil (rd rs: ireg) (imm: int64) (**r add immediate long *)
| Pandil (rd rs: ireg) (imm: int64) (**r and immediate long *)
| Pnandil (rd rs: ireg) (imm: int64) (**r and immediate long *)
|