From 7873af34a9520ee5a8a6f10faddf3255a4ff02b2 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 3 May 2017 11:18:32 +0200 Subject: 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. --- powerpc/SelectOp.vp | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'powerpc/SelectOp.vp') diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 0a4b3ef6..2d9ae7a5 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -239,7 +239,7 @@ Definition mulhu (e1: expr) (e2: expr) := Eop Omulhu (e1 ::: e2 ::: Enil). (** ** Bitwise and, or, xor *) -Nondetfunction andimm (n1: int) (e2: expr) := +Nondetfunction andimm (n1: int) (e2: expr) := if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match e2 with @@ -249,7 +249,7 @@ Nondetfunction andimm (n1: int) (e2: expr) := let n := Int.and n1 n2 in if Int.eq (Int.shru (Int.shl n amount) amount) n && Int.ltu amount Int.iwordsize - then rolm t2 (Int.sub Int.iwordsize amount) + then rolm t2 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n) else Eop (Oandimm n) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil) | Eop (Oandimm n2) (t2:::Enil) => @@ -259,7 +259,7 @@ Nondetfunction andimm (n1: int) (e2: expr) := | Eop (Oshrimm amount) (t2:::Enil) => if Int.eq (Int.shru (Int.shl n1 amount) amount) n1 && Int.ltu amount Int.iwordsize - then rolm t2 (Int.sub Int.iwordsize amount) + then rolm t2 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n1) else Eop (Oandimm n1) (e2:::Enil) | _ => @@ -396,14 +396,14 @@ Nondetfunction compimm (default: comparison -> int -> condition) Eop (Ocmp (negate_condition c)) el else if Int.eq_dec n2 Int.one then Eop (Ocmp c) el - else + else Eop (Ointconst Int.zero) Enil | Cne, Eop (Ocmp c) el => if Int.eq_dec n2 Int.zero then Eop (Ocmp c) el else if Int.eq_dec n2 Int.one then Eop (Ocmp (negate_condition c)) el - else + else Eop (Ointconst Int.one) Enil | Ceq, Eop (Oandimm n1) (t1 ::: Enil) => if Int.eq_dec n2 Int.zero then @@ -483,7 +483,8 @@ Nondetfunction floatofintu (e: expr) := | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil | _ => - if Archi.ppc64 then Eop Ofloatofintu (e ::: Enil) else + if Archi.ppc64 then + Eop Ofloatofintu (e ::: Enil) else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil) end. @@ -493,7 +494,8 @@ Nondetfunction floatofint (e: expr) := | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil | _ => - if Archi.ppc64 then Eop Ofloatofint (e ::: Enil) else + if Archi.ppc64 then + Eop Ofloatofint (e ::: Enil) else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: addimm Float.ox8000_0000 e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil) @@ -517,7 +519,7 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). (** ** Recognition of addressing modes for load and store operations *) Definition can_use_Aindexed2 (chunk: memory_chunk): bool := - match chunk with Mint64 => false | _ => true end. + match chunk with Mint64 => Archi.ppc64 | _ => true end. Nondetfunction addressing (chunk: memory_chunk) (e: expr) := match e with @@ -539,6 +541,7 @@ Nondetfunction builtin_arg (e: expr) := | Eop (Ointconst n) Enil => BA_int n | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs + | Eop (Olongconst n) Enil => BA_long n | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => BA_long (Int64.ofwords h l) | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) -- cgit