From 5020a5a07da3fd690f5d171a48d0c73ef48f9430 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 1 Mar 2013 15:32:13 +0000 Subject: Revised Stacking and Asmgen passes and Mach semantics: - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgen.v | 503 ++++++++++++++++++++++++++++++++----------------------- 1 file changed, 294 insertions(+), 209 deletions(-) (limited to 'powerpc/Asmgen.v') diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 8ef249d..0035dff 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -22,6 +22,23 @@ Require Import Locations. Require Import Mach. Require Import Asm. +Open Local Scope string_scope. +Open Local Scope error_monad_scope. + +(** The code generation functions take advantage of several + characteristics of the [Mach] code generated by earlier passes of the + compiler, mostly that argument and result registers are of the correct + types. These properties are true by construction, but it's easier to + recheck them during code generation and fail if they do not hold. *) + +(** Extracting integer or float registers. *) + +Definition ireg_of (r: mreg) : res ireg := + match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end. + +Definition freg_of (r: mreg) : res freg := + match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end. + (** Decomposition of integer constants. As noted in file [Asm], immediate arguments to PowerPC instructions must fit into 16 bits, and are interpreted after zero extension, sign extension, or @@ -106,30 +123,36 @@ Definition rolm (r1 r2: ireg) (amount mask: int) (k: code) := (** Accessing slots in the stack frame. *) Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := - if Int.eq (high_s ofs) Int.zero then - match ty with - | Tint => Plwz (ireg_of dst) (Cint ofs) base :: k - | Tfloat => Plfd (freg_of dst) (Cint ofs) base :: k - end - else - loadimm GPR0 ofs - (match ty with - | Tint => Plwzx (ireg_of dst) base GPR0 :: k - | Tfloat => Plfdx (freg_of dst) base GPR0 :: k - end). + match ty with + | Tint => + do r <- ireg_of dst; + OK (if Int.eq (high_s ofs) Int.zero then + Plwz r (Cint ofs) base :: k + else + loadimm GPR0 ofs (Plwzx r base GPR0 :: k)) + | Tfloat => + do r <- freg_of dst; + OK (if Int.eq (high_s ofs) Int.zero then + Plfd r (Cint ofs) base :: k + else + loadimm GPR0 ofs (Plfdx r base GPR0 :: k)) + end. Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := - if Int.eq (high_s ofs) Int.zero then - match ty with - | Tint => Pstw (ireg_of src) (Cint ofs) base :: k - | Tfloat => Pstfd (freg_of src) (Cint ofs) base :: k - end - else - loadimm GPR0 ofs - (match ty with - | Tint => Pstwx (ireg_of src) base GPR0 :: k - | Tfloat => Pstfdx (freg_of src) base GPR0 :: k - end). + match ty with + | Tint => + do r <- ireg_of src; + OK (if Int.eq (high_s ofs) Int.zero then + Pstw r (Cint ofs) base :: k + else + loadimm GPR0 ofs (Pstwx r base GPR0 :: k)) + | Tfloat => + do r <- freg_of src; + OK (if Int.eq (high_s ofs) Int.zero then + Pstfd r (Cint ofs) base :: k + else + loadimm GPR0 ofs (Pstfdx r base GPR0 :: k)) + end. (** Constructor for a floating-point comparison. The PowerPC has a single [fcmpu] instruction to compare floats, which sets @@ -156,29 +179,31 @@ Definition transl_cond (cond: condition) (args: list mreg) (k: code) := match cond, args with | Ccomp c, a1 :: a2 :: nil => - Pcmpw (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmpw r1 r2 :: k) | Ccompu c, a1 :: a2 :: nil => - Pcmplw (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmplw r1 r2 :: k) | Ccompimm c n, a1 :: nil => + do r1 <- ireg_of a1; if Int.eq (high_s n) Int.zero then - Pcmpwi (ireg_of a1) (Cint n) :: k + OK (Pcmpwi r1 (Cint n) :: k) else - loadimm GPR0 n (Pcmpw (ireg_of a1) GPR0 :: k) + OK (loadimm GPR0 n (Pcmpw r1 GPR0 :: k)) | Ccompuimm c n, a1 :: nil => + do r1 <- ireg_of a1; if Int.eq (high_u n) Int.zero then - Pcmplwi (ireg_of a1) (Cint n) :: k + OK (Pcmplwi r1 (Cint n) :: k) else - loadimm GPR0 n (Pcmplw (ireg_of a1) GPR0 :: k) + OK (loadimm GPR0 n (Pcmplw r1 GPR0 :: k)) | Ccompf cmp, a1 :: a2 :: nil => - floatcomp cmp (freg_of a1) (freg_of a2) k + do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 k) | Cnotcompf cmp, a1 :: a2 :: nil => - floatcomp cmp (freg_of a1) (freg_of a2) k + do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 k) | Cmaskzero n, a1 :: nil => - andimm_base GPR0 (ireg_of a1) n k + do r1 <- ireg_of a1; OK (andimm_base GPR0 r1 n k) | Cmasknotzero n, a1 :: nil => - andimm_base GPR0 (ireg_of a1) n k + do r1 <- ireg_of a1; OK (andimm_base GPR0 r1 n k) | _, _ => - k (**r never happens for well-typed code *) + Error(msg "Asmgen.transl_cond") end. (* CRbit_0 = Less @@ -264,180 +289,267 @@ Definition classify_condition (c: condition) (args: list mreg): condition_class Definition transl_cond_op (cond: condition) (args: list mreg) (r: mreg) (k: code) := + do r' <- ireg_of r; match classify_condition cond args with | condition_eq0 _ a _ => - Psubfic GPR0 (ireg_of a) (Cint Int.zero) :: - Padde (ireg_of r) GPR0 (ireg_of a) :: k + do a' <- ireg_of a; + OK (Psubfic GPR0 a' (Cint Int.zero) :: + Padde r' GPR0 a' :: k) | condition_ne0 _ a _ => - Paddic GPR0 (ireg_of a) (Cint Int.mone) :: - Psubfe (ireg_of r) GPR0 (ireg_of a) :: k + do a' <- ireg_of a; + OK (Paddic GPR0 a' (Cint Int.mone) :: + Psubfe r' GPR0 a' :: k) | condition_ge0 _ a _ => - Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: - Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k + do a' <- ireg_of a; + OK (Prlwinm r' a' Int.one Int.one :: + Pxori r' r' (Cint Int.one) :: k) | condition_lt0 _ a _ => - Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: k + do a' <- ireg_of a; + OK (Prlwinm r' a' Int.one Int.one :: k) | condition_default _ _ => let p := crbit_for_cond cond in transl_cond cond args - (Pmfcrbit (ireg_of r) (fst p) :: + (Pmfcrbit r' (fst p) :: if snd p then k - else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k) + else Pxori r' r' (Cint Int.one) :: k) end. (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) Definition transl_op - (op: operation) (args: list mreg) (r: mreg) (k: code) := + (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with | Omove, a1 :: nil => - match mreg_type a1 with - | Tint => Pmr (ireg_of r) (ireg_of a1) :: k - | Tfloat => Pfmr (freg_of r) (freg_of a1) :: k + match preg_of res, preg_of a1 with + | IR r, IR a => OK (Pmr r a :: k) + | FR r, FR a => OK (Pfmr r a :: k) + | _ , _ => Error(msg "Asmgen.Omove") end | Ointconst n, nil => - loadimm (ireg_of r) n k + do r <- ireg_of res; OK (loadimm r n k) | Ofloatconst f, nil => - Plfi (freg_of r) f :: k + do r <- freg_of res; OK (Plfi r f :: k) | Oaddrsymbol s ofs, nil => - if symbol_is_small_data s ofs then - Paddi (ireg_of r) GPR0 (Csymbol_sda s ofs) :: k - else - Paddis GPR12 GPR0 (Csymbol_high s ofs) :: - Paddi (ireg_of r) GPR12 (Csymbol_low s ofs) :: k + do r <- ireg_of res; + OK (if symbol_is_small_data s ofs then + Paddi r GPR0 (Csymbol_sda s ofs) :: k + else + Paddis GPR12 GPR0 (Csymbol_high s ofs) :: + Paddi r GPR12 (Csymbol_low s ofs) :: k) | Oaddrstack n, nil => - addimm (ireg_of r) GPR1 n k + do r <- ireg_of res; OK (addimm r GPR1 n k) | Ocast8signed, a1 :: nil => - Pextsb (ireg_of r) (ireg_of a1) :: k + do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pextsb r r1 :: k) | Ocast16signed, a1 :: nil => - Pextsh (ireg_of r) (ireg_of a1) :: k + do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pextsh r r1 :: k) | Oadd, a1 :: a2 :: nil => - Padd (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Padd r r1 r2 :: k) | Oaddimm n, a1 :: nil => - addimm (ireg_of r) (ireg_of a1) n k + do r1 <- ireg_of a1; do r <- ireg_of res; OK (addimm r r1 n k) | Osub, a1 :: a2 :: nil => - Psubfc (ireg_of r) (ireg_of a2) (ireg_of a1) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Psubfc r r2 r1 :: k) | Osubimm n, a1 :: nil => - if Int.eq (high_s n) Int.zero then - Psubfic (ireg_of r) (ireg_of a1) (Cint n) :: k - else - loadimm GPR0 n (Psubfc (ireg_of r) (ireg_of a1) GPR0 :: k) + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (if Int.eq (high_s n) Int.zero then + Psubfic r r1 (Cint n) :: k + else + loadimm GPR0 n (Psubfc r r1 GPR0 :: k)) | Omul, a1 :: a2 :: nil => - Pmullw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pmullw r r1 r2 :: k) | Omulimm n, a1 :: nil => - if Int.eq (high_s n) Int.zero then - Pmulli (ireg_of r) (ireg_of a1) (Cint n) :: k - else - loadimm GPR0 n (Pmullw (ireg_of r) (ireg_of a1) GPR0 :: k) + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (if Int.eq (high_s n) Int.zero then + Pmulli r r1 (Cint n) :: k + else + loadimm GPR0 n (Pmullw r r1 GPR0 :: k)) | Odiv, a1 :: a2 :: nil => - Pdivw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pdivw r r1 r2 :: k) | Odivu, a1 :: a2 :: nil => - Pdivwu (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pdivwu r r1 r2 :: k) | Oand, a1 :: a2 :: nil => - Pand_ (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pand_ r r1 r2 :: k) | Oandimm n, a1 :: nil => - andimm (ireg_of r) (ireg_of a1) n k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (andimm r r1 n k) | Oor, a1 :: a2 :: nil => - Por (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Por r r1 r2 :: k) | Oorimm n, a1 :: nil => - orimm (ireg_of r) (ireg_of a1) n k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (orimm r r1 n k) | Oxor, a1 :: a2 :: nil => - Pxor (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pxor r r1 r2 :: k) | Oxorimm n, a1 :: nil => - xorimm (ireg_of r) (ireg_of a1) n k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (xorimm r r1 n k) | Onot, a1 :: nil => - Pnor (ireg_of r) (ireg_of a1) (ireg_of a1) :: k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Pnor r r1 r1 :: k) | Onand, a1 :: a2 :: nil => - Pnand (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pnand r r1 r2 :: k) | Onor, a1 :: a2 :: nil => - Pnor (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pnor r r1 r2 :: k) | Onxor, a1 :: a2 :: nil => - Peqv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Peqv r r1 r2 :: k) | Oandc, a1 :: a2 :: nil => - Pandc (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pandc r r1 r2 :: k) | Oorc, a1 :: a2 :: nil => - Porc (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Porc r r1 r2 :: k) | Oshl, a1 :: a2 :: nil => - Pslw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pslw r r1 r2 :: k) | Oshr, a1 :: a2 :: nil => - Psraw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Psraw r r1 r2 :: k) | Oshrimm n, a1 :: nil => - Psrawi (ireg_of r) (ireg_of a1) n :: k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Psrawi r r1 n :: k) | Oshrximm n, a1 :: nil => - Psrawi (ireg_of r) (ireg_of a1) n :: - Paddze (ireg_of r) (ireg_of r) :: k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Psrawi r r1 n :: Paddze r r :: k) | Oshru, a1 :: a2 :: nil => - Psrw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Psrw r r1 r2 :: k) | Orolm amount mask, a1 :: nil => - rolm (ireg_of r) (ireg_of a1) amount mask k + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (rolm r r1 amount mask k) | Oroli amount mask, a1 :: a2 :: nil => - if mreg_eq a1 r then (**r should always be true *) - Prlwimi (ireg_of r) (ireg_of a2) amount mask :: k - else - Pmr GPR0 (ireg_of a1) :: - Prlwimi GPR0 (ireg_of a2) amount mask :: - Pmr (ireg_of r) GPR0 :: k + do x <- assertion (mreg_eq a1 res); + do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Prlwimi r r2 amount mask :: k) | Onegf, a1 :: nil => - Pfneg (freg_of r) (freg_of a1) :: k + do r1 <- freg_of a1; do r <- freg_of res; + OK (Pfneg r r1 :: k) | Oabsf, a1 :: nil => - Pfabs (freg_of r) (freg_of a1) :: k + do r1 <- freg_of a1; do r <- freg_of res; + OK (Pfabs r r1 :: k) | Oaddf, a1 :: a2 :: nil => - Pfadd (freg_of r) (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfadd r r1 r2 :: k) | Osubf, a1 :: a2 :: nil => - Pfsub (freg_of r) (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfsub r r1 r2 :: k) | Omulf, a1 :: a2 :: nil => - Pfmul (freg_of r) (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfmul r r1 r2 :: k) | Odivf, a1 :: a2 :: nil => - Pfdiv (freg_of r) (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfdiv r r1 r2 :: k) | Osingleoffloat, a1 :: nil => - Pfrsp (freg_of r) (freg_of a1) :: k + do r1 <- freg_of a1; do r <- freg_of res; + OK (Pfrsp r r1 :: k) | Ointoffloat, a1 :: nil => - Pfcti (ireg_of r) (freg_of a1) :: k + do r1 <- freg_of a1; do r <- ireg_of res; + OK (Pfcti r r1 :: k) | Ofloatofwords, a1 :: a2 :: nil => - Pfmake (freg_of r) (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res; + OK (Pfmake r r1 r2 :: k) | Ocmp cmp, _ => - transl_cond_op cmp args r k + transl_cond_op cmp args res k | _, _ => - k (**r never happens for well-typed code *) + Error(msg "Asmgen.transl_op") end. -(** Common code to translate [Mload] and [Mstore] instructions. *) +(** Translation of memory accesses: loads, and stores. *) Definition int_temp_for (r: mreg) := if mreg_eq r IT2 then GPR11 else GPR12. -Definition transl_load_store +Definition transl_memory_access (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) (addr: addressing) (args: list mreg) (temp: ireg) (k: code) := match addr, args with | Aindexed ofs, a1 :: nil => - if Int.eq (high_s ofs) Int.zero then - mk1 (Cint ofs) (ireg_of a1) :: k - else - Paddis temp (ireg_of a1) (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) temp :: k + do r1 <- ireg_of a1; + OK (if Int.eq (high_s ofs) Int.zero then + mk1 (Cint ofs) r1 :: k + else + Paddis temp r1 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) temp :: k) | Aindexed2, a1 :: a2 :: nil => - mk2 (ireg_of a1) (ireg_of a2) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (mk2 r1 r2 :: k) | Aglobal symb ofs, nil => - if symbol_is_small_data symb ofs then - mk1 (Csymbol_sda symb ofs) GPR0 :: k - else - Paddis temp GPR0 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) temp :: k + OK (if symbol_is_small_data symb ofs then + mk1 (Csymbol_sda symb ofs) GPR0 :: k + else + Paddis temp GPR0 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) temp :: k) | Abased symb ofs, a1 :: nil => - Paddis temp (ireg_of a1) (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) temp :: k + do r1 <- ireg_of a1; + OK (Paddis temp r1 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) temp :: k) | Ainstack ofs, nil => - if Int.eq (high_s ofs) Int.zero then - mk1 (Cint ofs) GPR1 :: k - else - Paddis temp GPR1 (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) temp :: k + OK (if Int.eq (high_s ofs) Int.zero then + mk1 (Cint ofs) GPR1 :: k + else + Paddis temp GPR1 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) temp :: k) | _, _ => - (* should not happen *) k + Error(msg "Asmgen.transl_memory_access") + end. + +Definition transl_load (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (dst: mreg) (k: code) := + match chunk with + | Mint8signed => + do r <- ireg_of dst; + transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 (Pextsb r r :: k) + | Mint8unsigned => + do r <- ireg_of dst; + transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 k + | Mint16signed => + do r <- ireg_of dst; + transl_memory_access (Plha r) (Plhax r) addr args GPR12 k + | Mint16unsigned => + do r <- ireg_of dst; + transl_memory_access (Plhz r) (Plhzx r) addr args GPR12 k + | Mint32 => + do r <- ireg_of dst; + transl_memory_access (Plwz r) (Plwzx r) addr args GPR12 k + | Mfloat32 => + do r <- freg_of dst; + transl_memory_access (Plfs r) (Plfsx r) addr args GPR12 k + | Mfloat64 | Mfloat64al32 => + do r <- freg_of dst; + transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k + end. + +Definition transl_store (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (src: mreg) (k: code) := + let temp := int_temp_for src in + match chunk with + | Mint8signed | Mint8unsigned => + do r <- ireg_of src; + transl_memory_access (Pstb r) (Pstbx r) addr args temp k + | Mint16signed | Mint16unsigned => + do r <- ireg_of src; + transl_memory_access (Psth r) (Psthx r) addr args temp k + | Mint32 => + do r <- ireg_of src; + transl_memory_access (Pstw r) (Pstwx r) addr args temp k + | Mfloat32 => + do r <- freg_of src; + transl_memory_access (Pstfs r) (Pstfsx r) addr args temp k + | Mfloat64 | Mfloat64al32 => + do r <- freg_of src; + transl_memory_access (Pstfd r) (Pstfdx r) addr args temp k end. (** Translation of arguments to annotations *) @@ -450,105 +562,80 @@ Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param := (** Translation of a Mach instruction. *) -Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := +Definition transl_instr (f: Mach.function) (i: Mach.instruction) + (r11_is_parent: bool) (k: code) := match i with | Mgetstack ofs ty dst => loadind GPR1 ofs ty dst k | Msetstack src ofs ty => storeind src GPR1 ofs ty k | Mgetparam ofs ty dst => - Plwz GPR11 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR11 ofs ty dst k + if r11_is_parent then + loadind GPR11 ofs ty dst k + else + (do k1 <- loadind GPR11 ofs ty dst k; + loadind GPR1 f.(fn_link_ofs) Tint IT1 k1) | Mop op args res => transl_op op args res k | Mload chunk addr args dst => - match chunk with - | Mint8signed => - transl_load_store - (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args GPR12 - (Pextsb (ireg_of dst) (ireg_of dst) :: k) - | Mint8unsigned => - transl_load_store - (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) addr args GPR12 k - | Mint16signed => - transl_load_store - (Plha (ireg_of dst)) (Plhax (ireg_of dst)) addr args GPR12 k - | Mint16unsigned => - transl_load_store - (Plhz (ireg_of dst)) (Plhzx (ireg_of dst)) addr args GPR12 k - | Mint32 => - transl_load_store - (Plwz (ireg_of dst)) (Plwzx (ireg_of dst)) addr args GPR12 k - | Mfloat32 => - transl_load_store - (Plfs (freg_of dst)) (Plfsx (freg_of dst)) addr args GPR12 k - | Mfloat64 | Mfloat64al32 => - transl_load_store - (Plfd (freg_of dst)) (Plfdx (freg_of dst)) addr args GPR12 k - end + transl_load chunk addr args dst k | Mstore chunk addr args src => - let temp := int_temp_for src in - match chunk with - | Mint8signed => - transl_load_store - (Pstb (ireg_of src)) (Pstbx (ireg_of src)) addr args temp k - | Mint8unsigned => - transl_load_store - (Pstb (ireg_of src)) (Pstbx (ireg_of src)) addr args temp k - | Mint16signed => - transl_load_store - (Psth (ireg_of src)) (Psthx (ireg_of src)) addr args temp k - | Mint16unsigned => - transl_load_store - (Psth (ireg_of src)) (Psthx (ireg_of src)) addr args temp k - | Mint32 => - transl_load_store - (Pstw (ireg_of src)) (Pstwx (ireg_of src)) addr args temp k - | Mfloat32 => - transl_load_store - (Pstfs (freg_of src)) (Pstfsx (freg_of src)) addr args temp k - | Mfloat64 | Mfloat64al32 => - transl_load_store - (Pstfd (freg_of src)) (Pstfdx (freg_of src)) addr args temp k - end + transl_store chunk addr args src k | Mcall sig (inl r) => - Pmtctr (ireg_of r) :: Pbctrl :: k + do r1 <- ireg_of r; OK (Pmtctr r1 :: Pbctrl :: k) | Mcall sig (inr symb) => - Pbl symb :: k + OK (Pbl symb :: k) | Mtailcall sig (inl r) => - Pmtctr (ireg_of r) :: - Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR0 :: - Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pbctr :: k + do r1 <- ireg_of r; + OK (Pmtctr r1 :: + Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR0 :: + Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pbctr :: k) | Mtailcall sig (inr symb) => - Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR0 :: - Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pbs symb :: k + OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR0 :: + Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pbs symb :: k) | Mbuiltin ef args res => - Pbuiltin ef (map preg_of args) (preg_of res) :: k + OK (Pbuiltin ef (map preg_of args) (preg_of res) :: k) | Mannot ef args => - Pannot ef (map transl_annot_param args) :: k + OK (Pannot ef (map transl_annot_param args) :: k) | Mlabel lbl => - Plabel lbl :: k + OK (Plabel lbl :: k) | Mgoto lbl => - Pb lbl :: k + OK (Pb lbl :: k) | Mcond cond args lbl => let p := crbit_for_cond cond in transl_cond cond args (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k) | Mjumptable arg tbl => - Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: - Pbtbl GPR12 tbl :: k + do r <- ireg_of arg; + OK (Pbtbl r tbl :: k) | Mreturn => - Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR0 :: - Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pblr :: k + OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR0 :: + Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pblr :: k) + end. + +(** Translation of a code sequence *) + +Definition r11_is_parent (before: bool) (i: Mach.instruction) : bool := + match i with + | Msetstack src ofs ty => before + | Mgetparam ofs ty dst => negb (mreg_eq dst IT1) + | Mop Omove args res => before && negb (mreg_eq res IT1) + | _ => false end. -Definition transl_code (f: Mach.function) (il: list Mach.instruction) := - List.fold_right (transl_instr f) nil il. +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (r11p: bool) := + match il with + | nil => OK nil + | i1 :: il' => + do k <- transl_code f il' (r11_is_parent r11p i1); + transl_instr f i1 r11p k + end. (** Translation of a whole function. Note that we must check that the generated code contains less than [2^32] instructions, @@ -556,18 +643,16 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) := around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pmflr GPR0 :: - Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: - transl_code f f.(fn_code). - -Open Local Scope string_scope. + do c <- transl_code f f.(Mach.fn_code) false; + OK (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pmflr GPR0 :: + Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: c). Definition transf_function (f: Mach.function) : res Asm.code := - let c := transl_function f in + do c <- transl_function f; if zlt Int.max_unsigned (list_length_z c) - then Errors.Error (msg "code size exceeded") - else Errors.OK c. + then Error (msg "code size exceeded") + else OK c. Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := transf_partial_fundef transf_function f. -- cgit v1.2.3