aarch64/Asmblock: Merge RR, RF, FR, FF, RspRsp

1 files changed, 41 insertions, 85 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 7373e926..be3389c4 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -306,7 +306,7 @@ Inductive arith_comparison_p : Type :=
   | Ptstimm (sz: isize) (n: Z)                        (**r and, then set flags *)
 .
 
-Inductive arith_rr : Type :=
+Inductive arith_pp : Type :=
   (** Move integer register *)
   | Pmov
   (** PC-relative addressing *)
@@ -323,6 +323,24 @@ Inductive arith_rr : Type :=
   | Prev (sz: isize)                            (**r reverse bytes *)
   | Prev16 (sz: isize)                          (**r reverse bytes in each 16-bit word *)
 *)
+  (** Floating-point move *)
+  | Pfmov
+  (** Floating-point conversions *)
+  | Pfcvtds                                           (**r convert float32 to float64 *)
+  | Pfcvtsd                                           (**r convert float64 to float32 *)
+  (** Floating-point arithmetic *)
+  | Pfabs (sz: fsize)                                 (**r absolute value *)
+  | Pfneg (sz: fsize)                                 (**r negation *)
+  (* Pfsqrt is not used in the semantics of aarch64/asm
+  | Pfsqrt (sz: fsize)                                (**r square root *) *)
+  (** Floating-point conversions *)
+  | Pscvtf (fsz: fsize) (isz: isize)                  (**r convert signed int to float *)
+  | Pucvtf (fsz: fsize) (isz: isize)                  (**r convert unsigned int to float *)
+  | Pfcvtzs (isz: isize) (fsz: fsize)                 (**r convert float to signed int *)
+  | Pfcvtzu (isz: isize) (fsz: fsize)                 (**r convert float to unsigned int *)
+  (** Integer arithmetic, immediate *)
+  | Paddimm (sz: isize) (n: Z)                        (**r addition *)
+  | Psubimm (sz: isize) (n: Z)                        (**r subtraction *)
 .
 
 Inductive arith_comparison_w_r0r : Type :=
@@ -347,34 +365,11 @@ Inductive arith_comparison_rr : Type :=
   | Pcmnext (x: extend_op)                      (**r int64-int32 cmn *)
 .
 
-Inductive arith_ff : Type :=
-  (** Floating-point move *)
-  | Pfmov
-  (** Floating-point conversions *)
-  | Pfcvtds                                           (**r convert float32 to float64 *)
-  | Pfcvtsd                                           (**r convert float64 to float32 *)
-  (** Floating-point arithmetic *)
-  | Pfabs (sz: fsize)                                 (**r absolute value *)
-  | Pfneg (sz: fsize)                                 (**r negation *)
-  (* Pfsqrt is not used in the semantics of aarch64/asm
-  | Pfsqrt (sz: fsize)                                (**r square root *) *)
-.
-
 Inductive arith_comparison_ff : Type :=
   (** Floating-point comparison *)
   | Pfcmp (sz: fsize)                                 (**r compare [r1] and [r2] *)
 .
 
-(* TODO? Can arith_fr and arith_rf be collapsed into one type
- * (switching the argument order when evaluating for one of them)?
- * Or must these be two different types since the target register is
- * either an integer or a floating point register? *)
-Inductive arith_fr : Type :=
-  (** Floating-point conversions *)
-  | Pscvtf (fsz: fsize) (isz: isize)                  (**r convert signed int to float *)
-  | Pucvtf (fsz: fsize) (isz: isize)                  (**r convert unsigned int to float *)
-.
-
 Inductive arith_sw_fr0 : Type :=
   (** Floating-point move *)
   | PfmoviSW                                          (**r copy int reg to FP reg *)
@@ -385,12 +380,6 @@ Inductive arith_dx_fr0 : Type :=
   | PfmoviDX                                          (**r copy int reg to FP reg *)
 .
 
-Inductive arith_rf : Type := 
-  (** Floating-point conversions *)
-  | Pfcvtzs (isz: isize) (fsz: fsize)                 (**r convert float to signed int *)
-  | Pfcvtzu (isz: isize) (fsz: fsize)                 (**r convert float to unsigned int *)
-.
-
 Inductive arith_rrr : Type :=
   (** Variable shifts *)
   | Pasrv (sz: isize)                                 (**r arithmetic right shift *)
