diff options
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 09564718..5660f718 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -40,6 +40,25 @@ Proof. exists tp; split. apply Asm.transf_program_match; auto. auto. Qed. +(** Return Address Offset *) + +Inductive code_tail: Z -> code -> code -> Prop := + | code_tail_0: forall c, + code_tail 0 c c + | code_tail_S: forall pos i c1 c2, + code_tail pos c1 c2 -> + code_tail (pos + 1) (i :: c1) c2. + +Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop := + forall tf tc, + Asmgen.transf_function f = OK tf -> + Asmgen.transl_code f c = OK tc -> + code_tail (Ptrofs.unsigned ofs) (fn_code tf) tc. + +Axiom return_address_exists: + forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> + exists ra, return_address_offset f c ra. + Section PRESERVATION. Variable prog: Mach.program. @@ -49,7 +68,7 @@ Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. Theorem transf_program_correct: - forward_simulation (Mach.semantics (inv_trans_rao return_address_offset) prog) (Asm.semantics tprog). + forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. unfold match_prog in TRANSF. simpl in TRANSF. inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. @@ -60,4 +79,5 @@ Qed. End PRESERVATION. -Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes).
\ No newline at end of file +Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes). + |