diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-30 09:54:35 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-30 09:54:35 +0000 |
commit | 1fe68ad575178f7d8a775906947d2fed94d40976 (patch) | |
tree | 3bb4b2d1b101f66bcb6f84bd36ce8e334082f7ea /arm/Asmgen.v | |
parent | 9b45e1d24a337e3f0047bf5056315169d4203b49 (diff) |
ARM codegen ported to new ABI + VFD floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/Asmgen.v')
-rw-r--r-- | arm/Asmgen.v | 75 |
1 files changed, 40 insertions, 35 deletions
diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 91a636b..4d36f91 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -152,9 +152,9 @@ Definition transl_cond else loadimm IR14 n (Pcmp (ireg_of a1) (SOreg IR14) :: k) | Ccompf cmp, a1 :: a2 :: nil => - Pcmf (freg_of a1) (freg_of a2) :: k + Pfcmpd (freg_of a1) (freg_of a2) :: k | Cnotcompf cmp, a1 :: a2 :: nil => - Pcmf (freg_of a1) (freg_of a2) :: k + Pfcmpd (freg_of a1) (freg_of a2) :: k | _, _ => k (**r never happens for well-typed code *) end. @@ -220,12 +220,12 @@ Definition transl_op | Omove, a1 :: nil => match mreg_type a1 with | Tint => Pmov (ireg_of r) (SOreg (ireg_of a1)) :: k - | Tfloat => Pmvfd (freg_of r) (freg_of a1) :: k + | Tfloat => Pfcpyd (freg_of r) (freg_of a1) :: k end | Ointconst n, nil => loadimm (ireg_of r) n k | Ofloatconst f, nil => - Plifd (freg_of r) f :: k + Pflid (freg_of r) f :: k | Oaddrsymbol s ofs, nil => Ploadsymbol (ireg_of r) s ofs :: k | Oaddrstack n, nil => @@ -304,23 +304,27 @@ Definition transl_op (Pmovc CRge IR14 (SOreg (ireg_of a1)) :: Pmov (ireg_of r) (SOasrimm IR14 n) :: k) | Onegf, a1 :: nil => - Pmnfd (freg_of r) (freg_of a1) :: k + Pfnegd (freg_of r) (freg_of a1) :: k | Oabsf, a1 :: nil => - Pabsd (freg_of r) (freg_of a1) :: k + Pfabsd (freg_of r) (freg_of a1) :: k | Oaddf, a1 :: a2 :: nil => - Padfd (freg_of r) (freg_of a1) (freg_of a2) :: k + Pfaddd (freg_of r) (freg_of a1) (freg_of a2) :: k | Osubf, a1 :: a2 :: nil => - Psufd (freg_of r) (freg_of a1) (freg_of a2) :: k + Pfsubd (freg_of r) (freg_of a1) (freg_of a2) :: k | Omulf, a1 :: a2 :: nil => - Pmufd (freg_of r) (freg_of a1) (freg_of a2) :: k + Pfmuld (freg_of r) (freg_of a1) (freg_of a2) :: k | Odivf, a1 :: a2 :: nil => - Pdvfd (freg_of r) (freg_of a1) (freg_of a2) :: k + Pfdivd (freg_of r) (freg_of a1) (freg_of a2) :: k | Osingleoffloat, a1 :: nil => - Pmvfs (freg_of r) (freg_of a1) :: k + Pfcvtsd (freg_of r) (freg_of a1) :: k | Ointoffloat, a1 :: nil => - Pfixz (ireg_of r) (freg_of a1) :: k + Pftosizd (ireg_of r) (freg_of a1) :: k + | Ointuoffloat, a1 :: nil => + Pftouizd (ireg_of r) (freg_of a1) :: k | Ofloatofint, a1 :: nil => - Pfltd (freg_of r) (ireg_of a1) :: k + Pfsitod (freg_of r) (ireg_of a1) :: k + | Ofloatofintu, a1 :: nil => + Pfuitod (freg_of r) (ireg_of a1) :: k | Ocmp cmp, _ => transl_cond cmp args (Pmov (ireg_of r) (SOimm Int.zero) :: @@ -405,10 +409,10 @@ Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) := Definition loadind_float (base: ireg) (ofs: int) (dst: freg) (k: code) := if is_immed_mem_float ofs then - Pldfd dst base ofs :: k + Pfldd dst base ofs :: k else addimm IR14 base ofs - (Pldfd dst IR14 Int.zero :: k). + (Pfldd dst IR14 Int.zero :: k). Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := match ty with @@ -425,10 +429,10 @@ Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) := Definition storeind_float (src: freg) (base: ireg) (ofs: int) (k: code) := if is_immed_mem_float ofs then - Pstfd src base ofs :: k + Pfstd src base ofs :: k else addimm IR14 base ofs - (Pstfd src IR14 Int.zero :: k). + (Pfstd src IR14 Int.zero :: k). Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := match ty with @@ -461,7 +465,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := | Mint8signed => transl_load_store_int Pldrsb is_immed_mem_small dst addr args k | Mint8unsigned => - transl_load_store_int Pldrb is_immed_mem_small dst addr args k + 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 => @@ -469,16 +473,16 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := | Mint32 => transl_load_store_int Pldr is_immed_mem_word dst addr args k | Mfloat32 => - transl_load_store_float Pldfs is_immed_mem_float dst addr args k + transl_load_store_float Pflds is_immed_mem_float dst addr args k | Mfloat64 => - transl_load_store_float Pldfd is_immed_mem_float dst addr args k + transl_load_store_float Pfldd is_immed_mem_float dst addr args k end | 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_small src addr args k + 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 => @@ -486,20 +490,20 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := | Mint32 => transl_load_store_int Pstr is_immed_mem_word src addr args k | Mfloat32 => - transl_load_store_float Pstfs is_immed_mem_float src addr args k + transl_load_store_float Pfsts is_immed_mem_float src addr args k | Mfloat64 => - transl_load_store_float Pstfd is_immed_mem_float src addr args k + transl_load_store_float Pfstd is_immed_mem_float src addr args k end | Mcall sig (inl r) => - Pblreg (ireg_of r) :: k + Pblreg (ireg_of r) sig :: k | Mcall sig (inr symb) => - Pblsymb symb :: k + 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) :: k) + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg (ireg_of 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 :: k) + (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 | Mannot ef args => @@ -515,7 +519,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Pbtbl IR14 tbl :: k | Mreturn => loadind_int IR13 f.(fn_retaddr_ofs) IR14 - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: k) + (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) := @@ -527,9 +531,10 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) := around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) :: - transl_code f f.(fn_code). + 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 @@ -539,11 +544,11 @@ Fixpoint code_size (c: code) : Z := Open Local Scope string_scope. -Definition transf_function (f: Mach.function) : res Asm.code := - let c := transl_function f in - if zlt Int.max_unsigned (code_size 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 c. + else Errors.OK tf. Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := transf_partial_fundef transf_function f. |