Asmblock: Use i as variable name for instructions

1 files changed, 73 insertions, 73 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 14613fd3..c8172d1c 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -1308,8 +1308,8 @@ Definition arith_eval_c_r (i : arith_name_c_r) (c : option bool) : val :=
     end)
   end.
 
-Definition arith_eval_rr n v :=
-  match n with
+Definition arith_eval_rr i v :=
+  match i with
   | Pmov => v
   (* XXX change from ge to lk *)
   | Paddadr id ofs => Val.addl v (symbol_low lk id ofs)
@@ -1324,8 +1324,8 @@ Definition arith_eval_rr n v :=
   end.
 
 
-Definition arith_eval_rf n v :=
-  match n with
+Definition arith_eval_rf i v :=
+  match i with
   | Pfcvtzs W S => Val.maketotal (Val.intofsingle v)
   | Pfcvtzs W D => Val.maketotal (Val.intoffloat v)
   | Pfcvtzs X S => Val.maketotal (Val.longofsingle v)
@@ -1336,8 +1336,8 @@ Definition arith_eval_rf n v :=
   | Pfcvtzu X D => Val.maketotal (Val.longuoffloat v)
   end.
 
-Definition arith_eval_rrr n v1 v2 :=
-  match n with
+Definition arith_eval_rrr i v1 v2 :=
+  match i with
   | Pasrv W => Val.shr v1 v2
   | Pasrv X => Val.shrl v1 v2
   | Plslv W => Val.shl v1 v2
