diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-07 17:27:08 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-07 17:27:08 +0100 |
| commit | 8486b4c046914b1388b68fe906fe267108f84267 (patch) | |
| tree | 2a09eb912526825848fac77df54fe9e4917cd385 /src/translation/HTLgen.v | |
| parent | e63fef0613ed9e497279ae47b746413a093e9530 (diff) | |
| download | vericert-kvx-8486b4c046914b1388b68fe906fe267108f84267.tar.gz vericert-kvx-8486b4c046914b1388b68fe906fe267108f84267.zip | |
Fixes to operators
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index e0f860e..1cc30c7 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -366,7 +366,9 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := (Vlit (intToValue n))))*) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) - | Op.Ororimm n, r::nil => ret (boplit Vror r n) + | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32))) + (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*) | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n))) | Op.Ocmp c, _ => translate_condition c args | Op.Osel c AST.Tint, r1::r2::rl => |