diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-24 13:25:48 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-24 13:25:48 +0100 |
| commit | ae33e6a4c48ccc298a3ff6f01d89ba0c469cdbd6 (patch) | |
| tree | 9f1d321b22f18539119bcf008f8cd95d5af37720 | |
| parent | f87842f41e42bcb34be7b45110b0b2dccbc4c0f5 (diff) | |
| download | vericert-kvx-ae33e6a4c48ccc298a3ff6f01d89ba0c469cdbd6.tar.gz vericert-kvx-ae33e6a4c48ccc298a3ff6f01d89ba0c469cdbd6.zip | |
Add instructions for Cmaskzero and Cmasknotzero
| -rw-r--r-- | src/translation/HTLgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index f109a8e..c96d4c7 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -275,8 +275,8 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : | Op.Ccompu c, _ => translate_comparison c args | Op.Ccompimm c i, _ => translate_comparison_imm c args i | Op.Ccompuimm c i, _ => translate_comparison_imm c args i - | Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero") - | Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero") + | Op.Cmaskzero n, r::nil => ret (Vbinop Veq (boplit Vand r n) (Vlit (ZToValue 32 0))) + | Op.Cmasknotzero n, r::nil => ret (Vbinop Vne (boplit Vand r n) (Vlit (ZToValue 32 0))) | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") end. |