diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-14 15:41:26 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-14 15:41:26 +0000 |
commit | 5aea6849eed83009e300b04ef17786643ead9cbc (patch) | |
tree | eb9a329ce46a7ddc568a2fba7692b8eaea1e618f /ia32/Asmgen.v | |
parent | fd0f28867db2f183216b27d7030265ae9e887586 (diff) | |
download | compcert-5aea6849eed83009e300b04ef17786643ead9cbc.tar.gz compcert-5aea6849eed83009e300b04ef17786643ead9cbc.zip |
Locations.v: add Loc.diff_dec.
ia32: lift restriction that 1st arg of ops cannot be ECX
(could be useful for a future, better reloading strategy)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1711 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asmgen.v')
-rw-r--r-- | ia32/Asmgen.v | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 452f2e7c..4c1167b5 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -33,8 +33,6 @@ Open Local Scope error_monad_scope. - Argument and result registers are of the correct type. - For two-address instructions, the result and the first argument are in the same register. (True by construction in [RTLgen], and preserved by [Reload].) -- The first argument register is never [ECX] (a.k.a. [IT2]) nor [XMM7] - (a.k.a [FT2]). - The top of the floating-point stack ([ST0], a.k.a. [FP0]) can only appear in [mov] instructions, but never in arithmetic instructions. @@ -64,10 +62,24 @@ Definition mk_shift (shift_instr: ireg -> instruction) (r1 r2: ireg) (k: code) : res code := if ireg_eq r2 ECX then OK (shift_instr r1 :: k) + else if ireg_eq r1 ECX then + OK (Pxchg_rr r2 ECX :: shift_instr r2 :: Pxchg_rr r2 ECX :: k) else - do x <- assertion (negb (ireg_eq r1 ECX)); OK (Pmov_rr ECX r2 :: shift_instr r1 :: k). +Definition mk_mov2 (src1 dst1 src2 dst2: ireg) (k: code) : code := + if ireg_eq src1 dst1 then + Pmov_rr dst2 src2 :: k + else if ireg_eq src2 dst2 then + Pmov_rr dst1 src1 :: k + else if ireg_eq src2 dst1 then + if ireg_eq src1 dst2 then + Pxchg_rr src1 src2 :: k + else + Pmov_rr dst2 src2 :: Pmov_rr dst1 src1 :: k + else + Pmov_rr dst1 src1 :: Pmov_rr dst2 src2 :: k. + Definition mk_div (div_instr: ireg -> instruction) (r1 r2: ireg) (k: code) : res code := if ireg_eq r1 EAX then @@ -76,15 +88,9 @@ Definition mk_div (div_instr: ireg -> instruction) else OK (div_instr r2 :: k) else - do x <- assertion (negb (ireg_eq r1 ECX)); - if ireg_eq r2 EAX then - OK (Pmov_rr ECX EAX :: Pmov_rr EAX r1 :: - div_instr ECX :: - Pmov_rr r1 EAX :: Pmov_rr EAX ECX :: k) - else - OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX r2 :: Pmov_rr EAX r1 :: - div_instr ECX :: - Pmov_rr r2 ECX :: Pmov_rr r1 EAX :: Pmovd_rf EAX XMM7 :: k). + OK (Pmovd_fr XMM7 EAX :: + mk_mov2 r1 EAX r2 ECX + (div_instr ECX :: Pmov_rr r1 EAX :: Pmovd_rf EAX XMM7 :: k)). Definition mk_mod (div_instr: ireg -> instruction) (r1 r2: ireg) (k: code) : res code := @@ -94,22 +100,16 @@ Definition mk_mod (div_instr: ireg -> instruction) else OK (div_instr r2 :: Pmov_rr EAX EDX :: k) else - do x <- assertion (negb (ireg_eq r1 ECX)); - if ireg_eq r2 EDX then - OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX EDX :: Pmov_rr EAX r1 :: - div_instr ECX :: - Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k) - else - OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX r2 :: Pmov_rr EAX r1 :: - div_instr ECX :: - Pmov_rr r2 ECX :: Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k). + OK (Pmovd_fr XMM7 EAX :: + mk_mov2 r1 EAX r2 ECX + (div_instr ECX :: Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k)). Definition mk_shrximm (r: ireg) (n: int) (k: code) : res code := - do x <- assertion (negb (ireg_eq r ECX)); + let tmp := if ireg_eq r ECX then EDX else ECX in let p := Int.sub (Int.shl Int.one n) Int.one in OK (Ptest_rr r r :: - Plea ECX (Addrmode (Some r) None (inl _ p)) :: - Pcmov Cond_l r ECX :: + Plea tmp (Addrmode (Some r) None (inl _ p)) :: + Pcmov Cond_l r tmp :: Psar_ri r n :: k). Definition low_ireg (r: ireg) : bool := |