@@ -1365,8 +1365,8 @@ Definition arith_eval_c_rrr (i : arith_name_c_rrr) (v1 v2 : val) (c : option boo
   end.
 
 (* obtain v1 by rs##r1 *)
-Definition arith_eval_w_rr0r n v1 v2 :=
-  match n with
+Definition arith_eval_w_rr0r i v1 v2 :=
+  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)
@@ -1378,8 +1378,8 @@ Definition arith_eval_w_rr0r n v1 v2 :=
   end.
 
 (* obtain v1 by rs###r1 *)
-Definition arith_eval_x_rr0r n v1 v2 :=
-  match n with
+Definition arith_eval_x_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)
@@ -1406,8 +1406,8 @@ Definition arith_eval_x_rr0 i v :=
   | PorrimmX n => Val.orl v (Vlong (Int64.repr n))
   end.
 
-Definition arith_eval_rsprspr n v1 v2 :=
-  match n with
+Definition arith_eval_rsprspr i v1 v2 :=
+  match i with
   | Paddext x => Val.addl v1 (eval_extend v2 x)
   | Psubext x => Val.subl v2 (eval_extend v2 x)
   end.
@@ -1421,21 +1421,21 @@ Definition arith_eval_rsprsp i v :=
   end.
 
 (* obtain v3 by rs##r3 *)
-Definition arith_eval_w_arrrr0 n v1 v2 v3 :=
-  match n with
+Definition arith_eval_w_arrrr0 i v1 v2 v3 :=
+  match i with
   | PmaddW => Val.add v3 (Val.mul v1 v2)
   | PmsubW => Val.sub v3 (Val.mul v1 v2)
   end.
 
 (* obtain v3 by rs###r3 *)
-Definition arith_eval_x_arrrr0 n v1 v2 v3 :=
-  match n with
+Definition arith_eval_x_arrrr0 i v1 v2 v3 :=
+  match i with
   | PmaddX => Val.addl v3 (Val.mull v1 v2)
   | PmsubX => Val.subl v3 (Val.mull v1 v2)
   end.
 
-Definition arith_eval_ff n v :=
-  match n with
+Definition arith_eval_ff i v :=
+  match i with
   | Pfmov => v
   | Pfcvtds => Val.floatofsingle v
   | Pfcvtsd => Val.singleoffloat v
@@ -1451,8 +1451,8 @@ Definition arith_eval_f i :=
   | Pfmovimmd f => Vfloat f
   end.
 
-Definition arith_eval_fr n v :=
-  match n with
+Definition arith_eval_fr i v :=
+  match i with
   | Pscvtf S W => Val.maketotal (Val.singleofint v)
   | Pscvtf D W => Val.maketotal (Val.floatofint v)
   | Pscvtf S X => Val.maketotal (Val.singleoflong v)
@@ -1464,19 +1464,19 @@ Definition arith_eval_fr n v :=
   end.
 
 (* obtain v via rs##r1 *)
-Definition arith_eval_sw_fr0 n v :=
-  match n with
+Definition arith_eval_sw_fr0 i v :=
+  match i with
   | PfmoviSW => float32_of_bits v
   end.
 
 (* obtain v via rs###r1 *)
-Definition arith_eval_dx_fr0 n v :=
-  match n with
+Definition arith_eval_dx_fr0 i v :=
+  match i with
   | PfmoviDX => float64_of_bits v
   end.
 
-Definition arith_eval_fff n v1 v2 :=
-  match n with
+Definition arith_eval_fff i v1 v2 :=
+  match i with
   | Pfadd S => Val.addfs v1 v2
   | Pfadd D => Val.addf v1 v2
   | Pfdiv S => Val.divfs v1 v2
@@ -1497,27 +1497,27 @@ Definition arith_eval_c_fff (i : arith_name_c_fff) (v1 v2 : val) (c : option boo
     end)
   end.
 
-Definition arith_eval_afff n v1 v2 :=
-  match n with
+Definition arith_eval_afff i v1 v2 :=
+  match i with
   | Pfnmul S => Val.negfs (Val.mulfs v1 v2)
   | Pfnmul D => Val.negf (Val.mulf v1 v2)
   end.
 
-Definition arith_prepare_comparison_rr n (v1 v2 : val) :=
-  match n with
+Definition arith_prepare_comparison_rr i (v1 v2 : val) :=
+  match i with
   | Pcmpext x => (v1, (eval_extend v2 x))
   | Pcmnext x => (v1, (Val.negl (eval_extend v2 x)))
   end.
 
-Definition arith_prepare_comparison_w_r0r n v1 v2 :=
-  match n with
+Definition arith_prepare_comparison_w_r0r i v1 v2 :=
+  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))
   end.
 
-Definition arith_prepare_comparison_x_r0r n v1 v2 :=
-  match n with
+Definition arith_prepare_comparison_x_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))
@@ -1534,14 +1534,14 @@ Definition arith_prepare_comparison_r i v :=
   end.
 
 (* Without val annotation unification fails *)
-Definition arith_prepare_comparison_f n (v : val) :=
-  match n with
+Definition arith_prepare_comparison_f i (v : val) :=
+  match i with
   | Pfcmp0 S => (v, (Vsingle Float32.zero))
   | Pfcmp0 D => (v, (Vfloat Float.zero))
   end.
 
-Definition arith_prepare_comparison_ff n (v1 v2 : val) :=
-  match n with
+Definition arith_prepare_comparison_ff i (v1 v2 : val) :=
+  match i with
   | Pfcmp _ => (v1, v2)
   end.
 
@@ -1549,58 +1549,58 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithR i d => rs#d <- (arith_eval_r i)
   | PArithCR i d c => rs#d <- (arith_eval_c_r i (eval_testcond c rs))
-  | PArithRR n d s => rs#d <- (arith_eval_rr n rs#s)
-  | PArithRF n d s => rs#d <- (arith_eval_rf n rs#s)
-  | PArithRRR n d s1 s2 => rs#d <- (arith_eval_rrr n rs#s1 rs#s2)
-  | PArithCRRR n d s1 s2 c => rs#d <- (arith_eval_c_rrr n rs#s1 rs#s2 (eval_testcond c rs))
+  | PArithRR i d s => rs#d <- (arith_eval_rr i rs#s)
+  | PArithRF i d s => rs#d <- (arith_eval_rf i rs#s)
+  | PArithRRR i d s1 s2 => rs#d <- (arith_eval_rrr i rs#s1 rs#s2)
+  | PArithCRRR i d s1 s2 c => rs#d <- (arith_eval_c_rrr i rs#s1 rs#s2 (eval_testcond c rs))
 
-  | PArithWRR0R n d s1 s2 => rs#d <- (arith_eval_w_rr0r n rs##s1 rs#s2)
-  | PArithXRR0R n d s1 s2 => rs#d <- (arith_eval_x_rr0r n rs###s1 rs#s2)
+  | 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)
 
-  | PArithWRR0 n d s => rs#d <- (arith_eval_w_rr0 n rs##s)
-  | PArithXRR0 n d s => rs#d <- (arith_eval_x_rr0 n rs###s)
+  | 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)
 
