Merging arith_name_r and arith_name_ri into arith_r

1 files changed, 18 insertions, 24 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 66a8f14e..9d368d35 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -271,9 +271,14 @@ Inductive store_rs_a : Type :=
  *   Coercion PStore : st_instruction >-> basic.
  *)
 
-Inductive arith_name_r : Type :=
+Inductive arith_r : Type :=
   (** PC-relative addressing *)
   | Padrp (id: ident) (ofs: ptrofs)                        (**r set [rd] to high address of [id + ofs] *)
+  (** Move wide immediate *)
+  | Pmovz (sz: isize) (n: Z) (pos: Z)                      (**r move [n << pos] to [rd] *)
+  | Pmovn (sz: isize) (n: Z) (pos: Z)                      (**r move [NOT(n << pos)] to [rd] *)
+  (* 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 *)
@@ -375,13 +380,6 @@ Inductive arith_name_rf : Type :=
   | Pfcvtzu (isz: isize) (fsz: fsize)                 (**r convert float to unsigned int *)
 .
 
-Inductive arith_name_ri : Type :=
-  (** Move wide immediate *)
-  | Pmovz (sz: isize) (pos: Z)                        (**r move [n << pos] to [rd] *)
-  | Pmovn (sz: isize) (pos: Z)                        (**r move [NOT(n << pos)] to [rd] *)
-  (* 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 *) *)
-.
 
 Inductive arith_name_comparison_ri : Type :=
   (** Integer arithmetic, immediate *)
@@ -529,9 +527,8 @@ Inductive arith_name_aaffff : Type :=
  *             Instead, the condition register is mutated.
  *)
 Inductive ar_instruction : Type :=
-  | PArithR (i : arith_name_r) (rd : ireg)
+  | PArithR (i : arith_r) (rd : ireg)
   | PArithRR (i : arith_name_rr) (rd rs : ireg)
-  | PArithRI (i : arith_name_ri) (rd : ireg) (n : Z)
   | PArithRF (i : arith_name_rf) (rd : ireg) (rs : freg)
   | PArithRRR (i : arith_name_rrr) (rd r1 r2 : ireg)
   | PArithWRR0R (i : arith_name_w_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
@@ -1286,10 +1283,18 @@ Definition exec_cfi (f: function) (cfi: cf_instruction) (rs: regset) (m: mem) :
       end
   end.
 
-Definition arith_eval_r n :=
-  match n with
+Definition arith_eval_r i :=
+  match i with
   (* XXX change from ge to lk similar to ADadr change *)
   | Padrp id ofs => symbol_high lk id ofs
+  (** Move wide immediate *)
+  | Pmovz W n pos => Vint (Int.repr (Z.shiftl n pos))
+  | Pmovz X n pos => Vlong (Int64.repr (Z.shiftl n pos))
+  | Pmovn W n pos => Vint (Int.repr (Z.lnot (Z.shiftl n pos)))
+  | Pmovn X n pos => Vlong (Int64.repr (Z.lnot (Z.shiftl n pos)))
+  (* 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_rr n v :=
@@ -1307,16 +1312,6 @@ Definition arith_eval_rr n v :=
   | Pubfx X r s => Val.zero_ext_l s (Val.shrlu v (Vint r))
   end.
 
-Definition arith_eval_ri n i :=
-  match n with
-  | Pmovz W pos => Vint (Int.repr (Z.shiftl i pos))
-  | Pmovz X pos => Vlong (Int64.repr (Z.shiftl i pos))
-  | Pmovn W pos => Vint (Int.repr (Z.lnot (Z.shiftl i pos)))
-  | Pmovn X pos => Vlong (Int64.repr (Z.lnot (Z.shiftl i pos)))
-  (* 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_rf n v :=
   match n with
@@ -1525,9 +1520,8 @@ Definition arith_prepare_comparison_ff n (v1 v2 : val) :=
 
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
-  | PArithR n d => rs#d <- (arith_eval_r n)
+  | PArithR i d => rs#d <- (arith_eval_r i)
   | PArithRR n d s => rs#d <- (arith_eval_rr n rs#s)
-  | PArithRI n d i => rs#d <- (arith_eval_ri n i)
   | PArithRF n d s => rs#d <- (arith_eval_rf n rs#s)
   | PArithRRR n d s1 s2 => rs#d <- (arith_eval_rrr n rs#s1 rs#s2)