@@ -456,12 +445,6 @@ Inductive arith_c_fff : Type :=
   | Pfsel
 .
 
-Inductive arith_rsprsp : Type :=
-  (** Integer arithmetic, immediate *)
-  | Paddimm (sz: isize) (n: Z)                      (**r addition *)
-  | Psubimm (sz: isize) (n: Z)                      (**r subtraction *)
-.
-
 Inductive arith_w_rr0 : Type :=
   (** Logical, immediate *)
   | PandimmW (n: Z)                                 (**r and *)
@@ -523,8 +506,7 @@ Inductive arith_aaffff : Type :=
 Inductive ar_instruction : Type :=
   | PArithP (i : arith_p) (rd : preg)
   | PArithCP (i : arith_c_p) (rd : preg) (c : testcond)
-  | PArithRR (i : arith_rr) (rd rs : ireg)
-  | PArithRF (i : arith_rf) (rd : ireg) (rs : freg)
+  | PArithPP (i : arith_pp) (rd rs : preg)
   | PArithRRR (i : arith_rrr) (rd r1 r2 : ireg)
   | PArithCRRR (i : arith_c_rrr) (rd r1 r2 : ireg) (c : testcond)
   | PArithWRR0R (i : arith_w_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
@@ -532,11 +514,8 @@ Inductive ar_instruction : Type :=
   | PArithWRR0 (i : arith_w_rr0) (rd : ireg) (r1 : ireg0)
   | PArithXRR0 (i : arith_x_rr0) (rd : ireg) (r1 : ireg0)
   | PArithRspRspR (i : arith_rsprspr) (rd r1 : iregsp) (r2 : ireg)
-  | 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)
-  | PArithFF (i : arith_ff) (rd rs : freg)
-  | PArithFR (i : arith_fr) (rd : freg) (rs : ireg)
   | PArithSWFR0 (i : arith_sw_fr0) (rd : freg) (rs : ireg0)
   | PArithDXFR0 (i : arith_dx_fr0) (rd : freg) (rs : ireg0)
   | PArithFFF (i : arith_fff) (rd r1 r2 : freg)
@@ -1303,10 +1282,9 @@ Definition arith_eval_c_p (i : arith_c_p) (c : option bool) : val :=
     end)
   end.
 
-Definition arith_eval_rr i v :=
+Definition arith_eval_pp i v :=
   match i with
   | Pmov => v
-  (* XXX change from ge to lk *)
   | 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)
@@ -1316,11 +1294,13 @@ Definition arith_eval_rr i v :=
   | Pubfiz X r s => Val.shll (Val.zero_ext_l s v) (Vint r)
   | Pubfx W r s => Val.zero_ext s (Val.shru v (Vint r))
   | Pubfx X r s => Val.zero_ext_l s (Val.shrlu v (Vint r))
-  end.
-
-
-Definition arith_eval_rf i v :=
-  match i with
+  | Pfmov => v
+  | Pfcvtds => Val.floatofsingle v
+  | Pfcvtsd => Val.singleoffloat v
+  | Pfabs S => Val.absfs v
+  | Pfabs D => Val.absf v
+  | Pfneg S => Val.negfs v
+  | Pfneg D => Val.negf v
   | Pfcvtzs W S => Val.maketotal (Val.intofsingle v)
   | Pfcvtzs W D => Val.maketotal (Val.intoffloat v)
   | Pfcvtzs X S => Val.maketotal (Val.longofsingle v)
@@ -1329,6 +1309,18 @@ Definition arith_eval_rf i v :=
   | Pfcvtzu W D => Val.maketotal (Val.intuoffloat v)
   | Pfcvtzu X S => Val.maketotal (Val.longuofsingle v)
   | Pfcvtzu X D => Val.maketotal (Val.longuoffloat v)
