From aef6fea9eabe3a3d169986253a3daccabdf78615 Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Mon, 6 Jul 2020 16:12:10 +0200 Subject: aarch64/Asmblock: Move Pmovk to arith_pp --- aarch64/Asmblock.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'aarch64/Asmblock.v') 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) -- cgit