aarch64/Asmblock: Move Pmovk to arith_pp

1 files changed, 5 insertions, 5 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 09228abc..81c55415 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -282,8 +282,6 @@ Inductive arith_p : Type :=
   (** Floating-point move *)
   | Pfmovimms (f: float32)                                 (**r load float32 constant *)
   | Pfmovimmd (f: float)                                   (**r load float64 constant *)
-  (* TODO? move to rri since we need the value of rd
-  | Pmovk (sz: isize) (pos: Z)                        (**r insert 16 bits of [n] at [pos] in rd *) *)
 .
 
 (* Arithmetic instructions with conditional execution *)
@@ -309,6 +307,9 @@ Inductive arith_comparison_p : Type :=
 Inductive arith_pp : Type :=
   (** Move integer register *)
   | Pmov
+  (** Move wide immediate *)
+  (* XXX: has to have the same register supplied both times *)
+  | Pmovk (sz: isize) (n: Z) (pos: Z)           (**r insert 16 bits of [n] at [pos] in rd *)
   (** PC-relative addressing *)
   | Paddadr (id: ident) (ofs: ptrofs)           (**r add the low address of [id + ofs] *)
   (** Bit-field operations *)
@@ -1250,9 +1251,6 @@ Definition arith_eval_p (i : arith_p) : val :=
   (** Floating-point move *)
   | Pfmovimms f => Vsingle f
   | Pfmovimmd f => Vfloat f
-  (* TODO need to move Pmovk to rri to make rd's old value available
-  | Pmovk W pos => insert_in_int rs#rd n pos 16
-  | Pmovk X pos => insert_in_long rs#rd n pos 16 *)
   end.
 
 Definition arith_eval_c_p (i : arith_c_p) (c : option bool) : val :=
@@ -1268,6 +1266,8 @@ Definition arith_eval_c_p (i : arith_c_p) (c : option bool) : val :=
 Definition arith_eval_pp i v :=
   match i with
   | Pmov => v
+  | Pmovk W n pos => insert_in_int v n pos 16
+  | Pmovk X n pos => insert_in_long v n pos 16
   | Paddadr id ofs => Val.addl v (symbol_low lk id ofs)
   | Psbfiz W r s => Val.shl (Val.sign_ext s v) (Vint r)
   | Psbfiz X r s => Val.shll (Val.sign_ext_l s v) (Vint r)