From 932a3eda6a597d534131068d87052967398f0229 Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Thu, 9 Jul 2020 08:50:09 +0200 Subject: Implement unfold function from Asmblock to Asm Largely semi-automatically generated with vim regexes and macros. Right now the only interesting case is Pmovk: here we ckeck that on the Asmblock level the source and target register are the same. Then, we can safely translate to Asm's Pmovk which takes a single register (mutating it in-place). --- aarch64/Asmgen.v | 301 ++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 299 insertions(+), 2 deletions(-) (limited to 'aarch64/Asmgen.v') diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index b0fec14b..7b30ba40 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -22,14 +22,311 @@ Require Import Mach Asm Asmblock Asmblockgen Machblockgen PseudoAsmblock PseudoA Local Open Scope error_monad_scope. -(** * Translation from Asmblock to assembly language +(** * Translation from Asmblock to assembly language Inspired from the KVX backend (see kvx/Asm.v and kvx/Asmgen.v) *) Module Asmblock_TRANSF. (* STUB *) +Definition ireg_of_preg (p : Asmblock.preg) : res ireg := + match p with + | IR (RR1 r) => OK r + | _ => Error (msg "Asmgen.ireg_of_preg") + end. + +Definition freg_of_preg (p : Asmblock.preg) : res freg := + match p with + | FR r => OK r + | _ => Error (msg "Asmgen.freg_of_preg") + end. + +Definition iregsp_of_preg (p : Asmblock.preg) : res iregsp := + match p with + | IR r => OK r + | _ => Error (msg "Asmgen.iregsp_of_preg") + end. + +Definition basic_to_instruction (b: basic) : res Asm.instruction := + match b with + (* Aithmetic instructions *) + | PArith (PArithP (Padrp id ofs) rd) => do rd' <- ireg_of_preg rd; + OK (Asm.Padrp rd' id ofs) + | PArith (PArithP (Pmovz sz n pos) rd) => do rd' <- ireg_of_preg rd; + OK (Asm.Pmovz sz rd' n pos) + | PArith (PArithP (Pmovn sz n pos) rd) => do rd' <- ireg_of_preg rd; + OK (Asm.Pmovn sz rd' n pos) + | PArith (PArithP (Pfmovimms f) rd) => do rd' <- freg_of_preg rd; + OK (Asm.Pfmovimms rd' f) + | PArith (PArithP (Pfmovimmd f) rd) => do rd' <- freg_of_preg rd; + OK (Asm.Pfmovimmd rd' f) + + | PArith (PArithPP (Pmovk sz n pos) rd rs) => + do rd' <- ireg_of_preg rd; do rs' <- ireg_of_preg rs; + if (Asmblock.preg_eq rd rs) then + OK (Asm.Pmovk sz rd' n pos) + else + Error (msg "Asmgen.basic_to_instruction: Pmovk uses a single register as both source and target") + | PArith (PArithPP Pmov rd rs) => do rd' <- iregsp_of_preg rd; + do rs' <- iregsp_of_preg rs; + OK (Asm.Pmov rd' rs') + | PArith (PArithPP (Paddadr id ofs) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Paddadr rd' rs' id ofs) + | PArith (PArithPP (Psbfiz sz r s) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Psbfiz sz rd' rs' r s) + | PArith (PArithPP (Psbfx sz r s) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Psbfx sz rd' rs' r s) + | PArith (PArithPP (Pubfiz sz r s) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Pubfiz sz rd' rs' r s) + | PArith (PArithPP (Pubfx sz r s) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Pubfx sz rd' rs' r s) + | PArith (PArithPP Pfmov rd rs) => do rd' <- freg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfmov rd' rs') + | PArith (PArithPP Pfcvtds rd rs) => do rd' <- freg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfcvtds rd' rs') + | PArith (PArithPP Pfcvtsd rd rs) => do rd' <- freg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfcvtsd rd' rs') + | PArith (PArithPP (Pfabs sz) rd rs) => do rd' <- freg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfabs sz rd' rs') + | PArith (PArithPP (Pfneg sz) rd rs) => do rd' <- freg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfneg sz rd' rs') + | PArith (PArithPP (Pscvtf fsz isz) rd rs) => do rd' <- freg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Pscvtf fsz isz rd' rs') + | PArith (PArithPP (Pucvtf fsz isz) rd rs) => do rd' <- freg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Pucvtf fsz isz rd' rs') + | PArith (PArithPP (Pfcvtzs isz fsz) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfcvtzs isz fsz rd' rs') + | PArith (PArithPP (Pfcvtzu isz fsz) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- freg_of_preg rs; + OK (Asm.Pfcvtzu isz fsz rd' rs') + | PArith (PArithPP (Paddimm sz n) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Paddimm sz rd' rs' n) + | PArith (PArithPP (Psubimm sz n) rd rs) => do rd' <- ireg_of_preg rd; + do rs' <- ireg_of_preg rs; + OK (Asm.Psubimm sz rd' rs' n) + + | PArith (PArithPPP (Pasrv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Pasrv sz rd' r1' r2') + | PArith (PArithPPP (Plslv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Plslv sz rd' r1' r2') + | PArith (PArithPPP (Plsrv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Plsrv sz rd' r1' r2') + | PArith (PArithPPP (Prorv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Prorv sz rd' r1' r2') + | PArith (PArithPPP Psmulh rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Psmulh rd' r1' r2') + | PArith (PArithPPP Pumulh rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Pumulh rd' r1' r2') + | PArith (PArithPPP (Psdiv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Psdiv sz rd' r1' r2') + | PArith (PArithPPP (Pudiv sz) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Pudiv sz rd' r1' r2') + | PArith (PArithPPP (Paddext x) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Paddext rd' r1' r2' x) + | PArith (PArithPPP (Psubext x) rd r1 r2) => do rd' <- ireg_of_preg rd; + do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Psubext rd' r1' r2' x) + | PArith (PArithPPP (Pfadd sz) rd r1 r2) => do rd' <- freg_of_preg rd; + do r1' <- freg_of_preg r1; + do r2' <- freg_of_preg r2; + OK (Asm.Pfadd sz rd' r1' r2') + | PArith (PArithPPP (Pfdiv sz) rd r1 r2) => do rd' <- freg_of_preg rd; + do r1' <- freg_of_preg r1; + do r2' <- freg_of_preg r2; + OK (Asm.Pfdiv sz rd' r1' r2') + | PArith (PArithPPP (Pfmul sz) rd r1 r2) => do rd' <- freg_of_preg rd; + do r1' <- freg_of_preg r1; + do r2' <- freg_of_preg r2; + OK (Asm.Pfmul sz rd' r1' r2') + | PArith (PArithPPP (Pfsub sz) rd r1 r2) => do rd' <- freg_of_preg rd; + do r1' <- freg_of_preg r1; + do r2' <- freg_of_preg r2; + OK (Asm.Pfsub sz rd' r1' r2') + + | PArith (PArithRR0 (Pandimm sz n) rd r1) => OK (Asm.Pandimm sz rd r1 n) + | PArith (PArithRR0 (Peorimm sz n) rd r1) => OK (Asm.Peorimm sz rd r1 n) + | PArith (PArithRR0 (Porrimm sz n) rd r1) => OK (Asm.Porrimm sz rd r1 n) + + + | PArith (PArithRR0R (Padd sz s) rd r1 r2) => OK (Asm.Padd sz rd r1 r2 s) + | PArith (PArithRR0R (Psub sz s) rd r1 r2) => OK (Asm.Psub sz rd r1 r2 s) + | PArith (PArithRR0R (Pand sz s) rd r1 r2) => OK (Asm.Pand sz rd r1 r2 s) + | PArith (PArithRR0R (Pbic sz s) rd r1 r2) => OK (Asm.Pbic sz rd r1 r2 s) + | PArith (PArithRR0R (Peon sz s) rd r1 r2) => OK (Asm.Peon sz rd r1 r2 s) + | PArith (PArithRR0R (Peor sz s) rd r1 r2) => OK (Asm.Peor sz rd r1 r2 s) + | PArith (PArithRR0R (Porr sz s) rd r1 r2) => OK (Asm.Porr sz rd r1 r2 s) + | PArith (PArithRR0R (Porn sz s) rd r1 r2) => OK (Asm.Porn sz rd r1 r2 s) + + | PArith (PArithARRRR0 (Pmadd sz) rd r1 r2 r3) => OK (Asm.Pmadd sz rd r1 r2 r3) + | PArith (PArithARRRR0 (Pmsub sz) rd r1 r2 r3) => OK (Asm.Pmsub sz rd r1 r2 r3) + + | PArith (PArithComparisonPP (Pcmpext x) r1 r2) => do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Pcmpext r1' r2' x) + | PArith (PArithComparisonPP (Pcmnext x) r1 r2) => do r1' <- ireg_of_preg r1; + do r2' <- ireg_of_preg r2; + OK (Asm.Pcmnext r1' r2' x) + | PArith (PArithComparisonPP (Pfcmp sz) r1 r2) => do r1' <- freg_of_preg r1; + do r2' <- freg_of_preg r2; + OK (Asm.Pfcmp sz r1' r2') + + | PArith (PArithComparisonR0R (Pcmp is s) r1 r2) => OK (Asm.Pcmp is r1 r2 s) + | PArith (PArithComparisonR0R (Pcmn is s) r1 r2) => OK (Asm.Pcmn is r1 r2 s) + | PArith (PArithComparisonR0R (Ptst is s) r1 r2) => OK (Asm.Ptst is r1 r2 s) + + | PArith (PArithComparisonP (Pcmpimm sz n) r1) => do r1' <- ireg_of_preg r1; + OK (Asm.Pcmpimm sz r1' n) + | PArith (PArithComparisonP (Pcmnimm sz n) r1) => do r1' <- ireg_of_preg r1; + OK (Asm.Pcmnimm sz r1' n) + | PArith (PArithComparisonP (Ptstimm sz n) r1) => do r1' <- ireg_of_preg r1; + OK (Asm.Ptstimm sz r1' n) + | PArith (PArithComparisonP (Pfcmp0 sz) r1) => do r1' <- freg_of_preg r1; + OK (Asm.Pfcmp0 sz r1') + + | PArith (Pcset rd c) => OK (Asm.Pcset rd c) + | PArith (Pfmovi fsz rd r1) => OK (Asm.Pfmovi fsz rd r1) + | PArith (Pcsel rd r1 r2 c) => OK (Asm.Pcsel rd r1 r2 c) + | PArith (Pfnmul fsz rd r1 r2) => OK (Asm.Pfnmul fsz rd r1 r2) + + | PLoad Pldrw rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw rd' a) + | PLoad Pldrw_a rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw_a rd' a) + | PLoad Pldrx rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrx rd' a) + | PLoad Pldrx_a rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrx_a rd' a) + | PLoad (Pldrb sz) rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrb sz rd' a) + | PLoad (Pldrsb sz) rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsb sz rd' a) + | PLoad (Pldrh sz) rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrh sz rd' a) + | PLoad (Pldrsh sz) rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsh sz rd' a) + | PLoad Pldrzw rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrzw rd' a) + | PLoad Pldrsw rd a => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsw rd' a) + + | PLoad Pldrs rd a => do rd' <- freg_of_preg rd; OK (Asm.Pldrs rd' a) + | PLoad Pldrd rd a => do rd' <- freg_of_preg rd; OK (Asm.Pldrd rd' a) + | PLoad Pldrd_a rd a => do rd' <- freg_of_preg rd; OK (Asm.Pldrd_a rd' a) + + | PStore Pstrw r a => do r' <- ireg_of_preg r; OK (Asm.Pstrw r' a) + | PStore Pstrw_a r a => do r' <- ireg_of_preg r; OK (Asm.Pstrw_a r' a) + | PStore Pstrx r a => do r' <- ireg_of_preg r; OK (Asm.Pstrx r' a) + | PStore Pstrx_a r a => do r' <- ireg_of_preg r; OK (Asm.Pstrx_a r' a) + | PStore Pstrb r a => do r' <- ireg_of_preg r; OK (Asm.Pstrb r' a) + | PStore Pstrh r a => do r' <- ireg_of_preg r; OK (Asm.Pstrh r' a) + + | PStore Pstrs r a => do r' <- freg_of_preg r; OK (Asm.Pstrs r' a) + | PStore Pstrd r a => do r' <- freg_of_preg r; OK (Asm.Pstrd r' a) + | PStore Pstrd_a r a => do r' <- freg_of_preg r; OK (Asm.Pstrd_a r' a) + + | Pallocframe sz linkofs => OK (Asm.Pallocframe sz linkofs) + | Pfreeframe sz linkofs => OK (Asm.Pfreeframe sz linkofs) + + | Ploadsymbol rd id => OK (Asm.Ploadsymbol rd id) + + | Pcvtsw2x rd r1 => OK (Asm.Pcvtsw2x rd r1) + + | Pcvtuw2x rd r1 => OK (Asm.Pcvtuw2x rd r1) + + | Pcvtx2w rd => OK (Asm.Pcvtx2w rd) + end. + +Definition cf_instruction_to_instruction (cfi: cf_instruction) : Asm.instruction := + match cfi with + | Pb l => Asm.Pb l + | Pbc c lbl => Asm.Pbc c lbl + | Pbl id sg => Asm.Pbl id sg + | Pbs id sg => Asm.Pbs id sg + | Pblr r sg => Asm.Pblr r sg + | Pbr r sg => Asm.Pbr r sg + | Pret r => Asm.Pret r + | Pcbnz sz r lbl => Asm.Pcbnz sz r lbl + | Pcbz sz r lbl => Asm.Pcbz sz r lbl + | Ptbnz sz r n lbl => Asm.Ptbnz sz r n lbl + | Ptbz sz r n lbl => Asm.Ptbz sz r n lbl + | Pbtbl r1 tbl => Asm.Pbtbl r1 tbl + end. + +Definition control_to_instruction (c: control) := + match c with + | PCtlFlow i => cf_instruction_to_instruction i + | Pbuiltin ef args res => Asm.Pbuiltin ef args res + end. + +Fixpoint unfold_label (ll: list label) := + match ll with + | nil => nil + | l :: ll => Plabel l :: unfold_label ll + end. + +Fixpoint unfold_body (lb: list basic) : res Asm.code := + match lb with + | nil => OK nil + | b :: lb => + (* x_is: x's instructions *) + do b_is <- basic_to_instruction b; + do lb_is <- unfold_body lb; + OK (b_is :: lb_is) + end. + +Definition unfold_exit (oc: option control) := + match oc with + | None => nil + | Some c => control_to_instruction c :: nil + end. + +Definition unfold_bblock (bb: bblock) := + let lbl := unfold_label (header bb) in + do rest <- (match (body bb), (exit bb) with + | (((Asmblock.Pfreeframe _ _ + | Asmblock.Pallocframe _ _)::nil) as bo), None => + unfold_body bo + | bo, ex => + do bo_is <- unfold_body bo; + OK (bo_is ++ unfold_exit ex) + end) + ; OK (lbl ++ rest). + +Fixpoint unfold (bbs: Asmblock.bblocks) : res Asm.code := + match bbs with + | nil => OK (nil) + | bb :: bbs' => + do bb_is <- unfold_bblock bb; + do bbs'_is <- unfold bbs'; + OK (bb_is ++ bbs'_is) + end. + Definition transf_function (f: Asmblock.function) : res Asm.function := - Error (msg "Asmgen not yet implmented"). + do c <- unfold (Asmblock.fn_blocks f); + OK {| Asm.fn_sig := Asmblock.fn_sig f + ; Asm.fn_code := c |}. Definition transf_fundef (f: Asmblock.fundef) : res Asm.fundef := transf_partial_fundef transf_function f. -- cgit