diff options
Diffstat (limited to 'backend/PPCgenproof.v')
| -rw-r--r-- | backend/PPCgenproof.v | 1393 |
1 files changed, 0 insertions, 1393 deletions
diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v deleted file mode 100644 index 6db8b477..00000000 --- a/backend/PPCgenproof.v +++ /dev/null @@ -1,1393 +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. *) -(* *) -(* *********************************************************************) - -(** Correctness proof for PPC generation: main proof. *) - -Require Import Coqlib. -Require Import Maps. -Require Import Errors. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Mem. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Locations. -Require Import Mach. -Require Import Machconcr. -Require Import Machtyping. -Require Import PPC. -Require Import PPCgen. -Require Import PPCgenretaddr. -Require Import PPCgenproof1. - -Section PRESERVATION. - -Variable prog: Mach.program. -Variable tprog: PPC.program. -Hypothesis TRANSF: transf_program prog = Errors.OK tprog. - -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -Lemma symbols_preserved: - forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof. - intros. unfold ge, tge. - apply Genv.find_symbol_transf_partial with transf_fundef. - exact TRANSF. -Qed. - -Lemma functions_translated: - forall b f, - Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = Errors.OK tf. -Proof - (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF). - -Lemma functions_transl: - forall f b, - Genv.find_funct_ptr ge b = Some (Internal f) -> - Genv.find_funct_ptr tge b = Some (Internal (transl_function f)). -Proof. - intros. - destruct (functions_translated _ _ H) as [tf [A B]]. - rewrite A. generalize B. unfold transf_fundef, transf_partial_fundef, transf_function. - case (zlt Int.max_unsigned (code_size (transl_function f))); simpl; intro. - congruence. intro. inv B0. auto. -Qed. - -Lemma functions_transl_no_overflow: - forall b f, - Genv.find_funct_ptr ge b = Some (Internal f) -> - code_size (transl_function f) <= Int.max_unsigned. -Proof. - intros. - destruct (functions_translated _ _ H) as [tf [A B]]. - generalize B. unfold transf_fundef, transf_partial_fundef, transf_function. - case (zlt Int.max_unsigned (code_size (transl_function f))); simpl; intro. - congruence. intro; omega. -Qed. - -(** * Properties of control flow *) - -Lemma find_instr_in: - forall c pos i, - find_instr pos c = Some i -> In i c. -Proof. - induction c; simpl. intros; discriminate. - intros until i. case (zeq pos 0); intros. - left; congruence. right; eauto. -Qed. - -Lemma find_instr_tail: - forall c1 i c2 pos, - code_tail pos c1 (i :: c2) -> - find_instr pos c1 = Some i. -Proof. - induction c1; simpl; intros. - inv H. - destruct (zeq pos 0). subst pos. - inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction. - inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega. - eauto. -Qed. - -Remark code_size_pos: - forall fn, code_size fn >= 0. -Proof. - induction fn; simpl; omega. -Qed. - -Remark code_tail_bounds: - forall fn ofs i c, - code_tail ofs fn (i :: c) -> 0 <= ofs < code_size fn. -Proof. - assert (forall ofs fn c, code_tail ofs fn c -> - forall i c', c = i :: c' -> 0 <= ofs < code_size fn). - induction 1; intros; simpl. - rewrite H. simpl. generalize (code_size_pos c'). omega. - generalize (IHcode_tail _ _ H0). omega. - eauto. -Qed. - -Lemma code_tail_next: - forall fn ofs i c, - code_tail ofs fn (i :: c) -> - code_tail (ofs + 1) fn c. -Proof. - assert (forall ofs fn c, code_tail ofs fn c -> - forall i c', c = i :: c' -> code_tail (ofs + 1) fn c'). - induction 1; intros. - subst c. constructor. constructor. - constructor. eauto. - eauto. -Qed. - -Lemma code_tail_next_int: - forall fn ofs i c, - code_size fn <= Int.max_unsigned -> - code_tail (Int.unsigned ofs) fn (i :: c) -> - code_tail (Int.unsigned (Int.add ofs Int.one)) fn c. -Proof. - intros. rewrite Int.add_unsigned. - change (Int.unsigned Int.one) with 1. - rewrite Int.unsigned_repr. apply code_tail_next with i; auto. - generalize (code_tail_bounds _ _ _ _ H0). omega. -Qed. - -(** [transl_code_at_pc pc fn c] holds if the code pointer [pc] points - within the PPC code generated by translating Mach function [fn], - and [c] is the tail of the generated code at the position corresponding - to the code pointer [pc]. *) - -Inductive transl_code_at_pc: val -> block -> Mach.function -> Mach.code -> Prop := - transl_code_at_pc_intro: - forall b ofs f c, - Genv.find_funct_ptr ge b = Some (Internal f) -> - code_tail (Int.unsigned ofs) (transl_function f) (transl_code f c) -> - transl_code_at_pc (Vptr b ofs) b f c. - -(** The following lemmas show that straight-line executions - (predicate [exec_straight]) correspond to correct PPC executions - (predicate [exec_steps]) under adequate [transl_code_at_pc] hypotheses. *) - -Lemma exec_straight_steps_1: - forall fn c rs m c' rs' m', - exec_straight tge fn c rs m c' rs' m' -> - code_size fn <= Int.max_unsigned -> - forall b ofs, - rs#PC = Vptr b ofs -> - Genv.find_funct_ptr tge b = Some (Internal fn) -> - code_tail (Int.unsigned ofs) fn c -> - plus step tge (State rs m) E0 (State rs' m'). -Proof. - induction 1; intros. - apply plus_one. - econstructor; eauto. - eapply find_instr_tail. eauto. - eapply plus_left'. - econstructor; eauto. - eapply find_instr_tail. eauto. - apply IHexec_straight with b (Int.add ofs Int.one). - auto. rewrite H0. rewrite H3. reflexivity. - auto. - apply code_tail_next_int with i; auto. - traceEq. -Qed. - -Lemma exec_straight_steps_2: - forall fn c rs m c' rs' m', - exec_straight tge fn c rs m c' rs' m' -> - code_size fn <= Int.max_unsigned -> - forall b ofs, - rs#PC = Vptr b ofs -> - Genv.find_funct_ptr tge b = Some (Internal fn) -> - code_tail (Int.unsigned ofs) fn c -> - exists ofs', - rs'#PC = Vptr b ofs' - /\ code_tail (Int.unsigned ofs') fn c'. -Proof. - induction 1; intros. - exists (Int.add ofs Int.one). split. - rewrite H0. rewrite H2. auto. - apply code_tail_next_int with i1; auto. - apply IHexec_straight with (Int.add ofs Int.one). - auto. rewrite H0. rewrite H3. reflexivity. auto. - apply code_tail_next_int with i; auto. -Qed. - -Lemma exec_straight_exec: - forall fb f c c' rs m rs' m', - transl_code_at_pc (rs PC) fb f c -> - exec_straight tge (transl_function f) - (transl_code f c) rs m c' rs' m' -> - plus step tge (State rs m) E0 (State rs' m'). -Proof. - intros. inversion H. subst. - eapply exec_straight_steps_1; eauto. - eapply functions_transl_no_overflow; eauto. - eapply functions_transl; eauto. -Qed. - -Lemma exec_straight_at: - forall fb f c c' rs m rs' m', - transl_code_at_pc (rs PC) fb f c -> - exec_straight tge (transl_function f) - (transl_code f c) rs m (transl_code f c') rs' m' -> - transl_code_at_pc (rs' PC) fb f c'. -Proof. - intros. inversion H. subst. - generalize (functions_transl_no_overflow _ _ H2). intro. - generalize (functions_transl _ _ H2). intro. - generalize (exec_straight_steps_2 _ _ _ _ _ _ _ - H0 H4 _ _ (sym_equal H1) H5 H3). - intros [ofs' [PC' CT']]. - rewrite PC'. constructor; auto. -Qed. - -(** Correctness of the return addresses predicted by - [PPCgen.return_address_offset]. *) - -Remark code_tail_no_bigger: - forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat. -Proof. - induction 1; simpl; omega. -Qed. - -Remark code_tail_unique: - forall fn c pos pos', - code_tail pos fn c -> code_tail pos' fn c -> pos = pos'. -Proof. - induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - f_equal. eauto. -Qed. - -Lemma return_address_offset_correct: - forall b ofs fb f c ofs', - transl_code_at_pc (Vptr b ofs) fb f c -> - return_address_offset f c ofs' -> - ofs' = ofs. -Proof. - intros. inv H0. inv H. - generalize (code_tail_unique _ _ _ _ H1 H7). intro. rewrite H. - apply Int.repr_unsigned. -Qed. - -(** The [find_label] function returns the code tail starting at the - given label. A connection with [code_tail] is then established. *) - -Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := - match c with - | nil => None - | instr :: c' => - if is_label lbl instr then Some c' else find_label lbl c' - end. - -Lemma label_pos_code_tail: - forall lbl c pos c', - find_label lbl c = Some c' -> - exists pos', - label_pos lbl pos c = Some pos' - /\ code_tail (pos' - pos) c c' - /\ pos < pos' <= pos + code_size c. -Proof. - induction c. - simpl; intros. discriminate. - simpl; intros until c'. - case (is_label lbl a). - intro EQ; injection EQ; intro; subst c'. - exists (pos + 1). split. auto. split. - replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. - generalize (code_size_pos c). omega. - intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]]. - exists pos'. split. auto. split. - replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega. - constructor. auto. - omega. -Qed. - -(** The following lemmas show that the translation from Mach to PPC - preserves labels, in the sense that the following diagram commutes: -<< - translation - Mach code ------------------------ PPC instr sequence - | | - | Mach.find_label lbl find_label lbl | - | | - v v - Mach code tail ------------------- PPC instr seq tail - translation ->> - The proof demands many boring lemmas showing that PPC constructor - functions do not introduce new labels. -*) - -Section TRANSL_LABEL. - -Variable lbl: label. - -Remark loadimm_label: - forall r n k, find_label lbl (loadimm r n k) = find_label lbl k. -Proof. - intros. unfold loadimm. - case (Int.eq (high_s n) Int.zero). reflexivity. - case (Int.eq (low_s n) Int.zero). reflexivity. - reflexivity. -Qed. -Hint Rewrite loadimm_label: labels. - -Remark addimm_1_label: - forall r1 r2 n k, find_label lbl (addimm_1 r1 r2 n k) = find_label lbl k. -Proof. - intros; unfold addimm_1. - case (Int.eq (high_s n) Int.zero). reflexivity. - case (Int.eq (low_s n) Int.zero). reflexivity. reflexivity. -Qed. -Remark addimm_2_label: - forall r1 r2 n k, find_label lbl (addimm_2 r1 r2 n k) = find_label lbl k. -Proof. - intros; unfold addimm_2. autorewrite with labels. reflexivity. -Qed. -Remark addimm_label: - forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k. -Proof. - intros; unfold addimm. - case (ireg_eq r1 GPR0); intro. apply addimm_2_label. - case (ireg_eq r2 GPR0); intro. apply addimm_2_label. - apply addimm_1_label. -Qed. -Hint Rewrite addimm_label: labels. - -Remark andimm_label: - forall r1 r2 n k, find_label lbl (andimm r1 r2 n k) = find_label lbl k. -Proof. - intros; unfold andimm. - case (Int.eq (high_u n) Int.zero). reflexivity. - case (Int.eq (low_u n) Int.zero). reflexivity. - autorewrite with labels. reflexivity. -Qed. -Hint Rewrite andimm_label: labels. - -Remark orimm_label: - forall r1 r2 n k, find_label lbl (orimm r1 r2 n k) = find_label lbl k. -Proof. - intros; unfold orimm. - case (Int.eq (high_u n) Int.zero). reflexivity. - case (Int.eq (low_u n) Int.zero). reflexivity. reflexivity. -Qed. -Hint Rewrite orimm_label: labels. - -Remark xorimm_label: - forall r1 r2 n k, find_label lbl (xorimm r1 r2 n k) = find_label lbl k. -Proof. - intros; unfold xorimm. - case (Int.eq (high_u n) Int.zero). reflexivity. - case (Int.eq (low_u n) Int.zero). reflexivity. reflexivity. -Qed. -Hint Rewrite xorimm_label: labels. - -Remark loadind_aux_label: - forall base ofs ty dst k, find_label lbl (loadind_aux base ofs ty dst :: k) = find_label lbl k. -Proof. - intros; unfold loadind_aux. - case ty; reflexivity. -Qed. -Remark loadind_label: - forall base ofs ty dst k, find_label lbl (loadind base ofs ty dst k) = find_label lbl k. -Proof. - intros; unfold loadind. - case (Int.eq (high_s ofs) Int.zero). apply loadind_aux_label. - transitivity (find_label lbl (loadind_aux GPR12 (low_s ofs) ty dst :: k)). - reflexivity. apply loadind_aux_label. -Qed. -Hint Rewrite loadind_label: labels. -Remark storeind_aux_label: - forall base ofs ty dst k, find_label lbl (storeind_aux base ofs ty dst :: k) = find_label lbl k. -Proof. - intros; unfold storeind_aux. - case dst; reflexivity. -Qed. -Remark storeind_label: - forall base ofs ty src k, find_label lbl (storeind base src ofs ty k) = find_label lbl k. -Proof. - intros; unfold storeind. - case (Int.eq (high_s ofs) Int.zero). apply storeind_aux_label. - transitivity (find_label lbl (storeind_aux base GPR12 (low_s ofs) ty :: k)). - reflexivity. apply storeind_aux_label. -Qed. -Hint Rewrite storeind_label: labels. -Remark floatcomp_label: - forall cmp r1 r2 k, find_label lbl (floatcomp cmp r1 r2 k) = find_label lbl k. -Proof. - intros; unfold floatcomp. destruct cmp; reflexivity. -Qed. - -Remark transl_cond_label: - forall cond args k, find_label lbl (transl_cond cond args k) = find_label lbl k. -Proof. - intros; unfold transl_cond. - destruct cond; (destruct args; - [try reflexivity | destruct args; - [try reflexivity | destruct args; try reflexivity]]). - case (Int.eq (high_s i) Int.zero). reflexivity. - autorewrite with labels; reflexivity. - case (Int.eq (high_u i) Int.zero). reflexivity. - autorewrite with labels; reflexivity. - apply floatcomp_label. apply floatcomp_label. - apply andimm_label. apply andimm_label. -Qed. -Hint Rewrite transl_cond_label: labels. -Remark transl_op_label: - forall op args r k, find_label lbl (transl_op op args r k) = find_label lbl k. -Proof. - intros; unfold transl_op; - destruct op; destruct args; try (destruct args); try (destruct args); try (destruct args); - try reflexivity; autorewrite with labels; try reflexivity. - case (mreg_type m); reflexivity. - case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. - case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. - case (snd (crbit_for_cond c)); reflexivity. - case (snd (crbit_for_cond c)); reflexivity. - case (snd (crbit_for_cond c)); reflexivity. - case (snd (crbit_for_cond c)); reflexivity. - case (snd (crbit_for_cond c)); reflexivity. -Qed. -Hint Rewrite transl_op_label: labels. - -Remark transl_load_store_label: - forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - addr args k, - (forall c r, is_label lbl (mk1 c r) = false) -> - (forall r1 r2, is_label lbl (mk2 r1 r2) = false) -> - find_label lbl (transl_load_store mk1 mk2 addr args k) = find_label lbl k. -Proof. - intros; unfold transl_load_store. - destruct addr; destruct args; try (destruct args); try (destruct args); - try reflexivity. - case (ireg_eq (ireg_of m) GPR0); intro. - simpl. rewrite H. auto. - case (Int.eq (high_s i) Int.zero). simpl; rewrite H; auto. - simpl; rewrite H; auto. - simpl; rewrite H0; auto. - simpl; rewrite H; auto. - case (ireg_eq (ireg_of m) GPR0); intro; simpl; rewrite H; auto. - case (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto. -Qed. -Hint Rewrite transl_load_store_label: labels. - -Lemma transl_instr_label: - forall f i k, - find_label lbl (transl_instr f i k) = - if Mach.is_label lbl i then Some k else find_label lbl k. -Proof. - intros. generalize (Mach.is_label_correct lbl i). - case (Mach.is_label lbl i); intro. - subst i. simpl. rewrite peq_true. auto. - destruct i; simpl; autorewrite with labels; try reflexivity. - destruct m; rewrite transl_load_store_label; intros; reflexivity. - destruct m; rewrite transl_load_store_label; intros; reflexivity. - destruct s0; reflexivity. - destruct s0; reflexivity. - rewrite peq_false. auto. congruence. - case (snd (crbit_for_cond c)); reflexivity. -Qed. - -Lemma transl_code_label: - forall f c, - find_label lbl (transl_code f c) = - option_map (transl_code f) (Mach.find_label lbl c). -Proof. - induction c; simpl; intros. - auto. rewrite transl_instr_label. - case (Mach.is_label lbl a). reflexivity. - auto. -Qed. - -Lemma transl_find_label: - forall f, - find_label lbl (transl_function f) = - option_map (transl_code f) (Mach.find_label lbl f.(fn_code)). -Proof. - intros. unfold transl_function. simpl. apply transl_code_label. -Qed. - -End TRANSL_LABEL. - -(** A valid branch in a piece of Mach code translates to a valid ``go to'' - transition in the generated PPC code. *) - -Lemma find_label_goto_label: - forall f lbl rs m c' b ofs, - Genv.find_funct_ptr ge b = Some (Internal f) -> - rs PC = Vptr b ofs -> - Mach.find_label lbl f.(fn_code) = Some c' -> - exists rs', - goto_label (transl_function f) lbl rs m = OK rs' m - /\ transl_code_at_pc (rs' PC) b f c' - /\ forall r, r <> PC -> rs'#r = rs#r. -Proof. - intros. - generalize (transl_find_label lbl f). - rewrite H1; simpl. intro. - generalize (label_pos_code_tail lbl (transl_function f) 0 - (transl_code f c') H2). - intros [pos' [A [B C]]]. - exists (rs#PC <- (Vptr b (Int.repr pos'))). - split. unfold goto_label. rewrite A. rewrite H0. auto. - split. rewrite Pregmap.gss. constructor; auto. - rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in B. - auto. omega. - generalize (functions_transl_no_overflow _ _ H). - omega. - intros. apply Pregmap.gso; auto. -Qed. - -(** * Memory properties *) - -(** The PowerPC has no instruction for ``load 8-bit signed integer''. - We show that it can be synthesized as a ``load 8-bit unsigned integer'' - followed by a sign extension. *) - -Remark valid_access_equiv: - forall chunk1 chunk2 m b ofs, - size_chunk chunk1 = size_chunk chunk2 -> - valid_access m chunk1 b ofs -> - valid_access m chunk2 b ofs. -Proof. - intros. inv H0. rewrite H in H3. constructor; auto. -Qed. - -Remark in_bounds_equiv: - forall chunk1 chunk2 m b ofs (A: Set) (a1 a2: A), - size_chunk chunk1 = size_chunk chunk2 -> - (if in_bounds m chunk1 b ofs then a1 else a2) = - (if in_bounds m chunk2 b ofs then a1 else a2). -Proof. - intros. destruct (in_bounds m chunk1 b ofs). - rewrite in_bounds_true. auto. eapply valid_access_equiv; eauto. - destruct (in_bounds m chunk2 b ofs); auto. - elim n. eapply valid_access_equiv with (chunk1 := chunk2); eauto. -Qed. - -Lemma loadv_8_signed_unsigned: - forall m a, - Mem.loadv Mint8signed m a = - option_map (Val.sign_ext 8) (Mem.loadv Mint8unsigned m a). -Proof. - intros. unfold Mem.loadv. destruct a; try reflexivity. - unfold load. rewrite (in_bounds_equiv Mint8signed Mint8unsigned). - destruct (in_bounds m Mint8unsigned b (Int.signed i)); auto. - simpl. - destruct (getN 0 (Int.signed i) (contents (blocks m b))); auto. - simpl. rewrite Int.sign_ext_zero_ext. auto. compute; auto. - auto. -Qed. - -(** Similarly, we show that signed 8- and 16-bit stores can be performed - like unsigned stores. *) - -Lemma storev_8_signed_unsigned: - forall m a v, - Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. -Proof. - intros. unfold storev. destruct a; auto. - unfold store. rewrite (in_bounds_equiv Mint8signed Mint8unsigned). - auto. auto. -Qed. - -Lemma storev_16_signed_unsigned: - forall m a v, - Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. -Proof. - intros. unfold storev. destruct a; auto. - unfold store. rewrite (in_bounds_equiv Mint16signed Mint16unsigned). - auto. auto. -Qed. - -(** * Proof of semantic preservation *) - -(** Semantic preservation is proved using simulation diagrams - of the following form. -<< - st1 --------------- st2 - | | - t| *|t - | | - v v - st1'--------------- st2' ->> - The invariant is the [match_states] predicate below, which includes: -- The PPC code pointed by the PC register is the translation of - the current Mach code sequence. -- Mach register values and PPC register values agree. -*) - -Inductive match_stack: list Machconcr.stackframe -> Prop := - | match_stack_nil: - match_stack nil - | match_stack_cons: forall fb sp ra c s f, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - wt_function f -> - incl c f.(fn_code) -> - transl_code_at_pc ra fb f c -> - match_stack s -> - match_stack (Stackframe fb sp ra c :: s). - -Inductive match_states: Machconcr.state -> PPC.state -> Prop := - | match_states_intro: - forall s fb sp c ms m rs f - (STACKS: match_stack s) - (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) - (WTF: wt_function f) - (INCL: incl c f.(fn_code)) - (AT: transl_code_at_pc (rs PC) fb f c) - (AG: agree ms sp rs), - match_states (Machconcr.State s fb sp c ms m) - (PPC.State rs m) - | match_states_call: - forall s fb ms m rs - (STACKS: match_stack s) - (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = Vptr fb Int.zero) - (ATLR: rs LR = parent_ra s), - match_states (Machconcr.Callstate s fb ms m) - (PPC.State rs m) - | match_states_return: - forall s ms m rs - (STACKS: match_stack s) - (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = parent_ra s), - match_states (Machconcr.Returnstate s ms m) - (PPC.State rs m). - -Lemma exec_straight_steps: - forall s fb sp m1 f c1 rs1 c2 m2 ms2, - match_stack s -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - wt_function f -> - incl c2 f.(fn_code) -> - transl_code_at_pc (rs1 PC) fb f c1 -> - (exists rs2, - exec_straight tge (transl_function f) (transl_code f c1) rs1 m1 (transl_code f c2) rs2 m2 - /\ agree ms2 sp rs2) -> - exists st', - plus step tge (State rs1 m1) E0 st' /\ - match_states (Machconcr.State s fb sp c2 ms2 m2) st'. -Proof. - intros. destruct H4 as [rs2 [A B]]. - exists (State rs2 m2); split. - eapply exec_straight_exec; eauto. - econstructor; eauto. eapply exec_straight_at; eauto. -Qed. - -(** We need to show that, in the simulation diagram, we cannot - take infinitely many Mach transitions that correspond to zero - transitions on the PPC side. Actually, all Mach transitions - correspond to at least one PPC transition, except the - transition from [Machconcr.Returnstate] to [Machconcr.State]. - So, the following integer measure will suffice to rule out - the unwanted behaviour. *) - -Definition measure (s: Machconcr.state) : nat := - match s with - | Machconcr.State _ _ _ _ _ _ => 0%nat - | Machconcr.Callstate _ _ _ _ => 0%nat - | Machconcr.Returnstate _ _ _ => 1%nat - end. - -(** We show the simulation diagram by case analysis on the Mach transition - on the left. Since the proof is large, we break it into one lemma - per transition. *) - -Definition exec_instr_prop (s1: Machconcr.state) (t: trace) (s2: Machconcr.state) : Prop := - forall s1' (MS: match_states s1 s1'), - (exists s2', plus step tge s1' t s2' /\ match_states s2 s2') - \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat. - - -Lemma exec_Mlabel_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) - (m : mem), - exec_instr_prop (Machconcr.State s fb sp (Mlabel lbl :: c) ms m) E0 - (Machconcr.State s fb sp c ms m). -Proof. - intros; red; intros; inv MS. - left; eapply exec_straight_steps; eauto with coqlib. - exists (nextinstr rs); split. - simpl. apply exec_straight_one. reflexivity. reflexivity. - apply agree_nextinstr; auto. -Qed. - -Lemma exec_Mgetstack_prop: - forall (s : list stackframe) (fb : block) (sp : val) (ofs : int) - (ty : typ) (dst : mreg) (c : list Mach.instruction) - (ms : Mach.regset) (m : mem) (v : val), - load_stack m sp ty ofs = Some v -> - exec_instr_prop (Machconcr.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0 - (Machconcr.State s fb sp c (Regmap.set dst v ms) m). -Proof. - intros; red; intros; inv MS. - unfold load_stack in H. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - rewrite (sp_val _ _ _ AG) in H. - assert (NOTE: GPR1 <> GPR0). congruence. - generalize (loadind_correct tge (transl_function f) GPR1 ofs ty - dst (transl_code f c) rs m v H H1 NOTE). - intros [rs2 [EX [RES OTH]]]. - left; eapply exec_straight_steps; eauto with coqlib. - simpl. exists rs2; split. auto. - apply agree_exten_2 with (rs#(preg_of dst) <- v). - auto with ppcgen. - intros. case (preg_eq r0 (preg_of dst)); intro. - subst r0. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso; auto. -Qed. - -Lemma exec_Msetstack_prop: - forall (s : list stackframe) (fb : block) (sp : val) (src : mreg) - (ofs : int) (ty : typ) (c : list Mach.instruction) - (ms : mreg -> val) (m m' : mem), - store_stack m sp ty ofs (ms src) = Some m' -> - exec_instr_prop (Machconcr.State s fb sp (Msetstack src ofs ty :: c) ms m) E0 - (Machconcr.State s fb sp c ms m'). -Proof. - intros; red; intros; inv MS. - unfold store_stack in H. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - rewrite (sp_val _ _ _ AG) in H. - rewrite (preg_val ms sp rs) in H; auto. - assert (NOTE: GPR1 <> GPR0). congruence. - generalize (storeind_correct tge (transl_function f) GPR1 ofs ty - src (transl_code f c) rs m m' H H1 NOTE). - intros [rs2 [EX OTH]]. - left; eapply exec_straight_steps; eauto with coqlib. - exists rs2; split; auto. - apply agree_exten_2 with rs; auto. -Qed. - -Lemma exec_Mgetparam_prop: - forall (s : list stackframe) (fb : block) (f: Mach.function) (sp parent : val) - (ofs : int) (ty : typ) (dst : mreg) (c : list Mach.instruction) - (ms : Mach.regset) (m : mem) (v : val), - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m sp Tint f.(fn_link_ofs) = Some parent -> - load_stack m parent ty ofs = Some v -> - exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0 - (Machconcr.State s fb sp c (Regmap.set dst v ms) m). -Proof. - intros; red; intros; inv MS. - assert (f0 = f) by congruence. subst f0. - set (rs2 := nextinstr (rs#GPR12 <- parent)). - assert (EX1: exec_straight tge (transl_function f) - (transl_code f (Mgetparam ofs ty dst :: c)) rs m - (loadind GPR12 ofs ty dst (transl_code f c)) rs2 m). - simpl. apply exec_straight_one. - simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto with ppcgen. - unfold const_low. rewrite <- (sp_val ms sp rs); auto. - unfold load_stack in H0. simpl chunk_of_type in H0. - rewrite H0. reflexivity. reflexivity. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - unfold load_stack in H1. change parent with rs2#GPR12 in H1. - assert (NOTE: GPR12 <> GPR0). congruence. - generalize (loadind_correct tge (transl_function f) GPR12 ofs ty - dst (transl_code f c) rs2 m v H1 H3 NOTE). - intros [rs3 [EX2 [RES OTH]]]. - left; eapply exec_straight_steps; eauto with coqlib. - exists rs3; split; simpl. - eapply exec_straight_trans; eauto. - apply agree_exten_2 with (rs2#(preg_of dst) <- v). - unfold rs2; auto with ppcgen. - intros. case (preg_eq r0 (preg_of dst)); intro. - subst r0. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso; auto. -Qed. - -Lemma exec_Mop_prop: - forall (s : list stackframe) (fb : block) (sp : val) (op : operation) - (args : list mreg) (res : mreg) (c : list Mach.instruction) - (ms : mreg -> val) (m : mem) (v : val), - eval_operation ge sp op ms ## args m = Some v -> - exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0 - (Machconcr.State s fb sp c (Regmap.set res v ms) m). -Proof. - intros; red; intros; inv MS. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. - left; eapply exec_straight_steps; eauto with coqlib. - simpl. eapply transl_op_correct; auto. - rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. -Qed. - -Lemma exec_Mload_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (chunk : memory_chunk) (addr : addressing) (args : list mreg) - (dst : mreg) (c : list Mach.instruction) (ms : mreg -> val) - (m : mem) (a v : val), - eval_addressing ge sp addr ms ## args = Some a -> - loadv chunk m a = Some v -> - exec_instr_prop (Machconcr.State s fb sp (Mload chunk addr args dst :: c) ms m) - E0 (Machconcr.State s fb sp c (Regmap.set dst v ms) m). -Proof. - intros; red; intros; inv MS. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI; inversion WTI. - assert (eval_addressing tge sp addr ms##args = Some a). - rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. - left; eapply exec_straight_steps; eauto with coqlib; - destruct chunk; simpl; simpl in H6; - (* all cases but Mint8signed *) - try (eapply transl_load_correct; eauto; - intros; simpl; unfold preg_of; rewrite H6; auto). - (* Mint8signed *) - generalize (loadv_8_signed_unsigned m a). - rewrite H0. - caseEq (loadv Mint8unsigned m a); - [idtac | simpl;intros;discriminate]. - intros v' LOAD' EQ. simpl in EQ. injection EQ. intro EQ1. clear EQ. - assert (X1: forall (cst : constant) (r1 : ireg) (rs1 : regset), - exec_instr tge (transl_function f) (Plbz (ireg_of dst) cst r1) rs1 m = - load1 tge Mint8unsigned (preg_of dst) cst r1 rs1 m). - intros. unfold preg_of; rewrite H6. reflexivity. - assert (X2: forall (r1 r2 : ireg) (rs1 : regset), - exec_instr tge (transl_function f) (Plbzx (ireg_of dst) r1 r2) rs1 m = - load2 Mint8unsigned (preg_of dst) r1 r2 rs1 m). - intros. unfold preg_of; rewrite H6. reflexivity. - generalize (transl_load_correct tge (transl_function f) - (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) - Mint8unsigned addr args - (Pextsb (ireg_of dst) (ireg_of dst) :: transl_code f c) - ms sp rs m dst a v' - X1 X2 AG H3 H7 LOAD'). - intros [rs2 [EX1 AG1]]. - exists (nextinstr (rs2#(ireg_of dst) <- v)). - split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. - rewrite <- (ireg_val _ _ _ dst AG1);auto. rewrite Regmap.gss. - rewrite EQ1. reflexivity. reflexivity. - eauto with ppcgen. -Qed. - -Lemma exec_Mstore_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (chunk : memory_chunk) (addr : addressing) (args : list mreg) - (src : mreg) (c : list Mach.instruction) (ms : mreg -> val) - (m m' : mem) (a : val), - eval_addressing ge sp addr ms ## args = Some a -> - storev chunk m a (ms src) = Some m' -> - exec_instr_prop (Machconcr.State s fb sp (Mstore chunk addr args src :: c) ms m) E0 - (Machconcr.State s fb sp c ms m'). -Proof. - intros; red; intros; inv MS. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI; inversion WTI. - rewrite <- (eval_addressing_preserved symbols_preserved) in H. - left; eapply exec_straight_steps; eauto with coqlib. - destruct chunk; simpl; simpl in H6; - try (rewrite storev_8_signed_unsigned in H0); - try (rewrite storev_16_signed_unsigned in H0); - simpl; eapply transl_store_correct; eauto; - intros; unfold preg_of; rewrite H6; reflexivity. -Qed. - -Lemma exec_Mcall_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (sig : signature) (ros : mreg + ident) (c : Mach.code) - (ms : Mach.regset) (m : mem) (f : function) (f' : block) - (ra : int), - find_function_ptr ge ros ms = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - return_address_offset f c ra -> - exec_instr_prop (Machconcr.State s fb sp (Mcall sig ros :: c) ms m) E0 - (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' ms m). -Proof. - intros; red; intros; inv MS. - assert (f0 = f) by congruence. subst f0. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - inv AT. - assert (NOOV: code_size (transl_function f) <= Int.max_unsigned). - eapply functions_transl_no_overflow; eauto. - destruct ros; simpl in H; simpl transl_code in H7. - (* Indirect call *) - generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1. - generalize (code_tail_next_int _ _ _ _ NOOV CT1). intro CT2. - set (rs2 := nextinstr (rs#CTR <- (ms m0))). - set (rs3 := rs2 #LR <- (Val.add rs2#PC Vone) #PC <- (ms m0)). - assert (ATPC: rs3 PC = Vptr f' Int.zero). - change (rs3 PC) with (ms m0). - destruct (ms m0); try discriminate. - generalize H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. - exploit return_address_offset_correct; eauto. constructor; eauto. - intro RA_EQ. - assert (ATLR: rs3 LR = Vptr fb ra). - rewrite RA_EQ. - change (rs3 LR) with (Val.add (Val.add (rs PC) Vone) Vone). - rewrite <- H5. reflexivity. - assert (AG3: agree ms sp rs3). - unfold rs3, rs2; auto 8 with ppcgen. - left; exists (State rs3 m); split. - apply plus_left with E0 (State rs2 m) E0. - econstructor. eauto. apply functions_transl. eexact H0. - eapply find_instr_tail. eauto. - simpl. rewrite <- (ireg_val ms sp rs); auto. - apply star_one. econstructor. - change (rs2 PC) with (Val.add (rs PC) Vone). rewrite <- H5. - simpl. auto. - apply functions_transl. eexact H0. - eapply find_instr_tail. eauto. - simpl. reflexivity. - traceEq. - econstructor; eauto. - econstructor; eauto with coqlib. - rewrite RA_EQ. econstructor; eauto. - (* Direct call *) - generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1. - set (rs2 := rs #LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset tge i Int.zero)). - assert (ATPC: rs2 PC = Vptr f' Int.zero). - change (rs2 PC) with (symbol_offset tge i Int.zero). - unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. - exploit return_address_offset_correct; eauto. constructor; eauto. - intro RA_EQ. - assert (ATLR: rs2 LR = Vptr fb ra). - rewrite RA_EQ. - change (rs2 LR) with (Val.add (rs PC) Vone). - rewrite <- H5. reflexivity. - assert (AG2: agree ms sp rs2). - unfold rs2; auto 8 with ppcgen. - left; exists (State rs2 m); split. - apply plus_one. econstructor. - eauto. - apply functions_transl. eexact H0. - eapply find_instr_tail. eauto. - simpl. reflexivity. - econstructor; eauto with coqlib. - econstructor; eauto with coqlib. - rewrite RA_EQ. econstructor; eauto. -Qed. - -Lemma exec_Mtailcall_prop: - forall (s : list stackframe) (fb stk : block) (soff : int) - (sig : signature) (ros : mreg + ident) (c : list Mach.instruction) - (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block), - find_function_ptr ge ros ms = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> - exec_instr_prop - (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 - (Callstate s f' ms (free m stk)). -Proof. - intros; red; intros; inv MS. - assert (f0 = f) by congruence. subst f0. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - inversion AT. subst b f0 c0. - assert (NOOV: code_size (transl_function f) <= Int.max_unsigned). - eapply functions_transl_no_overflow; eauto. - destruct ros; simpl in H; simpl in H9. - (* Indirect call *) - set (rs2 := nextinstr (rs#CTR <- (ms m0))). - set (rs3 := nextinstr (rs2#GPR12 <- (parent_ra s))). - set (rs4 := nextinstr (rs3#LR <- (parent_ra s))). - set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))). - set (rs6 := rs5#PC <- (rs5 CTR)). - assert (exec_straight tge (transl_function f) - (transl_code f (Mtailcall sig (inl ident m0) :: c)) rs m - (Pbctr :: transl_code f c) rs5 (free m stk)). - simpl. apply exec_straight_step with rs2 m. - simpl. rewrite <- (ireg_val _ _ _ _ AG H6). reflexivity. reflexivity. - apply exec_straight_step with rs3 m. - simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - change (rs2 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. unfold load_stack in H2. simpl in H2. rewrite H2. - reflexivity. discriminate. reflexivity. - apply exec_straight_step with rs4 m. - simpl. reflexivity. reflexivity. - apply exec_straight_one. - simpl. change (rs4 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - unfold load_stack in H1; simpl in H1. - simpl. rewrite H1. reflexivity. reflexivity. - left; exists (State rs6 (free m stk)); split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. - change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone) Vone). - rewrite <- H7; simpl. eauto. - eapply functions_transl; eauto. - eapply find_instr_tail. - repeat (eapply code_tail_next_int; auto). eauto. - simpl. reflexivity. traceEq. - (* match states *) - econstructor; eauto. - assert (AG4: agree ms (Vptr stk soff) rs4). - unfold rs4, rs3, rs2; auto 10 with ppcgen. - assert (AG5: agree ms (parent_sp s) rs5). - unfold rs5. apply agree_nextinstr. - split. reflexivity. intros. inv AG4. rewrite H12. - rewrite Pregmap.gso; auto with ppcgen. - unfold rs6; auto with ppcgen. - change (rs6 PC) with (ms m0). - generalize H. destruct (ms m0); try congruence. - predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. - (* direct call *) - set (rs2 := nextinstr (rs#GPR12 <- (parent_ra s))). - set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). - set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). - set (rs5 := rs4#PC <- (Vptr f' Int.zero)). - assert (exec_straight tge (transl_function f) - (transl_code f (Mtailcall sig (inr mreg i) :: c)) rs m - (Pbs i :: transl_code f c) rs4 (free m stk)). - simpl. apply exec_straight_step with rs2 m. - simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - rewrite <- (sp_val _ _ _ AG). - simpl. unfold load_stack in H2. simpl in H2. rewrite H2. - reflexivity. discriminate. reflexivity. - apply exec_straight_step with rs3 m. - simpl. reflexivity. reflexivity. - apply exec_straight_one. - simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - unfold load_stack in H1; simpl in H1. - simpl. rewrite H1. reflexivity. reflexivity. - left; exists (State rs5 (free m stk)); split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. - change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). - rewrite <- H7; simpl. eauto. - eapply functions_transl; eauto. - eapply find_instr_tail. - repeat (eapply code_tail_next_int; auto). eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. - reflexivity. traceEq. - (* match states *) - econstructor; eauto. - assert (AG3: agree ms (Vptr stk soff) rs3). - unfold rs3, rs2; auto 10 with ppcgen. - assert (AG4: agree ms (parent_sp s) rs4). - unfold rs4. apply agree_nextinstr. - split. reflexivity. intros. inv AG3. rewrite H12. - rewrite Pregmap.gso; auto with ppcgen. - unfold rs5; auto with ppcgen. -Qed. - -Lemma exec_Malloc_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (c : list Mach.instruction) (ms : mreg -> val) (m : mem) (sz : int) - (m' : mem) (blk : block), - ms Conventions.loc_alloc_argument = Vint sz -> - alloc m 0 (Int.signed sz) = (m', blk) -> - exec_instr_prop (Machconcr.State s fb sp (Malloc :: c) ms m) E0 - (Machconcr.State s fb sp c - (Regmap.set (Conventions.loc_alloc_result) (Vptr blk Int.zero) ms) m'). -Proof. - intros; red; intros; inv MS. - left; eapply exec_straight_steps; eauto with coqlib. - simpl. eapply transl_alloc_correct; eauto. -Qed. - -Lemma exec_Mgoto_prop: - forall (s : list stackframe) (fb : block) (f : function) (sp : val) - (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) - (m : mem) (c' : Mach.code), - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl (fn_code f) = Some c' -> - exec_instr_prop (Machconcr.State s fb sp (Mgoto lbl :: c) ms m) E0 - (Machconcr.State s fb sp c' ms m). -Proof. - intros; red; intros; inv MS. - assert (f0 = f) by congruence. subst f0. - inv AT. simpl in H3. - generalize (find_label_goto_label f lbl rs m _ _ _ FIND (sym_equal H1) H0). - intros [rs2 [GOTO [AT2 INV]]]. - left; exists (State rs2 m); split. - apply plus_one. econstructor; eauto. - apply functions_transl; eauto. - eapply find_instr_tail; eauto. - simpl; auto. - econstructor; eauto. - eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs; auto. -Qed. - -Lemma exec_Mcond_true_prop: - forall (s : list stackframe) (fb : block) (f : function) (sp : val) - (cond : condition) (args : list mreg) (lbl : Mach.label) - (c : list Mach.instruction) (ms : mreg -> val) (m : mem) - (c' : Mach.code), - eval_condition cond ms ## args m = Some true -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl (fn_code f) = Some c' -> - exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machconcr.State s fb sp c' ms m). -Proof. - intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inv WTI. - pose (k1 := - if snd (crbit_for_cond cond) - then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c - else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c). - generalize (transl_cond_correct tge (transl_function f) - cond args k1 ms sp rs m true H3 AG H). - simpl. intros [rs2 [EX [RES AG2]]]. - inv AT. simpl in H5. - generalize (functions_transl _ _ H4); intro FN. - generalize (functions_transl_no_overflow _ _ H4); intro NOOV. - exploit exec_straight_steps_2; eauto. - intros [ofs' [PC2 CT2]]. - generalize (find_label_goto_label f lbl rs2 m _ _ _ FIND PC2 H1). - intros [rs3 [GOTO [AT3 INV3]]]. - left; exists (State rs3 m); split. - eapply plus_right'. - eapply exec_straight_steps_1; eauto. - caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES. - econstructor; eauto. - eapply find_instr_tail. unfold k1 in CT2; rewrite ISSET in CT2. eauto. - simpl. rewrite RES. simpl. auto. - econstructor; eauto. - eapply find_instr_tail. unfold k1 in CT2; rewrite ISSET in CT2. eauto. - simpl. rewrite RES. simpl. auto. - traceEq. - econstructor; eauto. - eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs2; auto. -Qed. - -Lemma exec_Mcond_false_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (cond : condition) (args : list mreg) (lbl : Mach.label) - (c : list Mach.instruction) (ms : mreg -> val) (m : mem), - eval_condition cond ms ## args m = Some false -> - exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machconcr.State s fb sp c ms m). -Proof. - intros; red; intros; inv MS. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - pose (k1 := - if snd (crbit_for_cond cond) - then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c - else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c). - generalize (transl_cond_correct tge (transl_function f) - cond args k1 ms sp rs m false H1 AG H). - simpl. intros [rs2 [EX [RES AG2]]]. - left; eapply exec_straight_steps; eauto with coqlib. - exists (nextinstr rs2); split. - simpl. eapply exec_straight_trans. eexact EX. - caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES. - unfold k1; rewrite ISSET; apply exec_straight_one. - simpl. rewrite RES. reflexivity. - reflexivity. - unfold k1; rewrite ISSET; apply exec_straight_one. - simpl. rewrite RES. reflexivity. - reflexivity. - auto with ppcgen. -Qed. - -Lemma exec_Mreturn_prop: - forall (s : list stackframe) (fb stk : block) (soff : int) - (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function), - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> - exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 - (Returnstate s ms (free m stk)). -Proof. - intros; red; intros; inv MS. - assert (f0 = f) by congruence. subst f0. - set (rs2 := nextinstr (rs#GPR12 <- (parent_ra s))). - set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). - set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). - set (rs5 := rs4#PC <- (parent_ra s)). - assert (exec_straight tge (transl_function f) - (transl_code f (Mreturn :: c)) rs m - (Pblr :: transl_code f c) rs4 (free m stk)). - simpl. apply exec_straight_three with rs2 m rs3 m. - simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - unfold load_stack in H1. simpl in H1. - rewrite <- (sp_val _ _ _ AG). simpl. rewrite H1. - reflexivity. discriminate. - unfold rs3. change (parent_ra s) with rs2#GPR12. reflexivity. - simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. - unfold load_stack in H0. simpl in H0. - rewrite H0. reflexivity. - reflexivity. reflexivity. reflexivity. - left; exists (State rs5 (free m stk)); split. - (* execution *) - apply plus_right' with E0 (State rs4 (free m stk)) E0. - eapply exec_straight_exec; eauto. - inv AT. econstructor. - change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). - rewrite <- H3. simpl. eauto. - apply functions_transl; eauto. - generalize (functions_transl_no_overflow _ _ H4); intro NOOV. - simpl in H5. eapply find_instr_tail. - eapply code_tail_next_int; auto. - eapply code_tail_next_int; auto. - eapply code_tail_next_int; eauto. - reflexivity. traceEq. - (* match states *) - econstructor; eauto. - assert (AG3: agree ms (Vptr stk soff) rs3). - unfold rs3, rs2; auto 10 with ppcgen. - assert (AG4: agree ms (parent_sp s) rs4). - split. reflexivity. intros. unfold rs4. - rewrite nextinstr_inv. rewrite Pregmap.gso. - elim AG3; auto. auto with ppcgen. auto with ppcgen. - unfold rs5; auto with ppcgen. -Qed. - -Hypothesis wt_prog: wt_program prog. - -Lemma exec_function_internal_prop: - forall (s : list stackframe) (fb : block) (ms : Mach.regset) - (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block), - Genv.find_funct_ptr ge fb = Some (Internal f) -> - alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) -> - let sp := Vptr stk (Int.repr (- fn_framesize f)) in - store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 -> - store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> - exec_instr_prop (Machconcr.Callstate s fb ms m) E0 - (Machconcr.State s fb sp (fn_code f) ms m3). -Proof. - intros; red; intros; inv MS. - assert (WTF: wt_function f). - generalize (Genv.find_funct_ptr_prop wt_fundef wt_prog H); intro TY. - inversion TY; auto. - exploit functions_transl; eauto. intro TFIND. - generalize (functions_transl_no_overflow _ _ H); intro NOOV. - set (rs2 := nextinstr (rs#GPR1 <- sp #GPR12 <- Vundef)). - set (rs3 := nextinstr (rs2#GPR12 <- (parent_ra s))). - set (rs4 := nextinstr rs3). - (* Execution of function prologue *) - assert (EXEC_PROLOGUE: - exec_straight tge (transl_function f) - (transl_function f) rs m - (transl_code f (fn_code f)) rs4 m3). - unfold transl_function at 2. - apply exec_straight_three with rs2 m2 rs3 m2. - unfold exec_instr. rewrite H0. fold sp. - unfold store_stack in H1. simpl chunk_of_type in H1. - rewrite <- (sp_val _ _ _ AG). rewrite H1. reflexivity. - simpl. change (rs2 LR) with (rs LR). rewrite ATLR. reflexivity. - simpl. unfold store1. rewrite gpr_or_zero_not_zero. - unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR12) with (parent_ra s). - unfold store_stack in H2. simpl chunk_of_type in H2. rewrite H2. reflexivity. - discriminate. reflexivity. reflexivity. reflexivity. - (* Agreement at end of prologue *) - assert (AT4: transl_code_at_pc rs4#PC fb f f.(fn_code)). - change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). - rewrite ATPC. simpl. constructor. auto. - eapply code_tail_next_int; auto. - eapply code_tail_next_int; auto. - eapply code_tail_next_int; auto. - change (Int.unsigned Int.zero) with 0. - unfold transl_function. constructor. - assert (AG2: agree ms sp rs2). - split. reflexivity. - intros. unfold rs2. rewrite nextinstr_inv. - repeat (rewrite Pregmap.gso). elim AG; auto. - auto with ppcgen. auto with ppcgen. auto with ppcgen. - assert (AG4: agree ms sp rs4). - unfold rs4, rs3; auto with ppcgen. - left; exists (State rs4 m3); split. - (* execution *) - eapply exec_straight_steps_1; eauto. - change (Int.unsigned Int.zero) with 0. constructor. - (* match states *) - econstructor; eauto with coqlib. -Qed. - -Lemma exec_function_external_prop: - forall (s : list stackframe) (fb : block) (ms : Mach.regset) - (m : mem) (t0 : trace) (ms' : RegEq.t -> val) - (ef : external_function) (args : list val) (res : val), - Genv.find_funct_ptr ge fb = Some (External ef) -> - event_match ef args t0 res -> - Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> - ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms -> - exec_instr_prop (Machconcr.Callstate s fb ms m) - t0 (Machconcr.Returnstate s ms' m). -Proof. - intros; red; intros; inv MS. - exploit functions_translated; eauto. - intros [tf [A B]]. simpl in B. inv B. - left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs LR)) - m); split. - apply plus_one. eapply exec_step_external; eauto. - eapply extcall_arguments_match; eauto. - econstructor; eauto. - rewrite loc_external_result_match. auto with ppcgen. -Qed. - -Lemma exec_return_prop: - forall (s : list stackframe) (fb : block) (sp ra : val) - (c : Mach.code) (ms : Mach.regset) (m : mem), - exec_instr_prop (Machconcr.Returnstate (Stackframe fb sp ra c :: s) ms m) E0 - (Machconcr.State s fb sp c ms m). -Proof. - intros; red; intros; inv MS. inv STACKS. simpl in *. - right. split. omega. split. auto. - econstructor; eauto. rewrite ATPC; auto. -Qed. - -Theorem transf_instr_correct: - forall s1 t s2, Machconcr.step ge s1 t s2 -> - exec_instr_prop s1 t s2. -Proof - (Machconcr.step_ind ge exec_instr_prop - exec_Mlabel_prop - exec_Mgetstack_prop - exec_Msetstack_prop - exec_Mgetparam_prop - exec_Mop_prop - exec_Mload_prop - exec_Mstore_prop - exec_Mcall_prop - exec_Mtailcall_prop - exec_Malloc_prop - exec_Mgoto_prop - exec_Mcond_true_prop - exec_Mcond_false_prop - exec_Mreturn_prop - exec_function_internal_prop - exec_function_external_prop - exec_return_prop). - -Lemma transf_initial_states: - forall st1, Machconcr.initial_state prog st1 -> - exists st2, PPC.initial_state tprog st2 /\ match_states st1 st2. -Proof. - intros. inversion H. unfold ge0 in *. - econstructor; split. - econstructor. - replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero) - with (Vptr fb Int.zero). - rewrite (Genv.init_mem_transf_partial _ _ TRANSF). - econstructor; eauto. constructor. - split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen. - unfold symbol_offset. - rewrite (transform_partial_program_main _ _ TRANSF). - rewrite symbols_preserved. unfold ge; rewrite H0. auto. -Qed. - -Lemma transf_final_states: - forall st1 st2 r, - match_states st1 st2 -> Machconcr.final_state st1 r -> PPC.final_state st2 r. -Proof. - intros. inv H0. inv H. constructor. auto. - rewrite (ireg_val _ _ _ R3 AG) in H1. auto. auto. -Qed. - -Theorem transf_program_correct: - forall (beh: program_behavior), - Machconcr.exec_program prog beh -> PPC.exec_program tprog beh. -Proof. - unfold Machconcr.exec_program, PPC.exec_program; intros. - eapply simulation_star_preservation with (measure := measure); eauto. - eexact transf_initial_states. - eexact transf_final_states. - exact transf_instr_correct. -Qed. - -End PRESERVATION. |