Merge PArith(W|X)RR0 and PArith(W|X)ARRRR0

1 files changed, 30 insertions, 47 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 2d0eeb11..81df119d 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -412,31 +412,17 @@ Inductive arith_rr0r : Type :=
 .
 
 
-Inductive arith_w_rr0 : Type :=
+Inductive arith_rr0 : Type :=
   (** Logical, immediate *)
-  | PandimmW (n: Z)                                 (**r and *)
-  | PeorimmW (n: Z)                                 (**r xor *)
-  | PorrimmW (n: Z)                                 (**r or *)
+  | Pandimm (sz: isize) (n: Z)                     (**r and *)
+  | Peorimm (sz: isize) (n: Z)                     (**r xor *)
+  | Porrimm (sz: isize) (n: Z)                     (**r or *)
 .
 
-Inductive arith_x_rr0 : Type :=
-  (** Logical, immediate *)
-  | PandimmX (n: Z)                                 (**r and *)
-  | PeorimmX (n: Z)                                 (**r xor *)
-  | PorrimmX (n: Z)                                 (**r or *)
-.
-
-
-Inductive arith_w_arrrr0 : Type :=
-  (** Integer multiply/divide *)
-  | PmaddW                                          (**r multiply-add *)
-  | PmsubW                                          (**r multiply-sub *)
-.
-
-Inductive arith_x_arrrr0 : Type :=
+Inductive arith_arrrr0 : Type :=
   (** Integer multiply/divide *)
-  | PmaddX                                          (**r multiply-add *)
-  | PmsubX                                          (**r multiply-sub *)
+  | Pmadd (sz: isize)                               (**r multiply-add *)
+  | Pmsub (sz: isize)                               (**r multiply-sub *)
 .
 
 Inductive arith_appp : Type :=
@@ -478,10 +464,8 @@ Inductive ar_instruction : Type :=
   | PArithPPP (i : arith_ppp) (rd r1 r2 : preg)
   | PArithCPPP (i : arith_c_ppp) (rd r1 r2 : preg) (c : testcond)
   | PArithRR0R (i : arith_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
-  | PArithWRR0 (i : arith_w_rr0) (rd : ireg) (r1 : ireg0)
-  | PArithXRR0 (i : arith_x_rr0) (rd : ireg) (r1 : ireg0)
-  | PArithWARRRR0 (i : arith_w_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
-  | PArithXARRRR0 (i : arith_x_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
+  | PArithRR0 (i : arith_rr0) (rd : ireg) (r1 : ireg0)
+  | PArithARRRR0 (i : arith_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
   | PArithSWFR0 (i : arith_sw_fr0) (rd : freg) (rs : ireg0)
   | PArithDXFR0 (i : arith_dx_fr0) (rd : freg) (rs : ireg0)
   | PArithAPPP (i : arith_appp) (rd r1 r2 : preg)
@@ -1364,34 +1348,34 @@ Definition arith_eval_rr0r i v1 v2 :=
   | Porn X s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s))
   end.
 
-(* obtain v by rs##r1 *)
-Definition arith_eval_w_rr0 i v :=
+Definition arith_rr0_isize (i : arith_rr0) :=
   match i with
-  | PandimmW n => Val.and v (Vint (Int.repr n))
-  | PeorimmW n => Val.xor v (Vint (Int.repr n))
-  | PorrimmW n => Val.or v (Vint (Int.repr n))
+  | Pandimm is _ | Peorimm is _ | Porrimm is _ => is
   end.
 
-(* obtain v by rs###r1 *)
-Definition arith_eval_x_rr0 i v :=
+(* obtain v by [ir0 (arith_rr0_isize i) rs s] *)
+Definition arith_eval_rr0 i v :=
   match i with
-  | PandimmX n => Val.andl v (Vlong (Int64.repr n))
-  | PeorimmX n => Val.xorl v (Vlong (Int64.repr n))
-  | PorrimmX n => Val.orl v (Vlong (Int64.repr n))
+  | Pandimm W n => Val.and v (Vint (Int.repr n))
+  | Pandimm X n => Val.andl v (Vlong (Int64.repr n))
+  | Peorimm W n => Val.xor v (Vint (Int.repr n))
+  | Peorimm X n => Val.xorl v (Vlong (Int64.repr n))
+  | Porrimm W n => Val.or v (Vint (Int.repr n))
+  | Porrimm X n => Val.orl v (Vlong (Int64.repr n))
   end.
 
-(* obtain v3 by rs##r3 *)
-Definition arith_eval_w_arrrr0 i v1 v2 v3 :=
+Definition arith_arrrr0_isize (i : arith_arrrr0) :=
   match i with
-  | PmaddW => Val.add v3 (Val.mul v1 v2)
-  | PmsubW => Val.sub v3 (Val.mul v1 v2)
+  | Pmadd is | Pmsub is => is
   end.
 
-(* obtain v3 by rs###r3 *)
-Definition arith_eval_x_arrrr0 i v1 v2 v3 :=
+(* obtain v3 by [ir0 (arith_arrrr0_isize i) rs s3] *)
+Definition arith_eval_arrrr0 i v1 v2 v3 :=
   match i with
-  | PmaddX => Val.addl v3 (Val.mull v1 v2)
-  | PmsubX => Val.subl v3 (Val.mull v1 v2)
+  | Pmadd W => Val.add v3 (Val.mul v1 v2)
+  | Pmadd X => Val.addl v3 (Val.mull v1 v2)
+  | Pmsub W => Val.sub v3 (Val.mul v1 v2)
+  | Pmsub X => Val.subl v3 (Val.mull v1 v2)
   end.
 
 (* obtain v via rs##r1 *)
@@ -1473,11 +1457,10 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
 
   | PArithRR0R i d s1 s2 => rs#d <- (arith_eval_rr0r i (ir0 (arith_rr0r_isize i) rs s1) rs#s2)
 
-  | PArithWRR0 i d s => rs#d <- (arith_eval_w_rr0 i rs##s)
-  | PArithXRR0 i d s => rs#d <- (arith_eval_x_rr0 i rs###s)
+  | PArithRR0 i d s => rs#d <- (arith_eval_rr0 i (ir0 (arith_rr0_isize 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)
+  | PArithARRRR0 i d s1 s2 s3 =>
+    rs#d <- (arith_eval_arrrr0 i rs#s1 rs#s2 (ir0 (arith_arrrr0_isize i) rs s3))
 
   | 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)