From 0750711831cda72ae9fe85a83db048027b0d0dff Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Tue, 7 Jul 2020 09:20:06 +0200 Subject: Merge PArith(W|X)RR0 and PArith(W|X)ARRRR0 --- aarch64/Asmblock.v | 77 +++++++++++++++++++++--------------------------------- 1 file changed, 30 insertions(+), 47 deletions(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 2d0eeb11..81df119d 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -412,31 +412,17 @@ Inductive arith_rr0r : Type := . -Inductive arith_w_rr0 : Type := +Inductive arith_rr0 : Type := (** Logical, immediate *) - | PandimmW (n: Z) (**r and *) - | PeorimmW (n: Z) (**r xor *) - | PorrimmW (n: Z) (**r or *) + | Pandimm (sz: isize) (n: Z) (**r and *) + | Peorimm (sz: isize) (n: Z) (**r xor *) + | Porrimm (sz: isize) (n: Z) (**r or *) . -Inductive arith_x_rr0 : Type := - (** Logical, immediate *) - | PandimmX (n: Z) (**r and *) - | PeorimmX (n: Z) (**r xor *) - | PorrimmX (n: Z) (**r or *) -. - - -Inductive arith_w_arrrr0 : Type := - (** Integer multiply/divide *) - | PmaddW (**r multiply-add *) - | PmsubW (**r multiply-sub *) -. - -Inductive arith_x_arrrr0 : Type := +Inductive arith_arrrr0 : Type := (** Integer multiply/divide *) - | PmaddX (**r multiply-add *) - | PmsubX (**r multiply-sub *) + | Pmadd (sz: isize) (**r multiply-add *) + | Pmsub (sz: isize) (**r multiply-sub *) . Inductive arith_appp : Type := @@ -478,10 +464,8 @@ Inductive ar_instruction : Type := | PArithPPP (i : arith_ppp) (rd r1 r2 : preg) | PArithCPPP (i : arith_c_ppp) (rd r1 r2 : preg) (c : testcond) | PArithRR0R (i : arith_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg) - | PArithWRR0 (i : arith_w_rr0) (rd : ireg) (r1 : ireg0) - | PArithXRR0 (i : arith_x_rr0) (rd : ireg) (r1 : ireg0) - | PArithWARRRR0 (i : arith_w_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0) - | PArithXARRRR0 (i : arith_x_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0) + | 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) | PArithAPPP (i : arith_appp) (rd r1 r2 : preg) @@ -1364,34 +1348,34 @@ Definition arith_eval_rr0r i v1 v2 := | Porn X s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s)) end. -(* obtain v by rs##r1 *) -Definition arith_eval_w_rr0 i v := +Definition arith_rr0_isize (i : arith_rr0) := match i with - | PandimmW n => Val.and v (Vint (Int.repr n)) - | PeorimmW n => Val.xor v (Vint (Int.repr n)) - | PorrimmW n => Val.or v (Vint (Int.repr n)) + | Pandimm is _ | Peorimm is _ | Porrimm is _ => is end. -(* obtain v by rs###r1 *) -Definition arith_eval_x_rr0 i v := +(* obtain v by [ir0 (arith_rr0_isize i) rs s] *) +Definition arith_eval_rr0 i v := match i with - | PandimmX n => Val.andl v (Vlong (Int64.repr n)) - | PeorimmX n => Val.xorl v (Vlong (Int64.repr n)) - | PorrimmX n => Val.orl v (Vlong (Int64.repr n)) + | Pandimm W n => Val.and v (Vint (Int.repr n)) + | Pandimm X n => Val.andl v (Vlong (Int64.repr n)) + | Peorimm W n => Val.xor v (Vint (Int.repr n)) + | Peorimm X n => Val.xorl v (Vlong (Int64.repr n)) + | Porrimm W n => Val.or v (Vint (Int.repr n)) + | Porrimm X n => Val.orl v (Vlong (Int64.repr n)) end. -(* obtain v3 by rs##r3 *) -Definition arith_eval_w_arrrr0 i v1 v2 v3 := +Definition arith_arrrr0_isize (i : arith_arrrr0) := match i with - | PmaddW => Val.add v3 (Val.mul v1 v2) - | PmsubW => Val.sub v3 (Val.mul v1 v2) + | Pmadd is | Pmsub is => is end. -(* obtain v3 by rs###r3 *) -Definition arith_eval_x_arrrr0 i v1 v2 v3 := +(* obtain v3 by [ir0 (arith_arrrr0_isize i) rs s3] *) +Definition arith_eval_arrrr0 i v1 v2 v3 := match i with - | PmaddX => Val.addl v3 (Val.mull v1 v2) - | PmsubX => Val.subl v3 (Val.mull v1 v2) + | Pmadd W => Val.add v3 (Val.mul v1 v2) + | Pmadd X => Val.addl v3 (Val.mull v1 v2) + | Pmsub W => Val.sub v3 (Val.mul v1 v2) + | Pmsub X => Val.subl v3 (Val.mull v1 v2) end. (* obtain v via rs##r1 *) @@ -1473,11 +1457,10 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := | PArithRR0R i d s1 s2 => rs#d <- (arith_eval_rr0r i (ir0 (arith_rr0r_isize i) rs s1) rs#s2) - | PArithWRR0 i d s => rs#d <- (arith_eval_w_rr0 i rs##s) - | PArithXRR0 i d s => rs#d <- (arith_eval_x_rr0 i rs###s) + | PArithRR0 i d s => rs#d <- (arith_eval_rr0 i (ir0 (arith_rr0_isize i) rs s)) - | PArithWARRRR0 i d s1 s2 s3 => rs#d <- (arith_eval_w_arrrr0 i rs#s1 rs#s2 rs##s3) - | PArithXARRRR0 i d s1 s2 s3 => rs#d <- (arith_eval_x_arrrr0 i rs#s1 rs#s2 rs###s3) + | 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) -- cgit