diff options
Diffstat (limited to 'powerpc/Asmgen.v')
| -rw-r--r-- | powerpc/Asmgen.v | 67 |
1 files changed, 57 insertions, 10 deletions
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 8c296f0a..a686414a 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -125,17 +125,35 @@ Definition rolm (r1 r2: ireg) (amount mask: int) (k: code) := Definition low64_u (n: int64) := Int64.zero_ext 16 n. Definition low64_s (n: int64) := Int64.sign_ext 16 n. -Definition loadimm64 (r: ireg) (n: int64) (k: code) := +Definition loadimm64_32s (r: ireg) (n: int64) (k: code) := let lo_u := low64_u n in let lo_s := low64_s n in - let hi_s := Int64.sign_ext 16 (Int64.shr n (Int64.repr 16)) in + let hi_s := low64_s (Int64.shr n (Int64.repr 16)) in if Int64.eq n lo_s then Paddi64 r GPR0 n :: k - else if Int64.eq n (Int64.or (Int64.shl hi_s (Int64.repr 16)) lo_u) then - Paddis64 r GPR0 hi_s :: Pori64 r r lo_u :: k + else + Paddis64 r GPR0 hi_s :: Pori64 r r lo_u :: k. + +Definition loadimm64 (r: ireg) (n: int64) (k: code) := + if Int64.eq n (Int64.sign_ext 32 n) then + loadimm64_32s r n k else Pldi r n :: k. +(** [loadimm64_notemp] is a variant of [loadimm64] that uses no temporary + register. The code it produces is larger and slower than the code + produced by [loadimm64], but it is sometimes useful to preserve all registers + except the destination. *) + +Definition loadimm64_notemp (r: ireg) (n: int64) (k: code) := + if Int64.eq n (Int64.sign_ext 32 n) then + loadimm64_32s r n k + else + loadimm64_32s r (Int64.shru n (Int64.repr 32)) + (Prldinm r r (Int.repr 32) (Int64.shl Int64.mone (Int64.repr 32)) :: + Poris64 r r (low64_u (Int64.shru n (Int64.repr 16))) :: + Pori64 r r (low64_u n) :: k). + Definition opimm64 (insn2: ireg -> ireg -> ireg -> instruction) (insn1: ireg -> ireg -> int64 -> instruction) (r1 r2: ireg) (n: int64) (ok: bool) (k: code) := @@ -261,18 +279,14 @@ Definition transl_cond do r1 <- ireg_of a1; if Int64.eq n (low64_s n) then OK (Pcmpdi r1 n :: k) - else if ireg_eq r1 GPR12 then - OK (Pmr GPR0 GPR12 :: loadimm64 GPR12 n (Pcmpd GPR0 GPR12 :: k)) else - OK (loadimm64 GPR0 n (Pcmpd r1 GPR0 :: k)) + OK (loadimm64_notemp GPR0 n (Pcmpd r1 GPR0 :: k)) | Ccompluimm c n, a1 :: nil => do r1 <- ireg_of a1; if Int64.eq n (low64_u n) then OK (Pcmpldi r1 n :: k) - else if ireg_eq r1 GPR12 then - OK (Pmr GPR0 GPR12 :: loadimm64 GPR12 n (Pcmpld GPR0 GPR12 :: k)) else - OK (loadimm64 GPR0 n (Pcmpld r1 GPR0 :: k)) + OK (loadimm64_notemp GPR0 n (Pcmpld r1 GPR0 :: k)) | _, _ => Error(msg "Asmgen.transl_cond") end. @@ -390,6 +404,28 @@ Definition transl_cond_op else Pxori r' r' (Cint Int.one) :: k) end. +(** Translation of a select operation *) + +Definition transl_select_op + (cond: condition) (args: list mreg) (r1 r2 rd: ireg) (k: code) := + if ireg_eq r1 r2 then + OK (Pmr rd r1 :: k) + else + (let p := crbit_for_cond cond in + let r1' := if snd p then r1 else r2 in + let r2' := if snd p then r2 else r1 in + transl_cond cond args (Pisel rd r1' r2' (fst p) :: k)). + +Definition transl_fselect_op + (cond: condition) (args: list mreg) (r1 r2 rd: freg) (k: code) := + if freg_eq r1 r2 then + OK (Pfmr rd r1 :: k) + else + (let p := crbit_for_cond cond in + let r1' := if snd p then r1 else r2 in + let r2' := if snd p then r2 else r1 in + transl_cond cond args (Pfsel_gen rd r1' r2' (fst p) :: k)). + (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -596,6 +632,17 @@ Definition transl_op do r1 <- ireg_of a1; do r <- ireg_of res; OK (Plhi r r1 :: k) | Ocmp cmp, _ => transl_cond_op cmp args res k + | Osel cmp ty, a1 :: a2 :: args => + match preg_of res with + | IR r1 => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + transl_select_op cmp args r1 r2 r k + | FR r => + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + transl_fselect_op cmp args r1 r2 r k + | _ => + Error (msg "Asmgen.Osel") + end (*c PPC64 operations *) | Olongconst n, nil => do r <- ireg_of res; OK (loadimm64 r n k) |