diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 15:35:01 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 15:35:01 +0200 |
| commit | 1ecd47e848d3073c7317dc39c4fa72dbac66dd60 (patch) | |
| tree | 5b3d09bd9d1481fd09c1e97f9e3f8d5f75e96c95 /mppa_k1c/Asm.v | |
| parent | a6c79438ae754d969558bd37eb3a7676be6e66aa (diff) | |
| download | compcert-kvx-1ecd47e848d3073c7317dc39c4fa72dbac66dd60.tar.gz compcert-kvx-1ecd47e848d3073c7317dc39c4fa72dbac66dd60.zip | |
MPPA - Oshr
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d7007102..c2f145aa 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -193,6 +193,7 @@ Inductive instruction : Type := | 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 *) + | Psraw (rd: ireg) (rs1 rs2: ireg) (**r shift right arithmetic *) (** 32-bit integer register-register instructions *) | Paddw (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) @@ -743,6 +744,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Val.and rs##s1 rs##s2))) m | Pnegw d s => Next (nextinstr (rs#d <- (Val.neg rs###s))) m + | Psraw d s1 s2 => + Next (nextinstr (rs#d <- (Val.shr rs##s1 rs##s2))) m (** 64-bit integer register-immediate instructions *) | Paddil d s i => |