+  | Paddimm W n => Val.add v (Vint (Int.repr n))
+  | Paddimm X n => Val.addl v (Vlong (Int64.repr n))
+  | Psubimm W n => Val.sub v (Vint (Int.repr n))
+  | Psubimm X n => Val.subl v (Vlong (Int64.repr n))
+  | Pscvtf S W => Val.maketotal (Val.singleofint v)
+  | Pscvtf D W => Val.maketotal (Val.floatofint v)
+  | Pscvtf S X => Val.maketotal (Val.singleoflong v)
+  | Pscvtf D X => Val.maketotal (Val.floatoflong v)
+  | Pucvtf S W => Val.maketotal (Val.singleofintu v)
+  | Pucvtf D W => Val.maketotal (Val.floatofintu v)
+  | Pucvtf S X => Val.maketotal (Val.singleoflongu v)
+  | Pucvtf D X => Val.maketotal (Val.floatoflongu v)
   end.
 
 Definition arith_eval_rrr i v1 v2 :=
@@ -1407,14 +1399,6 @@ Definition arith_eval_rsprspr i v1 v2 :=
   | Psubext x => Val.subl v2 (eval_extend v2 x)
   end.
 
-Definition arith_eval_rsprsp i v :=
-  match i with
-  | Paddimm W n => Val.add v (Vint (Int.repr n))
-  | Paddimm X n => Val.addl v (Vlong (Int64.repr n))
-  | Psubimm W n => Val.sub v (Vint (Int.repr n))
-  | Psubimm X n => Val.subl v (Vlong (Int64.repr n))
-  end.
-
 (* obtain v3 by rs##r3 *)
 Definition arith_eval_w_arrrr0 i v1 v2 v3 :=
   match i with
@@ -1429,29 +1413,6 @@ Definition arith_eval_x_arrrr0 i v1 v2 v3 :=
   | PmsubX => Val.subl v3 (Val.mull v1 v2)
   end.
 
-Definition arith_eval_ff i v :=
-  match i with
-  | Pfmov => v
-  | Pfcvtds => Val.floatofsingle v
-  | Pfcvtsd => Val.singleoffloat v
-  | Pfabs S => Val.absfs v
-  | Pfabs D => Val.absf v
-  | Pfneg S => Val.negfs v
-  | Pfneg D => Val.negf v
-  end.
-
-Definition arith_eval_fr i v :=
-  match i with
-  | Pscvtf S W => Val.maketotal (Val.singleofint v)
-  | Pscvtf D W => Val.maketotal (Val.floatofint v)
-  | Pscvtf S X => Val.maketotal (Val.singleoflong v)
-  | Pscvtf D X => Val.maketotal (Val.floatoflong v)
-  | Pucvtf S W => Val.maketotal (Val.singleofintu v)
-  | Pucvtf D W => Val.maketotal (Val.floatofintu v)
-  | Pucvtf S X => Val.maketotal (Val.singleoflongu v)
-  | Pucvtf D X => Val.maketotal (Val.floatoflongu v)
-  end.
-
 (* obtain v via rs##r1 *)
 Definition arith_eval_sw_fr0 i v :=
   match i with
@@ -1533,8 +1494,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithP i d => rs#d <- (arith_eval_p i)
   | PArithCP i d c => rs#d <- (arith_eval_c_p 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)
+  | PArithPP i d s => rs#d <- (arith_eval_pp i rs#s)
   | PArithRRR i d s1 s2 => rs#d <- (arith_eval_rrr i rs#s1 rs#s2)
   | PArithCRRR i d s1 s2 c => rs#d <- (arith_eval_c_rrr i rs#s1 rs#s2 (eval_testcond c rs))
 
@@ -1545,14 +1505,10 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithXRR0 i d s => rs#d <- (arith_eval_x_rr0 i rs###s)
 
   | PArithRspRspR i d s1 s2 => rs#d <- (arith_eval_rsprspr i rs#s1 rs#s2)
-  | PArithRspRsp i d s => rs#d <- (arith_eval_rsprsp i rs#s)
 
   | 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)
 
-  | PArithFF i d s => rs#d <- (arith_eval_ff i rs#s)
-  | PArithFR i d s => rs#d <- (arith_eval_fr i rs#s)
-
   | PArithSWFR0 i d s => rs#d <- (arith_eval_sw_fr0 i rs##s)
   | PArithDXFR0 i d s => rs#d <- (arith_eval_dx_fr0 i rs###s)