Hybrid 64bit/32bit PowerPC port

This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.

The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.

In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.

1 files changed, 334 insertions, 1 deletions

diff --git a/powerpc/SelectLong.vp b/powerpc/SelectLong.vp
index cc7a38f6..5f13774b 100644
--- a/powerpc/SelectLong.vp
+++ b/powerpc/SelectLong.vp
@@ -18,4 +18,337 @@ Require Import AST Integers Floats.
 Require Import Op CminorSel.
 Require Import SelectOp SplitLong.
 
-(** This file is empty because we use the default implementation provided in [SplitLong]. *)
+Local Open Scope cminorsel_scope.
+Local Open Scope string_scope.
+
+Section SELECT.
+
+Context {hf: helper_functions}.
+
+Definition longconst (n: int64) : expr :=
+  if Archi.splitlong then SplitLong.longconst n else Eop (Olongconst n) Enil.
+
+Definition is_longconst (e: expr) :=
+  if Archi.splitlong then SplitLong.is_longconst e else
+  match e with
+  | Eop (Olongconst n) Enil => Some n
+  | _ => None
+  end.
+
+Definition intoflong (e: expr) :=
+  if Archi.splitlong then SplitLong.intoflong e else
+  match is_longconst e with
+  | Some n => Eop (Ointconst (Int.repr (Int64.unsigned n))) Enil
+  | None =>  Eop Olowlong (e ::: Enil)
+  end.
+
+Definition longofint (e: expr) :=
+  if Archi.splitlong then SplitLong.longofint e else
+  match is_intconst e with
+  | Some n => longconst (Int64.repr (Int.signed n))
+  | None =>  Eop Ocast32signed (e ::: Enil)
+  end.
+
+Definition longofintu (e: expr) :=
+  if Archi.splitlong then SplitLong.longofintu e else
+  match is_intconst e with
+  | Some n => longconst (Int64.repr (Int.unsigned n))
+  | None =>  Eop Ocast32unsigned (e ::: Enil)
+  end.
+
+Nondetfunction notl (e: expr) :=
+  if Archi.splitlong then SplitLong.notl e else
+  match e with
+  | Eop (Olongconst n) Enil => longconst (Int64.not n)
+  | Eop Onotl (t1:::Enil) => t1
+  | _ => Eop Onotl (e:::Enil)
+  end.
+
+Nondetfunction andlimm (n1: int64) (e2: expr) :=
+  if Int64.eq n1 Int64.zero then longconst Int64.zero else
+  if Int64.eq n1 Int64.mone then e2 else
+  match e2 with
+  | Eop (Olongconst n2) Enil =>
+      longconst (Int64.and n1 n2)
+  | Eop (Oandlimm n2) (t2:::Enil) =>
+      Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil)
+  | Eop (Orolml amount2 mask2) (t2:::Enil) =>
+      Eop (Orolml amount2 (Int64.and n1 mask2)) (t2:::Enil)
+  | _ =>
+      Eop (Oandlimm n1) (e2:::Enil)
+  end.
+
+Nondetfunction andl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.andl e1 e2 else
+  match e1, e2 with
+  | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2
+  | t1, Eop (Olongconst n2) Enil => andlimm n2 t1
+  | _, _ => Eop Oandl (e1:::e2:::Enil)
+  end.
+
+Nondetfunction orlimm (n1: int64) (e2: expr) :=
+  if Int64.eq n1 Int64.zero then e2 else
+  if Int64.eq n1 Int64.mone then longconst Int64.mone else
+  match e2 with
+  | Eop (Olongconst n2) Enil => longconst (Int64.or n1 n2)
+  | Eop (Oorlimm n2) (t2:::Enil) => Eop (Oorlimm (Int64.or n1 n2)) (t2:::Enil)
+  | _ => Eop (Oorlimm n1) (e2:::Enil)
+  end.
+
+Nondetfunction orl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.orl e1 e2 else
+  match e1, e2 with
+  | Eop (Orolml amount1  mask1) (t1:::Enil), Eop (Orolml amount2 mask2) (t2:::Enil) =>
+      if Int.eq amount1 amount2 && same_expr_pure t1 t2
+      then Eop (Orolml amount1 (Int64.or mask1 mask2)) (t1:::Enil)
+      else Eop Oorl (e1:::e2:::Enil)
+  | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2
+  | t1, Eop (Olongconst n2) Enil => orlimm n2 t1
+  | _, _ => Eop Oorl (e1:::e2:::Enil)
+  end.
+
+Nondetfunction xorlimm (n1: int64) (e2: expr) :=
+  if Int64.eq n1 Int64.zero then e2 else
+  if Int64.eq n1 Int64.mone then notl e2 else
+  match e2 with
+  | Eop (Olongconst n2) Enil => longconst (Int64.xor n1 n2)
+  | Eop (Oxorlimm n2) (t2:::Enil) => Eop (Oxorlimm (Int64.xor n1 n2)) (t2:::Enil)
+  | Eop Onotl (t2:::Enil) => Eop (Oxorlimm (Int64.not n1)) (t2:::Enil)
+  | _ => Eop (Oxorlimm n1) (e2:::Enil)
+  end.
+
+Nondetfunction xorl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.xorl e1 e2 else
+  match e1, e2 with
+  | Eop (Olongconst n1) Enil, t2 => xorlimm n1 t2
+  | t1, Eop (Olongconst n2) Enil => xorlimm n2 t1
+  | _, _ => Eop Oxorl (e1:::e2:::Enil)
+  end.
+
+Nondetfunction rolml (e1: expr) (amount2: int) (mask2: int64) :=
+  if Int.eq amount2 Int.zero then andlimm mask2 e1 else
+  match e1 with
+  | Eop (Olongconst n1) Enil =>
+      longconst (Int64.and (Int64.rol' n1 amount2) mask2)
+  | Eop (Orolml amount1 mask1) (t1:::Enil) =>
+      Eop (Orolml (Int.modu (Int.add amount1 amount2) Int64.iwordsize')
+                  (Int64.and (Int64.rol' mask1 amount2) mask2))
+          (t1:::Enil)
+  | Eop (Oandlimm mask1) (t1:::Enil) =>
+      Eop (Orolml amount2
+                  (Int64.and (Int64.rol' mask1 amount2) mask2))
+          (t1:::Enil)
+  | _ =>
+      Eop (Orolml amount2 mask2) (e1:::Enil)
+  end.
+
+Definition shllimm (e1: expr) (n: int) :=
+  if Archi.splitlong then SplitLong.shllimm e1 n else
+  if Int.eq n Int.zero then e1 else
+  if negb (Int.ltu n Int64.iwordsize') then
+    Eop Oshll (e1:::Eop (Ointconst n) Enil:::Enil)
+  else
+    let n' := Int64.repr (Int.unsigned n) in
+    rolml e1 n (Int64.shl Int64.mone n').
+
+Definition shrluimm (e1: expr) (n: int) :=
+  if Archi.splitlong then SplitLong.shrluimm e1 n else
+  if Int.eq n Int.zero then e1 else
+  if negb (Int.ltu n Int64.iwordsize') then
+    Eop Oshrlu (e1:::Eop (Ointconst n) Enil:::Enil)
+  else
+    let n' := Int64.repr (Int.unsigned n) in
+    rolml e1 (Int.sub Int64.iwordsize' n) (Int64.shru Int64.mone n').
+
+Nondetfunction shrlimm (e1: expr) (n: int) :=
+  if Archi.splitlong then SplitLong.shrlimm e1 n else
+  if Int.eq n Int.zero then e1 else
+  if negb (Int.ltu n Int64.iwordsize') then
+    Eop Oshrl (e1:::Eop (Ointconst n) Enil:::Enil)
+  else
+  match e1 with
+  | Eop (Olongconst n1) Enil =>
+      Eop (Olongconst(Int64.shr' n1 n)) Enil
+  | Eop (Oshrlimm n1) (t1:::Enil) =>
+      if Int.ltu (Int.add n n1) Int64.iwordsize'
+      then Eop (Oshrlimm (Int.add n n1)) (t1:::Enil)
+      else Eop (Oshrlimm n) (e1:::Enil)
+  | _ =>
+      Eop (Oshrlimm n) (e1:::Enil)
+  end.
+
+Definition shll (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.shll e1 e2 else
+  match is_intconst e2 with
+  | Some n2 => shllimm e1 n2
+  | None => Eop Oshll (e1:::e2:::Enil)
+  end.
+
+Definition shrl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.shrl e1 e2 else
+  match is_intconst e2 with
+  | Some n2 => shrlimm e1 n2
+  | None => Eop Oshrl (e1:::e2:::Enil)
+  end.
+
+Definition shrlu (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.shrlu e1 e2 else
+  match is_intconst e2 with
+  | Some n2 => shrluimm e1 n2
+  | _ => Eop Oshrlu (e1:::e2:::Enil)
+  end.
+
+Nondetfunction addlimm (n: int64) (e: expr) :=
+  if Int64.eq n Int64.zero then e else
+  match e with
+  | Eop (Olongconst m) Enil       => longconst (Int64.add m n)
+  | Eop (Oaddlimm m) (t ::: Enil) => Eop (Oaddlimm(Int64.add m n)) (t ::: Enil)
+  | _                             => Eop (Oaddlimm n) (e ::: Enil)
+  end.
+
+Nondetfunction addl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.addl e1 e2 else
+  match e1, e2 with
+  | Eop (Olongconst n1) Enil, t2 => addlimm n1 t2
+  | t1, Eop (Olongconst n2) Enil => addlimm n2 t1
+  | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddlimm n2) (t2:::Enil) =>
+      addlimm (Int64.add n1 n2) (Eop Oaddl (t1:::t2:::Enil))
+  | Eop (Oaddlimm n1) (t1:::Enil), t2 =>
+      addlimm n1 (Eop Oaddl (t1:::t2:::Enil))
+  | t1, Eop (Oaddlimm n2) (t2:::Enil) =>
+      addlimm n2 (Eop Oaddl (t1:::t2:::Enil))
+  | _, _ =>
+      Eop Oaddl (e1:::e2:::Enil)
+  end.
+
+Definition negl (e: expr) :=
+  if Archi.splitlong then SplitLong.negl e else
+  match is_longconst e with
+  | Some n => longconst (Int64.neg n)
+  | None =>  Eop Onegl (e ::: Enil)
+  end.
+
+Nondetfunction subl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.subl e1 e2 else
+  match e1, e2 with
+  | t1, Eop (Olongconst n2) Enil => addlimm (Int64.neg n2) t1
+  | _, _ =>
+      Eop Osubl (e1:::e2:::Enil)
+  end.
+
+Definition mullimm_base (n1: int64) (e2: expr) :=
+  match Int64.one_bits' n1 with
+  | i :: nil =>
+      shllimm e2 i
+  | i :: j :: nil =>
+      Elet e2 (addl (shllimm (Eletvar 0) i) (shllimm (Eletvar 0) j))
+  | _ =>
+       Eop Omull (e2:::longconst n1:::Enil)
+  end.
+
+Nondetfunction mullimm (n1: int64) (e2: expr) :=
+  if Archi.splitlong then SplitLong.mullimm n1 e2
+  else if Int64.eq n1 Int64.zero then longconst Int64.zero
+  else if Int64.eq n1 Int64.one then e2
+  else match e2 with
+  | Eop (Olongconst n2) Enil => longconst (Int64.mul n1 n2)
+  | _ => mullimm_base n1 e2
+  end.
+
+Nondetfunction mull (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.mull e1 e2 else
+  match e1, e2 with
+  | Eop (Olongconst n1) Enil, t2 => mullimm n1 t2
+  | t1, Eop (Olongconst n2) Enil => mullimm n2 t1
+  | _, _ => Eop Omull (e1:::e2:::Enil)
+  end.
+
+Definition mullhu (e1: expr) (n2: int64) :=
+  if Archi.splitlong then SplitLong.mullhu e1 n2 else
+  Eop Omullhu (e1 ::: longconst n2 ::: Enil).
+
+Definition mullhs (e1: expr) (n2: int64) :=
+  if Archi.splitlong then SplitLong.mullhs e1 n2 else
+  Eop Omullhs (e1 ::: longconst n2 ::: Enil).
+
+Definition shrxlimm (e: expr) (n: int) :=
+  if Archi.splitlong then SplitLong.shrxlimm e n else
+  if Int.eq n Int.zero then e else Eop (Oshrxlimm n) (e ::: Enil).
+
+
+Definition modl_aux (divop: operation) (e1 e2: expr) :=
+  Elet e1
+    (Elet (lift e2)
+      (Eop Osubl (Eletvar 1 :::
+                  Eop Omull (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) :::
+                             Eletvar 0 :::
+                             Enil) :::
+                  Enil))).
+
+Definition divls_base (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.divls_base e1 e2 else Eop Odivl (e1:::e2:::Enil).
+
+Definition divlu_base (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.divlu_base e1 e2 else Eop Odivlu (e1:::e2:::Enil).
+
+Definition modls_base (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.modls_base e1 e2 else
+  let default := modl_aux Odivl e1 e2 in
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 =>
+      if Int64.eq Int64.zero n2 then default else
+      if Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone then default
+      else longconst (Int64.mods n1 n2)
+  | _, _ => default
+  end.
+
+Definition modlu_base (e1 e2: expr) :=
+  if Archi.splitlong then SplitLong.modlu_base e1 e2 else
+  let default := modl_aux Odivlu e1 e2 in
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 =>
+      if Int64.eq Int64.zero n2
+      then default
+      else longconst (Int64.modu n1 n2)
+  | _, Some n2 =>
+      match Int64.is_power2 n2 with
+      | Some _ => andlimm (Int64.sub n2 Int64.one) e1
+      | _ => default
+      end
+  | _, _ => default
+  end.
+
+Definition cmplu (c: comparison) (e1 e2: expr) :=
+  if Archi.splitlong then SplitLong.cmplu c e1 e2 else
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 =>
+      Eop (Ointconst (if Int64.cmpu c n1 n2 then Int.one else Int.zero)) Enil
+  | Some n1, None => Eop (Ocmp (Ccompluimm (swap_comparison c) n1)) (e2:::Enil)
+  | None, Some n2 => Eop (Ocmp (Ccompluimm c n2)) (e1:::Enil)
+  | None, None => Eop (Ocmp (Ccomplu c)) (e1:::e2:::Enil)
+  end.
+
+Definition cmpl (c: comparison) (e1 e2: expr) :=
+  if Archi.splitlong then SplitLong.cmpl c e1 e2 else
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 =>
+      Eop (Ointconst (if Int64.cmp c n1 n2 then Int.one else Int.zero)) Enil
+  | Some n1, None => Eop (Ocmp (Ccomplimm (swap_comparison c) n1)) (e2:::Enil)
+  | None, Some n2 => Eop (Ocmp (Ccomplimm c n2)) (e1:::Enil)
+  | None, None => Eop (Ocmp (Ccompl c)) (e1:::e2:::Enil)
+  end.
+
+Definition longoffloat (e: expr) :=
+  if Archi.splitlong
+  then SplitLong.longoffloat e
+  else Eop Olongoffloat (e:::Enil).
+
+Definition floatoflong (e: expr) :=
+  if Archi.splitlong
+  then SplitLong.floatoflong e
+  else Eop Ofloatoflong (e:::Enil).
+
+Definition longofsingle (arg: expr) :=
+  longoffloat (floatofsingle arg).
+
+End SELECT.