From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asmgen.v | 505 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 505 insertions(+) create mode 100644 ia32/Asmgen.v (limited to 'ia32/Asmgen.v') diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v new file mode 100644 index 0000000..70929ff --- /dev/null +++ b/ia32/Asmgen.v @@ -0,0 +1,505 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Translation from Mach to IA32 Asm. *) + +Require Import Coqlib. +Require Import Maps. +Require Import Errors. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Op. +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: +- Argument and result registers are of the correct type. +- For two-address instructions, the result and the first argument + are in the same register. (True by construction in [RTLgen], and preserved by [Reload].) +- The first argument register is never [ECX] (a.k.a. [IT2]) nor [XMM7] + (a.k.a [FT2]). +- The top of the floating-point stack ([ST0], a.k.a. [FP0]) can only + appear in [mov] instructions, but never in arithmetic instructions. + +All these properties are true by construction, but it is painful to track them statically. Instead, we 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. + +(** Smart constructors for various operations. *) + +Definition mk_mov (rd rs: preg) (k: code) : res code := + match rd, rs with + | IR rd, IR rs => OK (Pmov_rr rd rs :: k) + | FR rd, FR rs => OK (Pmovsd_ff rd rs :: k) + | ST0, FR rs => OK (Pfld_f rs :: k) + | FR rd, ST0 => OK (Pfstp_f rd :: k) + | _, _ => Error(msg "Asmgen.mk_mov") + end. + +Definition mk_shift (shift_instr: ireg -> instruction) + (r1 r2: ireg) (k: code) : res code := + if ireg_eq r2 ECX then + OK (shift_instr r1 :: k) + else + do x <- assertion (negb (ireg_eq r1 ECX)); + OK (Pmov_rr ECX r2 :: shift_instr r1 :: k). + +Definition mk_div (div_instr: ireg -> instruction) + (r1 r2: ireg) (k: code) : res code := + if ireg_eq r1 EAX then + if ireg_eq r2 EDX then + OK (Pmov_rr ECX EDX :: div_instr ECX :: k) + else + OK (div_instr r2 :: k) + else + do x <- assertion (negb (ireg_eq r1 ECX)); + if ireg_eq r2 EAX then + OK (Pmov_rr ECX EAX :: Pmov_rr EAX r1 :: + div_instr ECX :: + Pmov_rr r1 EAX :: Pmov_rr EAX ECX :: k) + else + OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX r2 :: Pmov_rr EAX r1 :: + div_instr ECX :: + Pmov_rr r2 ECX :: Pmov_rr r1 EAX :: Pmovd_rf EAX XMM7 :: k). + +Definition mk_mod (div_instr: ireg -> instruction) + (r1 r2: ireg) (k: code) : res code := + if ireg_eq r1 EAX then + if ireg_eq r2 EDX then + OK (Pmov_rr ECX EDX :: div_instr ECX :: Pmov_rr EAX EDX :: k) + else + OK (div_instr r2 :: Pmov_rr EAX EDX :: k) + else + do x <- assertion (negb (ireg_eq r1 ECX)); + if ireg_eq r2 EDX then + OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX EDX :: Pmov_rr EAX r1 :: + div_instr ECX :: + Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k) + else + OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX r2 :: Pmov_rr EAX r1 :: + div_instr ECX :: + Pmov_rr r2 ECX :: Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k). + +Definition mk_shrximm (r: ireg) (n: int) (k: code) : res code := + do x <- assertion (negb (ireg_eq r ECX)); + let p := Int.sub (Int.shl Int.one n) Int.one in + OK (Ptest_rr r r :: + Plea ECX (Addrmode (Some r) None (inl _ p)) :: + Pcmov Cond_l r ECX :: + Psar_ri r n :: k). + +Definition low_ireg (r: ireg) : bool := + match r with + | EAX | EBX | ECX | EDX => true + | ESI | EDI | EBP | ESP => false + end. + +Definition mk_intconv (mk: ireg -> ireg -> instruction) (rd rs: ireg) (k: code) := + if low_ireg rs then + OK (mk rd rs :: k) + else + OK (Pmov_rr EDX rs :: mk rd EDX :: k). + +Definition mk_smallstore (sto: addrmode -> ireg ->instruction) + (addr: addrmode) (rs: ireg) (k: code) := + if low_ireg rs then + OK (sto addr rs :: k) + else + OK (Plea ECX addr :: Pmov_rr EDX rs :: + sto (Addrmode (Some ECX) None (inl _ Int.zero)) EDX :: k). + +(** Accessing slots in the stack frame. *) + +Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := + match ty with + | Tint => + do r <- ireg_of dst; + OK (Pmov_rm r (Addrmode (Some base) None (inl _ ofs)) :: k) + | Tfloat => + match preg_of dst with + | FR r => OK (Pmovsd_fm r (Addrmode (Some base) None (inl _ ofs)) :: k) + | ST0 => OK (Pfld_m (Addrmode (Some base) None (inl _ ofs)) :: k) + | _ => Error (msg "Asmgen.loadind") + end + end. + +Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := + match ty with + | Tint => + do r <- ireg_of src; + OK (Pmov_mr (Addrmode (Some base) None (inl _ ofs)) r :: k) + | Tfloat => + match preg_of src with + | FR r => OK (Pmovsd_mf (Addrmode (Some base) None (inl _ ofs)) r :: k) + | ST0 => OK (Pfstp_m (Addrmode (Some base) None (inl _ ofs)) :: k) + | _ => Error (msg "Asmgen.loadind") + end + end. + +(** Translation of addressing modes *) + +Definition transl_addressing (a: addressing) (args: list mreg): res addrmode := + match a, args with + | Aindexed n, a1 :: nil => + do r1 <- ireg_of a1; OK(Addrmode (Some r1) None (inl _ n)) + | Aindexed2 n, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK(Addrmode (Some r1) (Some(r2, Int.one)) (inl _ n)) + | Ascaled sc n, a1 :: nil => + do r1 <- ireg_of a1; OK(Addrmode None (Some(r1, sc)) (inl _ n)) + | Aindexed2scaled sc n, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK(Addrmode (Some r1) (Some(r2, sc)) (inl _ n)) + | Aglobal id ofs, nil => + OK(Addrmode None None (inr _ (id, ofs))) + | Abased id ofs, a1 :: nil => + do r1 <- ireg_of a1; OK(Addrmode (Some r1) None (inr _ (id, ofs))) + | Abasedscaled sc id ofs, a1 :: nil => + do r1 <- ireg_of a1; OK(Addrmode None (Some(r1, sc)) (inr _ (id, ofs))) + | Ainstack n, nil => + OK(Addrmode (Some ESP) None (inl _ n)) + | _, _ => + Error(msg "Asmgen.transl_addressing") + end. + +(** Floating-point comparison. We swap the operands in some cases + to simplify the handling of the unordered case. *) + +Definition floatcomp (cmp: comparison) (r1 r2: freg) : instruction := + match cmp with + | Clt | Cle => Pcomisd_ff r2 r1 + | Ceq | Cne | Cgt | Cge => Pcomisd_ff r1 r2 + end. + +(** Translation of a condition. Prepends to [k] the instructions + that evaluate the condition and leave its boolean result in bits + of the condition register. *) + +Definition transl_cond + (cond: condition) (args: list mreg) (k: code) : res code := + match cond, args with + | Ccomp c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmp_rr r1 r2 :: k) + | Ccompu c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmp_rr r1 r2 :: k) + | Ccompimm c n, a1 :: nil => + do r1 <- ireg_of a1; OK (Pcmp_ri r1 n :: k) + | Ccompuimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (if Int.eq_dec n Int.zero then Ptest_rr r1 r1 :: k else Pcmp_ri r1 n :: k) + | Ccompf cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k) + | Cnotcompf cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k) + | Cmaskzero n, a1 :: nil => + do r1 <- ireg_of a1; OK (Ptest_ri r1 n :: k) + | Cmasknotzero n, a1 :: nil => + do r1 <- ireg_of a1; OK (Ptest_ri r1 n :: k) + | _, _ => + Error(msg "Asmgen.transl_cond") + end. + +(** What processor condition to test for a given Mach condition. *) + +Definition testcond_for_signed_comparison (cmp: comparison) := + match cmp with + | Ceq => Cond_e + | Cne => Cond_ne + | Clt => Cond_l + | Cle => Cond_le + | Cgt => Cond_g + | Cge => Cond_ge + end. + +Definition testcond_for_unsigned_comparison (cmp: comparison) := + match cmp with + | Ceq => Cond_e + | Cne => Cond_ne + | Clt => Cond_b + | Cle => Cond_be + | Cgt => Cond_a + | Cge => Cond_ae + end. + +Definition testcond_for_condition (cond: condition) : testcond := + match cond with + | Ccomp c => testcond_for_signed_comparison c + | Ccompu c => testcond_for_unsigned_comparison c + | Ccompimm c n => testcond_for_signed_comparison c + | Ccompuimm c n => testcond_for_unsigned_comparison c + | Ccompf c => + match c with + | Ceq => Cond_enp + | Cne => Cond_nep + | Clt => Cond_a + | Cle => Cond_ae + | Cgt => Cond_a + | Cge => Cond_ae + end + | Cnotcompf c => + match c with + | Ceq => Cond_nep + | Cne => Cond_enp + | Clt => Cond_be + | Cle => Cond_b + | Cgt => Cond_be + | Cge => Cond_b + end + | Cmaskzero n => Cond_e + | Cmasknotzero n => Cond_ne + end. + +(** Translation of the arithmetic operation [r <- op(args)]. + The corresponding instructions are prepended to [k]. *) + +Definition transl_op + (op: operation) (args: list mreg) (res: mreg) (k: code) : Errors.res code := + match op, args with + | Omove, a1 :: nil => + mk_mov (preg_of res) (preg_of a1) k + | Ointconst n, nil => + do r <- ireg_of res; OK (Pmov_ri r n :: k) + | Ofloatconst f, nil => + do r <- freg_of res; OK (Pmovsd_fi r f :: k) + | Ocast8signed, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsb_rr r r1 k + | Ocast8unsigned, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovzb_rr r r1 k + | Ocast16signed, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsw_rr r r1 k + | Ocast16unsigned, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovzw_rr r r1 k + | Oneg, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pneg r :: k) + | Osub, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Psub_rr r r2 :: k) + | Omul, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pimul_rr r r2 :: k) + | Omulimm n, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pimul_ri r n :: k) + | Odiv, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; mk_div Pidiv r r2 k + | Odivu, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; mk_div Pdiv r r2 k + | Omod, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; mk_mod Pidiv r r2 k + | Omodu, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; mk_mod Pdiv r r2 k + | Oand, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pand_rr r r2 :: k) + | Oandimm n, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pand_ri r n :: k) + | Oor, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Por_rr r r2 :: k) + | Oorimm n, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Por_ri r n :: k) + | Oxor, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pxor_rr r r2 :: k) + | Oxorimm n, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pxor_ri r n :: k) + | Oshl, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; mk_shift Psal_rcl r r2 k + | Oshlimm n, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Psal_ri r n :: k) + | Oshr, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; mk_shift Psar_rcl r r2 k + | Oshrimm n, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Psar_ri r n :: k) + | Oshru, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; mk_shift Pshr_rcl r r2 k + | Oshruimm n, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pshr_ri r n :: k) + | Oshrximm n, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; mk_shrximm r n k + | Ororimm n, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pror_ri r n :: k) + | Olea addr, _ => + do am <- transl_addressing addr args; do r <- ireg_of res; + OK (Plea r am :: k) + | Onegf, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- freg_of res; OK (Pnegd r :: k) + | Oabsf, a1 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- freg_of res; OK (Pabsd r :: k) + | Oaddf, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Paddd_ff r r2 :: k) + | Osubf, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Psubd_ff r r2 :: k) + | Omulf, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Pmuld_ff r r2 :: k) + | Odivf, a1 :: a2 :: nil => + do x <- assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Pdivd_ff r r2 :: k) + | Osingleoffloat, a1 :: nil => + do r <- freg_of res; do r1 <- freg_of a1; OK (Pcvtsd2ss_ff r r1 :: k) + | Ointoffloat, a1 :: nil => + do r <- ireg_of res; do r1 <- freg_of a1; OK (Pcvttsd2si_rf r r1 :: k) + | Ofloatofint, a1 :: nil => + do r <- freg_of res; do r1 <- ireg_of a1; OK (Pcvtsi2sd_fr r r1 :: k) + | Ocmp c, args => + do r <- ireg_of res; + transl_cond c args (Psetcc (testcond_for_condition c) r :: k) + | _, _ => + Error(msg "Asmgen.transl_op") + end. + +(** Translation of memory loads and stores *) + +Definition transl_load (chunk: memory_chunk) + (addr: addressing) (args: list mreg) (dest: mreg) + (k: code) : res code := + do am <- transl_addressing addr args; + match chunk with + | Mint8unsigned => + do r <- ireg_of dest; OK(Pmovzb_rm r am :: k) + | Mint8signed => + do r <- ireg_of dest; OK(Pmovsb_rm r am :: k) + | Mint16unsigned => + do r <- ireg_of dest; OK(Pmovzw_rm r am :: k) + | Mint16signed => + do r <- ireg_of dest; OK(Pmovsw_rm r am :: k) + | Mint32 => + do r <- ireg_of dest; OK(Pmov_rm r am :: k) + | Mfloat32 => + do r <- freg_of dest; OK(Pcvtss2sd_fm r am :: k) + | Mfloat64 => + do r <- freg_of dest; OK(Pmovsd_fm r am :: k) + end. + +Definition transl_store (chunk: memory_chunk) + (addr: addressing) (args: list mreg) (src: mreg) + (k: code) : res code := + do am <- transl_addressing addr args; + match chunk with + | Mint8unsigned | Mint8signed => + do r <- ireg_of src; mk_smallstore Pmovb_mr am r k + | Mint16unsigned | Mint16signed => + do r <- ireg_of src; mk_smallstore Pmovw_mr am r k + | Mint32 => + do r <- ireg_of src; OK(Pmov_mr am r :: k) + | Mfloat32 => + do r <- freg_of src; OK(Pcvtsd2ss_mf am r :: k) + | Mfloat64 => + do r <- freg_of src; OK(Pmovsd_mf am r :: k) + end. + +(** Translation of a Mach instruction. *) + +Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := + match i with + | Mgetstack ofs ty dst => + loadind ESP ofs ty dst k + | Msetstack src ofs ty => + storeind src ESP ofs ty k + | Mgetparam ofs ty dst => + do k1 <- loadind EDX ofs ty dst k; + loadind ESP f.(fn_link_ofs) Tint IT1 k1 + | Mop op args res => + transl_op op args res k + | Mload chunk addr args dst => + transl_load chunk addr args dst k + | Mstore chunk addr args src => + transl_store chunk addr args src k + | Mcall sig (inl reg) => + do r <- ireg_of reg; OK (Pcall_r r :: k) + | Mcall sig (inr symb) => + OK (Pcall_s symb :: k) + | Mtailcall sig (inl reg) => + do r <- ireg_of reg; + OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) + f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + Pjmp_r r :: k) + | Mtailcall sig (inr symb) => + OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) + f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + Pjmp_s symb :: k) + | Mlabel lbl => + OK(Plabel lbl :: k) + | Mgoto lbl => + OK(Pjmp_l lbl :: k) + | Mcond cond args lbl => + transl_cond cond args (Pjcc (testcond_for_condition cond) lbl :: k) + | Mjumptable arg tbl => + do r <- ireg_of arg; OK (Pjmptbl r tbl :: k) + | Mreturn => + OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) + f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + Pret :: k) + | Mbuiltin ef args res => + OK (Pbuiltin ef (List.map preg_of args) (preg_of res) :: k) + end. + +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) := + match il with + | nil => OK nil + | i1 :: il' => do k <- transl_code f il'; transl_instr f i1 k + end. + +(** Translation of a whole function. Note that we must check + that the generated code contains less than [2^32] instructions, + otherwise the offset part of the [PC] code pointer could wrap + around, leading to incorrect executions. *) + +Definition transf_function (f: Mach.function) : res Asm.code := + do c <- transl_code f f.(fn_code); + if zlt (list_length_z c) Int.max_unsigned + then OK (Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) + f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c) + else Error (msg "code size exceeded"). + +Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: Mach.program) : res Asm.program := + transform_partial_program transf_fundef p. + -- cgit v1.2.3