Asmblock: PArithComparisonRI -> PArithComparisonR

Reflects the fact that immediates are not really relevant as scheduling
dependencies.

1 files changed, 17 insertions, 17 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index ae23cb93..c18d30b9 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -381,12 +381,12 @@ Inductive arith_name_rf : Type :=
 .
 
 
-Inductive arith_name_comparison_ri : Type :=
+Inductive arith_name_comparison_r : Type :=
   (** Integer arithmetic, immediate *)
-  | Pcmpimm (sz: isize)                               (**r compare *)
-  | Pcmnimm (sz: isize)                               (**r compare negative *)
+  | Pcmpimm (sz: isize) (n: Z)                        (**r compare *)
+  | Pcmnimm (sz: isize) (n: Z)                        (**r compare negative *)
   (** Logical, immediate *)
-  | Ptstimm (sz: isize)                               (**r and, then set flags *)
+  | Ptstimm (sz: isize) (n: Z)                        (**r and, then set flags *)
 .
 
 Inductive arith_name_ff32 : Type :=
@@ -554,7 +554,7 @@ Inductive ar_instruction : Type :=
   | PArithComparisonRR (i : arith_name_comparison_rr) (r1 r2 : ireg)
   | PArithComparisonWR0R (i : arith_name_comparison_w_r0r) (r1 : ireg0) (r2 : ireg)
   | PArithComparisonXR0R (i : arith_name_comparison_x_r0r) (r1 : ireg0) (r2 : ireg)
-  | PArithComparisonRI (i : arith_name_comparison_ri) (r1 : ireg) (n : Z)
+  | PArithComparisonR (i : arith_name_comparison_r) (r1 : ireg)
   | PArithComparisonF (i: arith_name_comparison_f) (r1 : freg)
   | PArithComparisonFF (i : arith_name_comparison_ff) (rd rs : freg)
 .
@@ -1496,14 +1496,14 @@ Definition arith_prepare_comparison_x_r0r n v1 v2 :=
   | PtstX s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero))
   end.
 
-Definition arith_prepare_comparison_ri n v i :=
-  match n with
-  | Pcmpimm W => (v, (Vint (Int.repr i)))
-  | Pcmpimm X => (v, (Vlong (Int64.repr i)))
-  | Pcmnimm W => (v, (Vint (Int.neg (Int.repr i))))
-  | Pcmnimm X => (v, (Vlong (Int64.neg (Int64.repr i))))
-  | Ptstimm W => ((Val.and v (Vint (Int.repr i))), (Vint Int.zero))
-  | Ptstimm X => ((Val.andl v (Vlong (Int64.repr i))), (Vlong Int64.zero))
+Definition arith_prepare_comparison_r i v :=
+  match i with
+  | Pcmpimm W n => (v, (Vint (Int.repr n)))
+  | Pcmpimm X n => (v, (Vlong (Int64.repr n)))
+  | Pcmnimm W n => (v, (Vint (Int.neg (Int.repr n))))
+  | Pcmnimm X n => (v, (Vlong (Int64.neg (Int64.repr n))))
+  | Ptstimm W n => ((Val.and v (Vint (Int.repr n))), (Vint Int.zero))
+  | Ptstimm X n => ((Val.andl v (Vlong (Int64.repr n))), (Vlong Int64.zero))
   end.
 
 (* Without val annotation unification fails *)
@@ -1557,11 +1557,11 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithComparisonXR0R n s1 s2 =>
     let (v1, v2) := arith_prepare_comparison_x_r0r n rs###s1 rs#s2 in
       compare_long rs v1 v2
-  | PArithComparisonRI n s i =>
-    let (v1, v2) := arith_prepare_comparison_ri n rs#s i in
+  | PArithComparisonR n s =>
+    let (v1, v2) := arith_prepare_comparison_r n rs#s in
       (match n with
-      | Pcmpimm W | Pcmnimm W | Ptstimm W => compare_int rs v1 v2
-      | Pcmpimm X | Pcmnimm X | Ptstimm X => compare_long rs v1 v2
+      | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int rs v1 v2
+      | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long rs v1 v2
       end)
   | PArithComparisonF n s =>
     let (v1, v2) := arith_prepare_comparison_f n rs#s in