From e28bf3a20d7448373ba9cc63bd0ac2566dafe027 Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Wed, 8 Jul 2020 18:20:34 +0200 Subject: Revert introduction of dreg This everts commits 91f991ab and df253300 --- aarch64/Asmblock.v | 278 +++++++++++++++++++++++------------------------------ 1 file changed, 120 insertions(+), 158 deletions(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index efaaf839..1abe7d90 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -88,19 +88,6 @@ Inductive crbit: Type := Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}. Proof. decide equality. Defined. -Inductive dreg : Type := - | DRSP: iregsp -> dreg - | DR0: ireg0 -> dreg - | DFR: freg -> dreg - . - -Coercion DRSP: iregsp >-> dreg. -(* Causes ambiguity warning - * ireg can be coerced to either ireg0 or iregsp and both coerce to dreg - * However I also want to coerce both XZR and XSP to dreg *) -Coercion DR0: ireg0 >-> dreg. -Coercion DFR: freg >-> dreg. - (** We model the following registers of the ARM architecture. *) Inductive preg: Type := @@ -212,7 +199,7 @@ Inductive cf_instruction : Type := | Ptbz (sz: isize) (r: ireg) (n: int) (lbl: label) (**r branch if bit n is zero *) (** Pseudo-instructions *) | Pbtbl (r1: ireg) (tbl: list label) (**r N-way branch through a jump table *) - . + . (* A builtin is considered as a control-flow instruction, because it could emit a trace (cf. Machblock semantics). @@ -297,7 +284,7 @@ Inductive arith_p : Type := | Pfmovimmd (f: float) (**r load float64 constant *) . -Inductive arith_comparison_d : Type := +Inductive arith_comparison_p : Type := (** Floating-point comparison *) | Pfcmp0 (sz: fsize) (**r compare [r1] and [+0.0] *) (** Integer arithmetic, immediate *) @@ -307,7 +294,7 @@ Inductive arith_comparison_d : Type := | Ptstimm (sz: isize) (n: Z) (**r and, then set flags *) . -Inductive arith_pd : Type := +Inductive arith_pp : Type := (** Move integer register *) | Pmov (** Move wide immediate *) @@ -345,26 +332,25 @@ Inductive arith_pd : Type := (** Integer arithmetic, immediate *) | Paddimm (sz: isize) (n: Z) (**r addition *) | Psubimm (sz: isize) (n: Z) (**r subtraction *) - (** Logical, immediate *) - | Pandimm (sz: isize) (n: Z) (**r and *) - | Peorimm (sz: isize) (n: Z) (**r xor *) - | Porrimm (sz: isize) (n: Z) (**r or *) . -Inductive arith_comparison_dd : Type := +Inductive arith_comparison_r0r : Type := + (** Integer arithmetic, shifted register *) + | Pcmp (is:isize) (s: shift_op) (**r compare *) + | Pcmn (is:isize) (s: shift_op) (**r compare negative *) + (** Logical, shifted register *) + | Ptst (is:isize) (s: shift_op) (**r and, then set flags *) +. + +Inductive arith_comparison_pp : Type := (** Integer arithmetic, extending register *) - | Pcmpext (x: extend_op) (**r int64-int32 cmp *) - | Pcmnext (x: extend_op) (**r int64-int32 cmn *) + | Pcmpext (x: extend_op) (**r int64-int32 cmp *) + | Pcmnext (x: extend_op) (**r int64-int32 cmn *) (** Floating-point comparison *) | Pfcmp (sz: fsize) (**r compare [r1] and [r2] *) - (** Integer arithmetic, shifted register *) - | Pcmp (is:isize) (s: shift_op) (**r compare *) - | Pcmn (is:isize) (s: shift_op) (**r compare negative *) - (** Logical, shifted register *) - | Ptst (is:isize) (s: shift_op) (**r and, then set flags *) . -Inductive arith_pdd : Type := +Inductive arith_ppp : Type := (** Variable shifts *) | Pasrv (sz: isize) (**r arithmetic right shift *) | Plslv (sz: isize) (**r left shift *) @@ -383,6 +369,9 @@ Inductive arith_pdd : Type := | Pfdiv (sz: fsize) (**r division *) | Pfmul (sz: fsize) (**r multiplication *) | Pfsub (sz: fsize) (**r subtraction *) +. + +Inductive arith_rr0r : Type := (** Integer arithmetic, shifted register *) | Padd (sz:isize) (s: shift_op) (**r addition *) | Psub (sz:isize) (s: shift_op) (**r subtraction *) @@ -395,7 +384,15 @@ Inductive arith_pdd : Type := | Porn (sz:isize) (s: shift_op) (**r or-not *) . -Inductive arith_apddd : Type := + +Inductive arith_rr0 : Type := + (** Logical, immediate *) + | Pandimm (sz: isize) (n: Z) (**r and *) + | Peorimm (sz: isize) (n: Z) (**r xor *) + | Porrimm (sz: isize) (n: Z) (**r or *) +. + +Inductive arith_arrrr0 : Type := (** Integer multiply/divide *) | Pmadd (sz: isize) (**r multiply-add *) | Pmsub (sz: isize) (**r multiply-sub *) @@ -430,15 +427,18 @@ Inductive arith_apddd : Type := *) Inductive ar_instruction : Type := | PArithP (i : arith_p) (rd : preg) - | PArithPD (i : arith_pd) (rd : preg) (rs : dreg) - | PArithPDD (i : arith_pdd) (rd : preg) (r1 r2 : dreg) - | PArithAPDDD (i : arith_apddd) (rd : preg) (r1 r2 r3 : dreg) + | PArithPP (i : arith_pp) (rd rs : preg) + | PArithPPP (i : arith_ppp) (rd r1 r2 : preg) + | 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) (* 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 | PArithAAPPPP (i : arith_aapppp) (rd r1 r2 r3 : preg) *) - | PArithComparisonD (i : arith_comparison_d) (r1 : dreg) - | PArithComparisonDD (i : arith_comparison_dd) (r1 r2 : dreg) + | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : preg) + | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg) + | PArithComparisonP (i : arith_comparison_p) (r1 : preg) (* Instructions without indirection sine they would be the only ones *) (* PArithCP: Pcsetm is commented out by aarch64/Asm, so Pcset is alone *) | Pcset (rd : ireg) (c : testcond) (**r set to 1/0 if cond is true/false *) @@ -698,23 +698,7 @@ Definition genv := Genv.t fundef unit. or 0. *) 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. - -Definition dr (is: option isize) (rs: regset) (dr: dreg) : option val := - match dr with - | DFR r => Some (rs (FR r)) - | DRSP r => Some (rs (IR r)) - | DR0 r0 => - match r0 with - | RR0 r => Some (rs (IR r)) - | XZR => - match is with - | Some W => Some (Vint Int.zero) - | Some X => Some (Vlong Int64.zero) - | None => None - end - end - end. + 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. *) @@ -723,7 +707,6 @@ Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : 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. (** Undefining some registers *) @@ -1209,18 +1192,7 @@ Definition if_opt_bool_val (c: option bool) v1 v2: val := | None => Vundef end. -Definition arith_pd_isize (i : arith_pd) : option isize := - match i with - | Pandimm is _ | Peorimm is _ | Porrimm is _ => Some is - | Pmov | Pmovk _ _ _ | Paddadr _ _ | Psbfiz _ _ _ - | Psbfx _ _ _ | Pubfiz _ _ _ | Pubfx _ _ _ | Pfmov - | Pfcvtds | Pfcvtsd | Pfabs _ | Pfneg _ - | Pscvtf _ _ | Pucvtf _ _ | Pfcvtzs _ _ | Pfcvtzu _ _ - | Paddimm _ _ | Psubimm _ _ - => None - end. - -Definition arith_eval_pd i v := +Definition arith_eval_pp i v := match i with | Pmov => v | Pmovk W n pos => insert_in_int v n pos 16 @@ -1261,28 +1233,9 @@ Definition arith_eval_pd i v := | Pucvtf D W => Val.maketotal (Val.floatofintu v) | Pucvtf S X => Val.maketotal (Val.singleoflongu v) | Pucvtf D X => Val.maketotal (Val.floatoflongu v) - | 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. - -Definition arith_pdd_isize (i: arith_pdd) : option isize := - match i with - | Padd is _ | Psub is _ | Pand is _ | Pbic is _ - | Peon is _ | Peor is _ | Porr is _ | Porn is _ - => Some is - (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *) - | Pasrv _ | Plslv _ | Plsrv _ | Prorv _ - | Psmulh | Pumulh | Psdiv _ | Pudiv _ - | Paddext _ | Psubext _ | Pfadd _ | Pfdiv _ - | Pfmul _ | Pfsub _ - => None end. -Definition arith_eval_pdd i v1 v2 := +Definition arith_eval_ppp i v1 v2 := match i with | Pasrv W => Val.shr v1 v2 | Pasrv X => Val.shrl v1 v2 @@ -1308,6 +1261,23 @@ Definition arith_eval_pdd i v1 v2 := | Pfmul D => Val.mulf v1 v2 | Pfsub S => Val.subfs v1 v2 | Pfsub D => Val.subf v1 v2 + end. + +Definition arith_rr0r_isize (i: arith_rr0r) := + match i with + | 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 [ir0 (arith_rr0r_isize i) rs s1] *) +Definition arith_eval_rr0r i v1 v2 := + match i with | 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) @@ -1326,12 +1296,29 @@ Definition arith_eval_pdd i v1 v2 := | Porn X s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s)) end. -Definition arith_apddd_isize (i : arith_apddd) : option isize := +Definition arith_rr0_isize (i : arith_rr0) := + match i with + | Pandimm is _ | Peorimm is _ | Porrimm is _ => is + end. + +(* obtain v by [ir0 (arith_rr0_isize i) rs s] *) +Definition arith_eval_rr0 i v := match i with - | Pmadd is | Pmsub is => Some is + | 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. -Definition arith_eval_apddd i v1 v2 v3 := +Definition arith_arrrr0_isize (i : arith_arrrr0) := + match i with + | Pmadd is | Pmsub is => is + end. + +(* obtain v3 by [ir0 (arith_arrrr0_isize i) rs s3] *) +Definition arith_eval_arrrr0 i v1 v2 v3 := match i with | Pmadd W => Val.add v3 (Val.mul v1 v2) | Pmadd X => Val.addl v3 (Val.mull v1 v2) @@ -1339,19 +1326,22 @@ Definition arith_eval_apddd i v1 v2 v3 := | Pmsub X => Val.subl v3 (Val.mull v1 v2) end. -Definition arith_comparison_dd_isize (i : arith_comparison_dd) : option isize := - match i with - | Pcmp is _ | Pcmn is _ | Ptst is _ - => Some is - | Pcmpext _ | Pcmnext _ | Pfcmp _ - => None - end. - -Definition arith_prepare_comparison_dd i (v1 v2 : val) := +Definition arith_prepare_comparison_pp i (v1 v2 : val) := match i with | Pcmpext x => (v1, (eval_extend v2 x)) | Pcmnext x => (v1, (Val.negl (eval_extend v2 x))) | Pfcmp _ => (v1, v2) + end. + +Definition arith_comparison_r0r_isize i := + match i with + | Pcmp is _ => is + | Pcmn is _ => is + | Ptst is _ => is + end. + +Definition arith_prepare_comparison_r0r i v1 v2 := + match i with | Pcmp W s => (v1, (eval_shift_op_int v2 s)) | Pcmp X s => (v1, (eval_shift_op_long v2 s)) | Pcmn W s => (v1, (Val.neg (eval_shift_op_int v2 s))) @@ -1360,13 +1350,7 @@ Definition arith_prepare_comparison_dd i (v1 v2 : val) := | Ptst X s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero)) end. -Definition arith_comparison_d_isize (i : arith_comparison_d) : option isize := - match i with - | Pcmpimm _ _ | Pcmnimm _ _ | Ptstimm _ _ | Pfcmp0 _ - => None - end. - -Definition arith_prepare_comparison_d i v := +Definition arith_prepare_comparison_p i v := match i with | Pcmpimm W n => (v, (Vint (Int.repr n))) | Pcmpimm X n => (v, (Vlong (Int64.repr n))) @@ -1378,17 +1362,14 @@ Definition arith_prepare_comparison_d i v := | Pfcmp0 D => (v, (Vfloat Float.zero)) end. -Definition arith_comparison_dd_compare i := +Definition arith_comparison_pp_compare i := match i with - | Pcmp W _ | Pcmn W _ | Ptst W _ - => compare_int - | Pcmp X _ | Pcmn X _ | Ptst X _ | Pcmpext _ | Pcmnext _ - => compare_long + | Pcmpext _ | Pcmnext _ => compare_long | Pfcmp S => compare_single | Pfcmp D => compare_float end. -Definition arith_comparison_d_compare i := +Definition arith_comparison_p_compare i := match i with | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long @@ -1396,60 +1377,41 @@ Definition arith_comparison_d_compare i := | Pfcmp0 D => compare_float end. -Definition exec_arith_instr (ai: ar_instruction) (rs: regset): option regset := +Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := match ai with - | PArithP i d => Some (rs#d <- (arith_eval_p i)) - | PArithPD i d s => - let is := arith_pd_isize i in - let get_val := (dr is rs) in - SOME v <- (get_val s) IN - Some (rs#d <- (arith_eval_pd i v)) - | PArithPDD i d s1 s2 => - let is := arith_pdd_isize i in - let get_val := (dr is rs) in - SOME v1 <- (get_val s1) IN - SOME v2 <- (get_val s2) IN - Some (rs#d <- (arith_eval_pdd i v1 v2)) - | PArithAPDDD i d s1 s2 s3 => - let is := arith_apddd_isize i in - let get_val := (dr is rs) in - SOME v1 <- (get_val s1) IN - SOME v2 <- (get_val s2) IN - SOME v3 <- (get_val s3) IN - Some (rs#d <- (arith_eval_apddd i v1 v2 v3)) - | PArithComparisonDD i s1 s2 => - let is := arith_comparison_dd_isize i in - let get_val := (dr is rs) in - (* register values *) - SOME rv1 <- (get_val s1) IN - SOME rv2 <- (get_val s2) IN - let (v1, v2) := arith_prepare_comparison_dd i rv1 rv2 in - Some (arith_comparison_dd_compare i rs v1 v2) - | PArithComparisonD i s => - let is := arith_comparison_d_isize i in - let get_val := (dr is rs) in - SOME rv <- (get_val s) IN - let (v1, v2) := arith_prepare_comparison_d i rv in - Some (arith_comparison_d_compare i rs v1 v2) - | Pcset d c => - Some (rs#d <- (if_opt_bool_val (eval_testcond c rs) (Vint Int.one) (Vint Int.zero))) - | Pfmovi S d s => - SOME v <- dr (Some W) rs s IN - Some (rs#d <- (float32_of_bits v)) - | Pfmovi D d s => - SOME v <- dr (Some X) rs s IN - Some (rs#d <- (float64_of_bits v)) - | Pcsel d s1 s2 c => Some (rs#d <- (if_opt_bool_val (eval_testcond c rs) (rs#s1) (rs#s2))) - | Pfnmul S d s1 s2 => Some (rs#d <- (Val.negfs (Val.mulfs rs#s1 rs#s2))) - | Pfnmul D d s1 s2 => Some (rs#d <- (Val.negf (Val.mulf rs#s1 rs#s2))) + | PArithP i d => rs#d <- (arith_eval_p i) + | PArithPP i d s => rs#d <- (arith_eval_pp i rs#s) + | PArithPPP i d s1 s2 => rs#d <- (arith_eval_ppp 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) + + | PArithRR0 i d s => rs#d <- (arith_eval_rr0 i (ir0 (arith_rr0_isize i) rs s)) + + | PArithARRRR0 i d s1 s2 s3 => + rs#d <- (arith_eval_arrrr0 i rs#s1 rs#s2 (ir0 (arith_arrrr0_isize i) rs s3)) + + | 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 + | PArithComparisonR0R i s1 s2 => + let is := arith_comparison_r0r_isize i in + let (v1, v2) := arith_prepare_comparison_r0r i (ir0 is rs s1) rs#s2 in + (if is (* is W *) then compare_int else compare_long) rs v1 v2 + | PArithComparisonP i s => + let (v1, v2) := arith_prepare_comparison_p i rs#s in + arith_comparison_p_compare i rs v1 v2 + | Pcset d c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (Vint Int.one) (Vint Int.zero)) + | 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 *) Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome := match b with - | PArith ai => - SOME rs' <- exec_arith_instr ai rs IN - Next rs' m + | PArith ai => Next (exec_arith_instr ai rs) m | PLoad ld rd a => exec_load (chunk_load_rd_a ld) (interp_load_rd_a ld) a rd rs m | PStore st r a => exec_store (chunk_store_rs_a st) a rs#r rs m | Pallocframe sz pos => -- cgit