From 972f6b9890ea3644626fc097e460035028b940eb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 4 Dec 2020 23:26:01 +0100 Subject: a first working draft on ldp/stp peephole --- aarch64/Asmblock.v | 109 ++++++++++++++++++++++++++++++++--------------------- 1 file changed, 66 insertions(+), 43 deletions(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 329c889e..3ad1d7f8 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -130,14 +130,16 @@ Inductive store_rs_a : Type := | Pstrd (**r store float64 *) | Pstrd_a (**r store float64 as any64 *) . -(* Actually, Pstp is not used in the aarch64/Asm semantics! - * Thus we skip this particular case: - * Inductive st_instruction : Type := - * | PSt_rs_a (st : store_rs_a) (rs : ireg) (a : addressing) - * | Pstp (rs1 rs2: ireg) (a: addressing) (**r store two int64 *) - * . - * Coercion PStore : st_instruction >-> basic. - *) + +Inductive store_rs1_rs2_a : Type := + | Pstpw + | Pstpx + . + +Inductive st_instruction : Type := + | PSt_rs_a (st: store_rs_a) (rs: dreg) (a: addressing) + | Pstp (st: store_rs1_rs2_a) (rs1 rs2: ireg) (a: addressing) (**r store two int64 *) + . Inductive arith_p : Type := (** PC-relative addressing *) @@ -318,23 +320,23 @@ Inductive ar_instruction : Type := Inductive basic : Type := | PArith (i: ar_instruction) (**r TODO *) - (*| PLoad (ld: load_rd_a) (rd: dreg) (a: addressing) [>*r TODO <]*) | PLoad (ld: ld_instruction) - | PStore (st: store_rs_a) (r: dreg) (a: addressing) (**r TODO *) + | PStore (st: st_instruction) | Pallocframe (sz: Z) (linkofs: ptrofs) (**r allocate new stack frame *) | Pfreeframe (sz: Z) (linkofs: ptrofs) (**r deallocate stack frame and restore previous frame *) | 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 *) -(* NOT USED IN THE SEMANTICS ! | Pnop (**r no operation *) +(* NOT USED IN THE SEMANTICS ! | Pcfi_adjust (ofs: int) (**r .cfi_adjust debug directive *) | Pcfi_rel_offset (ofs: int) (**r .cfi_rel_offset debug directive *) *) . Coercion PLoad: ld_instruction >-> basic. +Coercion PStore : st_instruction >-> basic. (* Not used in Coq, declared in ocaml directly in PostpassSchedulingOracle.ml Inductive instruction : Type := @@ -591,13 +593,7 @@ Definition eval_addressing (a: addressing) (rs: regset): val := | ADsxt base r n => Val.addl rs#base (Val.shll (Val.longofint rs#r) (Vint n)) | ADuxt base r n => Val.addl rs#base (Val.shll (Val.longofintu rs#r) (Vint n)) | ADadr base id ofs => Val.addl rs#base (symbol_low lk id ofs) - | ADpostincr base n => rs#base - end. - -Definition eval_addressing_update (a: addressing) (rs: regset): regset := - match a with - | ADpostincr base n => rs#base <- (Vlong n) - | _ => rs + | ADpostincr base n => Vundef end. (** Auxiliaries for memory accesses *) @@ -609,24 +605,42 @@ Definition exec_load_rd_a (chunk: memory_chunk) (transf: val -> val) Definition exec_load_double (chunk: memory_chunk) (transf: val -> val) (a: addressing) (rd1 rd2: preg) (rs: regset) (m: mem) := - let addr := (eval_addressing a rs) in - let ofs := match chunk with | Mint32 => 4 | _ => 8 end in - match Mem.loadv Mint32 m addr with - | None => Stuck - | Some v1 => - match Mem.loadv Mint32 m (Val.offset_ptr addr (Ptrofs.repr ofs)) with - | None => Stuck - | Some v2 => - Next (nextinstr (((eval_addressing_update a rs)#rd1 <- (transf v1))#rd2 <- (transf v2))) m - end - end. - -Definition exec_store (chunk: memory_chunk) + if is_pair_addressing_mode_correct a then + let addr := (eval_addressing a rs) in + let ofs := match chunk with | Mint32 => 4 | _ => 8 end in + let addr' := (eval_addressing (get_offset_addr a ofs) rs) in + match Mem.loadv chunk m addr with + | None => Stuck + | Some v1 => + match Mem.loadv chunk m addr' with + | None => Stuck + | Some v2 => + Next ((rs#rd1 <- (transf v1))#rd2 <- (transf v2)) m + end + end + else Stuck. + +Definition exec_store_rs_a (chunk: memory_chunk) (a: addressing) (v: val) (rs: regset) (m: mem) := SOME m' <- Mem.storev chunk m (eval_addressing a rs) v IN Next rs m'. +Definition exec_store_double (chunk: memory_chunk) + (a: addressing) (v1 v2: val) + (rs: regset) (m: mem) := + if is_pair_addressing_mode_correct a then + let addr := (eval_addressing a rs) in + let ofs := match chunk with | Mint32 => 4 | _ => 8 end in + let addr' := (eval_addressing (get_offset_addr a ofs) rs) in + match Mem.storev chunk m addr v1 with + | None => Stuck + | Some m' => match Mem.storev chunk m' addr' v2 with + | None => Stuck + | Some m'' => Next rs m'' + end + end + else Stuck. (** execution of loads *) @@ -647,20 +661,22 @@ Definition chunk_load (ld: ld_instruction): memory_chunk := | PLd_rd_a Pldrd _ _ => Mfloat64 | PLd_rd_a Pldrd_a _ _ => Many64 | Pldp Pldpw _ _ _ => Mint32 - | Pldp Pldpx _ _ _ => Mint32 + | Pldp Pldpx _ _ _ => Mint64 end. -Definition chunk_store_rs_a (st: store_rs_a) : memory_chunk := +Definition chunk_store (st: st_instruction) : memory_chunk := match st with - | Pstrw => Mint32 - | Pstrw_a => Many32 - | Pstrx => Mint64 - | Pstrx_a => Many64 - | Pstrb => Mint8unsigned - | Pstrh => Mint16unsigned - | Pstrs => Mfloat32 - | Pstrd => Mfloat64 - | Pstrd_a => Many64 + | PSt_rs_a Pstrw _ _ => Mint32 + | PSt_rs_a Pstrw_a _ _ => Many32 + | PSt_rs_a Pstrx _ _ => Mint64 + | PSt_rs_a Pstrx_a _ _ => Many64 + | PSt_rs_a Pstrb _ _ => Mint8unsigned + | PSt_rs_a Pstrh _ _ => Mint16unsigned + | PSt_rs_a Pstrs _ _ => Mfloat32 + | PSt_rs_a Pstrd _ _ => Mfloat64 + | PSt_rs_a Pstrd_a _ _ => Many64 + | Pstp Pstpw _ _ _ => Mint32 + | Pstp Pstpx _ _ _ => Mint64 end. Definition interp_load (ld: ld_instruction): val -> val := @@ -686,6 +702,12 @@ Definition exec_load (ldi: ld_instruction) (rs: regset) (m: mem) := | Pldp ld rd1 rd2 a => exec_load_double (chunk_load ldi) (interp_load ldi) a rd1 rd2 rs m end. +Definition exec_store (sti: st_instruction) (rs: regset) (m: mem) := + match sti with + | PSt_rs_a st rsr a => exec_store_rs_a (chunk_store sti) a rs#rsr rs m + | Pstp st rs1 rs2 a => exec_store_double (chunk_store sti) a rs#rs1 rs#rs2 rs m + end. + (** TODO: redundant w.r.t Machblock ?? *) Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. Proof. @@ -1022,7 +1044,7 @@ Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome := match b with | PArith ai => Next (exec_arith_instr ai rs) m | PLoad ldi => exec_load ldi rs m - | PStore st r a => exec_store (chunk_store_rs_a st) a rs#r rs m + | PStore sti => exec_store sti rs m | Pallocframe sz pos => let (m1, stk) := Mem.alloc m 0 sz in let sp := (Vptr stk Ptrofs.zero) in @@ -1044,6 +1066,7 @@ Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome := Next (rs#rd <- (Val.longofintu rs#r1)) m | Pcvtx2w rd => Next (rs#rd <- (Val.loword rs#rd)) m + | Pnop => Next rs m end. (* TODO: ORIGINAL EXECUTION OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED ! -- cgit