diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-10 07:49:49 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-10 07:49:49 +0000 |
commit | 637334181f54154f6c5598073c60f3f2c3ab5e87 (patch) | |
tree | 8789da87f5c26ecf09eda0d38ad44d58df60ad78 /ia32/Asmgen.v | |
parent | c9acadca7c8d5d29dd57b9acba99369067f93ae1 (diff) |
Improvements for int8 and int16 stores
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1507 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asmgen.v')
-rw-r--r-- | ia32/Asmgen.v | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 70929ff..f53ec81 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -124,13 +124,21 @@ Definition mk_intconv (mk: ireg -> ireg -> instruction) (rd rs: ireg) (k: code) else OK (Pmov_rr EDX rs :: mk rd EDX :: k). +Definition addressing_mentions (addr: addrmode) (r: ireg) : bool := + match addr with Addrmode base displ const => + match base with Some r' => ireg_eq r r' | None => false end + || match displ with Some(r', sc) => ireg_eq r r' | None => false end + end. + Definition mk_smallstore (sto: addrmode -> ireg ->instruction) (addr: addrmode) (rs: ireg) (k: code) := if low_ireg rs then OK (sto addr rs :: k) - else + else if addressing_mentions addr ECX then OK (Plea ECX addr :: Pmov_rr EDX rs :: - sto (Addrmode (Some ECX) None (inl _ Int.zero)) EDX :: k). + sto (Addrmode (Some ECX) None (inl _ Int.zero)) EDX :: k) + else + OK (Pmov_rr ECX rs :: sto addr ECX :: k). (** Accessing slots in the stack frame. *) @@ -424,7 +432,7 @@ Definition transl_store (chunk: memory_chunk) | Mint8unsigned | Mint8signed => do r <- ireg_of src; mk_smallstore Pmovb_mr am r k | Mint16unsigned | Mint16signed => - do r <- ireg_of src; mk_smallstore Pmovw_mr am r k + do r <- ireg_of src; OK(Pmovw_mr am r :: k) | Mint32 => do r <- ireg_of src; OK(Pmov_mr am r :: k) | Mfloat32 => |