diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 06:15:28 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 06:15:28 +0200 |
| commit | 483d0e37880dbe44af3dafdcac9b1110a37139c4 (patch) | |
| tree | c71b4677725f8455877afb87379131eff8d811ce /mppa_k1c/Asmblockgen.v | |
| parent | 53b6eb437c7988b44e881c7b7a9df2e735ded0ea (diff) | |
| download | compcert-kvx-483d0e37880dbe44af3dafdcac9b1110a37139c4.tar.gz compcert-kvx-483d0e37880dbe44af3dafdcac9b1110a37139c4.zip | |
Select cmplu
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index ce47cf52..d8706239 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -378,6 +378,17 @@ Definition btest_for_cmpuwz (c: comparison) := | Cgt => Error (msg "btest_for_compuwz: Cgt") end. +(* CoMPare Unsigned Words to Zero *) +Definition btest_for_cmpudz (c: comparison) := + match c with + | Cne => OK BTdnez + | Ceq => OK BTdeqz + | Clt => Error (msg "btest_for_compudz: Clt") + | Cge => Error (msg "btest_for_compudz: Cge") + | Cle => Error (msg "btest_for_compudz: Cle") + | Cgt => Error (msg "btest_for_compudz: Cgt") + end. + (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -753,7 +764,9 @@ Definition transl_op 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") + | Ccomplu0 cmp => + do bt <- btest_for_cmpudz cmp; + OK (Pcmoveu bt r0 rS r1 ::i k) end) | Oselectl, a0 :: a1 :: aS :: nil |