diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 17:03:52 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 17:03:52 +0200 |
| commit | b63085295d8495ff640f5eaff8b8ad52fc5c43d1 (patch) | |
| tree | fb854f158307f9a5185e92959e63df470566d538 /mppa_k1c/Asm.v | |
| parent | b17acc2e5f9c31a93164897c64c698fe8e490765 (diff) | |
| download | compcert-kvx-b63085295d8495ff640f5eaff8b8ad52fc5c43d1.tar.gz compcert-kvx-b63085295d8495ff640f5eaff8b8ad52fc5c43d1.zip | |
MPPA - More shifts
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index f11a8cbe..b2272f7a 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -192,7 +192,9 @@ 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 *) + | Psraiw (rd: ireg) (rs: ireg) (imm: int) (**r shift right arithmetic immediate *) | Psrliw (rd: ireg) (rs: ireg) (imm: int) (**r shift right logical immediate *) + | Pslliw (rd: ireg) (rs: ireg) (imm: int) (**r shift left logical immediate *) (** 32-bit integer register-register instructions *) | Paddw (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) @@ -201,6 +203,8 @@ Inductive instruction : Type := | Pandw (rd: ireg) (rs1 rs2: ireg) (**r integer andition *) | Pnegw (rd: ireg) (rs: ireg) (**r negate word *) | Psraw (rd: ireg) (rs1 rs2: ireg) (**r shift right arithmetic *) + | Psrlw (rd: ireg) (rs1 rs2: ireg) (**r shift right logical *) + | Psllw (rd: ireg) (rs1 rs2: ireg) (**r shift left logical word *) (** 64-bit integer register-immediate instructions *) | Paddil (rd: ireg) (rs: ireg) (imm: int64) (**r add immediate *) @@ -751,8 +755,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out 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 + | Psraiw d s i => + Next (nextinstr (rs#d <- (Val.shr rs##s (Vint i)))) m | Psrliw d s i => Next (nextinstr (rs#d <- (Val.shru rs##s (Vint i)))) m + | Pslliw d s i => + Next (nextinstr (rs#d <- (Val.shl rs##s (Vint i)))) m (** 32-bit integer register-register instructions *) | Paddw d s1 s2 => @@ -765,8 +773,12 @@ 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 + | Psrlw d s1 s2 => + Next (nextinstr (rs#d <- (Val.shru rs##s1 rs##s2))) m | Psraw d s1 s2 => Next (nextinstr (rs#d <- (Val.shr rs##s1 rs##s2))) m + | Psllw d s1 s2 => + Next (nextinstr (rs#d <- (Val.shl rs##s1 rs##s2))) m (** 64-bit integer register-immediate instructions *) | Paddil d s i => |