diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-05-21 16:34:36 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-05-21 16:39:48 +0200 |
| commit | 479aacd0254605942a3f48c3b8053af4d07f0f6c (patch) | |
| tree | 7ddbddf078b86a30e693ae35721e08f54a0af11e /mppa_k1c/Asmgen.v | |
| parent | b81dbb863781a5f450cad0b01f90f729fb1a2244 (diff) | |
| download | compcert-kvx-479aacd0254605942a3f48c3b8053af4d07f0f6c.tar.gz compcert-kvx-479aacd0254605942a3f48c3b8053af4d07f0f6c.zip | |
MPPA - Added modulo and division 64 bits. Non certified
32 bits version are not yet there.
Right now the code is directly from libgcc, compiled with k1-gcc because
of builtins.
Diffstat (limited to 'mppa_k1c/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index dbd7b4f5..6b6531c3 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -429,11 +429,11 @@ Definition transl_op | Ocast32signed, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (cast32signed rd rs k) -(*| Ocast32unsigned, a1 :: nil => + | Ocast32unsigned, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; assertion (ireg_eq rd rs); - OK (Pcvtw2l rd :: Psllil rd rd (Int.repr 32) :: Psrlil rd rd (Int.repr 32) :: k) -*)| Oaddl, a1 :: a2 :: nil => + 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) | Oaddlimm n, a1 :: nil => |