diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-11 11:51:16 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-11 11:51:16 +0200 |
| commit | e73d255ec045983787ed935ad02d31d45353a2b1 (patch) | |
| tree | 7a935f55c4c037863e607802c8f557ad13e8ed0b /ia32/Asmgenproof.v | |
| parent | 3c605199ab0d096cd66ba671a4e23eac9e79bbc2 (diff) | |
| download | compcert-kvx-e73d255ec045983787ed935ad02d31d45353a2b1.tar.gz compcert-kvx-e73d255ec045983787ed935ad02d31d45353a2b1.zip | |
x86-64 MacOS X support
- Avoid absolute addressing for labels, use RIP-relative addressing
- Different, RIP-relative implementation of jump tables
Diffstat (limited to 'ia32/Asmgenproof.v')
| -rw-r--r-- | ia32/Asmgenproof.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 79602e52..e56dc429 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -779,16 +779,18 @@ Opaque loadind. inv AT. monadInv H6. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H5); intro NOOV. - exploit find_label_goto_label; eauto. + set (rs1 := rs0 #RAX <- Vundef #RDX <- Vundef). + 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. apply plus_one. econstructor; eauto. eapply find_instr_tail; eauto. - simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eauto. + simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. econstructor; eauto. Transparent destroyed_by_jumptable. - simpl. eapply agree_exten; eauto. intros. rewrite C; auto with asmgen. + apply agree_undef_regs with rs0; auto. + simpl; intros. destruct H8. rewrite C by auto with asmgen. unfold rs1; Simplifs. congruence. - (* Mreturn *) |