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/Asm.v | |
| 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/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 31 |
1 files changed, 31 insertions, 0 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 |