merging arith_comparison_w_r0r and arith_comparison_x_r0r into arith_comparison_r0r

1 files changed, 20 insertions, 28 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 216f836d..b37b6e27 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -344,20 +344,12 @@ Inductive arith_pp : Type :=
   | Psubimm (sz: isize) (n: Z)                        (**r subtraction *)
 .
 
-Inductive arith_comparison_w_r0r : Type :=
+Inductive arith_comparison_r0r : Type :=
   (** Integer arithmetic, shifted register *)
-  | PcmpW (s: shift_op)             (**r compare *)
-  | PcmnW (s: shift_op)             (**r compare negative *)
+  | Pcmp (is:isize) (s: shift_op)             (**r compare *)
+  | Pcmn (is:isize) (s: shift_op)             (**r compare negative *)
   (** Logical, shifted register *)
-  | PtstW (s: shift_op)             (**r and, then set flags *)
-.
-
-Inductive arith_comparison_x_r0r : Type :=
-  (** Integer arithmetic, shifted register *)
-  | PcmpX (s: shift_op)             (**r compare *)
-  | PcmnX (s: shift_op)             (**r compare negative *)
-  (** Logical, shifted register *)
-  | PtstX (s: shift_op)             (**r and, then set flags *)
+  | Ptst (is:isize) (s: shift_op)             (**r and, then set flags *)
 .
 
 Inductive arith_comparison_pp : Type :=
@@ -498,8 +490,7 @@ Inductive ar_instruction : Type :=
   (* Pfnmadd and Pfnmsub are currently not used by the semantics of aarch64/Asm
   | PArithAAPPPP (i : arith_aapppp) (rd r1 r2 r3 : preg) *)
   | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : preg)
-  | PArithComparisonWR0R (i : arith_comparison_w_r0r) (r1 : ireg0) (r2 : ireg)
-  | PArithComparisonXR0R (i : arith_comparison_x_r0r) (r1 : ireg0) (r2 : ireg)
+  | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg)
   | PArithComparisonP (i : arith_comparison_p) (r1 : preg)
 .
 
@@ -1423,18 +1414,21 @@ Definition arith_prepare_comparison_pp i (v1 v2 : val) :=
   | Pfcmp _ => (v1, v2)
   end.
 
-Definition arith_prepare_comparison_w_r0r i v1 v2 :=
+Definition arith_comparison_r0r_isize i :=
   match i with
-  | PcmpW s => (v1, (eval_shift_op_int v2 s))
-  | PcmnW s => (v1, (Val.neg (eval_shift_op_int v2 s)))
-  | PtstW s => ((Val.and v1 (eval_shift_op_int v2 s)), (Vint Int.zero))
+  | Pcmp is _ => is
+  | Pcmn is _ => is
+  | Ptst is _ => is
   end.
 
-Definition arith_prepare_comparison_x_r0r i v1 v2 :=
+Definition arith_prepare_comparison_r0r i v1 v2 :=
   match i with
-  | PcmpX s => (v1, (eval_shift_op_long v2 s))
-  | PcmnX s => (v1, (Val.negl (eval_shift_op_long v2 s)))
-  | PtstX s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero))
+  | Pcmp W s => (v1, (eval_shift_op_int v2 s))
+  | Pcmp X s => (v1, (eval_shift_op_long v2 s))
+  | Pcmn W s => (v1, (Val.neg (eval_shift_op_int v2 s)))
+  | Pcmn X s => (v1, (Val.negl (eval_shift_op_long v2 s)))
+  | Ptst W s => ((Val.and v1 (eval_shift_op_int v2 s)), (Vint Int.zero))
+  | Ptst X s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero))
   end.
 
 Definition arith_prepare_comparison_p i v :=
@@ -1477,12 +1471,10 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
       | Pfcmp S => compare_single rs v1 v2
       | Pfcmp D => compare_float rs v1 v2
       end)
-  | PArithComparisonWR0R i s1 s2 =>
-    let (v1, v2) := arith_prepare_comparison_w_r0r i rs##s1 rs#s2 in
-      compare_int rs v1 v2
-  | PArithComparisonXR0R i s1 s2 =>
-    let (v1, v2) := arith_prepare_comparison_x_r0r i rs###s1 rs#s2 in
-      compare_long rs v1 v2
+  | PArithComparisonR0R i s1 s2 =>
+    let is := arith_comparison_r0r_isize i in
+    let (v1, v2) := arith_prepare_comparison_r0r i (ir0 is rs s1) rs#s2 in
+    (if is (* is W *) then compare_int else compare_long) rs v1 v2
   | PArithComparisonP i s =>
     let (v1, v2) := arith_prepare_comparison_p i rs#s in
       (match i with