diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-20 10:58:40 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-20 10:58:40 +0100 |
| commit | 948513fea60b0b226e0fa0d6d31f34fd4c490697 (patch) | |
| tree | 26fc46db3a33074a1ce52ebedd2351903111e567 | |
| parent | c4c4f264a54f3a1bd8ffbccf8043e26414c68332 (diff) | |
| download | vericert-kvx-948513fea60b0b226e0fa0d6d31f34fd4c490697.tar.gz vericert-kvx-948513fea60b0b226e0fa0d6d31f34fd4c490697.zip | |
Some fixes, but still buggy probably
| -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 4fcb557..935f9a1 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -291,8 +291,8 @@ 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 (Vbinop Vand (boplit Vshr r n) (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) n))) - | Op.Oshldimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshldimm") + | Op.Ororimm n, r::nil => ret (Vbinop Vor (boplit Vshr r n) (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) n))) + | 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 => do tc <- translate_condition c rl; |