diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-26 15:46:54 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-26 15:46:54 +0000 |
| commit | ad12162ff1f0d50c43afefc45e1593f27f197402 (patch) | |
| tree | f77430a75e0a4bf12a64b8ee676d40c88ede1041 /powerpc/Asmgen.v | |
| parent | 9fb435abe98f358b1dde5de6604663a176634e53 (diff) | |
| download | compcert-kvx-ad12162ff1f0d50c43afefc45e1593f27f197402.tar.gz compcert-kvx-ad12162ff1f0d50c43afefc45e1593f27f197402.zip | |
Future-proofing: keep signature information in IA32 and PowerPC Asm, just like we already do in ARM Asm.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asmgen.v')
| -rw-r--r-- | powerpc/Asmgen.v | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index b3f07224..39c0d1b6 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -623,21 +623,21 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mstore chunk addr args src => transl_store chunk addr args src k | Mcall sig (inl r) => - do r1 <- ireg_of r; OK (Pmtctr r1 :: Pbctrl :: k) + do r1 <- ireg_of r; OK (Pmtctr r1 :: Pbctrl sig :: k) | Mcall sig (inr symb) => - OK (Pbl symb :: k) + OK (Pbl symb sig :: k) | Mtailcall sig (inl r) => do r1 <- ireg_of r; OK (Pmtctr r1 :: Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR0 :: Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pbctr :: k) + Pbctr sig :: k) | Mtailcall sig (inr symb) => OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR0 :: Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pbs symb :: k) + Pbs symb sig :: k) | Mbuiltin ef args res => OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k) | Mannot ef args => @@ -703,15 +703,16 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo Definition transl_function (f: Mach.function) := do c <- transl_code' f f.(Mach.fn_code) false; - OK (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pmflr GPR0 :: - Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: c). - -Definition transf_function (f: Mach.function) : res Asm.code := - do c <- transl_function f; - if zlt Int.max_unsigned (list_length_z c) + OK (mkfunction f.(Mach.fn_sig) + (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pmflr GPR0 :: + Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: c)). + +Definition transf_function (f: Mach.function) : res Asm.function := + do tf <- transl_function f; + if zlt Int.max_unsigned (list_length_z tf.(fn_code)) then Error (msg "code size exceeded") - else OK c. + else OK tf. Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := transf_partial_fundef transf_function f. |