diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 10:08:14 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 10:08:14 +0100 |
| commit | c5170915a81ca1bca420cd4683855cc7ba8ff8c4 (patch) | |
| tree | 8c4dc8009cb5ac09b4be976f5c2ec9cd87ad7ec8 /src/translation | |
| parent | 11ff840afe29c5340582e513613dc70c13879997 (diff) | |
| parent | 9089af0dbd8dc079c16501c73727df82c34c530d (diff) | |
| download | vericert-c5170915a81ca1bca420cd4683855cc7ba8ff8c4.tar.gz vericert-c5170915a81ca1bca420cd4683855cc7ba8ff8c4.zip | |
Merge branch 'master' into develop
Diffstat (limited to 'src/translation')
| -rw-r--r-- | src/translation/HTLgen.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index b26b9e3..68f9900 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -260,7 +260,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex | _, _ => error (Errors.msg "Htlgen: eff_addressing instruction not implemented: other") end. -(** Translate an instruction to a statement. *) +(** Translate an instruction to a statement. FIX mulhs mulhu *) Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := match op, args with | Op.Omove, r::nil => ret (Vvar r) @@ -269,8 +269,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2) | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2) | Op.Omulimm n, r::nil => ret (boplit Vmul r n) - | Op.Omulhs, _ => error (Errors.msg "Htlgen: Instruction not implemented: Omulhs") - | Op.Omulhu, _ => error (Errors.msg "Htlgen: Instruction not implemented: Omulhu") + | Op.Omulhs, r1::r2::nil => ret (bop Vmul r1 r2) + | Op.Omulhu, r1::r2::nil => ret (bop Vmul r1 r2) | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) @@ -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 => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") - | 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; |