Inline Pfmovi in ar_instruction

1 files changed, 5 insertions, 24 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 90ca7e05..36a0afc0 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -350,11 +350,6 @@ Inductive arith_comparison_pp : Type :=
   | Pfcmp (sz: fsize)                                 (**r compare [r1] and [r2] *)
 .
 
-Inductive arith_fr0 : Type :=
-  (** Floating-point move *)
-  | Pfmovi (fsz: fsize)                               (**r copy int reg to FP reg *)
-.
-
 Inductive arith_ppp : Type :=
   (** Variable shifts *)
   | Pasrv (sz: isize)                                 (**r arithmetic right shift *)
@@ -448,7 +443,6 @@ Inductive ar_instruction : Type :=
   | PArithRR0R (i : arith_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
   | PArithRR0 (i : arith_rr0) (rd : ireg) (r1 : ireg0)
   | PArithARRRR0 (i : arith_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
-  | PArithFR0 (i : arith_fr0) (rd : freg) (rs : ireg0)
   | PArithAPPP (i : arith_appp) (rd r1 r2 : preg)
   (* Pfmadd and Pfmsub are currently not used by the semantics of aarch64/Asm
   | PArithAPPPP (i : arith_apppp) (rd r1 r2 r3 : preg) *)
@@ -459,7 +453,9 @@ Inductive ar_instruction : Type :=
   | PArithComparisonP (i : arith_comparison_p) (r1 : preg)
   (* Instructions without indirection sine they would be the only ones *)
   (* PArithCP: Pcsetm is commented out by aarch64/Asm, so Pcset is alone *)
-  | Pcset (rd : preg) (c : testcond)
+  | Pcset (rd : ireg) (c : testcond)
+  (* PArithFR0 *)
+  | Pfmovi (fsz : fsize) (rd : freg) (r1 : ireg0)
 .
 
 Inductive basic : Type :=
@@ -1357,21 +1353,6 @@ Definition arith_eval_arrrr0 i v1 v2 v3 :=
   | Pmsub X => Val.subl v3 (Val.mull v1 v2)
   end.
 
-Definition arith_fr0_isize (i : arith_fr0) :=
-  match i with
-  (* Pfmovi creates a 32-bit float (Single) from a 32-bit integer (W) *)
-  | Pfmovi S => W
-  (* Pfmovi creates a 64-bit float (Double) from a 64-bit integer (X) *)
-  | Pfmovi D => X
-  end.
-
-(* obtain v via [ir0 (arith_fr0_isize i) rs s] *)
-Definition arith_eval_fr0 i v :=
-  match i with
-  | Pfmovi S => float32_of_bits v
-  | Pfmovi D => float64_of_bits v
-  end.
-
 Definition arith_eval_appp i v1 v2 :=
   match i with
   | Pfnmul S => Val.negfs (Val.mulfs v1 v2)
@@ -1443,8 +1424,6 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithARRRR0 i d s1 s2 s3 =>
     rs#d <- (arith_eval_arrrr0 i rs#s1 rs#s2 (ir0 (arith_arrrr0_isize i) rs s3))
 
-  | PArithFR0 i d s => rs#d <- (arith_eval_fr0 i (ir0 (arith_fr0_isize i) rs s))
-
   | PArithAPPP i d s1 s2 => rs#d <- (arith_eval_appp i rs#s1 rs#s2)
 
   | PArithComparisonPP i s1 s2 =>
@@ -1458,6 +1437,8 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
     let (v1, v2) := arith_prepare_comparison_p i rs#s in
     arith_comparison_p_compare i rs v1 v2
   | Pcset d c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (Vint Int.one) (Vint Int.zero))
+  | Pfmovi S d s => rs#d <- (float32_of_bits rs##s)
+  | Pfmovi D d s => rs#d <- (float64_of_bits rs###s)
   end.
 
 (* basic exec *)