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/Stacklayout.v | |
| 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/Stacklayout.v')
| -rw-r--r-- | x86/Stacklayout.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v index 44fd43b2..22c68099 100644 --- a/x86/Stacklayout.v +++ b/x86/Stacklayout.v @@ -72,7 +72,7 @@ Local Opaque Z.add Z.mul sepconj range. assert (0 <= 4 * b.(bound_outgoing)) by omega. assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). assert (olink + w <= ocs) by (unfold ocs; omega). - assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). + assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega). @@ -88,13 +88,13 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap34. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split_2. fold olink. omega. omega. + apply range_split_2. fold olink. omega. omega. apply range_split. omega. apply range_split_2. fold ol. omega. omega. apply range_drop_right with ostkdata. omega. rewrite sep_swap. apply range_drop_left with (ostkdata + bound_stack_data b). omega. - rewrite sep_swap. + rewrite sep_swap. exact H. Qed. @@ -115,11 +115,11 @@ Proof. assert (0 <= 4 * b.(bound_outgoing)) by omega. assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). assert (olink + w <= ocs) by (unfold ocs; omega). - assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). + assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega). - split. omega. omega. + split. omega. omega. Qed. Lemma frame_env_aligned: |