-  | PArithRspRspR n d s1 s2 => rs#d <- (arith_eval_rsprspr n rs#s1 rs#s2)
-  | PArithRspRsp n d s => rs#d <- (arith_eval_rsprsp n rs#s)
+  | PArithRspRspR i d s1 s2 => rs#d <- (arith_eval_rsprspr i rs#s1 rs#s2)
+  | PArithRspRsp i d s => rs#d <- (arith_eval_rsprsp i rs#s)
 
-  | PArithWARRRR0 n d s1 s2 s3 => rs#d <- (arith_eval_w_arrrr0 n rs#s1 rs#s2 rs##s3)
-  | PArithXARRRR0 n d s1 s2 s3 => rs#d <- (arith_eval_x_arrrr0 n rs#s1 rs#s2 rs###s3)
+  | 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)
 
-  | PArithF n d => rs#d <- (arith_eval_f n)
-  | PArithFF n d s => rs#d <- (arith_eval_ff n rs#s)
-  | PArithFR n d s => rs#d <- (arith_eval_fr n rs#s)
+  | PArithF i d => rs#d <- (arith_eval_f i)
+  | PArithFF i d s => rs#d <- (arith_eval_ff i rs#s)
+  | PArithFR i d s => rs#d <- (arith_eval_fr i rs#s)
 
-  | PArithSWFR0 n d s => rs#d <- (arith_eval_sw_fr0 n rs##s)
-  | PArithDXFR0 n d s => rs#d <- (arith_eval_dx_fr0 n rs###s)
+  | 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)
 
-  | PArithFFF n d s1 s2 => rs#d <- (arith_eval_fff n rs#s1 rs#s2)
-  | PArithCFFF n d s1 s2 c => rs#d <- (arith_eval_c_fff n rs#s1 rs#s2 (eval_testcond c rs))
-  | PArithAFFF n d s1 s2 => rs#d <- (arith_eval_afff n rs#s1 rs#s2)
+  | PArithFFF i d s1 s2 => rs#d <- (arith_eval_fff i rs#s1 rs#s2)
+  | PArithCFFF i d s1 s2 c => rs#d <- (arith_eval_c_fff i rs#s1 rs#s2 (eval_testcond c rs))
+  | PArithAFFF i d s1 s2 => rs#d <- (arith_eval_afff i rs#s1 rs#s2)
 
-  | PArithComparisonRR n s1 s2 =>
-    let (v1, v2) := arith_prepare_comparison_rr n rs#s1 rs#s2 in
+  | PArithComparisonRR i s1 s2 =>
+    let (v1, v2) := arith_prepare_comparison_rr i rs#s1 rs#s2 in
       compare_long rs v1 v2
-  | PArithComparisonWR0R n s1 s2 =>
-    let (v1, v2) := arith_prepare_comparison_w_r0r n rs##s1 rs#s2 in
+  | PArithComparisonWR0R i s1 s2 =>
+    let (v1, v2) := arith_prepare_comparison_w_r0r i rs##s1 rs#s2 in
       compare_int rs v1 v2
-  | PArithComparisonXR0R n s1 s2 =>
-    let (v1, v2) := arith_prepare_comparison_x_r0r n rs###s1 rs#s2 in
+  | PArithComparisonXR0R i s1 s2 =>
+    let (v1, v2) := arith_prepare_comparison_x_r0r i rs###s1 rs#s2 in
       compare_long rs v1 v2
-  | PArithComparisonR n s =>
-    let (v1, v2) := arith_prepare_comparison_r n rs#s in
-      (match n with
+  | PArithComparisonR i s =>
+    let (v1, v2) := arith_prepare_comparison_r 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
       end)
-  | PArithComparisonF n s =>
-    let (v1, v2) := arith_prepare_comparison_f n rs#s in
-    (match n with
+  | PArithComparisonF i s =>
+    let (v1, v2) := arith_prepare_comparison_f i rs#s in
+    (match i with
     | Pfcmp0 S => compare_single rs v1 v2
     | Pfcmp0 D => compare_float rs v1 v2
     end)
-  | PArithComparisonFF n s1 s2 =>
-    let (v1, v2) := arith_prepare_comparison_ff n rs#s1 rs#s2 in
-    (match n with
+  | PArithComparisonFF i s1 s2 =>
+    let (v1, v2) := arith_prepare_comparison_ff i rs#s1 rs#s2 in
+    (match i with
     | Pfcmp S => compare_single rs v1 v2
     | Pfcmp D => compare_float rs v1 v2
     end)