Implement a `Osel` operation for ARM

The operation comples down to conditional moves.
Both integer and floating-point conditional moves are supported.

1 files changed, 9 insertions, 0 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index e6d1b4fc..194074ac 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -220,6 +220,7 @@ Inductive instruction : Type :=
   | Plabel: label -> instruction                    (**r define a code label *)
   | Ploadsymbol: ireg -> ident -> ptrofs -> instruction (**r load the address of a symbol *)
   | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *)
+  | Pfmovite: testcond -> freg -> freg -> freg -> instruction (**r FP conditional move *)
   | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *)
   | Padc: ireg -> ireg -> shift_op -> instruction     (**r add with carry *)
@@ -783,6 +784,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
         | None => Vundef
         end in
       Next (nextinstr (rs#r1 <- v)) m
+  | Pfmovite cond r1 ifso ifnot =>
+      let v :=
+        match eval_testcond cond rs with
+        | Some true => rs#ifso
+        | Some false => rs#ifnot
+        | None => Vundef
+        end in
+      Next (nextinstr (rs#r1 <- v)) m
   | Pbtbl r tbl =>
       match rs#r with
       | Vint n =>