summaryrefslogtreecommitdiff
path: root/ia32/Asmgenretaddr.v
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/Asmgenretaddr.v')
-rw-r--r--ia32/Asmgenretaddr.v259
1 files changed, 0 insertions, 259 deletions
diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v
deleted file mode 100644
index 29d2ba0..0000000
--- 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.
-
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-27 00:06:18 +0000