diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-05-03 11:18:32 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-05-03 11:18:32 +0200 |
| commit | 7873af34a9520ee5a8a6f10faddf3255a4ff02b2 (patch) | |
| tree | 74500c845c99b39ba91a5507656060dea60404ea /powerpc/Archi.v | |
| parent | 25ea686abc4cce13aba92196dbeb284f727b6e0e (diff) | |
| download | compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.tar.gz compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.zip | |
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.
Diffstat (limited to 'powerpc/Archi.v')
| -rw-r--r-- | powerpc/Archi.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 10dc5534..5d11aad1 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -27,11 +27,14 @@ Definition big_endian := true. Definition align_int64 := 8%Z. Definition align_float64 := 8%Z. -Definition splitlong := true. +(** Can we use the 64-bit extensions to the PowerPC architecture? *) +Parameter ppc64 : bool. + +Definition splitlong := negb ppc64. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. Proof. - unfold splitlong, ptr64; congruence. + reflexivity. Qed. Program Definition default_pl_64 : bool * nan_pl 53 := @@ -51,7 +54,4 @@ Definition float_of_single_preserves_sNaN := true. Global Opaque ptr64 big_endian splitlong default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 - float_of_single_preserves_sNaN. - -(** Can we use the 64-bit extensions to the PowerPC architecture? *) -Parameter ppc64: bool. + float_of_single_preserves_sNaN.
\ No newline at end of file |