From 5020a5a07da3fd690f5d171a48d0c73ef48f9430 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 1 Mar 2013 15:32:13 +0000 Subject: Revised Stacking and Asmgen passes and Mach semantics: - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asmgenretaddr.v | 259 --------------------------------------------------- 1 file changed, 259 deletions(-) delete mode 100644 ia32/Asmgenretaddr.v (limited to 'ia32/Asmgenretaddr.v') diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v deleted file mode 100644 index 29d2ba0a..00000000 --- a/ia32/Asmgenretaddr.v +++ /dev/null @@ -1,259 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Predictor for return addresses in generated IA32 code. - - The [return_address_offset] predicate defined here is used in the - semantics for Mach (module [Machsem]) to determine the - return addresses that are stored in activation records. *) - -Require Import Coqlib. -Require Import AST. -Require Import Errors. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import Locations. -Require Import Mach. -Require Import Asm. -Require Import Asmgen. - -(** The ``code tail'' of an instruction list [c] is the list of instructions - starting at PC [pos]. *) - -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. - -Lemma code_tail_pos: - forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. -Proof. - induction 1. omega. omega. -Qed. - -(** Consider a Mach function [f] and a sequence [c] of Mach instructions - representing the Mach code that remains to be executed after a - function call returns. The predicate [return_address_offset f c ofs] - holds if [ofs] is the integer offset of the PPC instruction - following the call in the Asm code obtained by translating the - code of [f]. Graphically: -<< - Mach function f |--------- Mcall ---------| - Mach code c | |--------| - | \ \ - | \ \ - | \ \ - Asm code | |--------| - Asm function |------------- Pcall ---------| - - <-------- ofs -------> ->> -*) - -Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop := - | return_address_offset_intro: - forall f c ofs, - (forall tf tc, - transf_function f = OK tf -> - transl_code f c false = OK tc -> - code_tail ofs tf tc) -> - return_address_offset f c (Int.repr ofs). - -(** We now show that such an offset always exists if the Mach code [c] - is a suffix of [f.(fn_code)]. This holds because the translation - from Mach to PPC is compositional: each Mach instruction becomes - zero, one or several PPC instructions, but the order of instructions - is preserved. *) - -Lemma is_tail_code_tail: - forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1. -Proof. - induction 1. exists 0; constructor. - destruct IHis_tail as [ofs CT]. exists (ofs + 1); constructor; auto. -Qed. - -Hint Resolve is_tail_refl: ppcretaddr. - -Ltac IsTail := - eauto with ppcretaddr; - match goal with - | [ |- is_tail _ (_ :: _) ] => constructor; IsTail - | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: OK _ = OK _ |- _ ] => inv H; IsTail - | [ H: bind _ _ = OK _ |- _ ] => monadInv H; IsTail - | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; IsTail - | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; IsTail - | _ => idtac - end. - -Lemma mk_mov_tail: - forall rd rs k c, mk_mov rd rs k = OK c -> is_tail k c. -Proof. - unfold mk_mov; intros. destruct rd; IsTail; destruct rs; IsTail. -Qed. - -Lemma mk_shift_tail: - forall si r1 r2 k c, mk_shift si r1 r2 k = OK c -> is_tail k c. -Proof. - unfold mk_shift; intros; IsTail. -Qed. - -Lemma mk_mov2_tail: - forall r1 r2 r3 r4 k, is_tail k (mk_mov2 r1 r2 r3 r4 k). -Proof. - unfold mk_mov2; intros. - destruct (ireg_eq r1 r2). IsTail. - destruct (ireg_eq r3 r4). IsTail. - destruct (ireg_eq r3 r2); IsTail. - destruct (ireg_eq r1 r4); IsTail. -Qed. - -Lemma mk_div_tail: - forall di r1 r2 k c, mk_div di r1 r2 k = OK c -> is_tail k c. -Proof. - unfold mk_div; intros; IsTail. - eapply is_tail_trans. 2: eapply mk_mov2_tail. IsTail. -Qed. - -Lemma mk_mod_tail: - forall di r1 r2 k c, mk_mod di r1 r2 k = OK c -> is_tail k c. -Proof. - unfold mk_mod; intros; IsTail. - eapply is_tail_trans. 2: eapply mk_mov2_tail. IsTail. -Qed. - -Lemma mk_shrximm_tail: - forall r n k c, mk_shrximm r n k = OK c -> is_tail k c. -Proof. - unfold mk_shrximm; intros; IsTail. -Qed. - -Lemma mk_intconv_tail: - forall mk rd rs k c, mk_intconv mk rd rs k = OK c -> is_tail k c. -Proof. - unfold mk_intconv; intros; IsTail. -Qed. - -Lemma mk_smallstore_tail: - forall sto addr rs k c, mk_smallstore sto addr rs k = OK c -> is_tail k c. -Proof. - unfold mk_smallstore; intros; IsTail. -Qed. - -Lemma loadind_tail: - forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> is_tail k c. -Proof. - unfold loadind; intros. destruct ty; IsTail. destruct (preg_of dst); IsTail. -Qed. - -Lemma storeind_tail: - forall src base ofs ty k c, storeind src base ofs ty k = OK c -> is_tail k c. -Proof. - unfold storeind; intros. destruct ty; IsTail. destruct (preg_of src); IsTail. -Qed. - -Lemma mk_setcc_tail: - forall cond rd k, is_tail k (mk_setcc cond rd k). -Proof. - unfold mk_setcc; intros. destruct cond. - IsTail. - destruct (ireg_eq rd EDX); IsTail. - destruct (ireg_eq rd EDX); IsTail. -Qed. - -Lemma mk_jcc_tail: - forall cond lbl k, is_tail k (mk_jcc cond lbl k). -Proof. - unfold mk_jcc; intros. destruct cond; IsTail. -Qed. - -Hint Resolve mk_mov_tail mk_shift_tail mk_div_tail mk_mod_tail mk_shrximm_tail - mk_intconv_tail mk_smallstore_tail loadind_tail storeind_tail - mk_setcc_tail mk_jcc_tail : ppcretaddr. - -Lemma transl_cond_tail: - forall cond args k c, transl_cond cond args k = OK c -> is_tail k c. -Proof. - unfold transl_cond; intros. destruct cond; IsTail; destruct (Int.eq_dec i Int.zero); IsTail. -Qed. - -Lemma transl_op_tail: - forall op args res k c, transl_op op args res k = OK c -> is_tail k c. -Proof. - unfold transl_op; intros. destruct op; IsTail. - eapply is_tail_trans. 2: eapply transl_cond_tail; eauto. IsTail. -Qed. - -Lemma transl_load_tail: - forall chunk addr args dest k c, transl_load chunk addr args dest k = OK c -> is_tail k c. -Proof. - unfold transl_load; intros. IsTail. destruct chunk; IsTail. -Qed. - -Lemma transl_store_tail: - forall chunk addr args src k c, transl_store chunk addr args src k = OK c -> is_tail k c. -Proof. - unfold transl_store; intros. IsTail. destruct chunk; IsTail. -Qed. - -Lemma transl_instr_tail: - forall f i ep k c, transl_instr f i ep k = OK c -> is_tail k c. -Proof. - unfold transl_instr; intros. destruct i; IsTail. - eapply is_tail_trans; eapply loadind_tail; eauto. - eapply transl_op_tail; eauto. - eapply transl_load_tail; eauto. - eapply transl_store_tail; eauto. - destruct s0; IsTail. - destruct s0; IsTail. - eapply is_tail_trans. 2: eapply transl_cond_tail; eauto. IsTail. -Qed. - -Lemma transl_code_tail: - forall f c1 c2, is_tail c1 c2 -> - forall tc2 ep2, transl_code f c2 ep2 = OK tc2 -> - exists tc1, exists ep1, transl_code f c1 ep1 = OK tc1 /\ is_tail tc1 tc2. -Proof. - induction 1; simpl; intros. - exists tc2; exists ep2; split; auto with coqlib. - monadInv H0. exploit IHis_tail; eauto. intros [tc1 [ep1 [A B]]]. - exists tc1; exists ep1; split. auto. - apply is_tail_trans with x. auto. eapply transl_instr_tail; eauto. -Qed. - -Lemma return_address_exists: - forall f sg ros c, is_tail (Mcall sg ros :: c) f.(fn_code) -> - exists ra, return_address_offset f c ra. -Proof. - intros. - caseEq (transf_function f). intros tf TF. - assert (exists tc1, transl_code f (fn_code f) true = OK tc1 /\ is_tail tc1 tf). - monadInv TF. - destruct (zlt (list_length_z x) Int.max_unsigned); monadInv EQ0. - econstructor; eauto with coqlib. - destruct H0 as [tc2 [A B]]. - exploit transl_code_tail; eauto. intros [tc1 [ep [C D]]]. -Opaque transl_instr. - monadInv C. - assert (is_tail x tf). - apply is_tail_trans with tc2; auto. - apply is_tail_trans with tc1; auto. - eapply transl_instr_tail; eauto. - exploit is_tail_code_tail. eexact H0. intros [ofs C]. - exists (Int.repr ofs). constructor; intros. congruence. - intros. exists (Int.repr 0). constructor; intros; congruence. -Qed. - - -- cgit