diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-04-15 15:21:49 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-05-20 18:00:46 +0200 |
commit | 996f2e071baaf52105714283d141af2eac8ffbfb (patch) | |
tree | 0d3968e7cb130b2399fe53a30ac7b3b6405d2284 /x86/Asm.v | |
parent | d002919334e83904447957f666f0d48704c5e55b (diff) | |
download | compcert-996f2e071baaf52105714283d141af2eac8ffbfb.tar.gz compcert-996f2e071baaf52105714283d141af2eac8ffbfb.zip |
Implement a `Osel` operation for x86
The operation compiles down to conditional moves.
Diffstat (limited to 'x86/Asm.v')
-rw-r--r-- | x86/Asm.v | 11 |
1 files changed, 6 insertions, 5 deletions
@@ -851,11 +851,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Ptestq_ri r1 n => Next (nextinstr (compare_longs (Val.andl (rs r1) (Vlong n)) (Vlong Int64.zero) rs m)) m | Pcmov c rd r1 => - match eval_testcond c rs with - | Some true => Next (nextinstr (rs#rd <- (rs#r1))) m - | Some false => Next (nextinstr rs) m - | None => Next (nextinstr (rs#rd <- Vundef)) m - end + let v := + match eval_testcond c rs with + | Some b => if b then rs#r1 else rs#rd + | None => Vundef + end in + Next (nextinstr (rs#rd <- v)) m | Psetcc c rd => Next (nextinstr (rs#rd <- (Val.of_optbool (eval_testcond c rs)))) m (** Arithmetic operations over double-precision floats *) |