diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-24 12:01:34 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-24 12:01:34 +0200 |
| commit | bde53a2d485b6ba071fdf456251357cccd3bb6f5 (patch) | |
| tree | 573f74767eac2b5a87c24860e585d0cacdcb58a1 /mppa_k1c/Asm.v | |
| parent | b1ab210e798c911a5e4952ed244e581a18c86312 (diff) | |
| download | compcert-kvx-bde53a2d485b6ba071fdf456251357cccd3bb6f5.tar.gz compcert-kvx-bde53a2d485b6ba071fdf456251357cccd3bb6f5.zip | |
MPPA - Added ops for comparison operators
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index c0caed5d..c39cf74f 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -187,8 +187,10 @@ Inductive instruction : Type := | Pmv (rd: ireg) (rs: ireg) (**r integer move *) (** Comparisons *) - | Pcompw (it: itest) (rd rs1 rs2: ireg) (**r integer comparison *) - | Pcompd (it: itest) (rd rs1 rs2: ireg) (**r integer comparison *) + | Pcompw (it: itest) (rd rs1 rs2: ireg) (**r integer comparison *) + | Pcompiw (it: itest) (rd rs1: ireg) (imm: int) (**r integer comparison imm *) + | Pcompd (it: itest) (rd rs1 rs2: ireg) (**r integer comparison double *) + | Pcompid (it: itest) (rd rs1: ireg) (imm: int64) (**r integer comparison double imm *) (** 32-bit integer register-immediate instructions *) | Paddiw (rd: ireg) (rs: ireg) (imm: int) (**r add immediate *) @@ -756,8 +758,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** Comparisons *) | Pcompw c d s1 s2 => Next (nextinstr (rs#d <- (compare_int c rs##s1 rs##s2 m))) m + | Pcompiw c d s i => + Next (nextinstr (rs#d <- (compare_int c rs##s (Vint i) m))) m | Pcompd c d s1 s2 => Next (nextinstr (rs#d <- (compare_long c rs###s1 rs###s2 m))) m + | Pcompid c d s i => + Next (nextinstr (rs#d <- (compare_long c rs###s (Vlong i) m))) m (** 32-bit integer register-immediate instructions *) | Paddiw d s i => |