aarch64/Asmblock: Merge arith_r and arith_f into arith_p

1 files changed, 10 insertions, 19 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 1b503f24..7949632c 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -273,12 +273,15 @@ Inductive store_rs_a : Type :=
  *   Coercion PStore : st_instruction >-> basic.
  *)
 
-Inductive arith_r : Type :=
+Inductive arith_p : 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] *)
+  (** 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 *) *)
 .
@@ -392,12 +395,6 @@ Inductive arith_comparison_r : Type :=
   | Ptstimm (sz: isize) (n: Z)                        (**r and, then set flags *)
 .
 
-Inductive arith_f : Type :=
-  (** Floating-point move *)
-  | Pfmovimms (f: float32)                            (**r load float32 constant *)
-  | Pfmovimmd (f: float)                              (**r load float64 constant *)
-.
-
 Inductive arith_rrr : Type :=
   (** Variable shifts *)
   | Pasrv (sz: isize)                                 (**r arithmetic right shift *)
@@ -528,7 +525,7 @@ Inductive arith_aaffff : Type :=
  *             Instead, the condition register is mutated.
  *)
 Inductive ar_instruction : Type :=
-  | PArithR (i : arith_r) (rd : ireg)
+  | PArithP (i : arith_p) (rd : preg)
   | PArithCR (i : arith_c_r) (rd : ireg) (c : testcond)
   | PArithRR (i : arith_rr) (rd rs : ireg)
   | PArithRF (i : arith_rf) (rd : ireg) (rs : freg)
@@ -542,7 +539,6 @@ Inductive ar_instruction : Type :=
   | PArithRspRsp (i : arith_rsprsp) (rd r1 : iregsp)
   | PArithWARRRR0 (i : arith_w_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
   | PArithXARRRR0 (i : arith_x_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
-  | PArithF (i : arith_f) (rd : freg)
   | PArithFF (i : arith_ff) (rd rs : freg)
   | PArithFR (i : arith_fr) (rd : freg) (rs : ireg)
   | PArithSWFR0 (i : arith_sw_fr0) (rd : freg) (rs : ireg0)
@@ -1286,15 +1282,17 @@ Definition exec_cfi (f: function) (cfi: cf_instruction) (rs: regset) (m: mem) :
       end
   end.
 
-Definition arith_eval_r (i:arith_r): val :=
+Definition arith_eval_p (i : arith_p) : val :=
   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)))
+  (** 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 *)
@@ -1447,12 +1445,6 @@ Definition arith_eval_ff i v :=
   | Pfneg D => Val.negf v
   end.
 
-Definition arith_eval_f i :=
-  match i with
-  | Pfmovimms f => Vsingle f
-  | Pfmovimmd f => Vfloat f
-  end.
-
 Definition arith_eval_fr i v :=
   match i with
   | Pscvtf S W => Val.maketotal (Val.singleofint v)
@@ -1549,7 +1541,7 @@ Definition arith_prepare_comparison_ff i (v1 v2 : val) :=
 
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
-  | PArithR i d => rs#d <- (arith_eval_r i)
+  | PArithP i d => rs#d <- (arith_eval_p i)
   | PArithCR i d c => rs#d <- (arith_eval_c_r i (eval_testcond c rs))
   | PArithRR i d s => rs#d <- (arith_eval_rr i rs#s)
   | PArithRF i d s => rs#d <- (arith_eval_rf i rs#s)
@@ -1568,7 +1560,6 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithWARRRR0 i d s1 s2 s3 => rs#d <- (arith_eval_w_arrrr0 i rs#s1 rs#s2 rs##s3)
   | PArithXARRRR0 i d s1 s2 s3 => rs#d <- (arith_eval_x_arrrr0 i rs#s1 rs#s2 rs###s3)
 
-  | PArithF i d => rs#d <- (arith_eval_f i)
   | PArithFF i d s => rs#d <- (arith_eval_ff i rs#s)
   | PArithFR i d s => rs#d <- (arith_eval_fr i rs#s)