From beab9a45ee3edbf87e92fddecaa87e7c3e452fee Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 6 Jul 2020 18:15:53 +0200 Subject: unifying arith_w_rr0r and arith_x_rr0r into arith_rr0r --- aarch64/Asmblock.v | 93 ++++++++++++++++++++++++------------------------------ 1 file changed, 42 insertions(+), 51 deletions(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 81c55415..216f836d 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -406,31 +406,19 @@ Inductive arith_c_ppp : Type := | Pfsel . -Inductive arith_w_rr0r : Type := +Inductive arith_rr0r : Type := (** Integer arithmetic, shifted register *) - | PaddW (s: shift_op) (**r addition *) - | PsubW (s: shift_op) (**r subtraction *) + | Padd (sz:isize) (s: shift_op) (**r addition *) + | Psub (sz:isize) (s: shift_op) (**r subtraction *) (** Logical, shifted register *) - | PandW (s: shift_op) (**r and *) - | PbicW (s: shift_op) (**r and-not *) - | PeonW (s: shift_op) (**r xor-not *) - | PeorW (s: shift_op) (**r xor *) - | PorrW (s: shift_op) (**r or *) - | PornW (s: shift_op) (**r or-not *) + | Pand (sz:isize) (s: shift_op) (**r and *) + | Pbic (sz:isize) (s: shift_op) (**r and-not *) + | Peon (sz:isize) (s: shift_op) (**r xor-not *) + | Peor (sz:isize) (s: shift_op) (**r xor *) + | Porr (sz:isize) (s: shift_op) (**r or *) + | Porn (sz:isize) (s: shift_op) (**r or-not *) . -Inductive arith_x_rr0r : Type := - (** Integer arithmetic, shifted register *) - | PaddX (s: shift_op) (**r addition *) - | PsubX (s: shift_op) (**r subtraction *) - (** Logical, shifted register *) - | PandX (s: shift_op) (**r and *) - | PbicX (s: shift_op) (**r and-not *) - | PeonX (s: shift_op) (**r xor-not *) - | PeorX (s: shift_op) (**r xor *) - | PorrX (s: shift_op) (**r or *) - | PornX (s: shift_op) (**r or-not *) -. Inductive arith_w_rr0 : Type := (** Logical, immediate *) @@ -497,8 +485,7 @@ Inductive ar_instruction : Type := | PArithPP (i : arith_pp) (rd rs : preg) | PArithPPP (i : arith_ppp) (rd r1 r2 : preg) | PArithCPPP (i : arith_c_ppp) (rd r1 r2 : preg) (c : testcond) - | PArithWRR0R (i : arith_w_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg) - | PArithXRR0R (i : arith_x_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg) + | 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) @@ -763,17 +750,15 @@ Definition genv := Genv.t fundef unit. (** The value of an [ireg0] is either the value of the integer register, or 0. *) -Definition ir0w (rs: regset) (r: ireg0) : val := - match r with RR0 r => rs (IR r) | XZR => Vint Int.zero end. -Definition ir0x (rs: regset) (r: ireg0) : val := - match r with RR0 r => rs (IR r) | XZR => Vlong Int64.zero end. +Definition ir0 (is:isize) (rs: regset) (r: ireg0) : val := + match r with RR0 r => rs (IR r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end. (** Concise notations for accessing and updating the values of registers. *) Notation "a # b" := (a b) (at level 1, only parsing) : asm. Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. -Notation "a ## b" := (ir0w a b) (at level 1, only parsing) : asm. -Notation "a ### b" := (ir0x a b) (at level 1, only parsing) : asm. +Notation "a ## b" := (ir0 W a b) (at level 1, only parsing) : asm. +Notation "a ### b" := (ir0 X a b) (at level 1, only parsing) : asm. Open Scope asm. @@ -1350,30 +1335,37 @@ Definition arith_eval_c_ppp (i : arith_c_ppp) (v1 v2 : val) (c : option bool) := end) end. -(* obtain v1 by rs##r1 *) -Definition arith_eval_w_rr0r i v1 v2 := +Definition arith_rr0r_isize (i: arith_rr0r) := match i with - | PaddW s => Val.add v1 (eval_shift_op_int v2 s) - | PsubW s => Val.sub v1 (eval_shift_op_int v2 s) - | PandW s => Val.and v1 (eval_shift_op_int v2 s) - | PbicW s => Val.and v1 (Val.notint (eval_shift_op_int v2 s)) - | PeonW s => Val.xor v1 (Val.notint (eval_shift_op_int v2 s)) - | PeorW s => Val.xor v1 (eval_shift_op_int v2 s) - | PorrW s => Val.or v1 (eval_shift_op_int v2 s) - | PornW s => Val.or v1 (Val.notint (eval_shift_op_int v2 s)) + | Padd is _ => is + | Psub is _ => is + | Pand is _ => is + | Pbic is _ => is + | Peon is _ => is + | Peor is _ => is + | Porr is _ => is + | Porn is _ => is end. -(* obtain v1 by rs###r1 *) -Definition arith_eval_x_rr0r i v1 v2 := +(* obtain v1 by [ir0 (arith_rr0r_isize i) rs s1] *) +Definition arith_eval_rr0r i v1 v2 := match i with - | PaddX s => Val.addl v1 (eval_shift_op_long v2 s) - | PsubX s => Val.subl v1 (eval_shift_op_long v2 s) - | PandX s => Val.andl v1 (eval_shift_op_long v2 s) - | PbicX s => Val.andl v1 (Val.notl (eval_shift_op_long v2 s)) - | PeonX s => Val.xorl v1 (Val.notl (eval_shift_op_long v2 s)) - | PeorX s => Val.xorl v1 (eval_shift_op_long v2 s) - | PorrX s => Val.orl v1 (eval_shift_op_long v2 s) - | PornX s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s)) + | Padd W s => Val.add v1 (eval_shift_op_int v2 s) + | Padd X s => Val.addl v1 (eval_shift_op_long v2 s) + | Psub W s => Val.sub v1 (eval_shift_op_int v2 s) + | Psub X s => Val.subl v1 (eval_shift_op_long v2 s) + | Pand W s => Val.and v1 (eval_shift_op_int v2 s) + | Pand X s => Val.andl v1 (eval_shift_op_long v2 s) + | Pbic W s => Val.and v1 (Val.notint (eval_shift_op_int v2 s)) + | Pbic X s => Val.andl v1 (Val.notl (eval_shift_op_long v2 s)) + | Peon W s => Val.xor v1 (Val.notint (eval_shift_op_int v2 s)) + | Peon X s => Val.xorl v1 (Val.notl (eval_shift_op_long v2 s)) + | Peor W s => Val.xor v1 (eval_shift_op_int v2 s) + | Peor X s => Val.xorl v1 (eval_shift_op_long v2 s) + | Porr W s => Val.or v1 (eval_shift_op_int v2 s) + | Porr X s => Val.orl v1 (eval_shift_op_long v2 s) + | Porn W s => Val.or v1 (Val.notint (eval_shift_op_int v2 s)) + | Porn X s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s)) end. (* obtain v by rs##r1 *) @@ -1465,8 +1457,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := | PArithPPP i d s1 s2 => rs#d <- (arith_eval_ppp i rs#s1 rs#s2) | PArithCPPP i d s1 s2 c => rs#d <- (arith_eval_c_ppp i rs#s1 rs#s2 (eval_testcond c rs)) - | PArithWRR0R i d s1 s2 => rs#d <- (arith_eval_w_rr0r i rs##s1 rs#s2) - | PArithXRR0R i d s1 s2 => rs#d <- (arith_eval_x_rr0r i rs###s1 rs#s2) + | 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) -- cgit