unifying arith_w_rr0r and arith_x_rr0r into arith_rr0r

1 files changed, 42 insertions, 51 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 81c55415..216f836d 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -406,31 +406,19 @@ Inductive arith_c_ppp : Type :=
   | Pfsel
 .
 
-Inductive arith_w_rr0r : Type :=
+Inductive arith_rr0r : Type :=
   (** Integer arithmetic, shifted register *)
-  | PaddW (s: shift_op)                               (**r addition *)
-  | PsubW (s: shift_op)                               (**r subtraction *)
+  | Padd (sz:isize) (s: shift_op)                               (**r addition *)
+  | Psub (sz:isize) (s: shift_op)                               (**r subtraction *)
   (** Logical, shifted register *)
-  | PandW (s: shift_op)                               (**r and *)
-  | PbicW (s: shift_op)                               (**r and-not *)
-  | PeonW (s: shift_op)                               (**r xor-not *)
-  | PeorW (s: shift_op)                               (**r xor *)
-  | PorrW (s: shift_op)                               (**r or *)
-  | PornW (s: shift_op)                               (**r or-not *)
+  | Pand (sz:isize) (s: shift_op)                               (**r and *)
+  | Pbic (sz:isize) (s: shift_op)                               (**r and-not *)
+  | Peon (sz:isize) (s: shift_op)                               (**r xor-not *)
+  | Peor (sz:isize) (s: shift_op)                               (**r xor *)
+  | Porr (sz:isize) (s: shift_op)                               (**r or *)
+  | Porn (sz:isize) (s: shift_op)                               (**r or-not *)
 .
 
-Inductive arith_x_rr0r : Type :=
-  (** Integer arithmetic, shifted register *)
-  | PaddX (s: shift_op)                               (**r addition *)
-  | PsubX (s: shift_op)                               (**r subtraction *)
-  (** Logical, shifted register *)
-  | PandX (s: shift_op)                               (**r and *)
-  | PbicX (s: shift_op)                               (**r and-not *)
-  | PeonX (s: shift_op)                               (**r xor-not *)
-  | PeorX (s: shift_op)                               (**r xor *)
-  | PorrX (s: shift_op)                               (**r or *)
-  | PornX (s: shift_op)                               (**r or-not *)
-.
 
 Inductive arith_w_rr0 : Type :=
   (** Logical, immediate *)
@@ -497,8 +485,7 @@ Inductive ar_instruction : Type :=
   | PArithPP (i : arith_pp) (rd rs : preg)
   | PArithPPP (i : arith_ppp) (rd r1 r2 : preg)
   | PArithCPPP (i : arith_c_ppp) (rd r1 r2 : preg) (c : testcond)
