From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asmgenproof.v | 1229 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1229 insertions(+) create mode 100644 ia32/Asmgenproof.v (limited to 'ia32/Asmgenproof.v') diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v new file mode 100644 index 0000000..ddf2769 --- /dev/null +++ b/ia32/Asmgenproof.v @@ -0,0 +1,1229 @@ +(* *********************************************************************) +(* *) +(* 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 Memory. +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 Conventions. +Require Import Asm. +Require Import Asmgen. +Require Import Asmgenretaddr. +Require Import Asmgenproof1. + +Section PRESERVATION. + +Variable prog: Mach.program. +Variable tprog: Asm.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 fb f tf, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transf_function f = OK tf -> + Genv.find_funct_ptr tge fb = Some (Internal tf). +Proof. + intros. exploit functions_translated; eauto. intros [tf' [A B]]. + monadInv B. rewrite H0 in EQ; inv EQ; auto. +Qed. + +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof. + intros. unfold ge, tge. + apply Genv.find_var_info_transf_partial with transf_fundef. + exact TRANSF. +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_tail_bounds: + forall fn ofs i c, + code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn. +Proof. + assert (forall ofs fn c, code_tail ofs fn c -> + forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn). + induction 1; intros; simpl. + rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega. + rewrite list_length_z_cons. 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, + list_length_z 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. + +Lemma transf_function_no_overflow: + forall f tf, + transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned. +Proof. + intros. monadInv H. destruct (zlt (list_length_z x) Int.max_unsigned); monadInv EQ0. + rewrite list_length_z_cons. omega. +Qed. + +(** [transl_code_at_pc pc fn c] holds if the code pointer [pc] points + within the IA32 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 -> + Asm.code -> Asm.code -> Prop := + transl_code_at_pc_intro: + forall b ofs f c tf tc, + Genv.find_funct_ptr ge b = Some (Internal f) -> + transf_function f = OK tf -> + transl_code f c = OK tc -> + code_tail (Int.unsigned ofs) tf tc -> + transl_code_at_pc (Vptr b ofs) b f c tf tc. + +(** 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' -> + list_length_z 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' -> + list_length_z 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 tf tc c' rs m rs' m', + transl_code_at_pc (rs PC) fb f c tf tc -> + exec_straight tge tf tc rs m c' rs' m' -> + plus step tge (State rs m) E0 (State rs' m'). +Proof. + intros. inv H. + eapply exec_straight_steps_1; eauto. + eapply transf_function_no_overflow; eauto. + eapply functions_transl; eauto. +Qed. + +Lemma exec_straight_at: + forall fb f c tf tc c' tc' rs m rs' m', + transl_code_at_pc (rs PC) fb f c tf tc -> + transl_code f c' = OK tc' -> + exec_straight tge tf tc rs m tc' rs' m' -> + transl_code_at_pc (rs' PC) fb f c' tf tc'. +Proof. + intros. inv H. + exploit exec_straight_steps_2; eauto. + eapply transf_function_no_overflow; eauto. + eapply functions_transl; eauto. + intros [ofs' [PC' CT']]. + rewrite PC'. constructor; auto. +Qed. + +(** Correctness of the return addresses predicted by + [Asmgen.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 tf tc ofs', + transl_code_at_pc (Vptr b ofs) fb f c tf tc -> + return_address_offset f c ofs' -> + ofs' = ofs. +Proof. + intros. inv H0. inv H. + exploit code_tail_unique. eexact H11. eapply H1; eauto. intro. + subst ofs0. 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 + list_length_z 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. + rewrite list_length_z_cons. generalize (list_length_z_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. + rewrite list_length_z_cons. omega. +Qed. + +(** The following lemmas show that the translation from Mach to Asm + preserves labels, in the sense that the following diagram commutes: +<< + translation + Mach code ------------------------ Asm instr sequence + | | + | Mach.find_label lbl find_label lbl | + | | + v v + Mach code tail ------------------- Asm instr seq tail + translation +>> + The proof demands many boring lemmas showing that Asm constructor + functions do not introduce new labels. +*) + +Section TRANSL_LABEL. + +Variable lbl: label. + +Remark mk_mov_label: + forall rd rs k c, mk_mov rd rs k = OK c -> find_label lbl c = find_label lbl k. +Proof. + unfold mk_mov; intros. + destruct rd; try discriminate; destruct rs; inv H; auto. +Qed. + +Remark mk_shift_label: + forall f r1 r2 k c, mk_shift f r1 r2 k = OK c -> + (forall r, is_label lbl (f r) = false) -> + find_label lbl c = find_label lbl k. +Proof. + unfold mk_shift; intros. + destruct (ireg_eq r2 ECX); monadInv H; simpl; rewrite H0; auto. +Qed. + +Remark mk_div_label: + forall f r1 r2 k c, mk_div f r1 r2 k = OK c -> + (forall r, is_label lbl (f r) = false) -> + find_label lbl c = find_label lbl k. +Proof. + unfold mk_div; intros. + destruct (ireg_eq r1 EAX). + destruct (ireg_eq r2 EDX); monadInv H; simpl; rewrite H0; auto. + destruct (ireg_eq r2 EAX); monadInv H; simpl; rewrite H0; auto. +Qed. + +Remark mk_mod_label: + forall f r1 r2 k c, mk_mod f r1 r2 k = OK c -> + (forall r, is_label lbl (f r) = false) -> + find_label lbl c = find_label lbl k. +Proof. + unfold mk_mod; intros. + destruct (ireg_eq r1 EAX). + destruct (ireg_eq r2 EDX); monadInv H; simpl; rewrite H0; auto. + destruct (ireg_eq r2 EDX); monadInv H; simpl; rewrite H0; auto. +Qed. + +Remark mk_shrximm_label: + forall r n k c, mk_shrximm r n k = OK c -> find_label lbl c = find_label lbl k. +Proof. + intros. monadInv H; auto. +Qed. + +Remark mk_intconv_label: + forall f r1 r2 k c, mk_intconv f r1 r2 k = OK c -> + (forall r r', is_label lbl (f r r') = false) -> + find_label lbl c = find_label lbl k. +Proof. + unfold mk_intconv; intros. destruct (low_ireg r2); inv H; simpl; rewrite H0; auto. +Qed. + +Remark mk_smallstore_label: + forall f addr r k c, mk_smallstore f addr r k = OK c -> + (forall r addr, is_label lbl (f r addr) = false) -> + find_label lbl c = find_label lbl k. +Proof. + unfold mk_smallstore; intros. destruct (low_ireg r); monadInv H; simpl; rewrite H0; auto. +Qed. + +Remark loadind_label: + forall base ofs ty dst k c, + loadind base ofs ty dst k = OK c -> + find_label lbl c = find_label lbl k. +Proof. + unfold loadind; intros. destruct ty. + monadInv H; auto. + destruct (preg_of dst); inv H; auto. +Qed. + +Remark storeind_label: + forall base ofs ty src k c, + storeind src base ofs ty k = OK c -> + find_label lbl c = find_label lbl k. +Proof. + unfold storeind; intros. destruct ty. + monadInv H; auto. + destruct (preg_of src); inv H; auto. +Qed. + +Ltac ArgsInv := + match goal with + | [ H: Error _ = OK _ |- _ ] => discriminate + | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args; ArgsInv + | [ H: bind _ _ = OK _ |- _ ] => monadInv H; ArgsInv + | _ => idtac + end. + +Remark transl_cond_label: + forall cond args k c, + transl_cond cond args k = OK c -> + find_label lbl c = find_label lbl k. +Proof. + unfold transl_cond; intros. + destruct cond; ArgsInv; auto. + destruct (Int.eq_dec i Int.zero); auto. + destruct c0; auto. + destruct c0; auto. +Qed. + + +Remark transl_op_label: + forall op args r k c, + transl_op op args r k = OK c -> + find_label lbl c = find_label lbl k. +Proof. + unfold transl_op; intros. destruct op; ArgsInv; auto. + eapply mk_mov_label; eauto. + eapply mk_intconv_label; eauto. + eapply mk_intconv_label; eauto. + eapply mk_intconv_label; eauto. + eapply mk_intconv_label; eauto. + eapply mk_div_label; eauto. + eapply mk_div_label; eauto. + eapply mk_mod_label; eauto. + eapply mk_mod_label; eauto. + eapply mk_shift_label; eauto. + eapply mk_shift_label; eauto. + eapply mk_shrximm_label; eauto. + eapply mk_shift_label; eauto. + eapply trans_eq. eapply transl_cond_label; eauto. auto. +Qed. + +Remark transl_load_label: + forall chunk addr args dest k c, + transl_load chunk addr args dest k = OK c -> + find_label lbl c = find_label lbl k. +Proof. + intros. monadInv H. destruct chunk; monadInv EQ0; auto. +Qed. + +Remark transl_store_label: + forall chunk addr args src k c, + transl_store chunk addr args src k = OK c -> + find_label lbl c = find_label lbl k. +Proof. + intros. monadInv H. destruct chunk; monadInv EQ0; auto; eapply mk_smallstore_label; eauto. +Qed. + +Lemma transl_instr_label: + forall f i k c, + transl_instr f i k = OK c -> + find_label lbl c = 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. monadInv H. simpl. rewrite peq_true. auto. +Opaque loadind. + destruct i; simpl in H. + eapply loadind_label; eauto. + eapply storeind_label; eauto. + monadInv H. eapply trans_eq; eapply loadind_label; eauto. + eapply transl_op_label; eauto. + eapply transl_load_label; eauto. + eapply transl_store_label; eauto. + destruct s0; monadInv H; auto. + destruct s0; monadInv H; auto. + monadInv H; auto. + inv H; simpl. destruct (peq lbl l). congruence. auto. + monadInv H; auto. + eapply trans_eq. eapply transl_cond_label; eauto. auto. + monadInv H; auto. + monadInv H; auto. +Qed. + +Lemma transl_code_label: + forall f c tc, + transl_code f c = OK tc -> + match Mach.find_label lbl c with + | None => find_label lbl tc = None + | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' = OK tc' + end. +Proof. + induction c; simpl; intros. + inv H. auto. + monadInv H. rewrite (transl_instr_label _ _ _ _ EQ0). + destruct (Mach.is_label lbl a). exists x; auto. apply IHc. auto. +Qed. + +Lemma transl_find_label: + forall f tf, + transf_function f = OK tf -> + match Mach.find_label lbl f.(fn_code) with + | None => find_label lbl tf = None + | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c = OK tc + end. +Proof. + intros. monadInv H. destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0. + simpl. apply transl_code_label; auto. +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 tf lbl rs m c' b ofs, + Genv.find_funct_ptr ge b = Some (Internal f) -> + transf_function f = OK tf -> + rs PC = Vptr b ofs -> + Mach.find_label lbl f.(fn_code) = Some c' -> + exists tc', exists rs', + goto_label tf lbl rs m = Next rs' m + /\ transl_code_at_pc (rs' PC) b f c' tf tc' + /\ forall r, r <> PC -> rs'#r = rs#r. +Proof. + intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. + intros [tc [A B]]. + exploit label_pos_code_tail; eauto. instantiate (1 := 0). + intros [pos' [P [Q R]]]. + exists tc; exists (rs#PC <- (Vptr b (Int.repr pos'))). + split. unfold goto_label. rewrite P. rewrite H1. auto. + split. rewrite Pregmap.gss. constructor; auto. + rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in Q. + auto. omega. + generalize (transf_function_no_overflow _ _ H0). omega. + intros. apply Pregmap.gso; 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 tf tc, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transl_code_at_pc ra fb f c tf tc -> + sp <> Vundef -> ra <> Vundef -> + match_stack s -> + match_stack (Stackframe fb sp ra c :: s). + +Inductive match_states: Machconcr.state -> Asm.state -> Prop := + | match_states_intro: + forall s fb sp c ms m m' rs f tf tc + (STACKS: match_stack s) + (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) + (MEXT: Mem.extends m m') + (AT: transl_code_at_pc (rs PC) fb f c tf tc) + (AG: agree ms sp rs), + match_states (Machconcr.State s fb sp c ms m) + (Asm.State rs m') + | match_states_call: + forall s fb ms m m' rs + (STACKS: match_stack s) + (MEXT: Mem.extends m m') + (AG: agree ms (parent_sp s) rs) + (ATPC: rs PC = Vptr fb Int.zero) + (ATLR: rs RA = parent_ra s), + match_states (Machconcr.Callstate s fb ms m) + (Asm.State rs m') + | match_states_return: + forall s ms m m' rs + (STACKS: match_stack s) + (MEXT: Mem.extends m m') + (AG: agree ms (parent_sp s) rs) + (ATPC: rs PC = parent_ra s), + match_states (Machconcr.Returnstate s ms m) + (Asm.State rs m'). + +Lemma exec_straight_steps: + forall s fb f rs1 i c tf tc m1' m2 m2' sp ms2, + match_stack s -> + Mem.extends m2 m2' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transl_code_at_pc (rs1 PC) fb f (i :: c) tf tc -> + (forall k c, transl_instr f i k = OK c -> + exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' /\ agree ms2 sp rs2) -> + exists st', + plus step tge (State rs1 m1') E0 st' /\ + match_states (Machconcr.State s fb sp c ms2 m2) st'. +Proof. + intros. inversion H2. subst. monadInv H7. + exploit H3; eauto. intros [rs2 [A B]]. + exists (State rs2 m2'); split. + eapply exec_straight_exec; eauto. + econstructor; eauto. eapply exec_straight_at; eauto. +Qed. + +Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. +Proof. induction 1; simpl. congruence. auto. Qed. + +Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. +Proof. induction 1; simpl. unfold Vzero. congruence. auto. Qed. + +Lemma lessdef_parent_sp: + forall s v, + match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s. +Proof. + intros. inv H0. auto. exploit parent_sp_def; eauto. tauto. +Qed. + +Lemma lessdef_parent_ra: + forall s v, + match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s. +Proof. + intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. +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 Asm 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; intros. + monadInv H. econstructor; split. apply exec_straight_one. simpl; eauto. auto. + 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. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ AG) in A. + left; eapply exec_straight_steps; eauto. intros. simpl in H0. + exploit loadind_correct; eauto. intros [rs' [P [Q R]]]. + exists rs'; split. eauto. eapply agree_set_mreg; eauto. congruence. +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. + assert (Val.lessdef (ms src) (rs (preg_of src))). eapply preg_val; eauto. + exploit Mem.storev_extends; eauto. intros [m2' [A B]]. + rewrite (sp_val _ _ _ AG) in A. + left; eapply exec_straight_steps; eauto. intros. simpl in H1. + exploit storeind_correct; eauto. intros [rs' [P Q]]. + exists rs'; split. eauto. eapply agree_exten; eauto. +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 (Regmap.set IT1 Vundef ms)) m). +Proof. + intros; red; intros; inv MS. + assert (f0 = f) by congruence. subst f0. + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H0. auto. + intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. + assert (parent' = parent). inv B. auto. simpl in H1. congruence. + subst parent'. + exploit Mem.loadv_extends. eauto. eexact H1. auto. + intros [v' [C D]]. +Opaque loadind. + left; eapply exec_straight_steps; eauto; intros. monadInv H2. + exploit loadind_correct. eexact EQ0. eauto. intros [rs1 [P [Q R]]]. simpl in Q. + exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. + intros [rs2 [S [T U]]]. + exists rs2; split. eapply exec_straight_trans; eauto. + eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. 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 = 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 (undef_op op ms)) m). +Proof. + intros; red; intros; inv MS. + assert (eval_operation tge sp op ms##args = Some v). + rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. + exploit eval_operation_lessdef. eapply preg_vals; eauto. eexact H0. + intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. + left; eapply exec_straight_steps; eauto; intros. simpl in H1. + exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. + exists rs2; split. eauto. + rewrite <- Q in B. + unfold undef_op. + destruct op; try (eapply agree_set_undef_mreg; eauto). eapply agree_set_mreg; eauto. +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 -> + Mem.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 (undef_temps ms)) m). +Proof. + intros; red; intros; inv MS. + assert (eval_addressing tge sp addr ms##args = Some a). + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. + intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. + exploit Mem.loadv_extends; eauto. intros [v' [C D]]. + left; eapply exec_straight_steps; eauto; intros. simpl in H2. + exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. + exists rs2; split. eauto. eapply agree_set_undef_mreg; eauto. congruence. +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 -> + Mem.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 (undef_temps ms) m'). +Proof. + intros; red; intros; inv MS. + assert (eval_addressing tge sp addr ms##args = Some a). + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. + intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. + assert (Val.lessdef (ms src) (rs (preg_of src))). eapply preg_val; eauto. + exploit Mem.storev_extends; eauto. intros [m2' [C D]]. + left; eapply exec_straight_steps; eauto; intros. simpl in H3. + exploit transl_store_correct; eauto. intros [rs2 [P Q]]. + exists rs2; split. eauto. eapply agree_exten_temps; eauto. +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. + inv AT. + assert (NOOV: list_length_z tf <= Int.max_unsigned). + eapply transf_function_no_overflow; eauto. + destruct ros as [rf|fid]; simpl in H; monadInv H5. + (* Indirect call *) + assert (DEST: ms rf = Vptr f' Int.zero). + destruct (ms rf); try discriminate. + generalize (Int.eq_spec i Int.zero); destruct (Int.eq i Int.zero); congruence. + clear H. + generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. + assert (TCA: transl_code_at_pc (Vptr fb (Int.add ofs Int.one)) fb f c tf x). + econstructor; eauto. + exploit return_address_offset_correct; eauto. intros; subst ra. + left; econstructor; split. + apply plus_one. eapply exec_step_internal. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. eauto. + constructor; auto. + econstructor; eauto. eapply agree_sp_def; eauto. congruence. + simpl. eapply agree_exten; eauto. intros. repeat rewrite Pregmap.gso; auto with ppcgen. + exploit ireg_val; eauto. rewrite DEST. intros LD. inv LD. auto. + rewrite <- H2. auto. + (* Direct call *) + generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. + assert (TCA: transl_code_at_pc (Vptr fb (Int.add ofs Int.one)) fb f c tf x). + econstructor; eauto. + exploit return_address_offset_correct; eauto. intros; subst ra. + left; econstructor; split. + apply plus_one. eapply exec_step_internal. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto. + constructor; auto. + econstructor; eauto. eapply agree_sp_def; eauto. congruence. + simpl. eapply agree_exten; eauto. intros. repeat rewrite Pregmap.gso; auto with ppcgen. + rewrite <- H2. auto. +Qed. + +Lemma agree_change_sp: + forall ms sp rs sp', + agree ms sp rs -> sp' <> Vundef -> + agree ms sp' (rs#ESP <- sp'). +Proof. + intros. inv H. split. apply Pregmap.gss. auto. + intros. rewrite Pregmap.gso; auto with ppcgen. +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) m', + 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) -> + Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> + exec_instr_prop + (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 + (Callstate s f' ms m'). +Proof. + intros; red; intros; inv MS. + assert (f0 = f) by congruence. subst f0. + inv AT. + assert (NOOV: list_length_z tf <= Int.max_unsigned). + eapply transf_function_no_overflow; eauto. + rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. + exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. + exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. intros [ra' [C D]]. + exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. + destruct ros as [rf|fid]; simpl in H; monadInv H7. + (* Indirect call *) + assert (DEST: ms rf = Vptr f' Int.zero). + destruct (ms rf); try discriminate. + generalize (Int.eq_spec i Int.zero); destruct (Int.eq i Int.zero); congruence. + clear H. + generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1. + left; econstructor; split. + eapply plus_left. eapply exec_step_internal. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. + apply star_one. eapply exec_step_internal. + transitivity (Val.add rs#PC Vone). auto. rewrite <- H4. simpl. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. eauto. traceEq. + constructor; auto. + apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto. + eapply agree_change_sp; eauto. eapply parent_sp_def; eauto. + rewrite Pregmap.gss. rewrite nextinstr_inv; auto with ppcgen. + repeat rewrite Pregmap.gso; auto with ppcgen. + exploit ireg_val; eauto. rewrite DEST. intros LD. inv LD. auto. + generalize (preg_of_not_ESP rf). rewrite (ireg_of_eq _ _ EQ1). congruence. + (* Direct call *) + generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1. + left; econstructor; split. + eapply plus_left. eapply exec_step_internal. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. + apply star_one. eapply exec_step_internal. + transitivity (Val.add rs#PC Vone). auto. rewrite <- H4. simpl. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. eauto. traceEq. + constructor; auto. + apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto. + eapply agree_change_sp; eauto. eapply parent_sp_def; eauto. + rewrite Pregmap.gss. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. +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. monadInv H4. + exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. + left; exists (State rs' m'); split. + apply plus_one. econstructor; eauto. + eapply functions_transl; eauto. + eapply find_instr_tail; eauto. + simpl; eauto. + econstructor; eauto. + eapply agree_exten; eauto with ppcgen. +Qed. + +Lemma exec_Mbuiltin_prop: + forall (s : list stackframe) (f : block) (sp : val) + (ms : Mach.regset) (m : mem) (ef : external_function) + (args : list mreg) (res : mreg) (b : list Mach.instruction) + (t : trace) (v : val) (m' : mem), + external_call ef ge ms ## args m t v m' -> + exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t + (Machconcr.State s f sp b (Regmap.set res v (undef_temps ms)) m'). +Proof. + intros; red; intros; inv MS. + inv AT. monadInv H3. + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H2); intro NOOV. + exploit external_call_mem_extends; eauto. eapply preg_vals; eauto. + intros [vres' [m2' [A [B [C D]]]]]. + left. econstructor; split. apply plus_one. + eapply exec_step_builtin. eauto. eauto. + eapply find_instr_tail; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. + instantiate (2 := tf); instantiate (1 := x). + unfold nextinstr_nf, nextinstr. rewrite Pregmap.gss. + simpl undef_regs. repeat rewrite Pregmap.gso; auto with ppcgen. + rewrite <- H0. simpl. constructor; auto. + eapply code_tail_next_int; eauto. + apply agree_nextinstr_nf. eapply agree_set_undef_mreg; eauto. + rewrite Pregmap.gss. auto. + intros. repeat rewrite Pregmap.gso; auto with ppcgen. +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 = 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' (undef_temps ms) m). +Proof. + intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros EC. + inv AT. monadInv H5. + exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. + generalize (functions_transl _ _ _ FIND H4); intro FN. + generalize (transf_function_no_overflow _ _ H4); intro NOOV. + exploit exec_straight_steps_2; eauto. + intros [ofs' [PC2 CT2]]. + exploit find_label_goto_label; eauto. + intros [tc' [rs3 [GOTO [AT3 INV3]]]]. + left; exists (State rs3 m'); split. + eapply plus_right'. + eapply exec_straight_steps_1; eauto. + econstructor; eauto. + eapply find_instr_tail. eauto. simpl. rewrite B. eauto. traceEq. + econstructor; eauto. + eapply agree_exten_temps; eauto. intros. rewrite INV3; auto with ppcgen. +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 = Some false -> + exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 + (Machconcr.State s fb sp c (undef_temps ms) m). +Proof. + intros; red; intros; inv MS. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros EC. + left; eapply exec_straight_steps; eauto. intros. simpl in H0. + exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B. eauto. auto. + apply agree_nextinstr. eapply agree_exten_temps; eauto. +Qed. + +Lemma exec_Mjumptable_prop: + forall (s : list stackframe) (fb : block) (f : function) (sp : val) + (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction) + (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label) + (c' : Mach.code), + rs arg = Vint n -> + list_nth_z tbl (Int.signed n) = Some lbl -> + 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 (Mjumptable arg tbl :: c) rs m) E0 + (Machconcr.State s fb sp c' (undef_temps rs) m). +Proof. + intros; red; intros; inv MS. + assert (f0 = f) by congruence. subst f0. + inv AT. monadInv H6. + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H5); intro NOOV. + exploit find_label_goto_label. eauto. eauto. instantiate (2 := rs0#ECX <- Vundef #EDX <- Vundef). + rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen. eauto. eauto. + intros [tc' [rs' [A [B C]]]]. + exploit ireg_val; eauto. rewrite H. intros LD; inv LD. + left; econstructor; split. + apply plus_one. econstructor; eauto. + eapply find_instr_tail; eauto. + simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eauto. + econstructor; eauto. + eapply agree_exten_temps; eauto. intros. rewrite C; auto with ppcgen. + repeat rewrite Pregmap.gso; 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) m', + 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) -> + Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> + exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 + (Returnstate s ms m'). +Proof. + intros; red; intros; inv MS. + assert (f0 = f) by congruence. subst f0. + inv AT. + assert (NOOV: list_length_z tf <= Int.max_unsigned). + eapply transf_function_no_overflow; eauto. + rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. + exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. + exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]]. + exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. + monadInv H6. + exploit code_tail_next_int; eauto. intro CT1. + left; econstructor; split. + eapply plus_left. eapply exec_step_internal. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. + apply star_one. eapply exec_step_internal. + transitivity (Val.add rs#PC Vone). auto. rewrite <- H3. simpl. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. eauto. traceEq. + constructor; auto. + apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto. + eapply agree_change_sp; eauto. eapply parent_sp_def; eauto. +Qed. + +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) -> + Mem.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. + exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. + generalize EQ; intros EQ'. monadInv EQ'. + destruct (zlt (list_length_z x0) Int.max_unsigned); inversion EQ1. clear EQ1. + unfold store_stack in *. + exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + intros [m1' [C D]]. + exploit Mem.storev_extends. eauto. eexact H1. eauto. eauto. + intros [m2' [E F]]. + exploit Mem.storev_extends. eexact F. eauto. eauto. eauto. + intros [m3' [P Q]]. + left; econstructor; split. + apply plus_one. econstructor; eauto. + rewrite <- H4; simpl. eauto. + simpl. rewrite C. simpl in E. rewrite (sp_val _ _ _ AG) in E. rewrite E. + rewrite ATLR. simpl in P. rewrite P. eauto. + econstructor; eauto. + unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with ppcgen. + rewrite ATPC. simpl. constructor; eauto. + subst x. eapply code_tail_next_int. rewrite list_length_z_cons. omega. + constructor. + apply agree_nextinstr. eapply agree_change_sp; eauto. congruence. +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) (m': mem), + Genv.find_funct_ptr ge fb = Some (External ef) -> + external_call ef ge args m t0 res m' -> + Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> + ms' = Regmap.set (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. + exploit extcall_arguments_match; eauto. + intros [args' [C D]]. + exploit external_call_mem_extends; eauto. + intros [res' [m2' [P [Q [R S]]]]]. + left; econstructor; split. + apply plus_one. eapply exec_step_external; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. + unfold loc_external_result. + eapply agree_set_mreg; eauto. + rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gss. auto. + intros. repeat rewrite Pregmap.gso; 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; eauto. +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_Mbuiltin_prop + exec_Mgoto_prop + exec_Mcond_true_prop + exec_Mcond_false_prop + exec_Mjumptable_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, Asm.initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inversion H. unfold ge0 in *. + econstructor; split. + econstructor. + eapply Genv.init_mem_transf_partial; eauto. + replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero) + with (Vptr fb Int.zero). + econstructor; eauto. constructor. apply Mem.extends_refl. + split. auto. unfold parent_sp; congruence. + intros. repeat rewrite Pregmap.gso; auto with ppcgen. + destruct r; simpl; congruence. + unfold symbol_offset. + rewrite (transform_partial_program_main _ _ TRANSF). + rewrite symbols_preserved. unfold ge; rewrite H1. auto. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> Machconcr.final_state st1 r -> Asm.final_state st2 r. +Proof. + intros. inv H0. inv H. constructor. auto. + compute in H1. + generalize (preg_val _ _ _ AX AG). rewrite H1. intros LD; inv LD. auto. +Qed. + +Theorem transf_program_correct: + forall (beh: program_behavior), not_wrong beh -> + Machconcr.exec_program prog beh -> Asm.exec_program tprog beh. +Proof. + unfold Machconcr.exec_program, Asm.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. -- cgit v1.2.3