From 2c563299fe0cf06fd5014afcde8d503b5ecbc4e1 Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Tue, 7 Jul 2020 11:35:53 +0200 Subject: Inline Pfnmul in ar_instruction --- aarch64/Asmblock.v | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) (limited to 'aarch64/Asmblock.v') 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 *) -- cgit