diff options
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 241 |
1 files changed, 128 insertions, 113 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 1abe7d90..63d590e6 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -88,6 +88,19 @@ 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 := @@ -199,7 +212,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). @@ -284,7 +297,7 @@ Inductive arith_p : Type := | Pfmovimmd (f: float) (**r load float64 constant *) . -Inductive arith_comparison_p : Type := +Inductive arith_comparison_d : Type := (** Floating-point comparison *) | Pfcmp0 (sz: fsize) (**r compare [r1] and [+0.0] *) (** Integer arithmetic, immediate *) @@ -294,7 +307,7 @@ Inductive arith_comparison_p : Type := | Ptstimm (sz: isize) (n: Z) (**r and, then set flags *) . -Inductive arith_pp : Type := +Inductive arith_pd : Type := (** Move integer register *) | Pmov (** Move wide immediate *) @@ -332,25 +345,26 @@ Inductive arith_pp : 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_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 := +Inductive arith_comparison_dd : 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_ppp : Type := +Inductive arith_pdd : Type := (** Variable shifts *) | Pasrv (sz: isize) (**r arithmetic right shift *) | Plslv (sz: isize) (**r left shift *) @@ -369,9 +383,6 @@ Inductive arith_ppp : 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 *) @@ -384,15 +395,7 @@ Inductive arith_rr0r : Type := | Porn (sz:isize) (s: shift_op) (**r or-not *) . - -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 := +Inductive arith_apddd : Type := (** Integer multiply/divide *) | Pmadd (sz: isize) (**r multiply-add *) | Pmsub (sz: isize) (**r multiply-sub *) @@ -427,18 +430,15 @@ Inductive arith_arrrr0 : Type := *) Inductive ar_instruction : Type := | PArithP (i : arith_p) (rd : preg) - | 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) + | 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) (* 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) *) - | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : preg) - | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg) - | PArithComparisonP (i : arith_comparison_p) (r1 : preg) + | PArithComparisonD (i : arith_comparison_d) (r1 : dreg) + | PArithComparisonDD (i : arith_comparison_dd) (r1 r2 : dreg) (* 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 *) @@ -697,15 +697,23 @@ Definition genv := Genv.t fundef unit. (** The value of an [ireg0] is either the value of the integer register, 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:isize) (rs: regset) (dr: dreg) : val := + match dr with + | DFR r => rs (FR r) + | DRSP r => rs (IR r) + | DR0 r0 => + match r0 with + | RR0 r => rs (IR r) + | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero + end + 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" := (ir0 W a b) (at level 1, only parsing) : asm. -Notation "a ### b" := (ir0 X a b) (at level 1, only parsing) : asm. +Notation "a ## b" := (dr W a b) (at level 1, only parsing) : asm. +Notation "a ### b" := (dr X a b) (at level 1, only parsing) : asm. Open Scope asm. @@ -1192,7 +1200,19 @@ Definition if_opt_bool_val (c: option bool) v1 v2: val := | None => Vundef end. -Definition arith_eval_pp i v := +Definition arith_pd_isize (i : arith_pd) := + match i with + | Pandimm is _ | Peorimm is _ | Porrimm is _ => is + (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *) + | Pmov | Pmovk _ _ _ | Paddadr _ _ | Psbfiz _ _ _ + | Psbfx _ _ _ | Pubfiz _ _ _ | Pubfx _ _ _ | Pfmov + | Pfcvtds | Pfcvtsd | Pfabs _ | Pfneg _ + | Pscvtf _ _ | Pucvtf _ _ | Pfcvtzs _ _ | Pfcvtzu _ _ + | Paddimm _ _ | Psubimm _ _ + => W + end. + +Definition arith_eval_pd i v := match i with | Pmov => v | Pmovk W n pos => insert_in_int v n pos 16 @@ -1233,9 +1253,28 @@ Definition arith_eval_pp 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) := + match i with + | Padd is _ | Psub is _ | Pand is _ | Pbic is _ + | Peon is _ | Peor is _ | Porr is _ | Porn is _ + => 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 _ + => W end. -Definition arith_eval_ppp i v1 v2 := +Definition arith_eval_pdd i v1 v2 := match i with | Pasrv W => Val.shr v1 v2 | Pasrv X => Val.shrl v1 v2 @@ -1261,23 +1300,6 @@ Definition arith_eval_ppp 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) @@ -1296,29 +1318,12 @@ Definition arith_eval_rr0r i v1 v2 := | Porn X s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s)) end. -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 - | 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_arrrr0_isize (i : arith_arrrr0) := +Definition arith_apddd_isize (i : arith_apddd) := 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 := +Definition arith_eval_apddd 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) @@ -1326,22 +1331,20 @@ Definition arith_eval_arrrr0 i v1 v2 v3 := | Pmsub X => Val.subl v3 (Val.mull v1 v2) end. -Definition arith_prepare_comparison_pp i (v1 v2 : val) := +Definition arith_comparison_dd_isize i := match i with - | Pcmpext x => (v1, (eval_extend v2 x)) - | Pcmnext x => (v1, (Val.negl (eval_extend v2 x))) - | Pfcmp _ => (v1, v2) + | Pcmp is _ | Pcmn is _ | Ptst is _ + => is + (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *) + | Pcmpext _ | Pcmnext _ | Pfcmp _ + => W 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 := +Definition arith_prepare_comparison_dd 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) | 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))) @@ -1350,7 +1353,14 @@ Definition arith_prepare_comparison_r0r i v1 v2 := | Ptst X s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero)) end. -Definition arith_prepare_comparison_p i v := +Definition arith_comparison_d_isize i := + match i with + (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *) + | Pcmpimm _ _ | Pcmnimm _ _ | Ptstimm _ _ | Pfcmp0 _ + => W + end. + +Definition arith_prepare_comparison_d i v := match i with | Pcmpimm W n => (v, (Vint (Int.repr n))) | Pcmpimm X n => (v, (Vlong (Int64.repr n))) @@ -1362,14 +1372,17 @@ Definition arith_prepare_comparison_p i v := | Pfcmp0 D => (v, (Vfloat Float.zero)) end. -Definition arith_comparison_pp_compare i := +Definition arith_comparison_dd_compare i := match i with - | Pcmpext _ | Pcmnext _ => compare_long + | Pcmp W _ | Pcmn W _ | Ptst W _ + => compare_int + | Pcmp X _ | Pcmn X _ | Ptst X _ | Pcmpext _ | Pcmnext _ + => compare_long | Pfcmp S => compare_single | Pfcmp D => compare_float end. -Definition arith_comparison_p_compare i := +Definition arith_comparison_d_compare i := match i with | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long @@ -1380,26 +1393,28 @@ Definition arith_comparison_p_compare i := Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := match ai with | 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 + | PArithPD i d s => + let is := arith_pd_isize i in + let get_val := (dr is rs) in + rs#d <- (arith_eval_pd i (get_val s)) + | PArithPDD i d s1 s2 => + let is := arith_pdd_isize i in + let get_val := (dr is rs) in + rs#d <- (arith_eval_pdd i (get_val s1) (get_val s2)) + | PArithAPDDD i d s1 s2 s3 => + let is := arith_apddd_isize i in + let get_val := (dr is rs) in + rs#d <- (arith_eval_apddd i (get_val s1) (get_val s2) (get_val s3)) + | PArithComparisonDD i s1 s2 => + let is := arith_comparison_dd_isize i in + let get_val := (dr is rs) in + let (v1, v2) := arith_prepare_comparison_dd i (get_val s1) (get_val s2) in + 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 + let (v1, v2) := arith_prepare_comparison_d i (get_val s) in + arith_comparison_d_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) |