diff options
Diffstat (limited to 'backend/PPCgenproof.v')
| -rw-r--r-- | backend/PPCgenproof.v | 1242 |
1 files changed, 1242 insertions, 0 deletions
diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v new file mode 100644 index 0000000..d89046f --- /dev/null +++ b/backend/PPCgenproof.v @@ -0,0 +1,1242 @@ +(** Correctness proof for PPC generation: main proof. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Import Op. +Require Import Locations. +Require Import Mach. +Require Import Machtyping. +Require Import PPC. +Require Import PPCgen. +Require Import PPCgenproof1. + +Section PRESERVATION. + +Variable prog: Mach.program. +Variable tprog: PPC.program. +Hypothesis TRANSF: transf_program prog = Some 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_function. + exact TRANSF. +Qed. + +Lemma functions_translated: + forall f b, + Genv.find_funct_ptr ge b = Some f -> + Genv.find_funct_ptr tge b = Some (transl_function f). +Proof. + intros. + generalize (Genv.find_funct_ptr_transf_partial + transf_function TRANSF H). + intros [A B]. + unfold tge. change code with (list instruction). rewrite A. + generalize B. unfold transf_function. + case (zlt Int.max_unsigned (code_size (transl_function f))); intro. + tauto. auto. +Qed. + +Lemma functions_translated_2: + forall f v, + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transl_function f). +Proof. + intros. + generalize (Genv.find_funct_transf_partial + transf_function TRANSF H). + intros [A B]. + unfold tge. change code with (list instruction). rewrite A. + generalize B. unfold transf_function. + case (zlt Int.max_unsigned (code_size (transl_function f))); intro. + tauto. auto. +Qed. + +Lemma functions_translated_no_overflow: + forall b f, + Genv.find_funct_ptr ge b = Some f -> + code_size (transl_function f) <= Int.max_unsigned. +Proof. + intros. + generalize (Genv.find_funct_ptr_transf_partial + transf_function TRANSF H). + intros [A B]. + generalize B. + unfold transf_function. + case (zlt Int.max_unsigned (code_size (transl_function f))); intro. + tauto. 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. + +(** The ``code tail'' of an instruction list [c] is the list of instructions + starting at PC [pos]. *) + +Fixpoint code_tail (pos: Z) (c: code) {struct c} : code := + match c with + | nil => nil + | i :: il => if zeq pos 0 then c else code_tail (pos - 1) il + end. +Proof. + +Lemma find_instr_tail: + forall c pos, + find_instr pos c = + match code_tail pos c with nil => None | i1 :: il => Some i1 end. +Proof. + induction c; simpl; intros. + auto. + case (zeq pos 0); auto. +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. + induction fn; simpl. + intros; discriminate. + intros until c. case (zeq ofs 0); intros. + generalize (code_size_pos fn). omega. + generalize (IHfn _ _ _ H). omega. +Qed. + +Remark code_tail_unfold: + forall ofs i c, + ofs >= 0 -> + code_tail (ofs + 1) (i :: c) = code_tail ofs c. +Proof. + intros. simpl. case (zeq (ofs + 1) 0); intros. + omegaContradiction. + replace (ofs + 1 - 1) with ofs. auto. omega. +Qed. + +Remark code_tail_zero: + forall fn, code_tail 0 fn = fn. +Proof. + intros. destruct fn; simpl. auto. auto. +Qed. + +Lemma code_tail_next: + forall fn ofs i c, + code_tail ofs fn = i :: c -> + code_tail (ofs + 1) fn = c. +Proof. + induction fn. + simpl; intros; discriminate. + intros until c. case (zeq ofs 0); intro. + subst ofs. intros. rewrite code_tail_zero in H. injection H. + intros. subst c. rewrite code_tail_unfold. apply code_tail_zero. + omega. + intro; generalize (code_tail_bounds _ _ _ _ H); intros [A B]. + assert (ofs = (ofs - 1) + 1). omega. + rewrite H0 in H. rewrite code_tail_unfold in H. + rewrite code_tail_unfold. rewrite H0. eauto. + omega. omega. +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. unfold Int.one. + repeat rewrite Int.unsigned_repr. apply code_tail_next with i; auto. + compute; intuition congruence. + generalize (code_tail_bounds _ _ _ _ H0). omega. + compute; intuition congruence. +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 -> Mach.function -> Mach.code -> Prop := + transl_code_at_pc_intro: + forall b ofs f c, + Genv.find_funct_ptr ge b = Some f -> + code_tail (Int.unsigned ofs) (transl_function f) = transl_code c -> + transl_code_at_pc (Vptr b ofs) 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 fn -> + code_tail (Int.unsigned ofs) fn = c -> + exec_steps tge rs m rs' m'. +Proof. + induction 1. + intros. apply exec_refl. + intros. apply exec_trans with rs2 m2. + apply exec_one; econstructor; eauto. + rewrite find_instr_tail. rewrite H5. auto. + 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. +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 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 ofs. split. auto. 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_steps: + forall f c c' rs m rs' m', + transl_code_at_pc (rs PC) f c -> + exec_straight tge (transl_function f) + (transl_code c) rs m (transl_code c') rs' m' -> + exec_steps tge rs m rs' m' /\ transl_code_at_pc (rs' PC) f c'. +Proof. + intros. inversion H. + generalize (functions_translated_no_overflow _ _ H2). intro. + generalize (functions_translated _ _ H2). intro. + split. eapply exec_straight_steps_1; eauto. + generalize (exec_straight_steps_2 _ _ _ _ _ _ _ + H0 H6 _ _ (sym_equal H1) H7 H3). + intros [ofs' [PC' CT']]. + rewrite PC'. constructor; auto. +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. + rewrite zeq_false. replace (pos + 1 - pos - 1) with 0. + apply code_tail_zero. omega. omega. + generalize (code_size_pos c). omega. + intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]]. + exists pos'. split. auto. split. + rewrite zeq_false. replace (pos' - pos - 1) with (pos' - (pos + 1)). + auto. omega. omega. 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 GPR2 (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 GPR2 (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 (mreg_type r); 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 i k, + find_label lbl (transl_instr 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. + rewrite peq_false. auto. congruence. + case (snd (crbit_for_cond c)); reflexivity. +Qed. + +Lemma transl_code_label: + forall c, + find_label lbl (transl_code c) = + option_map transl_code (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 (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 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) 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 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_translated_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. *) + +Lemma loadv_8_signed_unsigned: + forall m a, + Mem.loadv Mint8signed m a = + option_map Val.cast8signed (Mem.loadv Mint8unsigned m a). +Proof. + intros. unfold Mem.loadv. destruct a; try reflexivity. + unfold load. case (zlt b (nextblock m)); intro. + change (in_bounds Mint8unsigned (Int.signed i) (blocks m b)) + with (in_bounds Mint8signed (Int.signed i) (blocks m b)). + case (in_bounds Mint8signed (Int.signed i) (blocks m b)). + change (mem_chunk Mint8unsigned) with (mem_chunk Mint8signed). + set (v := (load_contents (mem_chunk Mint8signed) + (contents (blocks m b)) (Int.signed i))). + unfold Val.load_result. destruct v; try reflexivity. + simpl. rewrite Int.cast8_signed_unsigned. auto. + reflexivity. reflexivity. +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. reflexivity. +Qed. + +Lemma storev_16_signed_unsigned: + forall m a v, + Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. +Proof. + intros. reflexivity. +Qed. + +(** * Proof of semantic preservation *) + +(** The invariants for the inductive proof of simulation are as follows. + The simulation diagrams are of the form: +<< + c1, ms1, m1 --------------------- rs1, m1 + | | + | | + v v + c2, ms2, m2 --------------------- rs2, m2 +>> + Left: execution of one Mach instruction. Right: execution of zero, one + or several instructions. Precondition (top): agreement between + the Mach register set [ms1] and the PPC register set [rs1]; moreover, + [rs1 PC] points to the translation of code [c1]. Postcondition (bottom): + similar. +*) + +Definition exec_instr_prop + (f: Mach.function) (sp: val) + (c1: Mach.code) (ms1: Mach.regset) (m1: mem) + (c2: Mach.code) (ms2: Mach.regset) (m2: mem) := + forall rs1 + (WTF: wt_function f) + (INCL: incl c1 f.(fn_code)) + (AT: transl_code_at_pc (rs1 PC) f c1) + (AG: agree ms1 sp rs1), + exists rs2, + agree ms2 sp rs2 + /\ exec_steps tge rs1 m1 rs2 m2 + /\ transl_code_at_pc (rs2 PC) f c2. + +Definition exec_function_body_prop + (f: Mach.function) (parent: val) (ra: val) + (ms1: Mach.regset) (m1: mem) + (ms2: Mach.regset) (m2: mem) := + forall rs1 + (WTRA: Val.has_type ra Tint) + (RALR: rs1 LR = ra) + (WTF: wt_function f) + (AT: Genv.find_funct ge (rs1 PC) = Some f) + (AG: agree ms1 parent rs1), + exists rs2, + agree ms2 parent rs2 + /\ exec_steps tge rs1 m1 rs2 m2 + /\ rs2 PC = rs1 LR. + +Definition exec_function_prop + (f: Mach.function) (parent: val) + (ms1: Mach.regset) (m1: mem) + (ms2: Mach.regset) (m2: mem) := + forall rs1 + (WTF: wt_function f) + (AT: Genv.find_funct ge (rs1 PC) = Some f) + (AG: agree ms1 parent rs1) + (WTRA: Val.has_type (rs1 LR) Tint), + exists rs2, + agree ms2 parent rs2 + /\ exec_steps tge rs1 m1 rs2 m2 + /\ rs2 PC = rs1 LR. + +(** We show each case of the inductive proof of simulation as a separate + lemma. *) + +Lemma exec_Mlabel_prop: + forall (f : function) (sp : val) (lbl : Mach.label) + (c : list Mach.instruction) (rs : Mach.regset) (m : mem), + exec_instr_prop f sp (Mlabel lbl :: c) rs m c rs m. +Proof. + intros; red; intros. + assert (exec_straight tge (transl_function f) + (transl_code (Mlabel lbl :: c)) rs1 m + (transl_code c) (nextinstr rs1) m). + simpl. apply exec_straight_one. reflexivity. reflexivity. + exists (nextinstr rs1). split. apply agree_nextinstr; auto. + eapply exec_straight_steps; eauto. +Qed. + +Lemma exec_Mgetstack_prop: + forall (f : function) (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 f sp (Mgetstack ofs ty dst :: c) ms m c (Regmap.set dst v ms) m. +Proof. + intros; red; intros. + 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 c) rs1 m v H H1 NOTE). + intros [rs2 [EX [RES OTH]]]. + exists rs2. split. + apply agree_exten_2 with (rs1#(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. + eapply exec_straight_steps; eauto. +Qed. + +Lemma exec_Msetstack_prop: + forall (f : function) (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 f sp (Msetstack src ofs ty :: c) ms m c ms m'. +Proof. + intros; red; intros. + 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 rs1) in H; auto. + assert (NOTE: GPR1 <> GPR0). congruence. + generalize (storeind_correct tge (transl_function f) GPR1 ofs ty + src (transl_code c) rs1 m m' H H2 NOTE). + intros [rs2 [EX OTH]]. + exists rs2. split. + apply agree_exten_2 with rs1; auto. + eapply exec_straight_steps; eauto. +Qed. + +Lemma exec_Mgetparam_prop: + forall (f : function) (sp parent : val) (ofs : int) (ty : typ) + (dst : mreg) (c : list Mach.instruction) (ms : Mach.regset) + (m : mem) (v : val), + load_stack m sp Tint (Int.repr 0) = Some parent -> + load_stack m parent ty ofs = Some v -> + exec_instr_prop f sp (Mgetparam ofs ty dst :: c) ms m c (Regmap.set dst v ms) m. +Proof. + intros; red; intros. + set (rs2 := nextinstr (rs1#GPR2 <- parent)). + assert (EX1: exec_straight tge (transl_function f) + (transl_code (Mgetparam ofs ty dst :: c)) rs1 m + (loadind GPR2 ofs ty dst (transl_code 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 rs1); auto. + unfold load_stack in H. simpl chunk_of_type in H. + rewrite H. reflexivity. reflexivity. + generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). + intro WTI. inversion WTI. + unfold load_stack in H0. change parent with rs2#GPR2 in H0. + assert (NOTE: GPR2 <> GPR0). congruence. + generalize (loadind_correct tge (transl_function f) GPR2 ofs ty + dst (transl_code c) rs2 m v H0 H2 NOTE). + intros [rs3 [EX2 [RES OTH]]]. + exists rs3. split. + 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. + eapply exec_straight_steps; eauto. + eapply exec_straight_trans; eauto. +Qed. + +Lemma exec_straight_exec_prop: + forall f sp c1 rs1 m1 c2 m2 ms', + transl_code_at_pc (rs1 PC) f c1 -> + (exists rs2, + exec_straight tge (transl_function f) + (transl_code c1) rs1 m1 + (transl_code c2) rs2 m2 + /\ agree ms' sp rs2) -> + (exists rs2, + agree ms' sp rs2 + /\ exec_steps tge rs1 m1 rs2 m2 + /\ transl_code_at_pc (rs2 PC) f c2). +Proof. + intros until ms'. intros TRANS1 [rs2 [EX AG]]. + exists rs2. split. assumption. + eapply exec_straight_steps; eauto. +Qed. + +Lemma exec_Mop_prop: + forall (f : function) (sp : val) (op : operation) (args : list mreg) + (res : mreg) (c : list Mach.instruction) (ms: Mach.regset) + (m : mem) (v: val), + eval_operation ge sp op ms ## args = Some v -> + exec_instr_prop f sp (Mop op args res :: c) ms m c (Regmap.set res v ms) m. +Proof. + intros; red; intros. + generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). + intro WTI. + eapply exec_straight_exec_prop; eauto. + simpl. eapply transl_op_correct; auto. + rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. +Qed. + +Lemma exec_Mload_prop: + forall (f : function) (sp : val) (chunk : memory_chunk) + (addr : addressing) (args : list mreg) (dst : mreg) + (c : list Mach.instruction) (ms: Mach.regset) (m : mem) + (a v : val), + eval_addressing ge sp addr ms ## args = Some a -> + loadv chunk m a = Some v -> + exec_instr_prop f sp (Mload chunk addr args dst :: c) ms m c (Regmap.set dst v ms) m. +Proof. + intros; red; intros. + 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. + eapply exec_straight_exec_prop; eauto. + 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 c) + ms sp rs1 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 (f : function) (sp : val) (chunk : memory_chunk) + (addr : addressing) (args : list mreg) (src : mreg) + (c : list Mach.instruction) (ms: Mach.regset) (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 f sp (Mstore chunk addr args src :: c) ms m c ms m'. +Proof. + intros; red; intros. + generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). + intro WTI; inversion WTI. + rewrite <- (eval_addressing_preserved symbols_preserved) in H. + eapply exec_straight_exec_prop; eauto. + destruct chunk; simpl; simpl in H6; + try (rewrite storev_8_signed_unsigned in H); + try (rewrite storev_16_signed_unsigned in H); + simpl; eapply transl_store_correct; eauto; + intros; unfold preg_of; rewrite H6; reflexivity. +Qed. + +Hypothesis wt_prog: wt_program prog. + +Lemma exec_Mcall_prop: + forall (f : function) (sp : val) (sig : signature) + (mos : mreg + ident) (c : list Mach.instruction) (ms : Mach.regset) + (m : mem) (f' : function) (ms' : Mach.regset) (m' : mem), + find_function ge mos ms = Some f' -> + exec_function ge f' sp ms m ms' m' -> + exec_function_prop f' sp ms m ms' m' -> + exec_instr_prop f sp (Mcall sig mos :: c) ms m c ms' m'. +Proof. + intros; red; intros. + generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). + intro WTI. inversion WTI. + inversion AT. + assert (WTF': wt_function f'). + destruct mos; simpl in H. + apply (Genv.find_funct_prop wt_function wt_prog H). + destruct (Genv.find_symbol ge i); try discriminate. + apply (Genv.find_funct_ptr_prop wt_function wt_prog H). + assert (NOOV: code_size (transl_function f) <= Int.max_unsigned). + eapply functions_translated_no_overflow; eauto. + destruct mos; 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 (rs1#CTR <- (ms m0))). + set (rs3 := rs2 #LR <- (Val.add rs2#PC Vone) #PC <- (ms m0)). + assert (TFIND: Genv.find_funct ge (rs3#PC) = Some f'). + unfold rs3. rewrite Pregmap.gss. auto. + assert (AG3: agree ms sp rs3). + unfold rs3, rs2; auto 8 with ppcgen. + assert (WTRA: Val.has_type rs3#LR Tint). + change rs3#LR with (Val.add (Val.add rs1#PC Vone) Vone). + rewrite <- H5. exact I. + generalize (H1 rs3 WTF' TFIND AG3 WTRA). + intros [rs4 [AG4 [EXF' PC4]]]. + exists rs4. split. auto. split. + apply exec_trans with rs2 m. apply exec_one. econstructor. + eauto. apply functions_translated. eexact H6. + rewrite find_instr_tail. rewrite H7. reflexivity. + simpl. rewrite <- (ireg_val ms sp rs1); auto. + apply exec_trans with rs3 m. apply exec_one. econstructor. + unfold rs2, nextinstr. rewrite Pregmap.gss. + rewrite Pregmap.gso. rewrite <- H5. simpl. reflexivity. + discriminate. apply functions_translated. eexact H6. + rewrite find_instr_tail. rewrite CT1. reflexivity. + simpl. replace (rs2 CTR) with (ms m0). reflexivity. + unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss. + auto. discriminate. + exact EXF'. + rewrite PC4. unfold rs3. rewrite Pregmap.gso. rewrite Pregmap.gss. + unfold rs2, nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. + rewrite <- H5. simpl. constructor. auto. auto. + discriminate. discriminate. + (* Direct call *) + caseEq (Genv.find_symbol ge i). intros fblock FINDS. + rewrite FINDS in H. + generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1. + set (rs2 := rs1 #LR <- (Val.add rs1#PC Vone) #PC <- (symbol_offset tge i Int.zero)). + assert (TFIND: Genv.find_funct ge (rs2#PC) = Some f'). + unfold rs2. rewrite Pregmap.gss. + unfold symbol_offset. rewrite symbols_preserved. + rewrite FINDS. + rewrite Genv.find_funct_find_funct_ptr. assumption. + assert (AG2: agree ms sp rs2). + unfold rs2; auto 8 with ppcgen. + assert (WTRA: Val.has_type rs2#LR Tint). + change rs2#LR with (Val.add rs1#PC Vone). + rewrite <- H5. exact I. + generalize (H1 rs2 WTF' TFIND AG2 WTRA). + intros [rs3 [AG3 [EXF' PC3]]]. + exists rs3. split. auto. split. + apply exec_trans with rs2 m. apply exec_one. econstructor. + eauto. apply functions_translated. eexact H6. + rewrite find_instr_tail. rewrite H7. reflexivity. + simpl. reflexivity. + exact EXF'. + rewrite PC3. unfold rs2. rewrite Pregmap.gso. rewrite Pregmap.gss. + rewrite <- H5. simpl. constructor. auto. auto. + discriminate. + intro FINDS. rewrite FINDS in H. discriminate. +Qed. + +Lemma exec_Mgoto_prop: + forall (f : function) (sp : val) (lbl : Mach.label) + (c : list Mach.instruction) (ms : Mach.regset) (m : mem) + (c' : Mach.code), + Mach.find_label lbl (fn_code f) = Some c' -> + exec_instr_prop f sp (Mgoto lbl :: c) ms m c' ms m. +Proof. + intros; red; intros. + inversion AT. + generalize (find_label_goto_label f lbl rs1 m _ _ _ H1 (sym_equal H0) H). + intros [rs2 [GOTO [AT2 INV]]]. + exists rs2. split. apply agree_exten_2 with rs1; auto. + split. inversion AT. apply exec_one. econstructor; eauto. + apply functions_translated; eauto. + rewrite find_instr_tail. rewrite H7. simpl. reflexivity. + simpl. rewrite GOTO. auto. auto. +Qed. + +Lemma exec_Mcond_true_prop: + forall (f : function) (sp : val) (cond : condition) + (args : list mreg) (lbl : Mach.label) (c : list Mach.instruction) + (ms: Mach.regset) (m : mem) (c' : Mach.code), + eval_condition cond ms ## args = Some true -> + Mach.find_label lbl (fn_code f) = Some c' -> + exec_instr_prop f sp (Mcond cond args lbl :: c) ms m c' ms m. +Proof. + intros; red; intros. + 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 c + else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code c). + generalize (transl_cond_correct tge (transl_function f) + cond args k1 ms sp rs1 m true H2 AG H). + simpl. intros [rs2 [EX [RES AG2]]]. + inversion AT. + generalize (functions_translated _ _ H6); intro FN. + generalize (functions_translated_no_overflow _ _ H6); intro NOOV. + simpl in H7. + generalize (exec_straight_steps_2 _ _ _ _ _ _ _ EX + NOOV _ _ (sym_equal H5) FN H7). + intros [ofs' [PC2 CT2]]. + generalize (find_label_goto_label f lbl rs2 m _ _ _ H6 PC2 H0). + intros [rs3 [GOTO [AT3 INV3]]]. + exists rs3. split. + apply agree_exten_2 with rs2; auto. + split. eapply exec_trans. + eapply exec_straight_steps_1; eauto. + caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES. + apply exec_one. econstructor; eauto. + rewrite find_instr_tail. rewrite CT2. unfold k1. rewrite ISSET. reflexivity. + simpl. rewrite RES. simpl. auto. + apply exec_one. econstructor; eauto. + rewrite find_instr_tail. rewrite CT2. unfold k1. rewrite ISSET. reflexivity. + simpl. rewrite RES. simpl. auto. + auto. +Qed. + +Lemma exec_Mcond_false_prop: + forall (f : function) (sp : val) (cond : condition) + (args : list mreg) (lbl : Mach.label) (c : list Mach.instruction) + (ms : Mach.regset) (m : mem), + eval_condition cond ms ## args = Some false -> + exec_instr_prop f sp (Mcond cond args lbl :: c) ms m c ms m. +Proof. + intros; red; intros. + 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 c + else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code c). + generalize (transl_cond_correct tge (transl_function f) + cond args k1 ms sp rs1 m false H1 AG H). + simpl. intros [rs2 [EX [RES AG2]]]. + exists (nextinstr rs2). + split. auto with ppcgen. + eapply exec_straight_steps; eauto. + 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. +Qed. + +Lemma exec_instr_incl: + forall f sp c rs m c' rs' m', + Mach.exec_instr ge f sp c rs m c' rs' m' -> + incl c f.(fn_code) -> incl c' f.(fn_code). +Proof. + induction 1; intros; eauto with coqlib. + eapply incl_find_label; eauto. + eapply incl_find_label; eauto. +Qed. + +Lemma exec_instrs_incl: + forall f sp c rs m c' rs' m', + Mach.exec_instrs ge f sp c rs m c' rs' m' -> + incl c f.(fn_code) -> incl c' f.(fn_code). +Proof. + induction 1; intros. + auto. + eapply exec_instr_incl; eauto. + eauto. +Qed. + +Lemma exec_refl_prop: + forall (f : function) (sp : val) (c : Mach.code) (ms : Mach.regset) + (m : mem), exec_instr_prop f sp c ms m c ms m. +Proof. + intros; red; intros. + exists rs1. split. auto. split. apply exec_refl. auto. +Qed. + +Lemma exec_one_prop: + forall (f : function) (sp : val) (c : Mach.code) (ms : Mach.regset) + (m : mem) (c' : Mach.code) (ms' : Mach.regset) (m' : mem), + Mach.exec_instr ge f sp c ms m c' ms' m' -> + exec_instr_prop f sp c ms m c' ms' m' -> + exec_instr_prop f sp c ms m c' ms' m'. +Proof. + auto. +Qed. + +Lemma exec_trans_prop: + forall (f : function) (sp : val) (c1 : Mach.code) (ms1 : Mach.regset) + (m1 : mem) (c2 : Mach.code) (ms2 : Mach.regset) (m2 : mem) + (c3 : Mach.code) (ms3 : Mach.regset) (m3 : mem), + exec_instrs ge f sp c1 ms1 m1 c2 ms2 m2 -> + exec_instr_prop f sp c1 ms1 m1 c2 ms2 m2 -> + exec_instrs ge f sp c2 ms2 m2 c3 ms3 m3 -> + exec_instr_prop f sp c2 ms2 m2 c3 ms3 m3 -> + exec_instr_prop f sp c1 ms1 m1 c3 ms3 m3. +Proof. + intros; red; intros. + generalize (H0 rs1 WTF INCL AT AG). + intros [rs2 [AG2 [EX2 AT2]]]. + generalize (exec_instrs_incl _ _ _ _ _ _ _ _ H INCL). intro INCL2. + generalize (H2 rs2 WTF INCL2 AT2 AG2). + intros [rs3 [AG3 [EX3 AT3]]]. + exists rs3. split. auto. split. eapply exec_trans; eauto. auto. +Qed. + +Lemma exec_function_body_prop_: + forall (f : function) (parent ra : val) (ms : Mach.regset) (m : mem) + (ms' : Mach.regset) (m1 m2 m3 m4 : mem) (stk : block) + (c : list Mach.instruction), + alloc m (- fn_framesize f) + (align_16_top (- fn_framesize f) (fn_stacksize f)) = (m1, stk) -> + let sp := Vptr stk (Int.repr (- fn_framesize f)) in + store_stack m1 sp Tint (Int.repr 0) parent = Some m2 -> + store_stack m2 sp Tint (Int.repr 4) ra = Some m3 -> + exec_instrs ge f sp (fn_code f) ms m3 (Mreturn :: c) ms' m4 -> + exec_instr_prop f sp (fn_code f) ms m3 (Mreturn :: c) ms' m4 -> + load_stack m4 sp Tint (Int.repr 0) = Some parent -> + load_stack m4 sp Tint (Int.repr 4) = Some ra -> + exec_function_body_prop f parent ra ms m ms' (free m4 stk). +Proof. + intros; red; intros. + generalize (Genv.find_funct_inv AT). intros [b EQPC]. + generalize AT. rewrite EQPC. rewrite Genv.find_funct_find_funct_ptr. intro FN. + generalize (functions_translated_no_overflow _ _ FN); intro NOOV. + set (rs2 := nextinstr (rs1#GPR1 <- sp #GPR2 <- Vundef)). + set (rs3 := nextinstr (rs2#GPR2 <- ra)). + set (rs4 := nextinstr rs3). + assert (exec_straight tge (transl_function f) + (transl_function f) rs1 m + (transl_code (fn_code f)) rs4 m3). + unfold transl_function at 2. + apply exec_straight_three with rs2 m2 rs3 m2. + unfold exec_instr. rewrite H. fold sp. + generalize H0. unfold store_stack. change (Vint (Int.repr 0)) with Vzero. + replace (Val.add sp Vzero) with sp. simpl chunk_of_type. + rewrite (sp_val _ _ _ AG). intro. rewrite H6. clear H6. + reflexivity. unfold sp. simpl. rewrite Int.add_zero. reflexivity. + simpl. replace (rs2 LR) with ra. reflexivity. + simpl. unfold store1. rewrite gpr_or_zero_not_zero. + unfold const_low. replace (rs3 GPR1) with sp. replace (rs3 GPR2) with ra. + unfold store_stack in H1. simpl chunk_of_type in H1. rewrite H1. reflexivity. + reflexivity. reflexivity. discriminate. + reflexivity. reflexivity. reflexivity. + assert (AT2: transl_code_at_pc rs4#PC f f.(fn_code)). + change (rs4 PC) with (Val.add (Val.add (Val.add (rs1 PC) Vone) Vone) Vone). + rewrite EQPC. simpl. constructor. auto. + eapply code_tail_next_int; auto. + eapply code_tail_next_int; auto. + eapply code_tail_next_int; auto. + unfold Int.zero. rewrite Int.unsigned_repr. + rewrite code_tail_zero. unfold transl_function. reflexivity. + compute. intuition congruence. + 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. + generalize (H3 rs4 WTF (incl_refl _) AT2 AG4). + intros [rs5 [AG5 [EXB AT5]]]. + set (rs6 := nextinstr (rs5#GPR2 <- ra)). + set (rs7 := nextinstr (rs6#LR <- ra)). + set (rs8 := nextinstr (rs7#GPR1 <- parent)). + set (rs9 := rs8#PC <- ra). + assert (exec_straight tge (transl_function f) + (transl_code (Mreturn :: c)) rs5 m4 + (Pblr :: transl_code c) rs8 (free m4 stk)). + simpl. apply exec_straight_three with rs6 m4 rs7 m4. + simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. + unfold load_stack in H5. simpl in H5. + rewrite <- (sp_val _ _ _ AG5). simpl. rewrite H5. + reflexivity. discriminate. + unfold rs7. change ra with rs6#GPR2. reflexivity. + unfold exec_instr. generalize H4. unfold load_stack. + replace (Val.add sp (Vint (Int.repr 0))) with sp. + simpl chunk_of_type. intro. change rs7#GPR1 with rs5#GPR1. + rewrite <- (sp_val _ _ _ AG5). rewrite H7. + unfold sp. reflexivity. + unfold sp. simpl. rewrite Int.add_zero. reflexivity. + reflexivity. reflexivity. reflexivity. + exists rs9. split. + (* agreement *) + assert (AG7: agree ms' sp rs7). + unfold rs7, rs6; auto 10 with ppcgen. + assert (AG8: agree ms' parent rs8). + split. reflexivity. intros. unfold rs8. + rewrite nextinstr_inv. rewrite Pregmap.gso. + elim AG7; auto. auto with ppcgen. auto with ppcgen. + unfold rs9; auto with ppcgen. + (* execution *) + split. apply exec_trans with rs4 m3. + eapply exec_straight_steps_1; eauto. + apply functions_translated; auto. + apply exec_trans with rs5 m4. assumption. + inversion AT5. + apply exec_trans with rs8 (free m4 stk). + eapply exec_straight_steps_1; eauto. + apply functions_translated; auto. + apply exec_one. econstructor. + change rs8#PC with (Val.add (Val.add (Val.add rs5#PC Vone) Vone) Vone). + rewrite <- H8. simpl. reflexivity. + apply functions_translated; eauto. + assert (code_tail (Int.unsigned (Int.add (Int.add (Int.add ofs Int.one) Int.one) Int.one)) + (transl_function f) = Pblr :: transl_code c). + eapply code_tail_next_int; auto. + eapply code_tail_next_int; auto. + eapply code_tail_next_int; auto. + rewrite H10. simpl. reflexivity. + rewrite find_instr_tail. rewrite H13. + reflexivity. + reflexivity. + (* LR preservation *) + change rs9#PC with ra. auto. +Qed. + +Lemma exec_function_prop_: + forall (f : function) (parent : val) (ms : Mach.regset) (m : mem) + (ms' : Mach.regset) (m' : mem), + (forall ra : val, + Val.has_type ra Tint -> + exec_function_body ge f parent ra ms m ms' m') -> + (forall ra : val, Val.has_type ra Tint -> + exec_function_body_prop f parent ra ms m ms' m') -> + exec_function_prop f parent ms m ms' m'. +Proof. + intros; red; intros. + apply (H0 rs1#LR WTRA rs1 WTRA (refl_equal _) WTF AT AG). +Qed. + +(** We then conclude by induction on the structure of the Mach +execution derivation. *) + +Theorem transf_function_correct: + forall f parent ms m ms' m', + Mach.exec_function ge f parent ms m ms' m' -> + exec_function_prop f parent ms m ms' m'. +Proof + (Mach.exec_function_ind4 ge + exec_instr_prop exec_instr_prop + exec_function_body_prop exec_function_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_Mgoto_prop + exec_Mcond_true_prop + exec_Mcond_false_prop + exec_refl_prop + exec_one_prop + exec_trans_prop + exec_function_body_prop_ + exec_function_prop_). + +End PRESERVATION. + +Theorem transf_program_correct: + forall (p: Mach.program) (tp: PPC.program) (r: val), + wt_program p -> + transf_program p = Some tp -> + Mach.exec_program p r -> + PPC.exec_program tp r. +Proof. + intros. + destruct H1 as [fptr [f [ms [m [FINDS [FINDF [EX RES]]]]]]]. + assert (WTF: wt_function f). + apply (Genv.find_funct_ptr_prop wt_function H FINDF). + set (ge := Genv.globalenv p) in *. + set (ms0 := Regmap.init Vundef) in *. + set (tge := Genv.globalenv tp). + set (rs0 := + (Pregmap.init Vundef) # PC <- (symbol_offset tge tp.(prog_main) Int.zero) + # LR <- Vzero + # GPR1 <- (Vptr Mem.nullptr Int.zero)). + assert (AT: Genv.find_funct ge (rs0 PC) = Some f). + change (rs0 PC) with (symbol_offset tge tp.(prog_main) Int.zero). + rewrite (transform_partial_program_main _ _ H0). + unfold symbol_offset. rewrite (symbols_preserved p tp H0). + fold ge. rewrite FINDS. + rewrite Genv.find_funct_find_funct_ptr. exact FINDF. + assert (AG: agree ms0 (Vptr Mem.nullptr Int.zero) rs0). + split. reflexivity. intros. unfold rs0. + repeat (rewrite Pregmap.gso; auto with ppcgen). + assert (WTRA: Val.has_type (rs0 LR) Tint). + exact I. + generalize (transf_function_correct p tp H0 H + _ _ _ _ _ _ EX rs0 WTF AT AG WTRA). + intros [rs [AG' [EX' RPC]]]. + red. exists rs; exists m. + split. rewrite (Genv.init_mem_transf_partial _ _ H0). exact EX'. + split. rewrite RPC. reflexivity. rewrite <- RES. + change (IR GPR3) with (preg_of R3). elim AG'; auto. +Qed. |