Inline Pfnmul in ar_instruction

1 files changed, 4 insertions, 14 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 492387bd..1abe7d90 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -398,11 +398,6 @@ Inductive arith_arrrr0 : Type :=
   | Pmsub (sz: isize)                               (**r multiply-sub *)
 .
 
-Inductive arith_appp : Type :=
-  (** Floating-point arithmetic *)
-  | Pfnmul (sz: fsize)                              (**r multiply-negate *)
-.
-
 (* Currently not used by the semantics of aarch64/Asm
  * Inductive arith_apppp : Type :=
  *   (** Floating-point arithmetic *)
@@ -437,7 +432,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)
-  | 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) *)
   (* Pfnmadd and Pfnmsub are currently not used by the semantics of aarch64/Asm
@@ -452,6 +446,8 @@ Inductive ar_instruction : Type :=
   | Pfmovi (fsz : fsize) (rd : freg) (r1 : ireg0)                     (**r copy int reg to FP reg *)
   (* PArithCPPP *)
   | Pcsel (rd r1 r2 : preg) (c : testcond)                            (**r int/float conditional move *)
+  (* PArithAFFF *)
+  | Pfnmul (fsz : fsize) (rd r1 r2 : freg)                            (**r multiply-negate *)
 .
 
 Inductive basic : Type :=
@@ -1330,12 +1326,6 @@ Definition arith_eval_arrrr0 i v1 v2 v3 :=
   | Pmsub X => Val.subl v3 (Val.mull v1 v2)
   end.
 
-Definition arith_eval_appp 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_pp i (v1 v2 : val) :=
   match i with
   | Pcmpext x => (v1, (eval_extend v2 x))
@@ -1400,8 +1390,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))
 
-  | PArithAPPP i d s1 s2 => rs#d <- (arith_eval_appp i rs#s1 rs#s2)
-
   | PArithComparisonPP i s1 s2 =>
     let (v1, v2) := arith_prepare_comparison_pp i rs#s1 rs#s2 in
     arith_comparison_pp_compare i rs v1 v2
@@ -1416,6 +1404,8 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | Pfmovi S d s => rs#d <- (float32_of_bits rs##s)
   | Pfmovi D d s => rs#d <- (float64_of_bits rs###s)
   | Pcsel d s1 s2 c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (rs#s1) (rs#s2))
+  | Pfnmul S d s1 s2 => rs#d <- (Val.negfs (Val.mulfs rs#s1 rs#s2))
+  | Pfnmul D d s1 s2 => rs#d <- (Val.negf (Val.mulf rs#s1 rs#s2))
   end.
 
 (* basic exec *)