diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-14 11:51:48 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:07 +0200 |
| commit | ad9f97729e9c708f8e220e6d93a1cdb442b60273 (patch) | |
| tree | 6439394772b7dd47be0ee0f680101ada3c2215d1 /mppa_k1c/Asm.v | |
| parent | 79597131ae07f1fe63485270486755481549470f (diff) | |
| download | compcert-kvx-ad9f97729e9c708f8e220e6d93a1cdb442b60273.tar.gz compcert-kvx-ad9f97729e9c708f8e220e6d93a1cdb442b60273.zip | |
MPPA - Removed Plui, replaced with Pmake, and modified make_immed64
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 22b2c7a3..5c8a6360 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -138,11 +138,11 @@ Inductive instruction : Type := | Pget (rd: ireg) (rs: preg) (**r get system register *) | Pset (rd: preg) (rs: ireg) (**r set system register *) | Pret (**r return *) -(* + | Pmv (rd: ireg) (rs: ireg) (**r integer move *) (** 32-bit integer register-immediate instructions *) - | Paddiw (rd: ireg) (rs: ireg0) (imm: int) (**r add immediate *) +(*| Paddiw (rd: ireg) (rs: ireg0) (imm: int) (**r add immediate *) | Psltiw (rd: ireg) (rs: ireg0) (imm: int) (**r set-less-than immediate *) | Psltiuw (rd: ireg) (rs: ireg0) (imm: int) (**r set-less-than unsigned immediate *) | Pandiw (rd: ireg) (rs: ireg0) (imm: int) (**r and immediate *) @@ -184,7 +184,8 @@ Inductive instruction : Type := | Psllil (rd: ireg) (rs: ireg0) (imm: int) (**r shift-left-logical immediate *) | Psrlil (rd: ireg) (rs: ireg0) (imm: int) (**r shift-right-logical immediate *) | Psrail (rd: ireg) (rs: ireg0) (imm: int) (**r shift-right-arith immediate *) -*)| Pluil (rd: ireg) (imm: int64) (**r load upper-immediate *) + | Pluil (rd: ireg) (imm: int64) (**r FIXME - remove it ; load upper-immediate *) +*)| Pmake (rd: ireg) (imm: int64) (**r load immediate *) (** 64-bit integer register-register instructions *) | Paddl (rd: ireg) (rs1 rs2: ireg0) (**r integer addition *) (* | Psubl (rd: ireg) (rs1 rs2: ireg0) (**r integer subtraction *) @@ -634,11 +635,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | Pret => Next (rs#PC <- (rs#RA)) m -(* | Pmv d s => + | Pmv d s => Next (nextinstr (rs#d <- (rs#s))) m (** 32-bit integer register-immediate instructions *) - | Paddiw d s i => +(*| Paddiw d s i => Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m | Psltiw d s i => Next (nextinstr (rs#d <- (Val.cmp Clt rs##s (Vint i)))) m @@ -718,8 +719,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Val.shrlu rs###s (Vint i)))) m | Psrail d s i => Next (nextinstr (rs#d <- (Val.shrl rs###s (Vint i)))) m -*)| Pluil d i => + | Pluil d i => Next (nextinstr (rs#d <- (Vlong (Int64.sign_ext 32 (Int64.shl i (Int64.repr 12)))))) m +*)| Pmake d i => + Next (nextinstr (rs#d <- (Vlong i))) m (** 64-bit integer register-register instructions *) | Paddl d s1 s2 => |