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 /x86/Asmexpand.ml | |
| parent | 25ea686abc4cce13aba92196dbeb284f727b6e0e (diff) | |
| download | compcert-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.tar.gz compcert-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 'x86/Asmexpand.ml')
| -rw-r--r-- | x86/Asmexpand.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index 90dc0e69..8e69061e 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -29,7 +29,7 @@ let _1 = Integers.Int.one let _2 = coqint_of_camlint 2l let _4 = coqint_of_camlint 4l let _8 = coqint_of_camlint 8l - + let _0z = Z.zero let _1z = Z.one let _2z = Z.of_sint 2 @@ -49,7 +49,7 @@ let _Plea (r, addr) = let align n a = if n >= 0 then (n + a - 1) land (-a) else n land (-a) -let sp_adjustment_32 sz = +let sp_adjustment_32 sz = let sz = Z.to_int sz in (* Preserve proper alignment of the stack *) let sz = align sz (stack_alignment ()) in @@ -72,7 +72,7 @@ let sp_adjustment_64 sz = (* The top 8 bytes have already been allocated by the "call" instruction. *) (sz - 8, -1) end - + (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; @@ -500,7 +500,7 @@ let expand_instruction instr = emit (Pleaq (RAX, addr1)); emit (Pmovq_mr (addr2, RAX)); current_function_stacksize := Int64.of_int fullsz - end else begin + end else begin let sz = sp_adjustment_32 sz in (* Allocate frame *) let sz' = Z.of_uint sz in @@ -512,7 +512,7 @@ let expand_instruction instr = emit (Pleal (RAX,addr1)); emit (Pmovl_mr (addr2,RAX)); PrintAsmaux.current_function_stacksize := Int32.of_int sz - end + end | Pfreeframe(sz, ofs_ra, ofs_link) -> if Archi.ptr64 then begin let (sz, _) = sp_adjustment_64 sz in |