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 /ia32/Asmgen.v | |
| parent | 9fb435abe98f358b1dde5de6604663a176634e53 (diff) | |
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 'ia32/Asmgen.v')
| -rw-r--r-- | ia32/Asmgen.v | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 0410057..740dff8 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -496,16 +496,16 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | 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 :: k) + do r <- ireg_of reg; OK (Pcall_r r sig :: k) | Mcall sig (inr symb) => - OK (Pcall_s symb :: k) + 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 :: k) + 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 :: k) + Pjmp_s symb sig :: k) | Mlabel lbl => OK(Plabel lbl :: k) | Mgoto lbl => @@ -563,11 +563,16 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions. *) -Definition transf_function (f: Mach.function) : res Asm.code := +Definition transl_function (f: Mach.function) := do c <- transl_code' f f.(Mach.fn_code) true; - if zlt (list_length_z c) Int.max_unsigned - then OK (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c) - else Error (msg "code size exceeded"). + 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 Int.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. |