From 8dfd1db5c496821b8cb94ce7b121e4b9bba3d265 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 7 Dec 2020 23:51:58 +0100 Subject: Some cleanup in todos --- aarch64/Asmblock.v | 622 ++------------------------------------------------ aarch64/Asmblockgen.v | 12 - aarch64/Asmgenproof.v | 2 - aarch64/Peephole.v | 1 - 4 files changed, 13 insertions(+), 624 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 16f8e0c0..f12e8922 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -82,8 +82,6 @@ Inductive control: Type := (args: list (builtin_arg dreg)) (res: builtin_res dreg) (**r built-in function (pseudo) *) . -Coercion PCtlFlow: cf_instruction >-> control. - (** Basic instructions *) (* Loads waiting for (rd: dreg) (a: addressing) @@ -319,7 +317,7 @@ Inductive ar_instruction : Type := . Inductive basic : Type := - | PArith (i: ar_instruction) (**r TODO *) + | PArith (i: ar_instruction) | PLoad (ld: ld_instruction) | PStore (st: st_instruction) | Pallocframe (sz: Z) (linkofs: ptrofs) (**r allocate new stack frame *) @@ -335,8 +333,20 @@ Inductive basic : Type := *) . +Coercion PCtlFlow: cf_instruction >-> control. Coercion PLoad: ld_instruction >-> basic. Coercion PStore : st_instruction >-> basic. +Coercion PArithP: arith_p >-> Funclass. +Coercion PArithPP: arith_pp >-> Funclass. +Coercion PArithPPP: arith_ppp >-> Funclass. +Coercion PArithRR0: arith_rr0 >-> Funclass. +Coercion PArithRR0R: arith_rr0r >-> Funclass. +Coercion PArithARRRR0: arith_arrrr0 >-> Funclass. +Coercion PArithComparisonP: arith_comparison_p >-> Funclass. +Coercion PArithComparisonPP: arith_comparison_pp >-> Funclass. +Coercion PArithComparisonR0R: arith_comparison_r0r >-> Funclass. +Coercion PArith: ar_instruction >-> basic. + (* Not used in Coq, declared in ocaml directly in PostpassSchedulingOracle.ml Inductive instruction : Type := @@ -414,160 +424,6 @@ Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }. Definition fundef := AST.fundef function. Definition program := AST.program fundef unit. -(* TODO: ORIGINAL ABSTRACT SYNTAX OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED ! - -Inductive instruction: Type := - (** Branches *) - | Pb (lbl: label) (**r branch *) - | Pbc (c: testcond) (lbl: label) (**r conditional branch *) - | Pbl (id: ident) (sg: signature) (**r jump to function and link *) - | Pbs (id: ident) (sg: signature) (**r jump to function *) - | Pblr (r: ireg) (sg: signature) (**r indirect jump and link *) - | Pbr (r: ireg) (sg: signature) (**r indirect jump *) - | Pret (r: ireg) (**r return *) - | Pcbnz (sz: isize) (r: ireg) (lbl: label) (**r branch if not zero *) - | Pcbz (sz: isize) (r: ireg) (lbl: label) (**r branch if zero *) - | Ptbnz (sz: isize) (r: ireg) (n: int) (lbl: label) (**r branch if bit n is not zero *) - | Ptbz (sz: isize) (r: ireg) (n: int) (lbl: label) (**r branch if bit n is zero *) - (** Memory loads and stores *) - | Pldrw (rd: ireg) (a: addressing) (**r load int32 *) - | Pldrw_a (rd: ireg) (a: addressing) (**r load int32 as any32 *) - | Pldrx (rd: ireg) (a: addressing) (**r load int64 *) - | Pldrx_a (rd: ireg) (a: addressing) (**r load int64 as any64 *) - | Pldrb (sz: isize) (rd: ireg) (a: addressing) (**r load int8, zero-extend *) - | Pldrsb (sz: isize) (rd: ireg) (a: addressing) (**r load int8, sign-extend *) - | Pldrh (sz: isize) (rd: ireg) (a: addressing) (**r load int16, zero-extend *) - | Pldrsh (sz: isize) (rd: ireg) (a: addressing) (**r load int16, sign-extend *) - | Pldrzw (rd: ireg) (a: addressing) (**r load int32, zero-extend to int64 *) - | Pldrsw (rd: ireg) (a: addressing) (**r load int32, sign-extend to int64 *) - | Pldp (rd1 rd2: ireg) (a: addressing) (**r load two int64 *) - | Pstrw (rs: ireg) (a: addressing) (**r store int32 *) - | Pstrw_a (rs: ireg) (a: addressing) (**r store int32 as any32 *) - | Pstrx (rs: ireg) (a: addressing) (**r store int64 *) - | Pstrx_a (rs: ireg) (a: addressing) (**r store int64 as any64 *) - | Pstrb (rs: ireg) (a: addressing) (**r store int8 *) - | Pstrh (rs: ireg) (a: addressing) (**r store int16 *) - | Pstp (rs1 rs2: ireg) (a: addressing) (**r store two int64 *) - (** Integer arithmetic, immediate *) - | Paddimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z) (**r addition *) - | Psubimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z) (**r subtraction *) - | Pcmpimm (sz: isize) (r1: ireg) (n: Z) (**r compare *) - | Pcmnimm (sz: isize) (r1: ireg) (n: Z) (**r compare negative *) - (** Move integer register *) - | Pmov (rd: iregsp) (r1: iregsp) - (** Logical, immediate *) - | Pandimm (sz: isize) (rd: ireg) (r1: ireg0) (n: Z) (**r and *) - | Peorimm (sz: isize) (rd: ireg) (r1: ireg0) (n: Z) (**r xor *) - | Porrimm (sz: isize) (rd: ireg) (r1: ireg0) (n: Z) (**r or *) - | Ptstimm (sz: isize) (r1: ireg) (n: Z) (**r and, then set flags *) - (** Move wide immediate *) - | Pmovz (sz: isize) (rd: ireg) (n: Z) (pos: Z) (**r move [n << pos] to [rd] *) - | Pmovn (sz: isize) (rd: ireg) (n: Z) (pos: Z) (**r move [NOT(n << pos)] to [rd] *) - | Pmovk (sz: isize) (rd: ireg) (n: Z) (pos: Z) (**r insert 16 bits of [n] at [pos] in rd *) - (** PC-relative addressing *) - | Padrp (rd: ireg) (id: ident) (ofs: ptrofs) (**r set [rd] to high address of [id + ofs] *) - | Paddadr (rd: ireg) (r1: ireg) (id: ident) (ofs: ptrofs) (**r add the low address of [id + ofs] *) - (** Bit-field operations *) - | Psbfiz (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z) (**r sign extend and shift left *) - | Psbfx (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z) (**r shift right and sign extend *) - | Pubfiz (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z) (**r zero extend and shift left *) - | Pubfx (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z) (**r shift right and zero extend *) - (** Integer arithmetic, shifted register *) - | Padd (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op) (**r addition *) - | Psub (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op) (**r subtraction *) - | Pcmp (sz: isize) (r1: ireg0) (r2: ireg) (s: shift_op) (**r compare *) - | Pcmn (sz: isize) (r1: ireg0) (r2: ireg) (s: shift_op) (**r compare negative *) - (** Integer arithmetic, extending register *) - | Paddext (rd: iregsp) (r1: iregsp) (r2: ireg) (x: extend_op) (**r int64-int32 add *) - | Psubext (rd: iregsp) (r1: iregsp) (r2: ireg) (x: extend_op) (**r int64-int32 sub *) - | Pcmpext (r1: ireg) (r2: ireg) (x: extend_op) (**r int64-int32 cmp *) - | Pcmnext (r1: ireg) (r2: ireg) (x: extend_op) (**r int64-int32 cmn *) - (** Logical, shifted register *) - | Pand (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op) (**r and *) - | Pbic (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op) (**r and-not *) - | Peon (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op) (**r xor-not *) - | Peor (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op) (**r xor *) - | Porr (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op) (**r or *) - | Porn (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op) (**r or-not *) - | Ptst (sz: isize) (r1: ireg0) (r2: ireg) (s: shift_op) (**r and, then set flags *) - (** Variable shifts *) - | Pasrv (sz: isize) (rd: ireg) (r1 r2: ireg) (**r arithmetic right shift *) - | Plslv (sz: isize) (rd: ireg) (r1 r2: ireg) (**r left shift *) - | Plsrv (sz: isize) (rd: ireg) (r1 r2: ireg) (**r logical right shift *) - | Prorv (sz: isize) (rd: ireg) (r1 r2: ireg) (**r rotate right *) - (** Bit operations *) - | Pcls (sz: isize) (rd r1: ireg) (**r count leading sign bits *) - | Pclz (sz: isize) (rd r1: ireg) (**r count leading zero bits *) - | Prev (sz: isize) (rd r1: ireg) (**r reverse bytes *) - | Prev16 (sz: isize) (rd r1: ireg) (**r reverse bytes in each 16-bit word *) - (** Conditional data processing *) - | Pcsel (rd: ireg) (r1 r2: ireg) (c: testcond) (**r int conditional move *) - | Pcset (rd: ireg) (c: testcond) (**r set to 1/0 if cond is true/false *) -(* - | Pcsetm (rd: ireg) (c: testcond) (**r set to -1/0 if cond is true/false *) -*) - (** Integer multiply/divide *) - | Pmadd (sz: isize) (rd: ireg) (r1 r2: ireg) (r3: ireg0) (**r multiply-add *) - | Pmsub (sz: isize) (rd: ireg) (r1 r2: ireg) (r3: ireg0) (**r multiply-sub *) - | Psmulh (rd: ireg) (r1 r2: ireg) (**r signed multiply high *) - | Pumulh (rd: ireg) (r1 r2: ireg) (**r unsigned multiply high *) - | Psdiv (sz: isize) (rd: ireg) (r1 r2: ireg) (**r signed division *) - | Pudiv (sz: isize) (rd: ireg) (r1 r2: ireg) (**r unsigned division *) - (** Floating-point loads and stores *) - | Pldrs (rd: freg) (a: addressing) (**r load float32 (single precision) *) - | Pldrd (rd: freg) (a: addressing) (**r load float64 (double precision) *) - | Pldrd_a (rd: freg) (a: addressing) (**r load float64 as any64 *) - | Pstrs (rs: freg) (a: addressing) (**r store float32 *) - | Pstrd (rs: freg) (a: addressing) (**r store float64 *) - | Pstrd_a (rs: freg) (a: addressing) (**r store float64 as any64 *) - (** Floating-point move *) - | Pfmov (rd r1: freg) - | Pfmovimms (rd: freg) (f: float32) (**r load float32 constant *) - | Pfmovimmd (rd: freg) (f: float) (**r load float64 constant *) - | Pfmovi (fsz: fsize) (rd: freg) (r1: ireg0) (**r copy int reg to FP reg *) - (** Floating-point conversions *) - | Pfcvtds (rd r1: freg) (**r convert float32 to float64 *) - | Pfcvtsd (rd r1: freg) (**r convert float64 to float32 *) - | Pfcvtzs (isz: isize) (fsz: fsize) (rd: ireg) (r1: freg) (**r convert float to signed int *) - | Pfcvtzu (isz: isize) (fsz: fsize) (rd: ireg) (r1: freg) (**r convert float to unsigned int *) - | Pscvtf (fsz: fsize) (isz: isize) (rd: freg) (r1: ireg) (**r convert signed int to float *) - | Pucvtf (fsz: fsize) (isz: isize) (rd: freg) (r1: ireg) (**r convert unsigned int to float *) - (** Floating-point arithmetic *) - | Pfabs (sz: fsize) (rd r1: freg) (**r absolute value *) - | Pfneg (sz: fsize) (rd r1: freg) (**r negation *) - | Pfsqrt (sz: fsize) (rd r1: freg) (**r square root *) - | Pfadd (sz: fsize) (rd r1 r2: freg) (**r addition *) - | Pfdiv (sz: fsize) (rd r1 r2: freg) (**r division *) - | Pfmul (sz: fsize) (rd r1 r2: freg) (**r multiplication *) - | Pfnmul (sz: fsize) (rd r1 r2: freg) (**r multiply-negate *) - | Pfsub (sz: fsize) (rd r1 r2: freg) (**r subtraction *) - | Pfmadd (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = r3 + r1 * r2] *) - | Pfmsub (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = r3 - r1 * r2] *) - | Pfnmadd (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = - r3 - r1 * r2] *) - | Pfnmsub (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = - r3 + r1 * r2] *) - (** Floating-point comparison *) - | Pfcmp (sz: fsize) (r1 r2: freg) (**r compare [r1] and [r2] *) - | Pfcmp0 (sz: fsize) (r1: freg) (**r compare [r1] and [+0.0] *) - (** Floating-point conditional select *) - | Pfsel (rd r1 r2: freg) (cond: testcond) - (** Pseudo-instructions *) - | Pallocframe (sz: Z) (linkofs: ptrofs) (**r allocate new stack frame *) - | Pfreeframe (sz: Z) (linkofs: ptrofs) (**r deallocate stack frame and restore previous frame *) - | Plabel (lbl: label) (**r define a code label *) - | Ploadsymbol (rd: ireg) (id: ident) (**r load the address of [id] *) - | Pcvtsw2x (rd: ireg) (r1: ireg) (**r sign-extend 32-bit int to 64-bit *) - | Pcvtuw2x (rd: ireg) (r1: ireg) (**r zero-extend 32-bit int to 64-bit *) - | Pcvtx2w (rd: ireg) (**r retype a 64-bit int as a 32-bit int *) - | Pbtbl (r1: ireg) (tbl: list label) (**r N-way branch through a jump table *) - | Pbuiltin (ef: external_function) - (args: list (builtin_arg preg)) (res: builtin_res preg) (**r built-in function (pseudo) *) - | Pnop (**r no operation *) - | Pcfi_adjust (ofs: int) (**r .cfi_adjust debug directive *) - | Pcfi_rel_offset (ofs: int) (**r .cfi_rel_offset debug directive *) -. -*) - - (** * Operational semantics *) (** See "Parameters" of the same names in Asm.v *) @@ -1069,458 +925,6 @@ Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome := | Pnop => Next rs m end. -(* TODO: ORIGINAL EXECUTION OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED ! - -(** Execution of a single instruction [i] in initial state - [rs] and [m]. Return updated state. For instructions - that correspond to actual AArch64 instructions, the cases are - straightforward transliterations of the informal descriptions - given in the ARMv8 reference manuals. For pseudo-instructions, - refer to the informal descriptions given above. - - Note that we set to [Vundef] the registers used as temporaries by - the expansions of the pseudo-instructions, so that the code we - generate cannot use those registers to hold values that must - survive the execution of the pseudo-instruction. -*) - -Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome := - match i with - (** Branches *) - | Pb lbl => - goto_label f lbl rs m - | Pbc cond lbl => - match eval_testcond cond rs with - | Some true => goto_label f lbl rs m - | Some false => Next (nextinstr rs) m - | None => Stuck - end - | Pbl id sg => - Next (rs#RA <- (Val.offset_ptr rs#PC Ptrofs.one) #PC <- (Genv.symbol_address ge id Ptrofs.zero)) m - | Pbs id sg => - Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m - | Pblr r sg => - Next (rs#RA <- (Val.offset_ptr rs#PC Ptrofs.one) #PC <- (rs#r)) m - | Pbr r sg => - Next (rs#PC <- (rs#r)) m - | Pret r => - Next (rs#PC <- (rs#r)) m - | Pcbnz sz r lbl => - match eval_testzero sz rs#r m with - | Some true => Next (nextinstr rs) m - | Some false => goto_label f lbl rs m - | None => Stuck - end - | Pcbz sz r lbl => - match eval_testzero sz rs#r m with - | Some true => goto_label f lbl rs m - | Some false => Next (nextinstr rs) m - | None => Stuck - end - | Ptbnz sz r n lbl => - match eval_testbit sz rs#r n with - | Some true => goto_label f lbl rs m - | Some false => Next (nextinstr rs) m - | None => Stuck - end - | Ptbz sz r n lbl => - match eval_testbit sz rs#r n with - | Some true => Next (nextinstr rs) m - | Some false => goto_label f lbl rs m - | None => Stuck - end - (** Memory loads and stores *) - | Pldrw rd a => - exec_load Mint32 (fun v => v) a rd rs m - | Pldrw_a rd a => - exec_load Many32 (fun v => v) a rd rs m - | Pldrx rd a => - exec_load Mint64 (fun v => v) a rd rs m - | Pldrx_a rd a => - exec_load Many64 (fun v => v) a rd rs m - | Pldrb W rd a => - exec_load Mint8unsigned (fun v => v) a rd rs m - | Pldrb X rd a => - exec_load Mint8unsigned Val.longofintu a rd rs m - | Pldrsb W rd a => - exec_load Mint8signed (fun v => v) a rd rs m - | Pldrsb X rd a => - exec_load Mint8signed Val.longofint a rd rs m - | Pldrh W rd a => - exec_load Mint16unsigned (fun v => v) a rd rs m - | Pldrh X rd a => - exec_load Mint16unsigned Val.longofintu a rd rs m - | Pldrsh W rd a => - exec_load Mint16signed (fun v => v) a rd rs m - | Pldrsh X rd a => - exec_load Mint16signed Val.longofint a rd rs m - | Pldrzw rd a => - exec_load Mint32 Val.longofintu a rd rs m - | Pldrsw rd a => - exec_load Mint32 Val.longofint a rd rs m - | Pstrw r a => - exec_store Mint32 a rs#r rs m - | Pstrw_a r a => - exec_store Many32 a rs#r rs m - | Pstrx r a => - exec_store Mint64 a rs#r rs m - | Pstrx_a r a => - exec_store Many64 a rs#r rs m - | Pstrb r a => - exec_store Mint8unsigned a rs#r rs m - | Pstrh r a => - exec_store Mint16unsigned a rs#r rs m - (** Integer arithmetic, immediate *) - | Paddimm W rd r1 n => - Next (nextinstr (rs#rd <- (Val.add rs#r1 (Vint (Int.repr n))))) m - | Paddimm X rd r1 n => - Next (nextinstr (rs#rd <- (Val.addl rs#r1 (Vlong (Int64.repr n))))) m - | Psubimm W rd r1 n => - Next (nextinstr (rs#rd <- (Val.sub rs#r1 (Vint (Int.repr n))))) m - | Psubimm X rd r1 n => - Next (nextinstr (rs#rd <- (Val.subl rs#r1 (Vlong (Int64.repr n))))) m - | Pcmpimm W r1 n => - Next (nextinstr (compare_int rs rs#r1 (Vint (Int.repr n)) m)) m - | Pcmpimm X r1 n => - Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.repr n)) m)) m - | Pcmnimm W r1 n => - Next (nextinstr (compare_int rs rs#r1 (Vint (Int.neg (Int.repr n))) m)) m - | Pcmnimm X r1 n => - Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.neg (Int64.repr n))) m)) m - (** Move integer register *) - | Pmov rd r1 => - Next (nextinstr (rs#rd <- (rs#r1))) m - (** Logical, immediate *) - | Pandimm W rd r1 n => - Next (nextinstr (rs#rd <- (Val.and rs##r1 (Vint (Int.repr n))))) m - | Pandimm X rd r1 n => - Next (nextinstr (rs#rd <- (Val.andl rs###r1 (Vlong (Int64.repr n))))) m - | Peorimm W rd r1 n => - Next (nextinstr (rs#rd <- (Val.xor rs##r1 (Vint (Int.repr n))))) m - | Peorimm X rd r1 n => - Next (nextinstr (rs#rd <- (Val.xorl rs###r1 (Vlong (Int64.repr n))))) m - | Porrimm W rd r1 n => - Next (nextinstr (rs#rd <- (Val.or rs##r1 (Vint (Int.repr n))))) m - | Porrimm X rd r1 n => - Next (nextinstr (rs#rd <- (Val.orl rs###r1 (Vlong (Int64.repr n))))) m - | Ptstimm W r1 n => - Next (nextinstr (compare_int rs (Val.and rs#r1 (Vint (Int.repr n))) (Vint Int.zero) m)) m - | Ptstimm X r1 n => - Next (nextinstr (compare_long rs (Val.andl rs#r1 (Vlong (Int64.repr n))) (Vlong Int64.zero) m)) m - (** Move wide immediate *) - | Pmovz W rd n pos => - Next (nextinstr (rs#rd <- (Vint (Int.repr (Z.shiftl n pos))))) m - | Pmovz X rd n pos => - Next (nextinstr (rs#rd <- (Vlong (Int64.repr (Z.shiftl n pos))))) m - | Pmovn W rd n pos => - Next (nextinstr (rs#rd <- (Vint (Int.repr (Z.lnot (Z.shiftl n pos)))))) m - | Pmovn X rd n pos => - Next (nextinstr (rs#rd <- (Vlong (Int64.repr (Z.lnot (Z.shiftl n pos)))))) m - | Pmovk W rd n pos => - Next (nextinstr (rs#rd <- (insert_in_int rs#rd n pos 16))) m - | Pmovk X rd n pos => - Next (nextinstr (rs#rd <- (insert_in_long rs#rd n pos 16))) m - (** PC-relative addressing *) - | Padrp rd id ofs => - Next (nextinstr (rs#rd <- (symbol_high ge id ofs))) m - | Paddadr rd r1 id ofs => - Next (nextinstr (rs#rd <- (Val.addl rs#r1 (symbol_low ge id ofs)))) m - (** Bit-field operations *) - | Psbfiz W rd r1 r s => - Next (nextinstr (rs#rd <- (Val.shl (Val.sign_ext s rs#r1) (Vint r)))) m - | Psbfiz X rd r1 r s => - Next (nextinstr (rs#rd <- (Val.shll (Val.sign_ext_l s rs#r1) (Vint r)))) m - | Psbfx W rd r1 r s => - Next (nextinstr (rs#rd <- (Val.sign_ext s (Val.shr rs#r1 (Vint r))))) m - | Psbfx X rd r1 r s => - Next (nextinstr (rs#rd <- (Val.sign_ext_l s (Val.shrl rs#r1 (Vint r))))) m - | Pubfiz W rd r1 r s => - Next (nextinstr (rs#rd <- (Val.shl (Val.zero_ext s rs#r1) (Vint r)))) m - | Pubfiz X rd r1 r s => - Next (nextinstr (rs#rd <- (Val.shll (Val.zero_ext_l s rs#r1) (Vint r)))) m - | Pubfx W rd r1 r s => - Next (nextinstr (rs#rd <- (Val.zero_ext s (Val.shru rs#r1 (Vint r))))) m - | Pubfx X rd r1 r s => - Next (nextinstr (rs#rd <- (Val.zero_ext_l s (Val.shrlu rs#r1 (Vint r))))) m - (** Integer arithmetic, shifted register *) - | Padd W rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.add rs##r1 (eval_shift_op_int rs#r2 s)))) m - | Padd X rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.addl rs###r1 (eval_shift_op_long rs#r2 s)))) m - | Psub W rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.sub rs##r1 (eval_shift_op_int rs#r2 s)))) m - | Psub X rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.subl rs###r1 (eval_shift_op_long rs#r2 s)))) m - | Pcmp W r1 r2 s => - Next (nextinstr (compare_int rs rs##r1 (eval_shift_op_int rs#r2 s) m)) m - | Pcmp X r1 r2 s => - Next (nextinstr (compare_long rs rs###r1 (eval_shift_op_long rs#r2 s) m)) m - | Pcmn W r1 r2 s => - Next (nextinstr (compare_int rs rs##r1 (Val.neg (eval_shift_op_int rs#r2 s)) m)) m - | Pcmn X r1 r2 s => - Next (nextinstr (compare_long rs rs###r1 (Val.negl (eval_shift_op_long rs#r2 s)) m)) m - (** Integer arithmetic, extending register *) - | Paddext rd r1 r2 x => - Next (nextinstr (rs#rd <- (Val.addl rs#r1 (eval_extend rs#r2 x)))) m - | Psubext rd r1 r2 x => - Next (nextinstr (rs#rd <- (Val.subl rs#r1 (eval_extend rs#r2 x)))) m - | Pcmpext r1 r2 x => - Next (nextinstr (compare_long rs rs#r1 (eval_extend rs#r2 x) m)) m - | Pcmnext r1 r2 x => - Next (nextinstr (compare_long rs rs#r1 (Val.negl (eval_extend rs#r2 x)) m)) m - (** Logical, shifted register *) - | Pand W rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.and rs##r1 (eval_shift_op_int rs#r2 s)))) m - | Pand X rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.andl rs###r1 (eval_shift_op_long rs#r2 s)))) m - | Pbic W rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.and rs##r1 (Val.notint (eval_shift_op_int rs#r2 s))))) m - | Pbic X rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.andl rs###r1 (Val.notl (eval_shift_op_long rs#r2 s))))) m - | Peon W rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.xor rs##r1 (Val.notint (eval_shift_op_int rs#r2 s))))) m - | Peon X rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.xorl rs###r1 (Val.notl (eval_shift_op_long rs#r2 s))))) m - | Peor W rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.xor rs##r1 (eval_shift_op_int rs#r2 s)))) m - | Peor X rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.xorl rs###r1 (eval_shift_op_long rs#r2 s)))) m - | Porr W rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.or rs##r1 (eval_shift_op_int rs#r2 s)))) m - | Porr X rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.orl rs###r1 (eval_shift_op_long rs#r2 s)))) m - | Porn W rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.or rs##r1 (Val.notint (eval_shift_op_int rs#r2 s))))) m - | Porn X rd r1 r2 s => - Next (nextinstr (rs#rd <- (Val.orl rs###r1 (Val.notl (eval_shift_op_long rs#r2 s))))) m - | Ptst W r1 r2 s => - Next (nextinstr (compare_int rs (Val.and rs##r1 (eval_shift_op_int rs#r2 s)) (Vint Int.zero) m)) m - | Ptst X r1 r2 s => - Next (nextinstr (compare_long rs (Val.andl rs###r1 (eval_shift_op_long rs#r2 s)) (Vlong Int64.zero) m)) m - (** Variable shifts *) - | Pasrv W rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2))) m - | Pasrv X rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.shrl rs#r1 rs#r2))) m - | Plslv W rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m - | Plslv X rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.shll rs#r1 rs#r2))) m - | Plsrv W rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.shru rs#r1 rs#r2))) m - | Plsrv X rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.shrlu rs#r1 rs#r2))) m - | Prorv W rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.ror rs#r1 rs#r2))) m - | Prorv X rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.rorl rs#r1 rs#r2))) m - (** Conditional data processing *) - | Pcsel rd r1 r2 cond => - let v := - match eval_testcond cond rs with - | Some true => rs#r1 - | Some false => rs#r2 - | None => Vundef - end in - Next (nextinstr (rs#rd <- v)) m - | Pcset rd cond => - let v := - match cond rs with - | Some true => Vint Int.one - | Some false => Vint Int.zero - | None => Vundef - end in - Next (nextinstr (rs#rd <- v)) m - (** Integer multiply/divide *) - | Pmadd W rd r1 r2 r3 => - Next (nextinstr (rs#rd <- (Val.add rs##r3 (Val.mul rs#r1 rs#r2)))) m - | Pmadd X rd r1 r2 r3 => - Next (nextinstr (rs#rd <- (Val.addl rs###r3 (Val.mull rs#r1 rs#r2)))) m - | Pmsub W rd r1 r2 r3 => - Next (nextinstr (rs#rd <- (Val.sub rs##r3 (Val.mul rs#r1 rs#r2)))) m - | Pmsub X rd r1 r2 r3 => - Next (nextinstr (rs#rd <- (Val.subl rs###r3 (Val.mull rs#r1 rs#r2)))) m - | Psmulh rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.mullhs rs#r1 rs#r2))) m - | Pumulh rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.mullhu rs#r1 rs#r2))) m - | Psdiv W rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.divs rs#r1 rs#r2)))) m - | Psdiv X rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.divls rs#r1 rs#r2)))) m - | Pudiv W rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.divu rs#r1 rs#r2)))) m - | Pudiv X rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.divlu rs#r1 rs#r2)))) m - (** Floating-point loads and stores *) - | Pldrs rd a => - exec_load Mfloat32 (fun v => v) a rd rs m - | Pldrd rd a => - exec_load Mfloat64 (fun v => v) a rd rs m - | Pldrd_a rd a => - exec_load Many64 (fun v => v) a rd rs m - | Pstrs r a => - exec_store Mfloat32 a rs#r rs m - | Pstrd r a => - exec_store Mfloat64 a rs#r rs m - | Pstrd_a r a => - exec_store Many64 a rs#r rs m - (** Floating-point move *) - | Pfmov rd r1 => - Next (nextinstr (rs#rd <- (rs#r1))) m - | Pfmovimms rd f => - Next (nextinstr (rs#rd <- (Vsingle f))) m - | Pfmovimmd rd f => - Next (nextinstr (rs#rd <- (Vfloat f))) m - | Pfmovi S rd r1 => - Next (nextinstr (rs#rd <- (float32_of_bits rs##r1))) m - | Pfmovi D rd r1 => - Next (nextinstr (rs#rd <- (float64_of_bits rs###r1))) m - (** Floating-point conversions *) - | Pfcvtds rd r1 => - Next (nextinstr (rs#rd <- (Val.floatofsingle rs#r1))) m - | Pfcvtsd rd r1 => - Next (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m - | Pfcvtzs W S rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.intofsingle rs#r1)))) m - | Pfcvtzs W D rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m - | Pfcvtzs X S rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.longofsingle rs#r1)))) m - | Pfcvtzs X D rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m - | Pfcvtzu W S rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.intuofsingle rs#r1)))) m - | Pfcvtzu W D rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m - | Pfcvtzu X S rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.longuofsingle rs#r1)))) m - | Pfcvtzu X D rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.longuoffloat rs#r1)))) m - | Pscvtf S W rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleofint rs#r1)))) m - | Pscvtf D W rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m - | Pscvtf S X rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleoflong rs#r1)))) m - | Pscvtf D X rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong rs#r1)))) m - | Pucvtf S W rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleofintu rs#r1)))) m - | Pucvtf D W rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m - | Pucvtf S X rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleoflongu rs#r1)))) m - | Pucvtf D X rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflongu rs#r1)))) m - (** Floating-point arithmetic *) - | Pfabs S rd r1 => - Next (nextinstr (rs#rd <- (Val.absfs rs#r1))) m - | Pfabs D rd r1 => - Next (nextinstr (rs#rd <- (Val.absf rs#r1))) m - | Pfneg S rd r1 => - Next (nextinstr (rs#rd <- (Val.negfs rs#r1))) m - | Pfneg D rd r1 => - Next (nextinstr (rs#rd <- (Val.negf rs#r1))) m - | Pfadd S rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m - | Pfadd D rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m - | Pfdiv S rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.divfs rs#r1 rs#r2))) m - | Pfdiv D rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m - | Pfmul S rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.mulfs rs#r1 rs#r2))) m - | Pfmul D rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m - | Pfnmul S rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.negfs (Val.mulfs rs#r1 rs#r2)))) m - | Pfnmul D rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.negf (Val.mulf rs#r1 rs#r2)))) m - | Pfsub S rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.subfs rs#r1 rs#r2))) m - | Pfsub D rd r1 r2 => - Next (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m - (** Floating-point comparison *) - | Pfcmp S r1 r2 => - Next (nextinstr (compare_single rs rs#r1 rs#r2)) m - | Pfcmp D r1 r2 => - Next (nextinstr (compare_float rs rs#r1 rs#r2)) m - | Pfcmp0 S r1 => - Next (nextinstr (compare_single rs rs#r1 (Vsingle Float32.zero))) m - | Pfcmp0 D r1 => - Next (nextinstr (compare_float rs rs#r1 (Vfloat Float.zero))) m - (** Floating-point conditional select *) - | Pfsel rd r1 r2 cond => - let v := - match eval_testcond cond rs with - | Some true => rs#r1 - | Some false => rs#r2 - | None => Vundef - end in - Next (nextinstr (rs#rd <- v)) m - (** Pseudo-instructions *) - | Pallocframe sz pos => - let (m1, stk) := Mem.alloc m 0 sz in - let sp := (Vptr stk Ptrofs.zero) in - match Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP with - | None => Stuck - | Some m2 => Next (nextinstr (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef)) m2 - end - | Pfreeframe sz pos => - match Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) with - | None => Stuck - | Some v => - match rs#SP with - | Vptr stk ofs => - match Mem.free m stk 0 sz with - | None => Stuck - | Some m' => Next (nextinstr (rs#SP <- v #X16 <- Vundef)) m' - end - | _ => Stuck - end - end - | Plabel lbl => - Next (nextinstr rs) m - | Ploadsymbol rd id => - Next (nextinstr (rs#rd <- (Genv.symbol_address ge id Ptrofs.zero))) m - | Pcvtsw2x rd r1 => - Next (nextinstr (rs#rd <- (Val.longofint rs#r1))) m - | Pcvtuw2x rd r1 => - Next (nextinstr (rs#rd <- (Val.longofintu rs#r1))) m - | Pcvtx2w rd => - Next (nextinstr (rs#rd <- (Val.loword rs#rd))) m - | Pbtbl r tbl => - match (rs#X16 <- Vundef)#r with - | Vint n => - match list_nth_z tbl (Int.unsigned n) with - | None => Stuck - | Some lbl => goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m - end - | _ => Stuck - end - | Pbuiltin ef args res => Stuck (**r treated specially below *) - (** The following instructions and directives are not generated directly - by Asmgen, so we do not model them. *) - | Pldp _ _ _ - | Pstp _ _ _ - | Pcls _ _ _ - | Pclz _ _ _ - | Prev _ _ _ - | Prev16 _ _ _ - | Pfsqrt _ _ _ - | Pfmadd _ _ _ _ _ - | Pfmsub _ _ _ _ _ - | Pfnmadd _ _ _ _ _ - | Pfnmsub _ _ _ _ _ - | Pnop - | Pcfi_adjust _ - | Pcfi_rel_offset _ => - Stuck - end. -*) - (** execution of the body of a bblock *) Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := match body with diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 137b5871..fbbf7507 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -157,18 +157,6 @@ Program Definition insert_basic (bi: basic) (k:bblocks): bblocks := Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity). -(* TODO: Coercions to move in Asmblock ? *) -Coercion PArithP: arith_p >-> Funclass. -Coercion PArithPP: arith_pp >-> Funclass. -Coercion PArithPPP: arith_ppp >-> Funclass. -Coercion PArithRR0: arith_rr0 >-> Funclass. -Coercion PArithRR0R: arith_rr0r >-> Funclass. -Coercion PArithARRRR0: arith_arrrr0 >-> Funclass. -Coercion PArithComparisonP: arith_comparison_p >-> Funclass. -Coercion PArithComparisonPP: arith_comparison_pp >-> Funclass. -Coercion PArithComparisonR0R: arith_comparison_r0r >-> Funclass. -Coercion PArith: ar_instruction >-> basic. - (* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *) (** Alignment check for symbols *) Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity). diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index eac406a1..793d94f9 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -807,7 +807,6 @@ Proof. - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity). Qed. -(* TODO *) Lemma exec_basic_dont_move_PC bi rs m rs' m': forall (BASIC: exec_basic lk ge bi rs m = Next rs' m'), rs PC = rs' PC. @@ -1660,7 +1659,6 @@ Proof. + destruct H. Qed. -(* TODO *) Lemma no_label_in_basic_inst: forall a lbl x, basic_to_instruction a = OK x -> Asm.is_label lbl x = false. Proof. diff --git a/aarch64/Peephole.v b/aarch64/Peephole.v index a1bb6c6c..54670708 100644 --- a/aarch64/Peephole.v +++ b/aarch64/Peephole.v @@ -160,7 +160,6 @@ Fixpoint pair_rep (insns : list basic) : list basic := end. Definition optimize_body (insns : list basic) := - (* TODO ADD A FLAG TO ENABLE PEEPHOLE *) if Compopts.optim_coalesce_mem tt then (pair_rep insns) else insns. -- cgit