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/Asmgenproof.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 'x86/Asmgenproof.v')
| -rw-r--r-- | x86/Asmgenproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index e56dc429..6caf4531 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -780,7 +780,7 @@ Opaque loadind. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H5); intro NOOV. set (rs1 := rs0 #RAX <- Vundef #RDX <- Vundef). - exploit (find_label_goto_label f tf lbl rs1); eauto. + exploit (find_label_goto_label f tf lbl rs1); eauto. intros [tc' [rs' [A [B C]]]]. exploit ireg_val; eauto. rewrite H. intros LD; inv LD. left; econstructor; split. @@ -789,7 +789,7 @@ Opaque loadind. simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. econstructor; eauto. Transparent destroyed_by_jumptable. - apply agree_undef_regs with rs0; auto. + apply agree_undef_regs with rs0; auto. simpl; intros. destruct H8. rewrite C by auto with asmgen. unfold rs1; Simplifs. congruence. @@ -834,7 +834,7 @@ Transparent destroyed_by_jumptable. left; econstructor; split. apply plus_one. econstructor; eauto. simpl. rewrite Ptrofs.unsigned_zero. simpl. eauto. - simpl. rewrite C. simpl in F, P. + simpl. rewrite C. simpl in F, P. replace (chunk_of_type Tptr) with Mptr in F, P by (unfold Tptr, Mptr; destruct Archi.ptr64; auto). rewrite (sp_val _ _ _ AG) in F. rewrite F. rewrite ATLR. rewrite P. eauto. @@ -883,7 +883,7 @@ Proof. econstructor; eauto. constructor. apply Mem.extends_refl. - split. reflexivity. simpl. + split. reflexivity. simpl. unfold Vnullptr; destruct Archi.ptr64; congruence. intros. rewrite Regmap.gi. auto. unfold Genv.symbol_address. |