PowerPC: make sure evaluation of conditions do not destroy any register

This will be useful to implement a "select" (conditional move) operation later.

- Introduce `Asmgen.loadimm64_notemp` to load a 64-bit integer
constant into a register without going through memory and without
needing a temporary register.

- Use `Asmgen.loadimm64_notemp` instead of `Asmgen.loadimm64` in the
compilation of conditions, so that GPR12 is no longer needed as a
temporary.

- Share code and proofs common to the two `Asmgen.loadimm64_` functions
as the `Asmgen.loadimm64_32s` function.

1 files changed, 24 insertions, 10 deletions

diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 8c296f0a..dba24a5a 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.