diff options
Diffstat (limited to 'arm/Asmgenretaddr.v')
-rw-r--r-- | arm/Asmgenretaddr.v | 217 |
1 files changed, 0 insertions, 217 deletions
diff --git a/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v deleted file mode 100644 index 2d3c72d3..00000000 --- a/arm/Asmgenretaddr.v +++ /dev/null @@ -1,217 +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 PPC 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 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 PPC code obtained by translating the - code of [f]. Graphically: -<< - Mach function f |--------- Mcall ---------| - Mach code c | |--------| - | \ \ - | \ \ - | \ \ - PPC code | |--------| - PPC function |--------------- Pbl ---------| - - <-------- ofs -------> ->> -*) - -Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop := - | return_address_offset_intro: - forall c f ofs, - code_tail ofs (fn_code (transl_function f)) (transl_code f c) -> - 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 := - auto with ppcretaddr; - match goal with - | [ |- is_tail _ (_ :: _) ] => constructor; IsTail - | [ |- is_tail _ (match ?x with true => _ | false => _ end) ] => destruct x; IsTail - | [ |- is_tail _ (match ?x with left _ => _ | right _ => _ end) ] => destruct x; IsTail - | [ |- is_tail _ (match ?x with nil => _ | _ :: _ => _ end) ] => destruct x; IsTail - | [ |- is_tail _ (match ?x with Tint => _ | Tfloat => _ end) ] => destruct x; IsTail - | [ |- is_tail _ (?f _ _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail - | [ |- is_tail _ (?f _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail - | [ |- is_tail _ (?f _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail - | [ |- is_tail _ (?f _ _ _ ?k) ] => apply is_tail_trans with k; IsTail - | [ |- is_tail _ (?f _ _ ?k) ] => apply is_tail_trans with k; IsTail - | _ => idtac - end. - -Lemma iterate_op_tail: - forall op1 op2 l k, is_tail k (iterate_op op1 op2 l k). -Proof. - intros. unfold iterate_op. - destruct l. - auto with coqlib. - constructor. revert l; induction l; simpl; auto with coqlib. -Qed. -Hint Resolve iterate_op_tail: ppcretaddr. - -Lemma loadimm_tail: - forall r n k, is_tail k (loadimm r n k). -Proof. unfold loadimm; intros; IsTail. Qed. -Hint Resolve loadimm_tail: ppcretaddr. - -Lemma addimm_tail: - forall r1 r2 n k, is_tail k (addimm r1 r2 n k). -Proof. unfold addimm; intros; IsTail. Qed. -Hint Resolve addimm_tail: ppcretaddr. - -Lemma andimm_tail: - forall r1 r2 n k, is_tail k (andimm r1 r2 n k). -Proof. unfold andimm; intros; IsTail. Qed. -Hint Resolve andimm_tail: ppcretaddr. - -Lemma rsubimm_tail: - forall r1 r2 n k, is_tail k (rsubimm r1 r2 n k). -Proof. unfold rsubimm; intros; IsTail. Qed. -Hint Resolve rsubimm_tail: ppcretaddr. - -Lemma orimm_tail: - forall r1 r2 n k, is_tail k (orimm r1 r2 n k). -Proof. unfold orimm; intros; IsTail. Qed. -Hint Resolve orimm_tail: ppcretaddr. - -Lemma xorimm_tail: - forall r1 r2 n k, is_tail k (xorimm r1 r2 n k). -Proof. unfold xorimm; intros; IsTail. Qed. -Hint Resolve xorimm_tail: ppcretaddr. - -Lemma transl_cond_tail: - forall cond args k, is_tail k (transl_cond cond args k). -Proof. unfold transl_cond; intros; destruct cond; IsTail. Qed. -Hint Resolve transl_cond_tail: ppcretaddr. - -Lemma transl_op_tail: - forall op args r k, is_tail k (transl_op op args r k). -Proof. unfold transl_op; intros; destruct op; IsTail. Qed. -Hint Resolve transl_op_tail: ppcretaddr. - -Lemma transl_load_store_tail: - forall mk1 mk2 is_immed addr args k, - is_tail k (transl_load_store mk1 mk2 is_immed addr args k). -Proof. unfold transl_load_store; intros; destruct addr; IsTail. - destruct mk2; IsTail. destruct mk2; IsTail. Qed. -Hint Resolve transl_load_store_tail: ppcretaddr. - -Lemma transl_load_store_int_tail: - forall mk is_immed rd addr args k, - is_tail k (transl_load_store_int mk is_immed rd addr args k). -Proof. unfold transl_load_store_int; intros; IsTail. Qed. -Hint Resolve transl_load_store_int_tail: ppcretaddr. - -Lemma transl_load_store_float_tail: - forall mk is_immed rd addr args k, - is_tail k (transl_load_store_float mk is_immed rd addr args k). -Proof. unfold transl_load_store_float; intros; IsTail. Qed. -Hint Resolve transl_load_store_float_tail: ppcretaddr. - -Lemma loadind_int_tail: - forall base ofs dst k, is_tail k (loadind_int base ofs dst k). -Proof. unfold loadind_int; intros; IsTail. Qed. -Hint Resolve loadind_int_tail: ppcretaddr. - -Lemma loadind_tail: - forall base ofs ty dst k, is_tail k (loadind base ofs ty dst k). -Proof. unfold loadind, loadind_float; intros; IsTail. Qed. -Hint Resolve loadind_tail: ppcretaddr. - -Lemma storeind_int_tail: - forall src base ofs k, is_tail k (storeind_int src base ofs k). -Proof. unfold storeind_int; intros; IsTail. Qed. -Hint Resolve storeind_int_tail: ppcretaddr. - -Lemma storeind_tail: - forall src base ofs ty k, is_tail k (storeind src base ofs ty k). -Proof. unfold storeind, storeind_float; intros; IsTail. Qed. -Hint Resolve storeind_tail: ppcretaddr. - -Lemma transl_instr_tail: - forall f i k, is_tail k (transl_instr f i k). -Proof. - unfold transl_instr; intros; destruct i; IsTail. - destruct m; IsTail. - destruct m; IsTail. - destruct s0; IsTail. - destruct s0; IsTail. -Qed. -Hint Resolve transl_instr_tail: ppcretaddr. - -Lemma transl_code_tail: - forall f c1 c2, is_tail c1 c2 -> is_tail (transl_code f c1) (transl_code f c2). -Proof. - induction 1; simpl. constructor. eapply is_tail_trans; eauto with ppcretaddr. -Qed. - -Lemma 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. -Proof. - intros. assert (is_tail (transl_code f c) (fn_code (transl_function f))). - unfold transl_function. simpl. IsTail. apply transl_code_tail; eauto with coqlib. - destruct (is_tail_code_tail _ _ H0) as [ofs A]. - exists (Int.repr ofs). constructor. auto. -Qed. - - |