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).

1 files changed, 299 insertions, 2 deletions

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.