diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-22 16:18:22 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-22 16:18:22 +0100 |
| commit | 6acefcbbc51aa7d2edb7b2098a5b15d06e742604 (patch) | |
| tree | 7c82b4e1c690ec27171dab9c15630818f08270c9 /mppa_k1c/Asmblockgen.v | |
| parent | 8909fb3df6fd282d6b8f24b288ef5d7ddbdb741a (diff) | |
| download | compcert-kvx-6acefcbbc51aa7d2edb7b2098a5b15d06e742604.tar.gz compcert-kvx-6acefcbbc51aa7d2edb7b2098a5b15d06e742604.zip | |
Added sxwd and zxwd support
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 9a564117..0d1dd49c 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -115,12 +115,6 @@ Definition sltimm64 := opimm64 Psltl Psltil. Definition sltuimm64 := opimm64 Psltul Psltiul. *) -Definition cast32signed (rd rs: ireg) := - if (ireg_eq rd rs) - then Pcvtw2l rd - else Pmvw2l rd rs - . - Definition addptrofs (rd rs: ireg) (n: ptrofs) := if Ptrofs.eq_dec n Ptrofs.zero then Pmv rd rs @@ -460,11 +454,12 @@ Definition transl_op OK (Pcvtl2w rd rs ::i k) | Ocast32signed, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (cast32signed rd rs ::i k) + OK (Psxwd rd rs ::i k) | Ocast32unsigned, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - assertion (ireg_eq rd rs); - OK (Pcvtw2l rd ::i Psllil rd rd (Int.repr 32) ::i Psrlil rd rd (Int.repr 32) ::i k) + OK (Pzxwd rd rs ::i k) +(* assertion (ireg_eq rd rs); + OK (Pcvtw2l rd ::i Psllil rd rd (Int.repr 32) ::i Psrlil rd rd (Int.repr 32) ::i k) *) | Oaddl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Paddl rd rs1 rs2 ::i k) |