intermediate comparison function on arit_comparison_*

1 files changed, 17 insertions, 11 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index b37b6e27..193941aa 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -1443,6 +1443,21 @@ Definition arith_prepare_comparison_p i v :=
   | Pfcmp0 D => (v, (Vfloat Float.zero))
   end.
 
+Definition arith_comparison_pp_compare i :=
+  match i with
+  | Pcmpext _ | Pcmnext _ => compare_long
+  | Pfcmp S => compare_single
+  | Pfcmp D => compare_float
+  end.
+
+Definition arith_comparison_p_compare i :=
+   match i with
+   | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int
+   | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long
+   | Pfcmp0 S => compare_single
+   | Pfcmp0 D => compare_float
+   end.
+
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithP i d => rs#d <- (arith_eval_p i)
@@ -1466,23 +1481,14 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
 
   | PArithComparisonPP i s1 s2 =>
     let (v1, v2) := arith_prepare_comparison_pp i rs#s1 rs#s2 in
-      (match i with
-      | Pcmpext _ | Pcmnext _ => compare_long rs v1 v2
-      | Pfcmp S => compare_single rs v1 v2
-      | Pfcmp D => compare_float rs v1 v2
-      end)
+    arith_comparison_pp_compare i 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
-      | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int rs v1 v2
-      | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long rs v1 v2
-      | Pfcmp0 S => compare_single rs v1 v2
-      | Pfcmp0 D => compare_float rs v1 v2
-      end)
+    arith_comparison_p_compare i rs v1 v2
   end.
 
 (* basic exec *)