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 --- arm/Asmgen.v | 456 +++++++++++++++++++++++++++++++++++------------------------ 1 file changed, 274 insertions(+), 182 deletions(-) (limited to 'arm/Asmgen.v') diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 05e7010e..562cf221 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -22,6 +22,17 @@ Require Import Locations. Require Import Mach. Require Import Asm. +Open Local Scope string_scope. +Open Local Scope error_monad_scope. + +(** 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. + (** Recognition of integer immediate arguments. - For arithmetic operations, immediates are 8-bit quantities zero-extended and rotated right by 0, 2, 4, ... 30 bits. @@ -130,33 +141,43 @@ Definition transl_cond (cond: condition) (args: list mreg) (k: code) := match cond, args with | Ccomp c, a1 :: a2 :: nil => - Pcmp (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp r1(SOreg r2) :: k) | Ccompu c, a1 :: a2 :: nil => - Pcmp (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp r1 (SOreg r2) :: k) | Ccompshift c s, a1 :: a2 :: nil => - Pcmp (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp r1 (transl_shift s r2) :: k) | Ccompushift c s, a1 :: a2 :: nil => - Pcmp (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp r1 (transl_shift s r2) :: k) | Ccompimm c n, a1 :: nil => - if is_immed_arith n then - Pcmp (ireg_of a1) (SOimm n) :: k - else - loadimm IR14 n (Pcmp (ireg_of a1) (SOreg IR14) :: k) + do r1 <- ireg_of a1; + OK (if is_immed_arith n then + Pcmp r1 (SOimm n) :: k + else + loadimm IR14 n (Pcmp r1 (SOreg IR14) :: k)) | Ccompuimm c n, a1 :: nil => - if is_immed_arith n then - Pcmp (ireg_of a1) (SOimm n) :: k - else - loadimm IR14 n (Pcmp (ireg_of a1) (SOreg IR14) :: k) + do r1 <- ireg_of a1; + OK (if is_immed_arith n then + Pcmp r1 (SOimm n) :: k + else + loadimm IR14 n (Pcmp r1 (SOreg IR14) :: k)) | Ccompf cmp, a1 :: a2 :: nil => - Pfcmpd (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmpd r1 r2 :: k) | Cnotcompf cmp, a1 :: a2 :: nil => - Pfcmpd (freg_of a1) (freg_of a2) :: k + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmpd r1 r2 :: k) | Ccompfzero cmp, a1 :: nil => - Pfcmpzd (freg_of a1) :: k + do r1 <- freg_of a1; + OK (Pfcmpzd r1 :: k) | Cnotcompfzero cmp, a1 :: nil => - Pfcmpzd (freg_of a1) :: k + do r1 <- freg_of a1; + OK (Pfcmpzd r1 :: k) | _, _ => - k (**r never happens for well-typed code *) + Error(msg "Asmgen.transl_cond") end. Definition crbit_for_signed_cmp (cmp: comparison) := @@ -217,115 +238,159 @@ Definition crbit_for_cond (cond: condition) := 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 => Pmov (ireg_of r) (SOreg (ireg_of a1)) :: k - | Tfloat => Pfcpyd (freg_of r) (freg_of a1) :: k + match preg_of res, preg_of a1 with + | IR r, IR a => OK (Pmov r (SOreg a) :: k) + | FR r, FR a => OK (Pfcpyd 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 => - Pflid (freg_of r) f :: k + do r <- freg_of res; + OK (Pflid r f :: k) | Oaddrsymbol s ofs, nil => - Ploadsymbol (ireg_of r) s ofs :: k + do r <- ireg_of res; + OK (Ploadsymbol r s ofs :: k) | Oaddrstack n, nil => - addimm (ireg_of r) IR13 n k + do r <- ireg_of res; + OK (addimm r IR13 n k) | Oadd, a1 :: a2 :: nil => - Padd (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd r r1 (SOreg r2) :: k) | Oaddshift s, a1 :: a2 :: nil => - Padd (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd r r1 (transl_shift s r2) :: k) | Oaddimm n, a1 :: nil => - addimm (ireg_of r) (ireg_of a1) n k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (addimm r r1 n k) | Osub, a1 :: a2 :: nil => - Psub (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub r r1 (SOreg r2) :: k) | Osubshift s, a1 :: a2 :: nil => - Psub (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub r r1 (transl_shift s r2) :: k) | Orsubshift s, a1 :: a2 :: nil => - Prsb (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Prsb r r1 (transl_shift s r2) :: k) | Orsubimm n, a1 :: nil => - rsubimm (ireg_of r) (ireg_of a1) n k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (rsubimm r r1 n k) | Omul, a1 :: a2 :: nil => - if ireg_eq (ireg_of r) (ireg_of a1) - || ireg_eq (ireg_of r) (ireg_of a2) - then Pmul IR14 (ireg_of a1) (ireg_of a2) :: Pmov (ireg_of r) (SOreg IR14) :: k - else Pmul (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (if ireg_eq r r1 || ireg_eq r r2 + then Pmul IR14 r1 r2 :: Pmov r (SOreg IR14) :: k + else Pmul r r1 r2 :: k) | Odiv, a1 :: a2 :: nil => - Psdiv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psdiv r r1 r2 :: k) | Odivu, a1 :: a2 :: nil => - Pudiv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pudiv r r1 r2 :: k) | Oand, a1 :: a2 :: nil => - Pand (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand r r1 (SOreg r2) :: k) | Oandshift s, a1 :: a2 :: nil => - Pand (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand r r1 (transl_shift s r2) :: k) | Oandimm n, a1 :: nil => - andimm (ireg_of r) (ireg_of a1) n k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (andimm r r1 n k) | Oor, a1 :: a2 :: nil => - Porr (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr r r1 (SOreg r2) :: k) | Oorshift s, a1 :: a2 :: nil => - Porr (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr r r1 (transl_shift s r2) :: k) | Oorimm n, a1 :: nil => - orimm (ireg_of r) (ireg_of a1) n k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (orimm r r1 n k) | Oxor, a1 :: a2 :: nil => - Peor (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor r r1 (SOreg r2) :: k) | Oxorshift s, a1 :: a2 :: nil => - Peor (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor r r1 (transl_shift s r2) :: k) | Oxorimm n, a1 :: nil => - xorimm (ireg_of r) (ireg_of a1) n k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (xorimm r r1 n k) | Obic, a1 :: a2 :: nil => - Pbic (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic r r1 (SOreg r2) :: k) | Obicshift s, a1 :: a2 :: nil => - Pbic (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic r r1 (transl_shift s r2) :: k) | Onot, a1 :: nil => - Pmvn (ireg_of r) (SOreg (ireg_of a1)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (Pmvn r (SOreg r1) :: k) | Onotshift s, a1 :: nil => - Pmvn (ireg_of r) (transl_shift s (ireg_of a1)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (Pmvn r (transl_shift s r1) :: k) | Oshl, a1 :: a2 :: nil => - Pmov (ireg_of r) (SOlslreg (ireg_of a1) (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pmov r (SOlslreg r1 r2) :: k) | Oshr, a1 :: a2 :: nil => - Pmov (ireg_of r) (SOasrreg (ireg_of a1) (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pmov r (SOasrreg r1 r2) :: k) | Oshru, a1 :: a2 :: nil => - Pmov (ireg_of r) (SOlsrreg (ireg_of a1) (ireg_of a2)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pmov r (SOlsrreg r1 r2) :: k) | Oshift s, a1 :: nil => - Pmov (ireg_of r) (transl_shift s (ireg_of a1)) :: k + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (Pmov r (transl_shift s r1) :: k) | Oshrximm n, a1 :: nil => - Pcmp (ireg_of a1) (SOimm Int.zero) :: - addimm IR14 (ireg_of a1) (Int.sub (Int.shl Int.one n) Int.one) - (Pmovc CRge IR14 (SOreg (ireg_of a1)) :: - Pmov (ireg_of r) (SOasrimm IR14 n) :: k) + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (Pcmp r1 (SOimm Int.zero) :: + addimm IR14 r1 (Int.sub (Int.shl Int.one n) Int.one) + (Pmovc CRge IR14 (SOreg r1) :: + Pmov r (SOasrimm IR14 n) :: k)) | Onegf, a1 :: nil => - Pfnegd (freg_of r) (freg_of a1) :: k + do r <- freg_of res; do r1 <- freg_of a1; + OK (Pfnegd r r1 :: k) | Oabsf, a1 :: nil => - Pfabsd (freg_of r) (freg_of a1) :: k + do r <- freg_of res; do r1 <- freg_of a1; + OK (Pfabsd r r1 :: k) | Oaddf, a1 :: a2 :: nil => - Pfaddd (freg_of r) (freg_of a1) (freg_of a2) :: k + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfaddd r r1 r2 :: k) | Osubf, a1 :: a2 :: nil => - Pfsubd (freg_of r) (freg_of a1) (freg_of a2) :: k + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfsubd r r1 r2 :: k) | Omulf, a1 :: a2 :: nil => - Pfmuld (freg_of r) (freg_of a1) (freg_of a2) :: k + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfmuld r r1 r2 :: k) | Odivf, a1 :: a2 :: nil => - Pfdivd (freg_of r) (freg_of a1) (freg_of a2) :: k + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfdivd r r1 r2 :: k) | Osingleoffloat, a1 :: nil => - Pfcvtsd (freg_of r) (freg_of a1) :: k + do r <- freg_of res; do r1 <- freg_of a1; + OK (Pfcvtsd r r1 :: k) | Ointoffloat, a1 :: nil => - Pftosizd (ireg_of r) (freg_of a1) :: k + do r <- ireg_of res; do r1 <- freg_of a1; + OK (Pftosizd r r1 :: k) | Ointuoffloat, a1 :: nil => - Pftouizd (ireg_of r) (freg_of a1) :: k + do r <- ireg_of res; do r1 <- freg_of a1; + OK (Pftouizd r r1 :: k) | Ofloatofint, a1 :: nil => - Pfsitod (freg_of r) (ireg_of a1) :: k + do r <- freg_of res; do r1 <- ireg_of a1; + OK (Pfsitod r r1 :: k) | Ofloatofintu, a1 :: nil => - Pfuitod (freg_of r) (ireg_of a1) :: k + do r <- freg_of res; do r1 <- ireg_of a1; + OK (Pfuitod r r1 :: k) | Ocmp cmp, _ => + do r <- ireg_of res; transl_cond cmp args - (Pmov (ireg_of r) (SOimm Int.zero) :: - Pmovc (crbit_for_cond cmp) (ireg_of r) (SOimm Int.one) :: + (Pmov r (SOimm Int.zero) :: + Pmovc (crbit_for_cond cmp) r (SOimm Int.one) :: 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 transl_shift_addr (s: shift) (r: ireg) : shift_addr := match s with @@ -335,62 +400,106 @@ Definition transl_shift_addr (s: shift) (r: ireg) : shift_addr := | Sror n => SAror r (s_amount n) end. -Definition transl_load_store +Definition transl_memory_access (mk_instr_imm: ireg -> int -> instruction) (mk_instr_gen: option (ireg -> shift_addr -> instruction)) (is_immed: int -> bool) - (addr: addressing) (args: list mreg) (k: code) : code := + (addr: addressing) (args: list mreg) (k: code) := match addr, args with | Aindexed n, a1 :: nil => - if is_immed n then - mk_instr_imm (ireg_of a1) n :: k - else - addimm IR14 (ireg_of a1) n - (mk_instr_imm IR14 Int.zero :: k) + do r1 <- ireg_of a1; + OK (if is_immed n then + mk_instr_imm r1 n :: k + else + addimm IR14 r1 n + (mk_instr_imm IR14 Int.zero :: k)) | Aindexed2, a1 :: a2 :: nil => - match mk_instr_gen with - | Some f => - f (ireg_of a1) (SAreg (ireg_of a2)) :: k - | None => - Padd IR14 (ireg_of a1) (SOreg (ireg_of a2)) :: - mk_instr_imm IR14 Int.zero :: k - end + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (match mk_instr_gen with + | Some f => + f r1 (SAreg r2) :: k + | None => + Padd IR14 r1 (SOreg r2) :: + mk_instr_imm IR14 Int.zero :: k + end) | Aindexed2shift s, a1 :: a2 :: nil => - match mk_instr_gen with - | Some f => - f (ireg_of a1) (transl_shift_addr s (ireg_of a2)) :: k - | None => - Padd IR14 (ireg_of a1) (transl_shift s (ireg_of a2)) :: - mk_instr_imm IR14 Int.zero :: k - end + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (match mk_instr_gen with + | Some f => + f r1 (transl_shift_addr s r2) :: k + | None => + Padd IR14 r1 (transl_shift s r2) :: + mk_instr_imm IR14 Int.zero :: k + end) | Ainstack n, nil => - if is_immed n then - mk_instr_imm IR13 n :: k - else - addimm IR14 IR13 n - (mk_instr_imm IR14 Int.zero :: k) + OK (if is_immed n then + mk_instr_imm IR13 n :: k + else + addimm IR14 IR13 n (mk_instr_imm IR14 Int.zero :: k)) | _, _ => - (* should not happen *) k + Error(msg "Asmgen.transl_memory_access") end. -Definition transl_load_store_int +Definition transl_memory_access_int (mk_instr: ireg -> ireg -> shift_addr -> instruction) (is_immed: int -> bool) - (rd: mreg) (addr: addressing) (args: list mreg) (k: code) := - transl_load_store - (fun r n => mk_instr (ireg_of rd) r (SAimm n)) - (Some (mk_instr (ireg_of rd))) + (dst: mreg) (addr: addressing) (args: list mreg) (k: code) := + do rd <- ireg_of dst; + transl_memory_access + (fun r n => mk_instr rd r (SAimm n)) + (Some (mk_instr rd)) is_immed addr args k. -Definition transl_load_store_float +Definition transl_memory_access_float (mk_instr: freg -> ireg -> int -> instruction) (is_immed: int -> bool) - (rd: mreg) (addr: addressing) (args: list mreg) (k: code) := - transl_load_store - (mk_instr (freg_of rd)) + (dst: mreg) (addr: addressing) (args: list mreg) (k: code) := + do rd <- freg_of dst; + transl_memory_access + (mk_instr rd) None is_immed addr args k. +Definition transl_load (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (dst: mreg) (k: code) := + match chunk with + | Mint8signed => + transl_memory_access_int Pldrsb is_immed_mem_small dst addr args k + | Mint8unsigned => + transl_memory_access_int Pldrb is_immed_mem_word dst addr args k + | Mint16signed => + transl_memory_access_int Pldrsh is_immed_mem_small dst addr args k + | Mint16unsigned => + transl_memory_access_int Pldrh is_immed_mem_small dst addr args k + | Mint32 => + transl_memory_access_int Pldr is_immed_mem_word dst addr args k + | Mfloat32 => + transl_memory_access_float Pflds is_immed_mem_float dst addr args k + | Mfloat64 | Mfloat64al32 => + transl_memory_access_float Pfldd is_immed_mem_float dst addr args k + end. + +Definition transl_store (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (src: mreg) (k: code) := + match chunk with + | Mint8signed => + transl_memory_access_int Pstrb is_immed_mem_small src addr args k + | Mint8unsigned => + transl_memory_access_int Pstrb is_immed_mem_word src addr args k + | Mint16signed => + transl_memory_access_int Pstrh is_immed_mem_small src addr args k + | Mint16unsigned => + transl_memory_access_int Pstrh is_immed_mem_small src addr args k + | Mint32 => + transl_memory_access_int Pstr is_immed_mem_word src addr args k + | Mfloat32 => + transl_memory_access_float Pfsts is_immed_mem_float src addr args k + | Mfloat64 | Mfloat64al32 => + transl_memory_access_float Pfstd is_immed_mem_float src addr args k + end. + +(** Accessing data in the stack frame. *) + Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) := if is_immed_mem_word ofs then Pldr dst base (SAimm ofs) :: k @@ -407,8 +516,8 @@ Definition loadind_float (base: ireg) (ofs: int) (dst: freg) (k: code) := Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := match ty with - | Tint => loadind_int base ofs (ireg_of dst) k - | Tfloat => loadind_float base ofs (freg_of dst) k + | Tint => do r <- ireg_of dst; OK (loadind_int base ofs r k) + | Tfloat => do r <- freg_of dst; OK (loadind_float base ofs r k) end. Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) := @@ -427,8 +536,8 @@ Definition storeind_float (src: freg) (base: ireg) (ofs: int) (k: code) := Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := match ty with - | Tint => storeind_int (ireg_of src) base ofs k - | Tfloat => storeind_float (freg_of src) base ofs k + | Tint => do r <- ireg_of src; OK (storeind_int r base ofs k) + | Tfloat => do r <- freg_of src; OK (storeind_float r base ofs k) end. (** Translation of arguments to annotations *) @@ -441,80 +550,71 @@ 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) + (r10_is_parent: bool) (k: code) := match i with | Mgetstack ofs ty dst => loadind IR13 ofs ty dst k | Msetstack src ofs ty => storeind src IR13 ofs ty k | Mgetparam ofs ty dst => - loadind_int IR13 f.(fn_link_ofs) IR14 (loadind IR14 ofs ty dst k) + do c <- loadind IR10 ofs ty dst k; + OK (if r10_is_parent + then c + else loadind_int IR13 f.(fn_link_ofs) IR10 c) | Mop op args res => transl_op op args res k | Mload chunk addr args dst => - match chunk with - | Mint8signed => - transl_load_store_int Pldrsb is_immed_mem_small dst addr args k - | Mint8unsigned => - transl_load_store_int Pldrb is_immed_mem_word dst addr args k - | Mint16signed => - transl_load_store_int Pldrsh is_immed_mem_small dst addr args k - | Mint16unsigned => - transl_load_store_int Pldrh is_immed_mem_small dst addr args k - | Mint32 => - transl_load_store_int Pldr is_immed_mem_word dst addr args k - | Mfloat32 => - transl_load_store_float Pflds is_immed_mem_float dst addr args k - | Mfloat64 | Mfloat64al32 => - transl_load_store_float Pfldd is_immed_mem_float dst addr args k - end + transl_load chunk addr args dst k | Mstore chunk addr args src => - match chunk with - | Mint8signed => - transl_load_store_int Pstrb is_immed_mem_small src addr args k - | Mint8unsigned => - transl_load_store_int Pstrb is_immed_mem_word src addr args k - | Mint16signed => - transl_load_store_int Pstrh is_immed_mem_small src addr args k - | Mint16unsigned => - transl_load_store_int Pstrh is_immed_mem_small src addr args k - | Mint32 => - transl_load_store_int Pstr is_immed_mem_word src addr args k - | Mfloat32 => - transl_load_store_float Pfsts is_immed_mem_float src addr args k - | Mfloat64 | Mfloat64al32 => - transl_load_store_float Pfstd is_immed_mem_float src addr args k - end - | Mcall sig (inl r) => - Pblreg (ireg_of r) sig :: k + transl_store chunk addr args src k + | Mcall sig (inl arg) => + do r <- ireg_of arg; OK (Pblreg r sig :: k) | Mcall sig (inr symb) => - Pblsymb symb sig :: k - | Mtailcall sig (inl r) => - loadind_int IR13 f.(fn_retaddr_ofs) IR14 - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg (ireg_of r) sig :: k) + OK (Pblsymb symb sig :: k) + | Mtailcall sig (inl arg) => + do r <- ireg_of arg; + OK (loadind_int IR13 f.(fn_retaddr_ofs) IR14 + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg r sig :: k)) | Mtailcall sig (inr symb) => - loadind_int IR13 f.(fn_retaddr_ofs) IR14 - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb sig :: k) + OK (loadind_int IR13 f.(fn_retaddr_ofs) IR14 + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb sig :: 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 => transl_cond cond args (Pbc (crbit_for_cond cond) lbl :: k) | Mjumptable arg tbl => - Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) :: - Pbtbl IR14 tbl :: k + do r <- ireg_of arg; + OK (Pbtbl r tbl :: k) | Mreturn => - loadind_int IR13 f.(fn_retaddr_ofs) IR14 - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 f.(Mach.fn_sig) :: k) + OK (loadind_int IR13 f.(fn_retaddr_ofs) IR14 + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pbreg IR14 f.(Mach.fn_sig) :: k)) end. -Definition transl_code (f: Mach.function) (il: list Mach.instruction) := - List.fold_right (transl_instr f) nil il. +(** Translation of a code sequence *) + +Definition r10_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. + +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (r10p: bool) := + match il with + | nil => OK nil + | i1 :: il' => + do k <- transl_code f il' (r10_is_parent r10p i1); + transl_instr f i1 r10p k + end. (** Translation of a whole function. Note that we must check that the generated code contains less than [2^32] instructions, @@ -522,24 +622,16 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) := around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - mkfunction f.(Mach.fn_sig) - (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) :: - transl_code f f.(Mach.fn_code)). - -Fixpoint code_size (c: code) : Z := - match c with - | nil => 0 - | instr :: c' => code_size c' + 1 - end. - -Open Local Scope string_scope. + do c <- transl_code f f.(Mach.fn_code) true; + OK (mkfunction f.(Mach.fn_sig) + (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) :: c)). Definition transf_function (f: Mach.function) : res Asm.function := - let tf := transl_function f in - if zlt Int.max_unsigned (code_size tf.(fn_code)) - then Errors.Error (msg "code size exceeded") - else Errors.OK tf. + do tf <- transl_function f; + if zlt Int.max_unsigned (list_length_z tf.(fn_code)) + then Error (msg "code size exceeded") + else OK tf. Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := transf_partial_fundef transf_function f. -- cgit