diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 06:03:21 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 06:03:21 +0200 |
| commit | 53b6eb437c7988b44e881c7b7a9df2e735ded0ea (patch) | |
| tree | ffe451f96a6942088356246e8530fd0d9160cb7e /mppa_k1c/Asmblockgen.v | |
| parent | b27d386185527d1ee9d0bb77ebe3bacffc2bf05a (diff) | |
| download | compcert-kvx-53b6eb437c7988b44e881c7b7a9df2e735ded0ea.tar.gz compcert-kvx-53b6eb437c7988b44e881c7b7a9df2e735ded0ea.zip | |
select cmpu
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index d770eebc..ce47cf52 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -367,6 +367,17 @@ Definition transl_cond_op Error(msg "Asmblockgen.transl_cond_op") end. +(* CoMPare Unsigned Words to Zero *) +Definition btest_for_cmpuwz (c: comparison) := + match c with + | Cne => OK BTwnez + | Ceq => OK BTweqz + | Clt => Error (msg "btest_for_compuwz: Clt") + | Cge => Error (msg "btest_for_compuwz: Cge") + | Cle => Error (msg "btest_for_compuwz: Cle") + | Cgt => Error (msg "btest_for_compuwz: Cgt") + end. + (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -737,6 +748,9 @@ Definition transl_op (match cond with | Ccomp0 cmp => OK (Pcmove (btest_for_cmpswz cmp) r0 rS r1 ::i k) + | Ccompu0 cmp => + do bt <- btest_for_cmpuwz cmp; + OK (Pcmoveu bt r0 rS r1 ::i k) | Ccompl0 cmp => OK (Pcmove (btest_for_cmpsdz cmp) r0 rS r1 ::i k) | _ => Error (msg "Asmblockgen Oselect") |