diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-11-05 15:32:52 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-11-24 17:50:52 +0100 |
| commit | 0b78a7b471eecd1ab983bbc48dfe8b39a0985d47 (patch) | |
| tree | a8d71a353f69f3a8fae1ec9e7451c3bd59ba589c /powerpc/Asmgenproof.v | |
| parent | 10941819e09e2f9090e7fe39301a0b9026a0eba0 (diff) | |
| download | compcert-kvx-0b78a7b471eecd1ab983bbc48dfe8b39a0985d47.tar.gz compcert-kvx-0b78a7b471eecd1ab983bbc48dfe8b39a0985d47.zip | |
Update PowerPC port.
Diffstat (limited to 'powerpc/Asmgenproof.v')
| -rw-r--r-- | powerpc/Asmgenproof.v | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 9adf44dc..c7439c3d 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -49,6 +49,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof. + intros. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -755,7 +763,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. econstructor; eauto. Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto. @@ -777,7 +785,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. rewrite <- H1; simpl. econstructor; eauto. @@ -960,7 +968,7 @@ Local Transparent destroyed_by_jumptable. left; econstructor; split. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. unfold loc_external_result. apply agree_set_other; auto. apply agree_set_mregs; auto. @@ -1005,7 +1013,7 @@ Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact step_simulation. |