-  | PArithWRR0R (i : arith_w_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
-  | PArithXRR0R (i : arith_x_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
+  | 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)
@@ -763,17 +750,15 @@ Definition genv := Genv.t fundef unit.
 (** The value of an [ireg0] is either the value of the integer register,
     or 0. *)
 
-Definition ir0w (rs: regset) (r: ireg0) : val :=
-  match r with RR0 r => rs (IR r) | XZR => Vint Int.zero end.
-Definition ir0x (rs: regset) (r: ireg0) : val :=
-  match r with RR0 r => rs (IR r) | XZR => Vlong Int64.zero end.
+Definition ir0 (is:isize) (rs: regset) (r: ireg0) : val :=
+  match r with RR0 r => rs (IR r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end.
 
 (** Concise notations for accessing and updating the values of registers. *)
 
 Notation "a # b" := (a b) (at level 1, only parsing) : asm.
 Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
-Notation "a ## b" := (ir0w a b) (at level 1, only parsing) : asm.
-Notation "a ### b" := (ir0x a b) (at level 1, only parsing) : asm.
+Notation "a ## b" := (ir0 W a b) (at level 1, only parsing) : asm.
+Notation "a ### b" := (ir0 X a b) (at level 1, only parsing) : asm.
 
 Open Scope asm.
 
@@ -1350,30 +1335,37 @@ Definition arith_eval_c_ppp (i : arith_c_ppp) (v1 v2 : val) (c : option bool) :=
     end)
   end.
 
-(* obtain v1 by rs##r1 *)
-Definition arith_eval_w_rr0r i v1 v2 :=
+Definition arith_rr0r_isize (i: arith_rr0r) :=
   match i with
-  | PaddW s => Val.add v1 (eval_shift_op_int v2 s)
-  | PsubW s => Val.sub v1 (eval_shift_op_int v2 s)
-  | PandW s => Val.and v1 (eval_shift_op_int v2 s)
-  | PbicW s => Val.and v1 (Val.notint (eval_shift_op_int v2 s))
-  | PeonW s => Val.xor v1 (Val.notint (eval_shift_op_int v2 s))
-  | PeorW s => Val.xor v1 (eval_shift_op_int v2 s)
-  | PorrW s => Val.or v1 (eval_shift_op_int v2 s)
-  | PornW s => Val.or v1 (Val.notint (eval_shift_op_int v2 s))
+  | Padd is _ => is
+  | Psub is _ => is
+  | Pand is _ => is
+  | Pbic is _ => is
+  | Peon is _ => is
+  | Peor is _ => is
+  | Porr is _ => is
+  | Porn is _ => is
   end.
 
-(* obtain v1 by rs###r1 *)
-Definition arith_eval_x_rr0r i v1 v2 :=
+(* obtain v1 by [ir0 (arith_rr0r_isize i) rs s1] *)
+Definition arith_eval_rr0r i v1 v2 :=
   match i with
-  | PaddX s => Val.addl v1 (eval_shift_op_long v2 s)
-  | PsubX s => Val.subl v1 (eval_shift_op_long v2 s)
-  | PandX s => Val.andl v1 (eval_shift_op_long v2 s)
-  | PbicX s => Val.andl v1 (Val.notl (eval_shift_op_long v2 s))
-  | PeonX s => Val.xorl v1 (Val.notl (eval_shift_op_long v2 s))
-  | PeorX s => Val.xorl v1 (eval_shift_op_long v2 s)
-  | PorrX s => Val.orl v1 (eval_shift_op_long v2 s)
-  | PornX s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s))
+  | Padd W s => Val.add v1 (eval_shift_op_int v2 s)
+  | Padd X s => Val.addl v1 (eval_shift_op_long v2 s)
+  | Psub W s => Val.sub v1 (eval_shift_op_int v2 s)
+  | Psub X s => Val.subl v1 (eval_shift_op_long v2 s)
+  | Pand W s => Val.and v1 (eval_shift_op_int v2 s)
+  | Pand X s => Val.andl v1 (eval_shift_op_long v2 s)
+  | Pbic W s => Val.and v1 (Val.notint (eval_shift_op_int v2 s))
+  | Pbic X s => Val.andl v1 (Val.notl (eval_shift_op_long v2 s))
+  | Peon W s => Val.xor v1 (Val.notint (eval_shift_op_int v2 s))
+  | Peon X s => Val.xorl v1 (Val.notl (eval_shift_op_long v2 s))
+  | Peor W s => Val.xor v1 (eval_shift_op_int v2 s)
+  | Peor X s => Val.xorl v1 (eval_shift_op_long v2 s)
+  | Porr W s => Val.or v1 (eval_shift_op_int v2 s)
+  | Porr X s => Val.orl v1 (eval_shift_op_long v2 s)
+  | Porn W s => Val.or v1 (Val.notint (eval_shift_op_int v2 s))
+  | Porn X s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s))
   end.
 
 (* obtain v by rs##r1 *)
@@ -1465,8 +1457,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithPPP i d s1 s2 => rs#d <- (arith_eval_ppp i rs#s1 rs#s2)
   | PArithCPPP i d s1 s2 c => rs#d <- (arith_eval_c_ppp i rs#s1 rs#s2 (eval_testcond c rs))
 
-  | PArithWRR0R i d s1 s2 => rs#d <- (arith_eval_w_rr0r i rs##s1 rs#s2)
-  | PArithXRR0R i d s1 s2 => rs#d <- (arith_eval_x_rr0r i rs###s1 rs#s2)
+  | 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)