From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asmgen.v | 191 ++++++++++++++++++++++++++-------------------------------- 1 file changed, 87 insertions(+), 104 deletions(-) (limited to 'ia32/Asmgen.v') diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 6e3ccf8..78f7d6e 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -17,6 +17,7 @@ Require Import Errors. Require Import AST. Require Import Integers. Require Import Floats. +Require Import Memdata. Require Import Op. Require Import Locations. Require Import Mach. @@ -54,59 +55,12 @@ Definition mk_mov (rd rs: preg) (k: code) : res code := | _, _ => 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 if ireg_eq r1 ECX then - OK (Pxchg_rr r2 ECX :: shift_instr r2 :: Pxchg_rr r2 ECX :: k) - else - OK (Pmov_rr ECX r2 :: shift_instr r1 :: k). - -Definition mk_mov2 (src1 dst1 src2 dst2: ireg) (k: code) : code := - if ireg_eq src1 dst1 then - Pmov_rr dst2 src2 :: k - else if ireg_eq src2 dst2 then - Pmov_rr dst1 src1 :: k - else if ireg_eq src2 dst1 then - if ireg_eq src1 dst2 then - Pxchg_rr src1 src2 :: k - else - Pmov_rr dst2 src2 :: Pmov_rr dst1 src1 :: k - else - Pmov_rr dst1 src1 :: Pmov_rr dst2 src2 :: 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 - OK (Pmovd_fr XMM7 EAX :: - mk_mov2 r1 EAX r2 ECX - (div_instr 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 - OK (Pmovd_fr XMM7 EAX :: - mk_mov2 r1 EAX r2 ECX - (div_instr ECX :: Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k)). - -Definition mk_shrximm (r: ireg) (n: int) (k: code) : res code := - let tmp := if ireg_eq r ECX then EDX else ECX in +Definition mk_shrximm (n: int) (k: code) : res code := let p := Int.sub (Int.shl Int.one n) Int.one in - OK (Ptest_rr r r :: - Plea tmp (Addrmode (Some r) None (inl _ p)) :: - Pcmov Cond_l r tmp :: - Psar_ri r n :: k). + OK (Ptest_rr EAX EAX :: + Plea ECX (Addrmode (Some EAX) None (inl _ p)) :: + Pcmov Cond_l EAX ECX :: + Psar_ri EAX n :: k). Definition low_ireg (r: ireg) : bool := match r with @@ -118,7 +72,7 @@ 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). + OK (Pmov_rr EAX rs :: mk rd EAX :: k). Definition addressing_mentions (addr: addrmode) (r: ireg) : bool := match addr with Addrmode base displ const => @@ -130,11 +84,11 @@ Definition mk_smallstore (sto: addrmode -> ireg ->instruction) (addr: addrmode) (rs: ireg) (k: code) := if low_ireg rs then OK (sto addr rs :: k) - else if addressing_mentions addr ECX then - OK (Plea ECX addr :: Pmov_rr EDX rs :: - sto (Addrmode (Some ECX) None (inl _ Int.zero)) EDX :: k) + else if addressing_mentions addr EAX then + OK (Plea ECX addr :: Pmov_rr EAX rs :: + sto (Addrmode (Some ECX) None (inl _ Int.zero)) EAX :: k) else - OK (Pmov_rr ECX rs :: sto addr ECX :: k). + OK (Pmov_rr EAX rs :: sto addr EAX :: k). (** Accessing slots in the stack frame. *) @@ -149,6 +103,8 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := | ST0 => OK (Pfld_m (Addrmode (Some base) None (inl _ ofs)) :: k) | _ => Error (msg "Asmgen.loadind") end + | Tlong => + Error (msg "Asmgen.loadind") end. Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := @@ -162,6 +118,8 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := | ST0 => OK (Pfstp_m (Addrmode (Some base) None (inl _ ofs)) :: k) | _ => Error (msg "Asmgen.loadind") end + | Tlong => + Error (msg "Asmgen.storeind") end. (** Translation of addressing modes *) @@ -284,19 +242,25 @@ Definition testcond_for_condition (cond: condition) : extcond := (** Acting upon extended conditions. *) -Definition mk_setcc (cond: extcond) (rd: ireg) (k: code) := +Definition mk_setcc_base (cond: extcond) (rd: ireg) (k: code) := match cond with - | Cond_base c => Psetcc c rd :: k + | Cond_base c => + Psetcc c rd :: k | Cond_and c1 c2 => - if ireg_eq rd EDX - then Psetcc c1 EDX :: Psetcc c2 ECX :: Pand_rr EDX ECX :: k - else Psetcc c1 EDX :: Psetcc c2 rd :: Pand_rr rd EDX :: k + if ireg_eq rd EAX + then Psetcc c1 EAX :: Psetcc c2 ECX :: Pand_rr EAX ECX :: k + else Psetcc c1 EAX :: Psetcc c2 rd :: Pand_rr rd EAX :: k | Cond_or c1 c2 => - if ireg_eq rd EDX - then Psetcc c1 EDX :: Psetcc c2 ECX :: Por_rr EDX ECX :: k - else Psetcc c1 EDX :: Psetcc c2 rd :: Por_rr rd EDX :: k + if ireg_eq rd EAX + then Psetcc c1 EAX :: Psetcc c2 ECX :: Por_rr EAX ECX :: k + else Psetcc c1 EAX :: Psetcc c2 rd :: Por_rr rd EAX :: k end. +Definition mk_setcc (cond: extcond) (rd: ireg) (k: code) := + if low_ireg rd + then mk_setcc_base cond rd k + else mk_setcc_base cond EAX (Pmov_rr rd EAX :: k). + Definition mk_jcc (cond: extcond) (lbl: label) (k: code) := match cond with | Cond_base c => Pjcc c lbl :: k @@ -330,91 +294,106 @@ Definition transl_op | 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); + 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); + 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); + 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); + 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 + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res AX); + OK(Pidiv ECX :: 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 + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res AX); + OK(Pdiv ECX :: 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 + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res DX); + OK(Pidiv ECX :: 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 + assertion (mreg_eq a1 AX); + assertion (mreg_eq a2 CX); + assertion (mreg_eq res DX); + OK(Pdiv ECX :: k) | Oand, a1 :: a2 :: nil => - do x <- assertion (mreg_eq a1 res); + 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); + 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); + 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); + 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); + 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); + 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 + assertion (mreg_eq a1 res); + assertion (mreg_eq a2 CX); + do r <- ireg_of res; OK (Psal_rcl r :: k) | Oshlimm n, a1 :: nil => - do x <- assertion (mreg_eq a1 res); + 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 + assertion (mreg_eq a1 res); + assertion (mreg_eq a2 CX); + do r <- ireg_of res; OK (Psar_rcl r :: k) | Oshrimm n, a1 :: nil => - do x <- assertion (mreg_eq a1 res); + 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 + assertion (mreg_eq a1 res); + assertion (mreg_eq a2 CX); + do r <- ireg_of res; OK (Pshr_rcl r :: k) | Oshruimm n, a1 :: nil => - do x <- assertion (mreg_eq a1 res); + 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 + assertion (mreg_eq a1 AX); + assertion (mreg_eq res AX); + mk_shrximm n k | Ororimm n, a1 :: nil => - do x <- assertion (mreg_eq a1 res); + assertion (mreg_eq a1 res); do r <- ireg_of res; OK (Pror_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 (Plea r am :: k) | Onegf, a1 :: nil => - do x <- assertion (mreg_eq a1 res); + assertion (mreg_eq a1 res); do r <- freg_of res; OK (Pnegd r :: k) | Oabsf, a1 :: nil => - do x <- assertion (mreg_eq a1 res); + 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); + 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); + 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); + 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); + 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) @@ -450,6 +429,8 @@ Definition transl_load (chunk: memory_chunk) do r <- freg_of dest; OK(Pcvtss2sd_fm r am :: k) | Mfloat64 | Mfloat64al32 => do r <- freg_of dest; OK(Pmovsd_fm r am :: k) + | Mint64 => + Error (msg "Asmgen.transl_load") end. Definition transl_store (chunk: memory_chunk) @@ -467,6 +448,8 @@ Definition transl_store (chunk: memory_chunk) do r <- freg_of src; OK(Pcvtsd2ss_mf am r :: k) | Mfloat64 | Mfloat64al32 => do r <- freg_of src; OK(Pmovsd_mf am r :: k) + | Mint64 => + Error (msg "Asmgen.transl_store") end. (** Translation of arguments to annotations *) @@ -491,7 +474,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) loadind EDX ofs ty dst k else (do k1 <- loadind EDX ofs ty dst k; - loadind ESP f.(fn_link_ofs) Tint IT1 k1) + loadind ESP f.(fn_link_ofs) Tint DX k1) | Mop op args res => transl_op op args res k | Mload chunk addr args dst => @@ -521,7 +504,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) OK (Pfreeframe 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) + OK (Pbuiltin ef (List.map preg_of args) (List.map preg_of res) :: k) | Mannot ef args => OK (Pannot ef (map transl_annot_param args) :: k) end. @@ -531,7 +514,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) 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 IT1) + | Mgetparam ofs ty dst => negb (mreg_eq dst DX) | _ => false end. -- cgit v1.2.3