From ec1a33e664f3484772a06dcd7e3198aa80b5d993 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 10 Dec 2020 23:06:17 +0100 Subject: Big improvment in peephole, changing LDP/STP semantics --- aarch64/Asmblock.v | 103 +++++++++++++++++++++++++---------------------------- 1 file changed, 49 insertions(+), 54 deletions(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index f12e8922..a4decae7 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -112,7 +112,7 @@ Inductive load_rd1_rd2_a: Type := Inductive ld_instruction: Type := | PLd_rd_a (ld: load_rd_a) (rd: dreg) (a: addressing) - | Pldp (ld: load_rd1_rd2_a) (rd1 rd2: ireg) (a: addressing) (**r load two int64 *) + | Pldp (ld: load_rd1_rd2_a) (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two int64 *) . Inductive store_rs_a : Type := @@ -136,7 +136,7 @@ Inductive store_rs1_rs2_a : Type := 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 *) + | Pstp (st: store_rs1_rs2_a) (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *) . Inductive arith_p : Type := @@ -459,16 +459,16 @@ Definition exec_load_rd_a (chunk: memory_chunk) (transf: val -> val) SOME v <- Mem.loadv chunk m (eval_addressing a rs) IN Next (rs#r <- (transf v)) m. -Definition exec_load_double (chunk: memory_chunk) (transf: val -> val) +Definition exec_load_double (chk1 chk2: memory_chunk) (transf: val -> val) (a: addressing) (rd1 rd2: dreg) (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 ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in let addr' := (eval_addressing (get_offset_addr a ofs) rs) in - match Mem.loadv chunk m addr with + match Mem.loadv chk1 m addr with | None => Stuck | Some v1 => - match Mem.loadv chunk m addr' with + match Mem.loadv chk2 m addr' with | None => Stuck | Some v2 => Next ((rs#rd1 <- (transf v1))#rd2 <- (transf v2)) m @@ -482,16 +482,16 @@ Definition exec_store_rs_a (chunk: memory_chunk) SOME m' <- Mem.storev chunk m (eval_addressing a rs) v IN Next rs m'. -Definition exec_store_double (chunk: memory_chunk) +Definition exec_store_double (chk1 chk2: 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 ofs := match chk1 with | Mint32 | Many32 => 4 | _ => 8 end in let addr' := (eval_addressing (get_offset_addr a ofs) rs) in - match Mem.storev chunk m addr v1 with + match Mem.storev chk1 m addr v1 with | None => Stuck - | Some m' => match Mem.storev chunk m' addr' v2 with + | Some m' => match Mem.storev chk2 m' addr' v2 with | None => Stuck | Some m'' => Next rs m'' end @@ -501,67 +501,62 @@ Definition exec_store_double (chunk: memory_chunk) (** execution of loads *) -Definition chunk_load (ld: ld_instruction): memory_chunk := +Definition chunk_load (ld: load_rd_a): memory_chunk := match ld with - | PLd_rd_a Pldrw _ _ => Mint32 - | PLd_rd_a Pldrw_a _ _ => Many32 - | PLd_rd_a Pldrx _ _ => Mint64 - | PLd_rd_a Pldrx_a _ _ => Many64 - | PLd_rd_a (Pldrb _) _ _ => Mint8unsigned - | PLd_rd_a (Pldrsb _) _ _ => Mint8signed - | PLd_rd_a (Pldrh _) _ _ => Mint16unsigned - | PLd_rd_a (Pldrsh _) _ _ => Mint16signed - | PLd_rd_a Pldrzw _ _ => Mint32 - | PLd_rd_a Pldrsw _ _ => Mint32 - | PLd_rd_a Pldrs _ _ => Mfloat32 - | PLd_rd_a Pldrd _ _ => Mfloat64 - | PLd_rd_a Pldrd_a _ _ => Many64 - | Pldp Pldpw _ _ _ => Mint32 - | Pldp Pldpx _ _ _ => Mint64 + | Pldrw => Mint32 + | Pldrw_a => Many32 + | Pldrx => Mint64 + | Pldrx_a => Many64 + | Pldrb _ => Mint8unsigned + | Pldrsb _ => Mint8signed + | Pldrh _ => Mint16unsigned + | Pldrsh _ => Mint16signed + | Pldrzw => Mint32 + | Pldrsw => Mint32 + | Pldrs => Mfloat32 + | Pldrd => Mfloat64 + | Pldrd_a => Many64 end. -Definition chunk_store (st: st_instruction) : memory_chunk := +Definition chunk_store (st: store_rs_a) : memory_chunk := match st with - | 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 + | Pstrw => Mint32 + | Pstrw_a => Many32 + | Pstrx => Mint64 + | Pstrx_a => Many64 + | Pstrb => Mint8unsigned + | Pstrh => Mint16unsigned + | Pstrs => Mfloat32 + | Pstrd => Mfloat64 + | Pstrd_a => Many64 end. -Definition interp_load (ld: ld_instruction): val -> val := +Definition interp_load (ld: load_rd_a): val -> val := match ld with - | PLd_rd_a (Pldrb X) _ _ => Val.longofintu - | PLd_rd_a (Pldrsb X) _ _ => Val.longofint - | PLd_rd_a (Pldrh X) _ _ => Val.longofintu - | PLd_rd_a (Pldrsh X) _ _ => Val.longofint - | PLd_rd_a Pldrzw _ _ => Val.longofintu - | PLd_rd_a Pldrsw _ _ => Val.longofint + | Pldrb X => Val.longofintu + | Pldrsb X => Val.longofint + | Pldrh X => Val.longofintu + | Pldrsh X => Val.longofint + | Pldrzw => Val.longofintu + | Pldrsw => Val.longofint (* Changed to exhaustive list because I tend to forgot all the places I need * to check when changing things. *) - | PLd_rd_a (Pldrb W) _ _ | PLd_rd_a (Pldrsb W) _ _ | PLd_rd_a (Pldrh W) _ _ | PLd_rd_a (Pldrsh W) _ _ - | PLd_rd_a Pldrw _ _ | PLd_rd_a Pldrw_a _ _ | PLd_rd_a Pldrx _ _ - | PLd_rd_a Pldrx_a _ _ | PLd_rd_a Pldrs _ _ | PLd_rd_a Pldrd _ _ - | PLd_rd_a Pldrd_a _ _ - | Pldp _ _ _ _ => fun v => v + | Pldrb W | Pldrsb W | Pldrh W | Pldrsh W + | Pldrw | Pldrw_a | Pldrx + | Pldrx_a | Pldrs | Pldrd + | Pldrd_a => fun v => v end. Definition exec_load (ldi: ld_instruction) (rs: regset) (m: mem) := match ldi with - | PLd_rd_a ld rd a => exec_load_rd_a (chunk_load ldi) (interp_load ldi) a rd rs m - | Pldp ld rd1 rd2 a => exec_load_double (chunk_load ldi) (interp_load ldi) a rd1 rd2 rs m + | PLd_rd_a ld rd a => exec_load_rd_a (chunk_load ld) (interp_load ld) a rd rs m + | Pldp ld rd1 rd2 chk1 chk2 a => exec_load_double chk1 chk2 (fun v => v) 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 + | PSt_rs_a st rsr a => exec_store_rs_a (chunk_store st) a rs#rsr rs m + | Pstp st rs1 rs2 chk1 chk2 a => exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m end. (** TODO: redundant w.r.t Machblock ?? *) -- cgit