Asmblock: PArithRspRspI -> PArithRspRsp

1 files changed, 11 insertions, 11 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index c18d30b9..8b661885 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -462,10 +462,10 @@ Inductive arith_name_c_fff : Type :=
   | Pfsel (cond: testcond)
 .
 
-Inductive arith_name_rsprspi : Type :=
+Inductive arith_name_rsprsp : Type :=
   (** Integer arithmetic, immediate *)
-  | Paddimm (sz: isize)                             (**r addition *)
-  | Psubimm (sz: isize)                             (**r subtraction *)
+  | Paddimm (sz: isize) (n: Z)                      (**r addition *)
+  | Psubimm (sz: isize) (n: Z)                      (**r subtraction *)
 .
 
 Inductive arith_name_w_rr0i : Type :=
@@ -536,7 +536,7 @@ Inductive ar_instruction : Type :=
   | PArithWRR0I (i : arith_name_w_rr0i) (rd : ireg) (r1 : ireg0) (n : Z)
   | PArithXRR0I (i : arith_name_x_rr0i) (rd : ireg) (r1 : ireg0) (n : Z)
   | PArithRspRspR (i : arith_name_rsprspr) (rd r1 : iregsp) (r2 : ireg)
-  | PArithRspRspI (i : arith_name_rsprspi) (rd r1 : iregsp) (n : Z)
+  | PArithRspRsp (i : arith_name_rsprsp) (rd r1 : iregsp)
   | PArithWARRRR0 (i : arith_name_w_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
   | PArithXARRRR0 (i : arith_name_x_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
   | PArithFF (i : arith_name_ff) (rd rs : freg)
@@ -1391,12 +1391,12 @@ Definition arith_eval_rsprspr n v1 v2 :=
   | Psubext x => Val.subl v2 (eval_extend v2 x)
   end.
 
-Definition arith_eval_rsprspi n v i :=
-  match n with
-  | Paddimm W => Val.add v (Vint (Int.repr i))
-  | Paddimm X => Val.addl v (Vlong (Int64.repr i))
-  | Psubimm W => Val.sub v (Vint (Int.repr i))
-  | Psubimm X => Val.subl v (Vlong (Int64.repr i))
+Definition arith_eval_rsprsp i v :=
+  match i with
+  | Paddimm W n => Val.add v (Vint (Int.repr n))
+  | Paddimm X n => Val.addl v (Vlong (Int64.repr n))
+  | Psubimm W n => Val.sub v (Vint (Int.repr n))
+  | Psubimm X n => Val.subl v (Vlong (Int64.repr n))
   end.
 
 (* obtain v3 by rs##r3 *)
@@ -1532,7 +1532,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithXRR0I n d s i => rs#d <- (arith_eval_x_rr0i n rs###s i)
 
   | PArithRspRspR n d s1 s2 => rs#d <- (arith_eval_rsprspr n rs#s1 rs#s2)
-  | PArithRspRspI n d s i => rs#d <- (arith_eval_rsprspi n rs#s i)
+  | PArithRspRsp n d s => rs#d <- (arith_eval_rsprsp n 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)