From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asmgen.v | 43 +++++++++++++++++++++++++++---------------- 1 file changed, 27 insertions(+), 16 deletions(-) (limited to 'ia32/Asmgen.v') diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index f53ec81..0e14dee 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -215,10 +215,10 @@ Definition transl_cond | Ccompu c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmp_rr r1 r2 :: k) | Ccompimm c n, a1 :: nil => - do r1 <- ireg_of a1; OK (Pcmp_ri r1 n :: k) - | Ccompuimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if Int.eq_dec n Int.zero then Ptest_rr r1 r1 :: k else Pcmp_ri r1 n :: k) + | Ccompuimm c n, a1 :: nil => + do r1 <- ireg_of a1; OK (Pcmp_ri r1 n :: k) | Ccompf cmp, a1 :: a2 :: nil => do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k) | Cnotcompf cmp, a1 :: a2 :: nil => @@ -443,15 +443,19 @@ Definition transl_store (chunk: memory_chunk) (** Translation of a Mach instruction. *) -Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := +Definition transl_instr (f: Mach.function) (i: Mach.instruction) + (edx_is_parent: bool) (k: code) := match i with | Mgetstack ofs ty dst => loadind ESP ofs ty dst k | Msetstack src ofs ty => storeind src ESP ofs ty k | Mgetparam ofs ty dst => - do k1 <- loadind EDX ofs ty dst k; - loadind ESP f.(fn_link_ofs) Tint IT1 k1 + if edx_is_parent then + loadind EDX ofs ty dst k + else + (do k1 <- loadind EDX ofs ty dst k; + loadind ESP f.(fn_link_ofs) Tint IT1 k1) | Mop op args res => transl_op op args res k | Mload chunk addr args dst => @@ -464,12 +468,10 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := OK (Pcall_s symb :: k) | Mtailcall sig (inl reg) => do r <- ireg_of reg; - OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) - f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: Pjmp_r r :: k) | Mtailcall sig (inr symb) => - OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) - f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: Pjmp_s symb :: k) | Mlabel lbl => OK(Plabel lbl :: k) @@ -480,17 +482,27 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := | Mjumptable arg tbl => do r <- ireg_of arg; OK (Pjmptbl r tbl :: k) | Mreturn => - OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) - f.(fn_retaddr_ofs) f.(fn_link_ofs) :: + 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) end. -Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) := +(** Translation of a code sequence *) + +Definition edx_preserved (before: bool) (i: Mach.instruction) : bool := + match i with + | Msetstack src ofs ty => before + | Mgetparam ofs ty dst => negb (mreg_eq dst IT1) + | _ => false + end. + +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (edx_is_parent: bool) := match il with | nil => OK nil - | i1 :: il' => do k <- transl_code f il'; transl_instr f i1 k + | i1 :: il' => + do k <- transl_code f il' (edx_preserved edx_is_parent i1); + transl_instr f i1 edx_is_parent k end. (** Translation of a whole function. Note that we must check @@ -499,10 +511,9 @@ Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) := around, leading to incorrect executions. *) Definition transf_function (f: Mach.function) : res Asm.code := - do c <- transl_code f f.(fn_code); + do c <- transl_code f f.(fn_code) true; if zlt (list_length_z c) Int.max_unsigned - then OK (Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) - f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c) + then OK (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c) else Error (msg "code size exceeded"). Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := -- cgit v1.2.3