From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asmgen.v | 101 +++++++++++++++++++++++++++++++++++----------------------- 1 file changed, 62 insertions(+), 39 deletions(-) (limited to 'ia32/Asmgen.v') diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index f92d72c..9c0a76e 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -50,8 +50,6 @@ 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. @@ -90,42 +88,30 @@ Definition mk_smallstore (sto: addrmode -> ireg ->instruction) else OK (Pmov_rr EAX rs :: sto addr EAX :: k). -(** Accessing slots in the stack frame. *) +(** 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 - | Tsingle => - do r <- freg_of dst; - OK (Pcvtss2sd_fm r (Addrmode (Some base) None (inl _ ofs)) :: k) - | Tlong => - Error (msg "Asmgen.loadind") + match ty, preg_of dst with + | Tint, IR r => OK (Pmov_rm r (Addrmode (Some base) None (inl _ ofs)) :: k) + | Tsingle, FR r => OK (Pmovss_fm r (Addrmode (Some base) None (inl _ ofs)) :: k) + | Tsingle, ST0 => OK (Pflds_m (Addrmode (Some base) None (inl _ ofs)) :: k) + | Tfloat, FR r => OK (Pmovsd_fm r (Addrmode (Some base) None (inl _ ofs)) :: k) + | Tfloat, ST0 => OK (Pfldl_m (Addrmode (Some base) None (inl _ ofs)) :: k) + | Tany32, IR r => OK (Pmov_rm_a r (Addrmode (Some base) None (inl _ ofs)) :: k) + | Tany64, FR r => OK (Pmovsd_fm_a r (Addrmode (Some base) None (inl _ ofs)) :: k) + | _, _ => Error (msg "Asmgen.loadind") 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 - | Tsingle => - do r <- freg_of src; - OK (Pcvtsd2ss_mf (Addrmode (Some base) None (inl _ ofs)) r :: k) - | Tlong => - Error (msg "Asmgen.storeind") + match ty, preg_of src with + | Tint, IR r => OK (Pmov_mr (Addrmode (Some base) None (inl _ ofs)) r :: k) + | Tsingle, FR r => OK (Pmovss_mf (Addrmode (Some base) None (inl _ ofs)) r :: k) + | Tsingle, ST0 => OK (Pfstps_m (Addrmode (Some base) None (inl _ ofs)) :: k) + | Tfloat, FR r => OK (Pmovsd_mf (Addrmode (Some base) None (inl _ ofs)) r :: k) + | Tfloat, ST0 => OK (Pfstpl_m (Addrmode (Some base) None (inl _ ofs)) :: k) + | Tany32, IR r => OK (Pmov_mr_a (Addrmode (Some base) None (inl _ ofs)) r :: k) + | Tany64, FR r => OK (Pmovsd_mf_a (Addrmode (Some base) None (inl _ ofs)) r :: k) + | _, _ => Error (msg "Asmgen.storeind") end. (** Translation of addressing modes *) @@ -163,6 +149,12 @@ Definition floatcomp (cmp: comparison) (r1 r2: freg) : instruction := | 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. *) @@ -183,6 +175,10 @@ Definition transl_cond 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 (Ptest_ri r1 n :: k) | Cmasknotzero n, a1 :: nil => @@ -224,7 +220,7 @@ Definition testcond_for_condition (cond: condition) : extcond := | 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) - | Ccompf c => + | Ccompf c | Ccompfs c => match c with | Ceq => Cond_and Cond_np Cond_e | Cne => Cond_or Cond_p Cond_ne @@ -233,7 +229,7 @@ Definition testcond_for_condition (cond: condition) : extcond := | Cgt => Cond_base Cond_a | Cge => Cond_base Cond_ae end - | Cnotcompf c => + | Cnotcompf c | Cnotcompfs c => match c with | Ceq => Cond_or Cond_p Cond_ne | Cne => Cond_and Cond_np Cond_e @@ -288,6 +284,9 @@ Definition transl_op | 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_ra r id :: k) @@ -412,12 +411,36 @@ Definition transl_op | 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) | Ocmp c, args => do r <- ireg_of res; transl_cond c args (mk_setcc (testcond_for_condition c) r k) @@ -443,10 +466,10 @@ Definition transl_load (chunk: memory_chunk) | Mint32 => do r <- ireg_of dest; OK(Pmov_rm r am :: k) | Mfloat32 => - do r <- freg_of dest; OK(Pcvtss2sd_fm r am :: k) + do r <- freg_of dest; OK(Pmovss_fm r am :: k) | Mfloat64 => do r <- freg_of dest; OK(Pmovsd_fm r am :: k) - | Mint64 => + | _ => Error (msg "Asmgen.transl_load") end. @@ -462,10 +485,10 @@ Definition transl_store (chunk: memory_chunk) | Mint32 => do r <- ireg_of src; OK(Pmov_mr am r :: k) | Mfloat32 => - do r <- freg_of src; OK(Pcvtsd2ss_mf am r :: k) + do r <- freg_of src; OK(Pmovss_mf am r :: k) | Mfloat64 => do r <- freg_of src; OK(Pmovsd_mf am r :: k) - | Mint64 => + | _ => Error (msg "Asmgen.transl_store") end. -- cgit v1.2.3