From 1ddfc8323d64fb28fa1111b1cc630910cc2c27c3 Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Tue, 7 Jul 2020 09:33:27 +0200 Subject: Merge PArith(SW|DX)FR0 --- aarch64/Asmblock.v | 30 +++++++++++++----------------- 1 file changed, 13 insertions(+), 17 deletions(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 81df119d..a8157b17 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -360,14 +360,9 @@ Inductive arith_comparison_pp : Type := | Pfcmp (sz: fsize) (**r compare [r1] and [r2] *) . -Inductive arith_sw_fr0 : Type := +Inductive arith_fr0 : Type := (** Floating-point move *) - | PfmoviSW (**r copy int reg to FP reg *) -. - -Inductive arith_dx_fr0 : Type := - (** Floating-point move *) - | PfmoviDX (**r copy int reg to FP reg *) + | Pfmovi (fsz: fsize) (**r copy int reg to FP reg *) . Inductive arith_ppp : Type := @@ -466,8 +461,7 @@ 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) - | PArithSWFR0 (i : arith_sw_fr0) (rd : freg) (rs : ireg0) - | PArithDXFR0 (i : arith_dx_fr0) (rd : freg) (rs : 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) *) @@ -1378,16 +1372,19 @@ Definition arith_eval_arrrr0 i v1 v2 v3 := | Pmsub X => Val.subl v3 (Val.mull v1 v2) end. -(* obtain v via rs##r1 *) -Definition arith_eval_sw_fr0 i v := +Definition arith_fr0_isize (i : arith_fr0) := match i with - | PfmoviSW => float32_of_bits v + (* 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 rs###r1 *) -Definition arith_eval_dx_fr0 i v := +(* obtain v via [ir0 (arith_fr0_isize i) rs s] *) +Definition arith_eval_fr0 i v := match i with - | PfmoviDX => float64_of_bits v + | Pfmovi S => float32_of_bits v + | Pfmovi D => float64_of_bits v end. Definition arith_eval_appp i v1 v2 := @@ -1462,8 +1459,7 @@ 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)) - | 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) + | 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) -- cgit