From 241da496839a9101e843ce7b1da4a668f998498a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 2 Nov 2020 17:13:50 +0100 Subject: Preparation for postpass in aarch64 and refactoring --- aarch64/Asmblockgen.v | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) (limited to 'aarch64/Asmblockgen.v') diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index fc356d52..0a21485c 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -29,7 +29,7 @@ Local Open Scope error_monad_scope. Definition ireg_of (r: mreg) : res ireg := match preg_of r with - | IR' irs => match irs with + | IR irs => match irs with | RR1 mr => OK mr | _ => Error(msg "Asmgenblock.ireg_of") end @@ -37,7 +37,7 @@ Definition ireg_of (r: mreg) : res ireg := end. Definition freg_of (r: mreg) : res freg := - match preg_of r with FR' mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end. + match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end. (** Recognition of immediate arguments for logical integer operations.*) @@ -247,25 +247,25 @@ Definition indexed_memory_access_bc (insn: addressing -> basic) Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := match ty, preg_of dst with - | Tint, IR' rd => OK (indexed_memory_access_bc (PLoad Pldrw rd) 4 base ofs k) - | Tlong, IR' rd => OK (indexed_memory_access_bc (PLoad Pldrx rd) 8 base ofs k) - | Tsingle, FR' rd => OK (indexed_memory_access_bc (PLoad Pldrs rd) 4 base ofs k) - | Tfloat, FR' rd => OK (indexed_memory_access_bc (PLoad Pldrd rd) 8 base ofs k) - | Tany32, IR' rd => OK (indexed_memory_access_bc (PLoad Pldrw_a rd) 4 base ofs k) - | Tany64, IR' rd => OK (indexed_memory_access_bc (PLoad Pldrx_a rd) 8 base ofs k) - | Tany64, FR' rd => OK (indexed_memory_access_bc (PLoad Pldrd_a rd) 8 base ofs k) + | Tint, IR rd => OK (indexed_memory_access_bc (PLoad Pldrw rd) 4 base ofs k) + | Tlong, IR rd => OK (indexed_memory_access_bc (PLoad Pldrx rd) 8 base ofs k) + | Tsingle, FR rd => OK (indexed_memory_access_bc (PLoad Pldrs rd) 4 base ofs k) + | Tfloat, FR rd => OK (indexed_memory_access_bc (PLoad Pldrd rd) 8 base ofs k) + | Tany32, IR rd => OK (indexed_memory_access_bc (PLoad Pldrw_a rd) 4 base ofs k) + | Tany64, IR rd => OK (indexed_memory_access_bc (PLoad Pldrx_a rd) 8 base ofs k) + | Tany64, FR rd => OK (indexed_memory_access_bc (PLoad Pldrd_a rd) 8 base ofs k) | _, _ => Error (msg "Asmgen.loadind") end. Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode) := match ty, preg_of src with - | Tint, IR' rd => OK (indexed_memory_access_bc (PStore Pstrw rd) 4 base ofs k) - | Tlong, IR' rd => OK (indexed_memory_access_bc (PStore Pstrx rd) 8 base ofs k) - | Tsingle, FR' rd => OK (indexed_memory_access_bc (PStore Pstrs rd) 4 base ofs k) - | Tfloat, FR' rd => OK (indexed_memory_access_bc (PStore Pstrd rd) 8 base ofs k) - | Tany32, IR' rd => OK (indexed_memory_access_bc (PStore Pstrw_a rd) 4 base ofs k) - | Tany64, IR' rd => OK (indexed_memory_access_bc (PStore Pstrx_a rd) 8 base ofs k) - | Tany64, FR' rd => OK (indexed_memory_access_bc (PStore Pstrd_a rd) 8 base ofs k) + | Tint, IR rd => OK (indexed_memory_access_bc (PStore Pstrw rd) 4 base ofs k) + | Tlong, IR rd => OK (indexed_memory_access_bc (PStore Pstrx rd) 8 base ofs k) + | Tsingle, FR rd => OK (indexed_memory_access_bc (PStore Pstrs rd) 4 base ofs k) + | Tfloat, FR rd => OK (indexed_memory_access_bc (PStore Pstrd rd) 8 base ofs k) + | Tany32, IR rd => OK (indexed_memory_access_bc (PStore Pstrw_a rd) 4 base ofs k) + | Tany64, IR rd => OK (indexed_memory_access_bc (PStore Pstrx_a rd) 8 base ofs k) + | Tany64, FR rd => OK (indexed_memory_access_bc (PStore Pstrd_a rd) 8 base ofs k) | _, _ => Error (msg "Asmgen.storeind") end. @@ -621,8 +621,8 @@ Definition transl_op match op, args with | Omove, a1 :: nil => match preg_of res, preg_of a1 with - | IR' r, IR' a => OK (Pmov r a ::bi k) - | FR' r, FR' a => OK (Pfmov r a ::bi k) + | IR r, IR a => OK (Pmov r a ::bi k) + | FR r, FR a => OK (Pfmov r a ::bi k) | _ , _ => Error(msg "Asmgenblock.Omove") end | Ointconst n, nil => @@ -1009,10 +1009,10 @@ Definition transl_op (** Conditional move *) | Osel cmp ty, a1 :: a2 :: args => match preg_of res with - | IR' r => + | IR r => do r1 <- ireg_of a1; do r2 <- ireg_of a2; transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) ::bi k) - | FR' r => + | FR r => do r1 <- freg_of a1; do r2 <- freg_of a2; transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) ::bi k) | _ => -- cgit