diff options
Diffstat (limited to 'verilog/Asmgen.v')
| -rw-r--r-- | verilog/Asmgen.v | 788 |
1 files changed, 788 insertions, 0 deletions
diff --git a/verilog/Asmgen.v b/verilog/Asmgen.v new file mode 100644 index 00000000..73e3263e --- /dev/null +++ b/verilog/Asmgen.v @@ -0,0 +1,788 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris *) +(* *) +(* 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 assembly language *) + +Require Import Coqlib Errors. +Require Import AST Integers Floats Memdata. +Require Import Op Locations Mach Asm. + +Local Open Scope string_scope. +Local Open 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 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 some 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) + | _, _ => Error(msg "Asmgen.mk_mov") + end. + +Definition mk_shrximm (n: int) (k: code) : res code := + let p := Int.sub (Int.shl Int.one n) Int.one in + OK (Ptestl_rr RAX RAX :: + Pleal RCX (Addrmode (Some RAX) None (inl _ (Int.unsigned p))) :: + Pcmov Cond_l RAX RCX :: + Psarl_ri RAX n :: k). + +Definition mk_shrxlimm (n: int) (k: code) : res code := + OK (if Int.eq n Int.zero then Pmov_rr RAX RAX :: k else + Pcqto :: + Pshrq_ri RDX (Int.sub (Int.repr 64) n) :: + Pleaq RAX (Addrmode (Some RAX) (Some(RDX, 1)) (inl _ 0)) :: + Psarq_ri RAX n :: k). + +Definition low_ireg (r: ireg) : bool := + match r with RAX | RBX | RCX | RDX => true | _ => false end. + +Definition mk_intconv (mk: ireg -> ireg -> instruction) (rd rs: ireg) (k: code) := + if Archi.ptr64 || low_ireg rs then + OK (mk rd rs :: k) + else + OK (Pmov_rr RAX rs :: mk rd RAX :: k). + +Definition addressing_mentions (addr: addrmode) (r: ireg) : bool := + match addr with Addrmode base displ const => + match base with Some r' => ireg_eq r r' | None => false end + || match displ with Some(r', sc) => ireg_eq r r' | None => false end + end. + +Definition mk_storebyte (addr: addrmode) (rs: ireg) (k: code) := + if Archi.ptr64 || low_ireg rs then + OK (Pmovb_mr addr rs :: k) + else if addressing_mentions addr RAX then + OK (Pleal RCX addr :: Pmov_rr RAX rs :: + Pmovb_mr (Addrmode (Some RCX) None (inl _ 0)) RAX :: k) + else + OK (Pmov_rr RAX rs :: Pmovb_mr addr RAX :: k). + +(** Accessing slots in the stack frame. *) + +Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := + let a := Addrmode (Some base) None (inl _ (Ptrofs.unsigned ofs)) in + match ty, preg_of dst with + | Tint, IR r => OK (Pmovl_rm r a :: k) + | Tlong, IR r => OK (Pmovq_rm r a :: k) + | Tsingle, FR r => OK (Pmovss_fm r a :: k) + | Tsingle, ST0 => OK (Pflds_m a :: k) + | Tfloat, FR r => OK (Pmovsd_fm r a :: k) + | Tfloat, ST0 => OK (Pfldl_m a :: k) + | Tany32, IR r => if Archi.ptr64 then Error (msg "Asmgen.loadind1") else OK (Pmov_rm_a r a :: k) + | Tany64, IR r => if Archi.ptr64 then OK (Pmov_rm_a r a :: k) else Error (msg "Asmgen.loadind2") + | Tany64, FR r => OK (Pmovsd_fm_a r a :: k) + | _, _ => Error (msg "Asmgen.loadind") + end. + +Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) := + let a := Addrmode (Some base) None (inl _ (Ptrofs.unsigned ofs)) in + match ty, preg_of src with + | Tint, IR r => OK (Pmovl_mr a r :: k) + | Tlong, IR r => OK (Pmovq_mr a r :: k) + | Tsingle, FR r => OK (Pmovss_mf a r :: k) + | Tsingle, ST0 => OK (Pfstps_m a :: k) + | Tfloat, FR r => OK (Pmovsd_mf a r :: k) + | Tfloat, ST0 => OK (Pfstpl_m a :: k) + | Tany32, IR r => if Archi.ptr64 then Error (msg "Asmgen.storeind1") else OK (Pmov_mr_a a r :: k) + | Tany64, IR r => if Archi.ptr64 then OK (Pmov_mr_a a r :: k) else Error (msg "Asmgen.storeind2") + | Tany64, FR r => OK (Pmovsd_mf_a a r :: k) + | _, _ => Error (msg "Asmgen.storeind") + 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, 1)) (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 RSP) None (inl _ (Ptrofs.signed n))) + | _, _ => + Error(msg "Asmgen.transl_addressing") + end. + +Definition normalize_addrmode_32 (a: addrmode) := + match a with + | Addrmode base ofs (inl n) => + Addrmode base ofs (inl _ (Int.signed (Int.repr n))) + | Addrmode base ofs (inr _) => + a + end. + +Definition normalize_addrmode_64 (a: addrmode) := + match a with + | Addrmode base ofs (inl n) => + if Op.offset_in_range n + then (a, None) + else (Addrmode base ofs (inl _ 0), Some (Int64.repr n)) + | Addrmode base ofs (inr (id, delta)) => + if Op.ptroffset_in_range delta || negb Archi.ptr64 + then (a, None) + else (Addrmode base ofs (inr _ (id, Ptrofs.zero)), Some (Ptrofs.to_int64 delta)) + 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. + +Definition floatcomp32 (cmp: comparison) (r1 r2: freg) : instruction := + match cmp with + | Clt | Cle => Pcomiss_ff r2 r1 + | Ceq | Cne | Cgt | Cge => Pcomiss_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 (Pcmpl_rr r1 r2 :: k) + | Ccompu c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmpl_rr r1 r2 :: k) + | Ccompimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (if Int.eq_dec n Int.zero then Ptestl_rr r1 r1 :: k else Pcmpl_ri r1 n :: k) + | Ccompuimm c n, a1 :: nil => + do r1 <- ireg_of a1; OK (Pcmpl_ri r1 n :: k) + | Ccompl c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmpq_rr r1 r2 :: k) + | Ccomplu c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmpq_rr r1 r2 :: k) + | Ccomplimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (if Int64.eq_dec n Int64.zero then Ptestq_rr r1 r1 :: k else Pcmpq_ri r1 n :: k) + | Ccompluimm c n, a1 :: nil => + do r1 <- ireg_of a1; OK (Pcmpq_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) + | Ccompfs cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp32 cmp r1 r2 :: k) + | Cnotcompfs cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp32 cmp r1 r2 :: k) + | Cmaskzero n, a1 :: nil => + do r1 <- ireg_of a1; OK (Ptestl_ri r1 n :: k) + | Cmasknotzero n, a1 :: nil => + do r1 <- ireg_of a1; OK (Ptestl_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. + +Inductive extcond: Type := + | Cond_base (c: testcond) + | Cond_or (c1 c2: testcond) + | Cond_and (c1 c2: testcond). + +Definition testcond_for_condition (cond: condition) : extcond := + match cond with + | Ccomp c => Cond_base(testcond_for_signed_comparison c) + | Ccompu c => Cond_base(testcond_for_unsigned_comparison c) + | Ccompimm c n => Cond_base(testcond_for_signed_comparison c) + | Ccompuimm c n => Cond_base(testcond_for_unsigned_comparison c) + | Ccompl c => Cond_base(testcond_for_signed_comparison c) + | Ccomplu c => Cond_base(testcond_for_unsigned_comparison c) + | Ccomplimm c n => Cond_base(testcond_for_signed_comparison c) + | Ccompluimm c n => Cond_base(testcond_for_unsigned_comparison c) + | Ccompf c | Ccompfs c => + match c with + | Ceq => Cond_and Cond_np Cond_e + | Cne => Cond_or Cond_p Cond_ne + | Clt => Cond_base Cond_a + | Cle => Cond_base Cond_ae + | Cgt => Cond_base Cond_a + | Cge => Cond_base Cond_ae + end + | Cnotcompf c | Cnotcompfs c => + match c with + | Ceq => Cond_or Cond_p Cond_ne + | Cne => Cond_and Cond_np Cond_e + | Clt => Cond_base Cond_be + | Cle => Cond_base Cond_b + | Cgt => Cond_base Cond_be + | Cge => Cond_base Cond_b + end + | Cmaskzero n => Cond_base Cond_e + | Cmasknotzero n => Cond_base Cond_ne + end. + +(** Acting upon extended conditions. *) + +Definition mk_setcc_base (cond: extcond) (rd: ireg) (k: code) := + match cond with + | Cond_base c => + Psetcc c rd :: k + | Cond_and c1 c2 => + if ireg_eq rd RAX + then Psetcc c1 RAX :: Psetcc c2 RCX :: Pandl_rr RAX RCX :: k + else Psetcc c1 RAX :: Psetcc c2 rd :: Pandl_rr rd RAX :: k + | Cond_or c1 c2 => + if ireg_eq rd RAX + then Psetcc c1 RAX :: Psetcc c2 RCX :: Porl_rr RAX RCX :: k + else Psetcc c1 RAX :: Psetcc c2 rd :: Porl_rr rd RAX :: k + end. + +Definition mk_setcc (cond: extcond) (rd: ireg) (k: code) := + if Archi.ptr64 || low_ireg rd + then mk_setcc_base cond rd k + else mk_setcc_base cond RAX (Pmov_rr rd RAX :: k). + +Definition mk_jcc (cond: extcond) (lbl: label) (k: code) := + match cond with + | Cond_base c => Pjcc c lbl :: k + | Cond_and c1 c2 => Pjcc2 c1 c2 lbl :: k + | Cond_or c1 c2 => Pjcc c1 lbl :: Pjcc c2 lbl :: k + end. + +Definition negate_testcond (c: testcond) : testcond := + match c with + | Cond_e => Cond_ne | Cond_ne => Cond_e + | Cond_b => Cond_ae | Cond_be => Cond_a + | Cond_ae => Cond_b | Cond_a => Cond_be + | Cond_l => Cond_ge | Cond_le => Cond_g + | Cond_ge => Cond_l | Cond_g => Cond_le + | Cond_p => Cond_np | Cond_np => Cond_p + end. + +Definition mk_sel (cond: extcond) (rd r2: ireg) (k: code) := + match cond with + | Cond_base c => + OK (Pcmov (negate_testcond c) rd r2 :: k) + | Cond_and c1 c2 => + OK (Pcmov (negate_testcond c1) rd r2 :: + Pcmov (negate_testcond c2) rd r2 :: k) + | Cond_or c1 c2 => + Error (msg "Asmgen.mk_sel") (**r should never happen, see [SelectOp.select] *) + end. + +Definition transl_sel + (cond: condition) (args: list mreg) (rd r2: ireg) (k: code) : res code := + if ireg_eq rd r2 then + OK (Pmov_rr rd r2 :: k) (* must generate one instruction... *) + else + do k1 <- mk_sel (testcond_for_condition cond) rd r2 k; + transl_cond cond args k1. + +(** 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 ((if Int.eq_dec n Int.zero then Pxorl_r r else Pmovl_ri r n) :: k) + | Olongconst n, nil => + do r <- ireg_of res; + OK ((if Int64.eq_dec n Int64.zero then Pxorq_r r else Pmovq_ri r n) :: k) + | Ofloatconst f, nil => + do r <- freg_of res; + OK ((if Float.eq_dec f Float.zero then Pxorpd_f r else Pmovsd_fi r f) :: k) + | Osingleconst f, nil => + do r <- freg_of res; + OK ((if Float32.eq_dec f Float32.zero then Pxorps_f r else Pmovss_fi r f) :: k) + | Oindirectsymbol id, nil => + do r <- ireg_of res; + OK (Pmov_rs r id :: 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; OK (Pmovsw_rr r r1 :: k) + | Ocast16unsigned, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pmovzw_rr r r1 :: k) + | Oneg, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pnegl r :: k) + | Osub, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Psubl_rr r r2 :: k) + | Omul, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pimull_rr r r2 :: k) + | Omulimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pimull_ri r n :: k) + | Omulhs, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq res DX); + do r2 <- ireg_of a2; OK (Pimull_r r2 :: k) + | Omulhu, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq res DX); + do r2 <- ireg_of a2; OK (Pmull_r r2 :: k) + | Odiv, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res AX); + OK(Pcltd :: Pidivl RCX :: k) + | Odivu, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res AX); + OK(Pxorl_r RDX :: Pdivl RCX :: k) + | Omod, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res DX); + OK(Pcltd :: Pidivl RCX :: k) + | Omodu, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res DX); + OK(Pxorl_r RDX :: Pdivl RCX :: k) + | Oand, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pandl_rr r r2 :: k) + | Oandimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pandl_ri r n :: k) + | Oor, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Porl_rr r r2 :: k) + | Oorimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Porl_ri r n :: k) + | Oxor, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pxorl_rr r r2 :: k) + | Oxorimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pxorl_ri r n :: k) + | Onot, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pnotl r :: k) + | Oshl, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + assertion (mreg_eq a2 CX); + do r <- ireg_of res; OK (Psall_rcl r :: k) + | Oshlimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Psall_ri r n :: k) + | Oshr, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + assertion (mreg_eq a2 CX); + do r <- ireg_of res; OK (Psarl_rcl r :: k) + | Oshrimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Psarl_ri r n :: k) + | Oshru, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + assertion (mreg_eq a2 CX); + do r <- ireg_of res; OK (Pshrl_rcl r :: k) + | Oshruimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pshrl_ri r n :: k) + | Oshrximm n, a1 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq res AX); + mk_shrximm n k + | Ororimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Prorl_ri r n :: k) + | Oshldimm n, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pshld_ri r r2 n :: k) + | Olea addr, _ => + do am <- transl_addressing addr args; do r <- ireg_of res; + OK (Pleal r (normalize_addrmode_32 am) :: k) +(* 64-bit integer operations *) + | Olowlong, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pmovls_rr r :: k) + | Ocast32signed, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pmovsl_rr r r1 :: k) + | Ocast32unsigned, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pmovzl_rr r r1 :: k) + | Onegl, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pnegq r :: k) + | Oaddlimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Paddq_ri r n :: k) + | Osubl, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Psubq_rr r r2 :: k) + | Omull, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pimulq_rr r r2 :: k) + | Omullimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pimulq_ri r n :: k) + | Omullhs, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq res DX); + do r2 <- ireg_of a2; OK (Pimulq_r r2 :: k) + | Omullhu, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq res DX); + do r2 <- ireg_of a2; OK (Pmulq_r r2 :: k) + | Odivl, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res AX); + OK(Pcqto :: Pidivq RCX :: k) + | Odivlu, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res AX); + OK(Pxorq_r RDX :: Pdivq RCX :: k) + | Omodl, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res DX); + OK(Pcqto :: Pidivq RCX :: k) + | Omodlu, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res DX); + OK(Pxorq_r RDX :: Pdivq RCX :: k) + | Oandl, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pandq_rr r r2 :: k) + | Oandlimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pandq_ri r n :: k) + | Oorl, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Porq_rr r r2 :: k) + | Oorlimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Porq_ri r n :: k) + | Oxorl, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pxorq_rr r r2 :: k) + | Oxorlimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pxorq_ri r n :: k) + | Onotl, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pnotq r :: k) + | Oshll, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + assertion (mreg_eq a2 CX); + do r <- ireg_of res; OK (Psalq_rcl r :: k) + | Oshllimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Psalq_ri r n :: k) + | Oshrl, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + assertion (mreg_eq a2 CX); + do r <- ireg_of res; OK (Psarq_rcl r :: k) + | Oshrlimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Psarq_ri r n :: k) + | Oshrxlimm n, a1 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq res AX); + mk_shrxlimm n k + | Oshrlu, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + assertion (mreg_eq a2 CX); + do r <- ireg_of res; OK (Pshrq_rcl r :: k) + | Oshrluimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pshrq_ri r n :: k) + | Ororlimm n, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Prorq_ri r n :: k) + | Oleal addr, _ => + do am <- transl_addressing addr args; do r <- ireg_of res; + OK (match normalize_addrmode_64 am with + | (am', None) => Pleaq r am' :: k + | (am', Some delta) => Pleaq r am' :: Paddq_ri r delta :: k + end) +(**) + | Onegf, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- freg_of res; OK (Pnegd r :: k) + | Oabsf, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- freg_of res; OK (Pabsd r :: k) + | Oaddf, a1 :: a2 :: nil => + 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 => + 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 => + 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 => + assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Pdivd_ff r r2 :: k) + | Onegfs, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- freg_of res; OK (Pnegs r :: k) + | Oabsfs, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- freg_of res; OK (Pabss r :: k) + | Oaddfs, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Padds_ff r r2 :: k) + | Osubfs, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Psubs_ff r r2 :: k) + | Omulfs, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Pmuls_ff r r2 :: k) + | Odivfs, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Pdivs_ff r r2 :: k) + | Osingleoffloat, a1 :: nil => + do r <- freg_of res; do r1 <- freg_of a1; OK (Pcvtsd2ss_ff r r1 :: k) + | Ofloatofsingle, a1 :: nil => + do r <- freg_of res; do r1 <- freg_of a1; OK (Pcvtss2sd_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) + | Ointofsingle, a1 :: nil => + do r <- ireg_of res; do r1 <- freg_of a1; OK (Pcvttss2si_rf r r1 :: k) + | Osingleofint, a1 :: nil => + do r <- freg_of res; do r1 <- ireg_of a1; OK (Pcvtsi2ss_fr r r1 :: k) + | Olongoffloat, a1 :: nil => + do r <- ireg_of res; do r1 <- freg_of a1; OK (Pcvttsd2sl_rf r r1 :: k) + | Ofloatoflong, a1 :: nil => + do r <- freg_of res; do r1 <- ireg_of a1; OK (Pcvtsl2sd_fr r r1 :: k) + | Olongofsingle, a1 :: nil => + do r <- ireg_of res; do r1 <- freg_of a1; OK (Pcvttss2sl_rf r r1 :: k) + | Osingleoflong, a1 :: nil => + do r <- freg_of res; do r1 <- ireg_of a1; OK (Pcvtsl2ss_fr r r1 :: k) + | Ocmp c, args => + do r <- ireg_of res; + transl_cond c args (mk_setcc (testcond_for_condition c) r k) + | Osel c ty, a1 :: a2 :: args => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; + transl_sel c args r r2 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(Pmovl_rm r am :: k) + | Mint64 => + do r <- ireg_of dest; OK(Pmovq_rm r am :: k) + | Mfloat32 => + do r <- freg_of dest; OK(Pmovss_fm r am :: k) + | Mfloat64 => + do r <- freg_of dest; OK(Pmovsd_fm r am :: k) + | _ => + Error (msg "Asmgen.transl_load") + 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_storebyte am r k + | Mint16unsigned | Mint16signed => + do r <- ireg_of src; OK(Pmovw_mr am r :: k) + | Mint32 => + do r <- ireg_of src; OK(Pmovl_mr am r :: k) + | Mint64 => + do r <- ireg_of src; OK(Pmovq_mr am r :: k) + | Mfloat32 => + do r <- freg_of src; OK(Pmovss_mf am r :: k) + | Mfloat64 => + do r <- freg_of src; OK(Pmovsd_mf am r :: k) + | _ => + Error (msg "Asmgen.transl_store") + end. + +(** Translation of a Mach instruction. *) + +Definition transl_instr (f: Mach.function) (i: Mach.instruction) + (ax_is_parent: bool) (k: code) := + match i with + | Mgetstack ofs ty dst => + loadind RSP ofs ty dst k + | Msetstack src ofs ty => + storeind src RSP ofs ty k + | Mgetparam ofs ty dst => + if ax_is_parent then + loadind RAX ofs ty dst k + else + (do k1 <- loadind RAX ofs ty dst k; + loadind RSP f.(fn_link_ofs) Tptr AX 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 sig :: k) + | Mcall sig (inr symb) => + OK (Pcall_s symb sig :: k) + | Mtailcall sig (inl reg) => + do r <- ireg_of reg; + OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + Pjmp_r r sig :: k) + | Mtailcall sig (inr symb) => + OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + Pjmp_s symb sig :: k) + | Mlabel lbl => + OK(Plabel lbl :: k) + | Mgoto lbl => + OK(Pjmp_l lbl :: k) + | Mcond cond args lbl => + transl_cond cond args (mk_jcc (testcond_for_condition cond) lbl k) + | Mjumptable arg tbl => + do r <- ireg_of arg; OK (Pjmptbl r tbl :: k) + | Mreturn => + OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + Pret :: k) + | Mbuiltin ef args res => + OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k) + end. + +(** Translation of a code sequence *) + +Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool := + match i with + | Msetstack src ofs ty => before + | Mgetparam ofs ty dst => negb (mreg_eq dst AX) + | _ => false + end. + +(** This is the naive definition that we no longer use because it + is not tail-recursive. It is kept as specification. *) + +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (axp: bool) := + match il with + | nil => OK nil + | i1 :: il' => + do k <- transl_code f il' (it1_is_parent axp i1); + transl_instr f i1 axp k + end. + +(** This is an equivalent definition in continuation-passing style + that runs in constant stack space. *) + +Fixpoint transl_code_rec (f: Mach.function) (il: list Mach.instruction) + (axp: bool) (k: code -> res code) := + match il with + | nil => k nil + | i1 :: il' => + transl_code_rec f il' (it1_is_parent axp i1) + (fun c1 => do c2 <- transl_instr f i1 axp c1; k c2) + end. + +Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (axp: bool) := + transl_code_rec f il axp (fun c => OK c). + +(** 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 transl_function (f: Mach.function) := + do c <- transl_code' f f.(Mach.fn_code) true; + OK (mkfunction f.(Mach.fn_sig) + (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c)). + +Definition transf_function (f: Mach.function) : res Asm.function := + do tf <- transl_function f; + if zlt Ptrofs.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. + +Definition transf_program (p: Mach.program) : res Asm.program := + transform_partial_program transf_fundef p. + |