From 5020a5a07da3fd690f5d171a48d0c73ef48f9430 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 1 Mar 2013 15:32:13 +0000 Subject: Revised Stacking and Asmgen passes and Mach semantics: - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgenproof.v | 1723 ++++++++++++++++++------------------------------- 1 file changed, 630 insertions(+), 1093 deletions(-) (limited to 'powerpc/Asmgenproof.v') diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index de9decbd..6c95744a 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -27,11 +27,9 @@ Require Import Op. Require Import Locations. Require Import Conventions. Require Import Mach. -Require Import Machsem. -Require Import Machtyping. Require Import Asm. Require Import Asmgen. -Require Import Asmgenretaddr. +Require Import Asmgenproof0. Require Import Asmgenproof1. Section PRESERVATION. @@ -67,210 +65,53 @@ Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). Lemma functions_transl: - forall f b, + forall f b tf, Genv.find_funct_ptr ge b = Some (Internal f) -> - Genv.find_funct_ptr tge b = Some (Internal (transl_function f)). + transf_function f = OK tf -> + Genv.find_funct_ptr tge b = Some (Internal tf). 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 (list_length_z (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) -> - list_length_z (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 (list_length_z (transl_function f))); simpl; intro. - congruence. intro; omega. + destruct (functions_translated _ _ H) as [tf' [A B]]. + rewrite A. monadInv B. f_equal. congruence. 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. +Lemma transf_function_no_overflow: + forall f tf, + transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned. 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. - -(** [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' -> - 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. + intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. + omega. 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' -> + forall f c ep tf tc c' rs m rs' m', + transl_code_at_pc ge (rs PC) f c ep tf tc -> + exec_straight tge tf tc rs m c' rs' m' -> plus step tge (State rs m) E0 (State rs' m'). Proof. - intros. inversion H. subst. + intros. inv H. eapply exec_straight_steps_1; eauto. - eapply functions_transl_no_overflow; eauto. - eapply functions_transl; eauto. + eapply transf_function_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'. + forall f c ep tf tc c' ep' tc' rs m rs' m', + transl_code_at_pc ge (rs PC) f c ep tf tc -> + transl_code f c' ep' = OK tc' -> + exec_straight tge tf tc rs m tc' rs' m' -> + transl_code_at_pc ge (rs' PC) f c' ep' tf tc'. 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. 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 - [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. *) @@ -391,119 +232,137 @@ Qed. Hint Rewrite rolm_label: labels. Remark loadind_label: - forall base ofs ty dst k, find_label lbl (loadind base ofs ty dst k) = find_label lbl k. + forall base ofs ty dst k c, + loadind base ofs ty dst k = OK c -> + find_label lbl c = find_label lbl k. Proof. - intros; unfold loadind. - destruct (Int.eq (high_s ofs) Int.zero); destruct ty; autorewrite with labels; auto. + unfold loadind; intros. + destruct ty; destruct (Int.eq (high_s ofs) Int.zero); monadInv H; + autorewrite with labels; auto. Qed. -Hint Rewrite loadind_label: labels. Remark storeind_label: - forall base ofs ty src k, find_label lbl (storeind base src ofs ty k) = find_label lbl k. + forall base ofs ty src k c, + storeind base src ofs ty k = OK c -> + find_label lbl c = find_label lbl k. Proof. - intros; unfold storeind. - destruct (Int.eq (high_s ofs) Int.zero); destruct ty; autorewrite with labels; auto. + unfold storeind; intros. + destruct ty; destruct (Int.eq (high_s ofs) Int.zero); monadInv H; + autorewrite with labels; auto. 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. +Hint Rewrite floatcomp_label: labels. Remark transl_cond_label: - forall cond args k, find_label lbl (transl_cond cond args k) = find_label lbl k. + forall cond args k c, + transl_cond cond args k = OK c -> find_label lbl c = 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_base_label. apply andimm_base_label. + unfold transl_cond; intros; destruct cond; + (destruct args; + [try discriminate | destruct args; + [try discriminate | destruct args; try discriminate]]); + monadInv H; autorewrite with labels; auto. + destruct (Int.eq (high_s i) Int.zero); inv EQ0; autorewrite with labels; auto. + destruct (Int.eq (high_u i) Int.zero); inv EQ0; autorewrite with labels; auto. Qed. -Hint Rewrite transl_cond_label: labels. Remark transl_cond_op_label: - forall c args r k, - find_label lbl (transl_cond_op c args r k) = find_label lbl k. + forall cond args r k c, + transl_cond_op cond args r k = OK c -> find_label lbl c = find_label lbl k. Proof. - intros c args. - unfold transl_cond_op. destruct (classify_condition c args); intros; auto. - autorewrite with labels. destruct (snd (crbit_for_cond c)); auto. + unfold transl_cond_op; intros; destruct (classify_condition cond args); + monadInv H; auto. + erewrite transl_cond_label. 2: eauto. + destruct (snd (crbit_for_cond c0)); auto. Qed. -Hint Rewrite transl_cond_op_label: labels. Remark transl_op_label: - forall op args r k, find_label lbl (transl_op op args r k) = find_label lbl k. + forall op args r k c, + transl_op op args r k = OK c -> find_label lbl c = 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 (symbol_is_small_data i i0); 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. - destruct (mreg_eq m r); reflexivity. + unfold transl_op; intros; destruct op; try (eapply transl_cond_op_label; eauto; fail); + (destruct args; + [try discriminate | destruct args; + [try discriminate | destruct args; try discriminate]]); + try (monadInv H); autorewrite with labels; auto. + destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; auto. + destruct (symbol_is_small_data i i0); auto. + destruct (Int.eq (high_s i) Int.zero); autorewrite with labels; auto. + destruct (Int.eq (high_s i) Int.zero); autorewrite with labels; auto. Qed. -Hint Rewrite transl_op_label: labels. -Remark transl_load_store_label: +Remark transl_memory_access_label: forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - addr args temp k, + addr args temp k c, + transl_memory_access mk1 mk2 addr args temp k = OK c -> (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 temp k) = find_label lbl k. -Proof. - intros; unfold transl_load_store. - destruct addr; destruct args; try (destruct args); try (destruct args); - try reflexivity. - destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto. + find_label lbl c = find_label lbl k. +Proof. + unfold transl_memory_access; intros; destruct addr; + (destruct args; + [try discriminate | destruct args; + [try discriminate | destruct args; try discriminate]]); + monadInv H; autorewrite with labels; auto. + destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H0; auto. + simpl; rewrite H1; auto. + destruct (symbol_is_small_data i i0); simpl; rewrite H0; auto. simpl; rewrite H0; auto. - destruct (symbol_is_small_data i i0); simpl; rewrite H; auto. - simpl; rewrite H; auto. - destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto. + destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H0; 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. + forall f i ep k c, + transl_instr f i ep k = OK c -> + find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. +Proof. + unfold transl_instr, Mach.is_label; intros; destruct i; try (monadInv H); + autorewrite with labels; auto. + eapply loadind_label; eauto. + eapply storeind_label; eauto. + destruct ep. eapply loadind_label; eauto. + monadInv H. transitivity (find_label lbl x); eapply loadind_label; eauto. + eapply transl_op_label; eauto. + destruct m; monadInv H; rewrite (transl_memory_access_label _ _ _ _ _ _ _ EQ0); auto. + destruct m; monadInv H; rewrite (transl_memory_access_label _ _ _ _ _ _ _ EQ0); auto. + destruct s0; monadInv H; auto. + destruct s0; monadInv H; auto. + erewrite transl_cond_label. 2: eauto. destruct (snd (crbit_for_cond c0)); auto. 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). + forall f c ep tc, + transl_code f c ep = 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' false = OK tc' + end. Proof. induction c; simpl; intros. - auto. rewrite transl_instr_label. - case (Mach.is_label lbl a). reflexivity. - auto. + inv H. auto. + monadInv H. rewrite (transl_instr_label _ _ _ _ _ EQ0). + generalize (Mach.is_label_correct lbl a). + destruct (Mach.is_label lbl a); intros. + subst a. simpl in EQ. exists x; auto. + eapply IHc; eauto. 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)). + forall f tf, + transf_function f = OK tf -> + match Mach.find_label lbl f.(Mach.fn_code) with + | None => find_label lbl tf = None + | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc + end. Proof. - intros. unfold transl_function. simpl. apply transl_code_label. + intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. + monadInv EQ. simpl. + eapply transl_code_label; eauto. Qed. End TRANSL_LABEL. @@ -512,28 +371,26 @@ End TRANSL_LABEL. transition in the generated PPC code. *) Lemma find_label_goto_label: - forall f lbl rs m c' b ofs, + 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 rs', - goto_label (transl_function f) lbl rs m = OK rs' m - /\ transl_code_at_pc (rs' PC) b f c' + Mach.find_label lbl f.(Mach.fn_code) = Some c' -> + exists tc', exists rs', + goto_label tf lbl rs m = Next rs' m + /\ transl_code_at_pc ge (rs' PC) f c' false tf tc' /\ 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. + 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 B. - auto. omega. - generalize (functions_transl_no_overflow _ _ H). - omega. + 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. @@ -555,108 +412,92 @@ Qed. - Mach register values and PPC register values agree. *) -Inductive match_stack: list Machsem.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 -> - sp <> Vundef -> - ra <> Vundef -> - match_stack s -> - match_stack (Stackframe fb sp ra c :: s). - -Inductive match_states: Machsem.state -> Asm.state -> Prop := +Inductive match_states: Mach.state -> Asm.state -> Prop := | match_states_intro: - forall s fb sp c ms m rs m' 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) - (MEXT: Mem.extends m m'), - match_states (Machsem.State s fb sp c ms m) + forall s f sp c ep ms m m' rs tf tc ra + (STACKS: match_stack ge s m m' ra sp) + (MEXT: Mem.extends m m') + (AT: transl_code_at_pc ge (rs PC) f c ep tf tc) + (AG: agree ms (Vptr sp Int.zero) rs) + (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra) + (DXP: ep = true -> rs#GPR11 = parent_sp s), + match_states (Mach.State s f (Vptr sp Int.zero) c ms m) (Asm.State rs m') | match_states_call: - forall s fb ms m rs m' - (STACKS: match_stack s) - (AG: agree ms (parent_sp s) rs) + forall s fd ms m m' rs fb + (STACKS: match_stack ge s m m' (rs LR) (Mem.nextblock m)) (MEXT: Mem.extends m m') + (AG: agree ms (parent_sp s) rs) (ATPC: rs PC = Vptr fb Int.zero) - (ATLR: rs LR = parent_ra s), - match_states (Machsem.Callstate s fb ms m) + (FUNCT: Genv.find_funct_ptr ge fb = Some fd) + (WTRA: Val.has_type (rs LR) Tint), + match_states (Mach.Callstate s fd ms m) (Asm.State rs m') | match_states_return: - forall s ms m rs m' - (STACKS: match_stack s) - (AG: agree ms (parent_sp s) rs) + forall s ms m m' rs + (STACKS: match_stack ge s m m' (rs PC) (Mem.nextblock m)) (MEXT: Mem.extends m m') - (ATPC: rs PC = parent_ra s), - match_states (Machsem.Returnstate s ms m) + (AG: agree ms (parent_sp s) rs), + match_states (Mach.Returnstate s ms m) (Asm.State rs m'). Lemma exec_straight_steps: - forall s fb sp m1' f c1 rs1 c2 m2 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) -> + forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 ra, + match_stack ge s m2 m2' ra sp -> Mem.extends m2 m2' -> + retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra -> + transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc -> + (forall k c (TR: transl_instr f i ep k = OK c), + exists rs2, + exec_straight tge tf c rs1 m1' k rs2 m2' + /\ agree ms2 (Vptr sp Int.zero) rs2 + /\ (r11_is_parent ep i = true -> rs2#GPR11 = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ - match_states (Machsem.State s fb sp c2 ms2 m2) st'. + match_states (Mach.State s f (Vptr sp Int.zero) c ms2 m2) st'. Proof. - intros. destruct H4 as [rs2 [A B]]. + intros. inversion H2; subst. monadInv H7. + exploit H3; eauto. intros [rs2 [A [B C]]]. exists (State rs2 m2'); split. - eapply exec_straight_exec; eauto. + eapply exec_straight_exec; eauto. econstructor; eauto. eapply exec_straight_at; eauto. Qed. -Lemma exec_straight_steps_bis: - 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 m2', - Mem.extends m2 m2' - /\ exists rs2, - exec_straight tge (transl_function f) (transl_code f c1) rs1 m1' (transl_code f c2) rs2 m2' - /\ agree ms2 sp rs2) -> +Lemma exec_straight_steps_goto: + forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c' ra, + match_stack ge s m2 m2' ra sp -> + Mem.extends m2 m2' -> + retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra -> + Mach.find_label lbl f.(Mach.fn_code) = Some c' -> + transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc -> + r11_is_parent ep i = false -> + (forall k c (TR: transl_instr f i ep k = OK c), + exists jmp, exists k', exists rs2, + exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' + /\ agree ms2 (Vptr sp Int.zero) rs2 + /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') -> exists st', plus step tge (State rs1 m1') E0 st' /\ - match_states (Machsem.State s fb sp c2 ms2 m2) st'. + match_states (Mach.State s f (Vptr sp Int.zero) c' ms2 m2) st'. Proof. - intros. destruct H4 as [m2' [A B]]. - eapply exec_straight_steps; 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. + intros. inversion H3; subst. monadInv H9. + exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]]. + generalize (functions_transl _ _ _ H7 H8); intro FN. + generalize (transf_function_no_overflow _ _ H8); intro NOOV. + exploit exec_straight_steps_2; eauto. + intros [ofs' [PC2 CT2]]. + exploit find_label_goto_label; eauto. + intros [tc' [rs3 [GOTO [AT' OTH]]]]. + exists (State rs3 m2'); split. + eapply plus_right'. + eapply exec_straight_steps_1; eauto. + econstructor; eauto. + eapply find_instr_tail. eauto. + rewrite C. eexact GOTO. + traceEq. + econstructor; eauto. + apply agree_exten with rs2; auto with asmgen. + congruence. Qed. (** We need to show that, in the simulation diagram, we cannot @@ -667,448 +508,285 @@ Qed. So, the following integer measure will suffice to rule out the unwanted behaviour. *) -Definition measure (s: Machsem.state) : nat := +Definition measure (s: Mach.state) : nat := match s with - | Machsem.State _ _ _ _ _ _ => 0%nat - | Machsem.Callstate _ _ _ _ => 0%nat - | Machsem.Returnstate _ _ _ => 1%nat + | Mach.State _ _ _ _ _ _ => 0%nat + | Mach.Callstate _ _ _ _ => 0%nat + | Mach.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: Machsem.state) (t: trace) (s2: Machsem.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 (Machsem.State s fb sp (Mlabel lbl :: c) ms m) E0 - (Machsem.State s fb sp c ms m). +Remark preg_of_not_GPR11: forall r, negb (mreg_eq r IT1) = true -> IR GPR11 <> preg_of r. 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. + intros. change (IR GPR11) with (preg_of IT1). red; intros. + exploit preg_of_injective; eauto. intros; subst r; discriminate. 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 (Machsem.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0 - (Machsem.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. - exploit Mem.loadv_extends; eauto. intros [v' [A B]]. - rewrite (sp_val _ _ _ AG) in A. - exploit (loadind_correct tge (transl_function f) GPR1 ofs ty dst (transl_code f c) rs m' v'). - auto. auto. congruence. - intros [rs2 [EX [RES OTH]]]. - left; eapply exec_straight_steps; eauto with coqlib. - simpl. exists rs2; split. auto. - apply agree_set_mreg with rs; auto with ppcgen. congruence. -Qed. +(** This is the simulation diagram. We prove it by case analysis on the Mach transition. *) -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 (Machsem.State s fb sp (Msetstack src ofs ty :: c) ms m) E0 - (Machsem.State s fb sp c ms m'). +Theorem step_simulation: + forall S1 t S2, Mach.step ge S1 t S2 -> + 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. Proof. - intros; red; intros; inv MS. - unfold store_stack in H. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inv WTI. - generalize (preg_val ms sp rs src AG). intro. - exploit Mem.storev_extends; eauto. - intros [m2' [A B]]. + induction 1; intros; inv MS. + +- (* Mlabel *) + left; eapply exec_straight_steps; eauto; intros. + monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split. apply agree_nextinstr; auto. simpl; congruence. + +- (* Mgetstack *) + unfold load_stack in H. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. - exploit (storeind_correct tge (transl_function f) GPR1 ofs (mreg_type src) - src (transl_code f c) rs). - eauto. auto. congruence. - intros [rs2 [EX OTH]]. - left; eapply exec_straight_steps; eauto with coqlib. - exists rs2; split; auto. - apply agree_exten with rs; auto with ppcgen. -Qed. + left; eapply exec_straight_steps; eauto. intros. simpl in TR. + exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]]. + exists rs'; split. eauto. + split. eapply agree_set_mreg; eauto with asmgen. congruence. + simpl; congruence. -Lemma exec_Mgetparam_prop: - forall (s : list stackframe) (fb : block) (f: Mach.function) (sp : 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_sp s) -> - load_stack m (parent_sp s) ty ofs = Some v -> - exec_instr_prop (Machsem.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0 - (Machsem.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. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inv WTI. - unfold load_stack in *. simpl in H0. +- (* Msetstack *) + unfold store_stack in H. + assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. + exploit Mem.storev_extends; eauto. intros [m2' [A B]]. + left; eapply exec_straight_steps; eauto. + eapply match_stack_storev; eauto. + eapply retaddr_stored_at_storev; eauto. + rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. + exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]]. + exists rs'; split. eauto. + split. change (undef_setstack rs) with rs. apply agree_exten with rs0; auto with asmgen. + simpl; intros. rewrite Q; auto with asmgen. + +- (* Mgetparam *) + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H. auto. + intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. + exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'. exploit Mem.loadv_extends. eauto. eexact H0. auto. - intros [parent' [A B]]. - exploit Mem.loadv_extends. eauto. eexact H1. - instantiate (1 := (Val.add parent' (Vint ofs))). - inv B. auto. simpl; auto. intros [v' [C D]]. - left; eapply exec_straight_steps; eauto with coqlib. simpl. - set (rs1 := nextinstr (rs#GPR11 <- parent')). - exploit (loadind_correct tge (transl_function f) GPR11 ofs (mreg_type dst) dst (transl_code f c) rs1 m' v'). - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. auto. congruence. - intros [rs2 [U [V W]]]. - exists rs2; split. - apply exec_straight_step with rs1 m'. - simpl. unfold load1. simpl. rewrite gpr_or_zero_not_zero. - rewrite <- (sp_val _ _ _ AG). rewrite A. auto. congruence. auto. - auto. - apply agree_set_mreg with rs1; auto with ppcgen. - unfold rs1. change (IR GPR11) with (preg_of IT1). - apply agree_nextinstr. apply agree_set_mreg with rs; auto with ppcgen. - intros. apply Pregmap.gso; auto with ppcgen. - congruence. -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 (Machsem.State s fb sp (Mop op args res :: c) ms m) E0 - (Machsem.State s fb sp c (Regmap.set res v (undef_op op 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; eauto. - rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. -Qed. - -Remark loadv_8_signed_unsigned: - forall m a v, - Mem.loadv Mint8signed m a = Some v -> - exists v', Mem.loadv Mint8unsigned m a = Some v' /\ v = Val.sign_ext 8 v'. -Proof. - unfold Mem.loadv; intros. destruct a; try congruence. - generalize (Mem.load_int8_signed_unsigned m b (Int.unsigned i)). - rewrite H. destruct (Mem.load Mint8unsigned m b (Int.unsigned i)). - simpl; intros. exists v0; split; congruence. +Opaque loadind. + left; eapply exec_straight_steps; eauto; intros. + destruct ep; simpl in TR. +(* GPR11 contains parent *) + exploit loadind_correct. eexact TR. + instantiate (2 := rs0). rewrite DXP; eauto. congruence. + intros [rs1 [P [Q R]]]. + exists rs1; split. eauto. + split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. + simpl; intros. rewrite R; auto with asmgen. + apply preg_of_not_GPR11; auto. +(* GPR11 does not contain parent *) + monadInv TR. + exploit loadind_correct. eexact EQ0. eauto. congruence. intros [rs1 [P [Q R]]]. simpl in Q. + exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. congruence. + intros [rs2 [S [T U]]]. + exists rs2; split. eapply exec_straight_trans; eauto. + split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto. + instantiate (1 := rs1#GPR11 <- (rs2#GPR11)). intros. + rewrite Pregmap.gso; auto with asmgen. + congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' GPR11). congruence. auto with asmgen. + simpl; intros. rewrite U; auto with asmgen. + apply preg_of_not_GPR11; auto. + +- (* Mop *) + assert (eval_operation tge (Vptr sp0 Int.zero) op rs##args m = Some v). + rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. + exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0. + intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. + left; eapply exec_straight_steps; eauto; intros. simpl in TR. + exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. + exists rs2; split. eauto. split. auto. + simpl. destruct op; try congruence. destruct ep; simpl; try congruence. intros. + rewrite R; auto. apply preg_of_not_GPR11; auto. + +- (* Mload *) + assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##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 TR. + exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. + exists rs2; split. eauto. + split. eapply agree_set_undef_mreg; eauto. congruence. + intros; auto with asmgen. simpl; congruence. -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 (Machsem.State s fb sp (Mload chunk addr args dst :: c) ms m) - E0 (Machsem.State s fb sp c (Regmap.set dst v (undef_temps 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). +- (* Mstore *) + assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##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 and Mfloat64 *) - try (eapply transl_load_correct; eauto; - intros; simpl; unfold preg_of; rewrite H6; auto; fail). - (* Mint8signed *) - exploit loadv_8_signed_unsigned; eauto. intros [v' [LOAD 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. - exploit transl_load_correct; eauto. - intros [rs2 [EX1 AG1]]. - econstructor; split. - eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. eauto. auto. - apply agree_nextinstr. - eapply agree_set_twice_mireg; eauto. - rewrite EQ. apply Val.sign_ext_lessdef. - generalize (ireg_val _ _ _ dst AG1 H6). rewrite Regmap.gss. auto. - (* Mfloat64 *) - exploit Mem.loadv_float64al32; eauto. intros. clear H0. - eapply transl_load_correct; eauto; - intros; simpl; unfold preg_of; rewrite H6; auto. -Qed. - -Lemma storev_8_signed_unsigned: - forall m a v, - Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. -Proof. - intros. unfold Mem.storev. destruct a; auto. - apply Mem.store_signed_unsigned_8. -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 Mem.storev. destruct a; auto. - apply Mem.store_signed_unsigned_16. -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 (Machsem.State s fb sp (Mstore chunk addr args src :: c) ms m) E0 - (Machsem.State s fb sp c (undef_temps ms) m'). -Proof. - intros; red; intros; inv MS. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI; inv WTI. - rewrite <- (eval_addressing_preserved _ _ symbols_preserved) in H. - left; eapply exec_straight_steps_bis; eauto with coqlib. - destruct chunk; simpl; simpl in H6; - try (generalize (Mem.storev_float64al32 _ _ _ _ H0); intros); - try (rewrite storev_8_signed_unsigned in H0); - try (rewrite storev_16_signed_unsigned in H0); - simpl; eapply transl_store_correct; eauto; - (unfold preg_of; rewrite H6; intros; econstructor; eauto). - split. simpl. rewrite H1. eauto. intros; apply Pregmap.gso; auto. - split. simpl. rewrite H1. eauto. intros; apply Pregmap.gso; auto. -Qed. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. + intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. + assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. + exploit Mem.storev_extends; eauto. intros [m2' [C D]]. + left; eapply exec_straight_steps; eauto. + eapply match_stack_storev; eauto. + eapply retaddr_stored_at_storev; eauto. + intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. + exists rs2; split. eauto. + split. eapply agree_exten_temps; eauto. intros; auto with asmgen. + simpl; congruence. -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 (Machsem.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. +- (* Mcall *) inv AT. - assert (NOOV: list_length_z (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. + assert (NOOV: list_length_z tf <= Int.max_unsigned). + eapply transf_function_no_overflow; eauto. + destruct ros as [rf|fid]; simpl in H; monadInv H3. ++ (* Indirect call *) + exploit Genv.find_funct_inv; eauto. intros [bf EQ2]. + rewrite EQ2 in H; rewrite Genv.find_funct_find_funct_ptr in H. + assert (rs0 x0 = Vptr bf Int.zero). + exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto. + generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1. generalize (code_tail_next_int _ _ _ _ NOOV CT1). intro CT2. - assert (P1: ms m0 = Vptr f' Int.zero). - destruct (ms m0); try congruence. - generalize H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. - assert (P2: rs (ireg_of m0) = Vptr f' Int.zero). - generalize (ireg_val _ _ _ m0 AG H3). - rewrite P1. intro. inv H2. auto. - set (rs2 := nextinstr (rs#CTR <- (Vptr f' Int.zero))). - set (rs3 := rs2 #LR <- (Val.add rs2#PC Vone) #PC <- (Vptr f' Int.zero)). - assert (ATPC: rs3 PC = Vptr f' Int.zero). reflexivity. - 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 P2. 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. + assert (TCA: transl_code_at_pc ge (Vptr b (Int.add (Int.add ofs Int.one) Int.one)) f c false tf x). + econstructor; eauto. + left; econstructor; split. + eapply plus_left. eapply exec_step_internal. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. eauto. + apply star_one. eapply exec_step_internal. Simpl. rewrite <- H0; simpl; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. eauto. traceEq. + econstructor; eauto. econstructor; eauto. - econstructor; eauto with coqlib. - rewrite RA_EQ. econstructor; eauto. - eapply agree_sp_def; eauto. congruence. - - (* 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. - eapply agree_sp_def; eauto. congruence. -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 0 f.(fn_stacksize) = Some m' -> - exec_instr_prop - (Machsem.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. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - inversion AT. subst b f0 c0. - assert (NOOV: list_length_z (transl_function f) <= Int.max_unsigned). - eapply functions_transl_no_overflow; eauto. - exploit Mem.free_parallel_extends; eauto. - intros [m2' [FREE' EXT']]. - unfold load_stack in *. simpl in H1; simpl in H2. - exploit Mem.load_extends. eexact MEXT. eexact H1. - intros [parent' [LOAD1 LD1]]. - rewrite (lessdef_parent_sp s parent' STACKS LD1) in LOAD1. - exploit Mem.load_extends. eexact MEXT. eexact H2. - intros [ra' [LOAD2 LD2]]. - rewrite (lessdef_parent_ra s ra' STACKS LD2) in LOAD2. - destruct ros; simpl in H; simpl in H9. - (* Indirect call *) - assert (P1: ms m0 = Vptr f' Int.zero). - destruct (ms m0); try congruence. - generalize H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. - assert (P2: rs (ireg_of m0) = Vptr f' Int.zero). - generalize (ireg_val _ _ _ m0 AG H7). - rewrite P1. intro. inv H11. auto. - set (rs2 := nextinstr (rs#CTR <- (Vptr f' Int.zero))). - set (rs3 := nextinstr (rs2#GPR0 <- (parent_ra s))). - set (rs4 := nextinstr (rs3#LR <- (parent_ra s))). + Simpl. rewrite <- H0; eexact TCA. + change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. + simpl. eapply agree_exten; eauto. intros. Simpl. + Simpl. rewrite <- H0. exact I. ++ (* Direct call *) + destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. + generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1. + assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x). + econstructor; eauto. + 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 FS. eauto. + econstructor; eauto. + econstructor; eauto. + rewrite <- H0. eexact TCA. + change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. + simpl. eapply agree_exten; eauto. intros. Simpl. + auto. + rewrite <- H0. exact I. + +- (* Mtailcall *) + inversion AT; subst. + 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. + assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 GPR1) (Vint (fn_retaddr_ofs f))) = Some ra). +Opaque Int.repr. + erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l. + eapply rsa_contains; eauto. + exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]]. + assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')). + apply match_stack_change_bound with stk. + eapply match_stack_free_left; eauto. + eapply match_stack_free_left; eauto. + eapply match_stack_free_right; eauto. + omega. + apply Z.lt_le_incl. change (Mem.valid_block m'' stk). + eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. + eapply retaddr_stored_at_valid; eauto. + destruct ros as [rf|fid]; simpl in H; monadInv H6. ++ (* Indirect call *) + exploit Genv.find_funct_inv; eauto. intros [bf EQ2]. + rewrite EQ2 in H; rewrite Genv.find_funct_find_funct_ptr in H. + assert (rs0 x0 = Vptr bf Int.zero). + exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto. + set (rs2 := nextinstr (rs0#CTR <- (Vptr bf Int.zero))). + set (rs3 := nextinstr (rs2#GPR0 <- ra)). + set (rs4 := nextinstr (rs3#LR <- ra)). 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'0 - (Pbctr :: transl_code f c) rs5 m2'). - simpl. apply exec_straight_step with rs2 m'0. - simpl. rewrite P2. auto. auto. + assert (exec_straight tge tf + (Pmtctr x0 :: Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0 + :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbctr :: x) + rs0 m'0 + (Pbctr :: x) rs5 m2'). + apply exec_straight_step with rs2 m'0. + simpl. rewrite H6. auto. auto. apply exec_straight_step with rs3 m'0. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - change (rs2 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. rewrite LOAD2. auto. congruence. auto. + change (rs2 GPR1) with (rs0 GPR1). rewrite C. auto. congruence. auto. apply exec_straight_step with rs4 m'0. simpl. reflexivity. reflexivity. apply exec_straight_one. - simpl. change (rs4 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity. + simpl. change (rs4 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG). + rewrite E. reflexivity. reflexivity. left; exists (State rs6 m2'); 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 <- H8; simpl. eauto. + change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone). + rewrite <- H3; 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. apply parent_sp_def; auto. - intros. inv AG4. rewrite Pregmap.gso; auto with ppcgen. - unfold rs6; auto with ppcgen. - (* direct call *) - set (rs2 := nextinstr (rs#GPR0 <- (parent_ra s))). - set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). +Hint Resolve agree_nextinstr agree_set_other: asmgen. + assert (AG4: agree rs (Vptr stk Int.zero) rs4). + unfold rs4, rs3, rs2; auto 10 with asmgen. + assert (AG5: agree rs (parent_sp s) rs5). + unfold rs5. apply agree_nextinstr. eapply agree_change_sp. eauto. + eapply parent_sp_def; eauto. + unfold rs6, rs5; auto 10 with asmgen. + reflexivity. + change (rs6 LR) with ra. eapply retaddr_stored_at_type; eauto. ++ (* Direct call *) + destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. + set (rs2 := nextinstr (rs0#GPR0 <- ra)). + set (rs3 := nextinstr (rs2#LR <- ra)). 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'0 - (Pbs i :: transl_code f c) rs4 m2'). - simpl. apply exec_straight_step with rs2 m'0. + set (rs5 := rs4#PC <- (Vptr bf Int.zero)). + assert (exec_straight tge tf + (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0 + :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid :: x) + rs0 m'0 + (Pbs fid :: x) rs4 m2'). + apply exec_straight_step with rs2 m'0. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - rewrite <- (sp_val _ _ _ AG). - simpl. rewrite LOAD2. auto. discriminate. auto. + rewrite C. auto. congruence. auto. apply exec_straight_step with rs3 m'0. simpl. reflexivity. reflexivity. apply exec_straight_one. - simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. rewrite LOAD1. rewrite FREE'. reflexivity. reflexivity. + simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG). + rewrite E. reflexivity. reflexivity. left; exists (State rs5 m2'); 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 <- H8; simpl. eauto. + change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). + rewrite <- H3; 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. + simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. auto. 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. - apply parent_sp_def; auto. - intros. inv AG3. rewrite Pregmap.gso; auto with ppcgen. - unfold rs5; auto with ppcgen. -Qed. +Hint Resolve agree_nextinstr agree_set_other: asmgen. + assert (AG3: agree rs (Vptr stk Int.zero) rs3). + unfold rs3, rs2; auto 10 with asmgen. + assert (AG4: agree rs (parent_sp s) rs4). + unfold rs4. apply agree_nextinstr. eapply agree_change_sp. eauto. + eapply parent_sp_def; eauto. + unfold rs5; auto 10 with asmgen. + reflexivity. + change (rs5 LR) with ra. eapply retaddr_stored_at_type; eauto. -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 (Machsem.State s f sp (Mbuiltin ef args res :: b) ms m) t - (Machsem.State s f sp b (Regmap.set res v (undef_temps ms)) m'). -Proof. - intros; red; intros; inv MS. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inv WTI. - inv AT. simpl in H3. - generalize (functions_transl _ _ FIND); intro FN. - generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. +- (* Mbuiltin *) + 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. @@ -1116,30 +794,23 @@ Proof. eapply find_instr_tail; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. - econstructor; eauto with coqlib. - unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with ppcgen. - rewrite <- H0. simpl. constructor; auto. - eapply code_tail_next_int; eauto. - apply sym_not_equal. auto with ppcgen. - apply agree_nextinstr. apply agree_set_mreg_undef_temps with rs; auto. - rewrite Pregmap.gss. auto. - intros. repeat rewrite Pregmap.gso; auto with ppcgen. -Qed. + econstructor; eauto. + eapply match_stack_extcall; eauto. + intros; eapply external_call_max_perm; eauto. + instantiate (2 := tf); instantiate (1 := x). + Simpl. rewrite <- H0. simpl. econstructor; eauto. + eapply code_tail_next_int; eauto. + apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. + rewrite Pregmap.gss. auto. + intros. Simpl. + eapply retaddr_stored_at_extcall; eauto. + intros; eapply external_call_max_perm; eauto. + congruence. -Lemma exec_Mannot_prop: - forall (s : list stackframe) (f : block) (sp : val) - (ms : Mach.regset) (m : mem) (ef : external_function) - (args : list Mach.annot_param) (b : list Mach.instruction) - (vargs: list val) (t : trace) (v : val) (m' : mem), - Machsem.annot_arguments ms m sp args vargs -> - external_call ef ge vargs m t v m' -> - exec_instr_prop (Machsem.State s f sp (Mannot ef args :: b) ms m) t - (Machsem.State s f sp b ms m'). -Proof. - intros; red; intros; inv MS. - inv AT. simpl in H3. - generalize (functions_transl _ _ FIND); intro FN. - generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. +- (* Mannot *) + inv AT. monadInv H4. + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H3); intro NOOV. exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. exploit external_call_mem_extends; eauto. intros [vres' [m2' [A [B [C D]]]]]. @@ -1148,373 +819,238 @@ Proof. eapply find_instr_tail; eauto. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. - econstructor; eauto with coqlib. + eapply match_states_intro with (ep := false); eauto with coqlib. + eapply match_stack_extcall; eauto. + intros; eapply external_call_max_perm; eauto. unfold nextinstr. rewrite Pregmap.gss. - rewrite <- H1; simpl. econstructor; auto. + rewrite <- H1; simpl. econstructor; eauto. eapply code_tail_next_int; eauto. apply agree_nextinstr. auto. -Qed. + eapply retaddr_stored_at_extcall; eauto. + intros; eapply external_call_max_perm; eauto. + congruence. -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 (Machsem.State s fb sp (Mgoto lbl :: c) ms m) E0 - (Machsem.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. +- (* Mgoto *) + inv AT. monadInv H3. + exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. + left; exists (State rs' m'); split. apply plus_one. econstructor; eauto. - apply functions_transl; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl; auto. - econstructor; eauto. - eapply Mach.find_label_incl; eauto. - apply agree_exten with rs; 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 m = Some true -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl (fn_code f) = Some c' -> - exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machsem.State s fb sp c' (undef_temps 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). - exploit transl_cond_correct; eauto. - 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. + simpl; eauto. 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_undef_temps with rs2; 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 m = Some false -> - exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machsem.State s fb sp c (undef_temps ms) m). -Proof. - intros; red; intros; inv MS. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - exploit transl_cond_correct; eauto. - 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. - apply exec_straight_one. simpl. rewrite RES. reflexivity. - reflexivity. - apply exec_straight_one. simpl. rewrite RES. reflexivity. - reflexivity. - apply agree_nextinstr. apply agree_undef_temps with rs2; auto. -Qed. + eapply agree_exten; eauto with asmgen. + congruence. -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.unsigned n) = Some lbl -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl (fn_code f) = Some c' -> - exec_instr_prop - (Machsem.State s fb sp (Mjumptable arg tbl :: c) rs m) E0 - (Machsem.State s fb sp c' (undef_temps rs) 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. - exploit list_nth_z_range; eauto. intro RANGE. - assert (SHIFT: Int.unsigned (Int.rolm n (Int.repr 2) (Int.repr (-4))) = Int.unsigned n * 4). - replace (Int.repr (-4)) with (Int.shl Int.mone (Int.repr 2)). - rewrite <- Int.shl_rolm. rewrite Int.shl_mul. - unfold Int.mul. apply Int.unsigned_repr. omega. - compute. reflexivity. - apply Int.mkint_eq. compute. reflexivity. - inv AT. simpl in H7. - set (k1 := Pbtbl GPR12 tbl :: transl_code f c). - set (rs1 := nextinstr (rs0 # GPR12 <- (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))))). - generalize (functions_transl _ _ H4); intro FN. - generalize (functions_transl_no_overflow _ _ H4); intro NOOV. - assert (exec_straight tge (transl_function f) - (Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: k1) rs0 m' - k1 rs1 m'). - apply exec_straight_one. - simpl. generalize (ireg_val _ _ _ arg AG H5). rewrite H. intro. inv H8. - reflexivity. reflexivity. - exploit exec_straight_steps_2; eauto. - intros [ofs' [PC1 CT1]]. - set (rs2 := rs1 # GPR12 <- Vundef # CTR <- Vundef). - assert (PC2: rs2 PC = Vptr fb ofs'). rewrite <- PC1. reflexivity. - generalize (find_label_goto_label f lbl rs2 m' _ _ _ FIND PC2 H2). - intros [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. unfold k1 in CT1. eauto. - unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen. - change (rs1 GPR12) with (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))). - lazy iota beta. rewrite SHIFT. rewrite Z_mod_mult. rewrite zeq_true. - rewrite Z_div_mult. - change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq. +- (* Mcond true *) + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. + left; eapply exec_straight_steps_goto; eauto. + intros. simpl in TR. + destruct (transl_cond_correct_1 tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. + rewrite EC in B. + destruct (snd (crbit_for_cond cond)). + (* Pbt, taken *) + econstructor; econstructor; econstructor; split. eexact A. + split. eapply agree_exten_temps; eauto with asmgen. + simpl. rewrite B. reflexivity. + (* Pbf, taken *) + econstructor; econstructor; econstructor; split. eexact A. + split. eapply agree_exten_temps; eauto with asmgen. + simpl. rewrite B. reflexivity. + +- (* Mcond false *) + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. + left; eapply exec_straight_steps; eauto. intros. simpl in TR. + destruct (transl_cond_correct_1 tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. + rewrite EC in B. + econstructor; split. + eapply exec_straight_trans. eexact A. + destruct (snd (crbit_for_cond cond)). + apply exec_straight_one. simpl. rewrite B. reflexivity. auto. + apply exec_straight_one. simpl. rewrite B. reflexivity. auto. + split. eapply agree_exten_temps; eauto with asmgen. + intros; Simpl. + simpl. congruence. + +- (* Mjumptable *) + inv AT. monadInv H5. + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H4); intro NOOV. + exploit find_label_goto_label. eauto. eauto. + instantiate (2 := rs0#GPR12 <- Vundef #CTR <- Vundef). + Simpl. 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 <- H8. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. econstructor; eauto. - eapply Mach.find_label_incl; eauto. - apply agree_undef_temps with rs0; auto. - intros. rewrite INV3; auto with ppcgen. - unfold rs2. repeat rewrite Pregmap.gso; auto with ppcgen. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. - apply Pregmap.gso; auto with ppcgen. -Qed. + eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simpl. + congruence. -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 0 f.(fn_stacksize) = Some m' -> - exec_instr_prop (Machsem.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. - exploit Mem.free_parallel_extends; eauto. - intros [m2' [FREE' EXT']]. - unfold load_stack in *. simpl in H0; simpl in H1. - exploit Mem.load_extends. eexact MEXT. eexact H0. - intros [parent' [LOAD1 LD1]]. - rewrite (lessdef_parent_sp s parent' STACKS LD1) in LOAD1. - exploit Mem.load_extends. eexact MEXT. eexact H1. - intros [ra' [LOAD2 LD2]]. - rewrite (lessdef_parent_ra s ra' STACKS LD2) in LOAD2. - set (rs2 := nextinstr (rs#GPR0 <- (parent_ra s))). - set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). +- (* Mreturn *) + inversion AT; subst. + 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 H. auto. simpl. intros [parent' [A B]]. + exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. + assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 GPR1) (Vint (fn_retaddr_ofs f))) = Some ra). +Opaque Int.repr. + erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l. + eapply rsa_contains; eauto. + exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]]. + assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')). + apply match_stack_change_bound with stk. + eapply match_stack_free_left; eauto. + eapply match_stack_free_left; eauto. + eapply match_stack_free_right; eauto. omega. + apply Z.lt_le_incl. change (Mem.valid_block m'' stk). + eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. + eapply retaddr_stored_at_valid; eauto. + monadInv H5. + set (rs2 := nextinstr (rs0#GPR0 <- ra)). + set (rs3 := nextinstr (rs2#LR <- ra)). 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'0 - (Pblr :: transl_code f c) rs4 m2'). + set (rs5 := rs4#PC <- ra). + assert (exec_straight tge tf + (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 + :: Pmtlr GPR0 + :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pblr :: x) rs0 m'0 + (Pblr :: x) rs4 m2'). simpl. apply exec_straight_three with rs2 m'0 rs3 m'0. - simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - rewrite <- (sp_val _ _ _ AG). simpl. rewrite LOAD2. - reflexivity. discriminate. - unfold rs3. reflexivity. - simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. rewrite LOAD1. rewrite FREE'. reflexivity. - reflexivity. reflexivity. reflexivity. + simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. rewrite C. auto. congruence. + simpl. auto. + simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A. + rewrite <- (sp_val _ _ _ AG). rewrite E. auto. + auto. auto. auto. left; exists (State rs5 m2'); split. (* execution *) apply plus_right' with E0 (State rs4 m2') 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 <- H4. simpl. eauto. - apply functions_transl; eauto. - generalize (functions_transl_no_overflow _ _ H5); intro NOOV. - simpl in H6. eapply find_instr_tail. + econstructor. + change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). + rewrite <- H2. simpl. eauto. + eapply functions_transl; eauto. + 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. apply parent_sp_def; auto. 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) -> - Mem.alloc m 0 (fn_stacksize f) = (m1, stk) -> - let sp := Vptr stk Int.zero 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 (Machsem.Callstate s fb ms m) E0 - (Machsem.State s fb sp (fn_code f) (undef_temps 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. - unfold store_stack in *; simpl in *. - exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. - intros [m1' [ALLOC' MEXT1]]. - exploit Mem.store_within_extends. eexact MEXT1. eexact H1. auto. - intros [m2' [STORE2 MEXT2]]. - exploit Mem.store_within_extends. eexact MEXT2. eexact H2. auto. - intros [m3' [STORE3 MEXT3]]. - set (rs2 := nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)). - set (rs3 := nextinstr (rs2#GPR0 <- (parent_ra s))). - set (rs4 := nextinstr rs3). + assert (AG3: agree rs (Vptr stk Int.zero) rs3). + unfold rs3, rs2; auto 10 with asmgen. + assert (AG4: agree rs (parent_sp s) rs4). + unfold rs4. apply agree_nextinstr. eapply agree_change_sp; eauto. + eapply parent_sp_def; eauto. + unfold rs5; auto with asmgen. + +- (* internal function *) + exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. + generalize EQ; intros EQ'. monadInv EQ'. + destruct (zlt Int.max_unsigned (list_length_z x0)); inversion EQ1. clear EQ1. + unfold store_stack in *. + exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + intros [m1' [C D]]. + assert (E: Mem.extends m2 m1') by (eapply Mem.free_left_extends; eauto). + exploit Mem.storev_extends. eexact E. eexact H1. eauto. eauto. + intros [m2' [F G]]. + exploit retaddr_stored_at_can_alloc. eexact H. eauto. eauto. eauto. eauto. + auto. auto. auto. auto. eauto. + intros [m3' [P [Q R]]]. (* Execution of function prologue *) + monadInv EQ0. + set (rs2 := nextinstr (rs0#GPR1 <- sp #GPR0 <- Vundef)). + set (rs3 := nextinstr (rs2#GPR0 <- (rs0#LR))). + set (rs4 := nextinstr rs3). 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. + exec_straight tge x + x rs0 m' + x1 rs4 m3'). + rewrite <- H5 at 2. apply exec_straight_three with rs2 m2' rs3 m2'. - unfold exec_instr. rewrite ALLOC'. fold sp. - rewrite <- (sp_val _ _ _ AG). unfold sp; simpl; rewrite STORE2. reflexivity. - simpl. change (rs2 LR) with (rs LR). rewrite ATLR. reflexivity. + unfold exec_instr. rewrite C. fold sp. + rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. + simpl. auto. simpl. unfold store1. rewrite gpr_or_zero_not_zero. - unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR0) with (parent_ra s). - simpl. rewrite STORE3. 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. unfold sp. congruence. - intros. unfold rs2. rewrite nextinstr_inv. - repeat (rewrite Pregmap.gso). inv AG; auto. - auto with ppcgen. auto with ppcgen. auto with ppcgen. - assert (AG4: agree ms sp rs4). - unfold rs4, rs3; auto with ppcgen. + change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). simpl. + rewrite Int.add_zero_l. rewrite P. auto. congruence. + auto. auto. auto. 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. apply agree_undef_temps with rs4; auto. -Qed. + eapply exec_straight_steps_1; eauto. unfold fn_code; omega. constructor. + econstructor; eauto. + assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto). + rewrite <- STK in STACKS. simpl in F. simpl in H1. + eapply match_stack_invariant; eauto. + intros. eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_free_3; eauto. + eapply Mem.perm_store_2; eauto. unfold block; omega. + intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. + eapply Mem.perm_alloc_1; eauto. + intros. erewrite Mem.load_store_other. 2: eauto. + erewrite Mem.load_store_other. 2: eauto. + eapply Mem.load_alloc_other; eauto. + left; unfold block; omega. + left; unfold block; omega. + change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). + rewrite ATPC. simpl. constructor; eauto. + subst x. unfold fn_code. eapply code_tail_next_int. omega. + eapply code_tail_next_int. omega. + eapply code_tail_next_int. omega. + constructor. + unfold rs4, rs3, rs2. + apply agree_nextinstr. apply agree_set_other; auto. apply agree_set_other; auto. + apply agree_nextinstr. apply agree_set_other; auto. + eapply agree_change_sp; eauto. apply agree_exten_temps with rs0; eauto. + unfold sp; congruence. + congruence. -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' -> - Machsem.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> - ms' = Regmap.set (loc_result (ef_sig ef)) res ms -> - exec_instr_prop (Machsem.Callstate s fb ms m) - t0 (Machsem.Returnstate s ms' m'). -Proof. - intros; red; intros; inv MS. +- (* external function *) exploit functions_translated; eauto. - intros [tf [A B]]. simpl in B. inv B. + intros [tf [A B]]. simpl in B. inv B. exploit extcall_arguments_match; eauto. intros [args' [C D]]. - exploit external_call_mem_extends; eauto. + exploit external_call_mem_extends; eauto. intros [res' [m2' [P [Q [R S]]]]]. - left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res' #PC <- (rs LR)) - m2'); split. + left; econstructor; split. apply plus_one. eapply exec_step_external; eauto. - eapply external_call_symbols_preserved; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - unfold loc_external_result. - apply agree_set_other; auto with ppcgen. - apply agree_set_mreg with rs; auto. - rewrite Pregmap.gss; auto. - intros; apply Pregmap.gso; auto. -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 (Machsem.Returnstate (Stackframe fb sp ra c :: s) ms m) E0 - (Machsem.State s fb sp c ms m). -Proof. - intros; red; intros; inv MS. inv STACKS. simpl in *. + rewrite Pregmap.gss. apply match_stack_change_bound with (Mem.nextblock m). + eapply match_stack_extcall; eauto. + intros. eapply external_call_max_perm; eauto. + eapply external_call_nextblock; eauto. + unfold loc_external_result. + eapply agree_set_mreg; eauto. + rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. + intros; Simpl. + +- (* return *) + inv STACKS. simpl in *. right. split. omega. split. auto. - econstructor; eauto. rewrite ATPC; auto. + econstructor; eauto. congruence. Qed. -Theorem transf_instr_correct: - forall s1 t s2, Machsem.step ge s1 t s2 -> - exec_instr_prop s1 t s2. -Proof - (Machsem.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_Mannot_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, Machsem.initial_state prog st1 -> + forall st1, Mach.initial_state prog st1 -> exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. unfold ge0 in *. + exploit functions_translated; eauto. intros [tf [A B]]. 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. - split. auto. simpl. congruence. - intros. repeat rewrite Pregmap.gso; auto with ppcgen. + with (Vptr b Int.zero). + econstructor; eauto. + constructor. apply Mem.extends_refl. + split. auto. intros. rewrite Regmap.gi. auto. + reflexivity. + exact I. unfold symbol_offset. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. unfold ge; rewrite H1. auto. @@ -1522,21 +1058,22 @@ Qed. Lemma transf_final_states: forall st1 st2 r, - match_states st1 st2 -> Machsem.final_state st1 r -> Asm.final_state st2 r. + match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r. Proof. - intros. inv H0. inv H. constructor. auto. - compute in H1. - exploit (ireg_val _ _ _ R3 AG). auto. rewrite H1; intro. inv H. auto. + intros. inv H0. inv H. inv STACKS. constructor. + auto. + compute in H1. + generalize (preg_val _ _ _ R3 AG). rewrite H1. intros LD; inv LD. auto. Qed. Theorem transf_program_correct: - forward_simulation (Machsem.semantics prog) (Asm.semantics tprog). + forward_simulation (Mach.semantics prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. - exact transf_instr_correct. + exact step_simulation. Qed. End PRESERVATION. -- cgit