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 --- backend/Asmgenproof0.v | 844 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 844 insertions(+) create mode 100644 backend/Asmgenproof0.v (limited to 'backend/Asmgenproof0.v') diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v new file mode 100644 index 00000000..06b54073 --- /dev/null +++ b/backend/Asmgenproof0.v @@ -0,0 +1,844 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness proof for Asm generation: machine-independent framework *) + +Require Import Coqlib. +Require Intv. +Require Import AST. +Require Import Errors. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. +Require Import Locations. +Require Import Mach. +Require Import Asm. +Require Import Asmgen. +Require Import Conventions. + +(** * Processor registers and register states *) + +Hint Extern 2 (_ <> _) => congruence: asmgen. + +Lemma ireg_of_eq: + forall r r', ireg_of r = OK r' -> preg_of r = IR r'. +Proof. + unfold ireg_of; intros. destruct (preg_of r); inv H; auto. +Qed. + +Lemma freg_of_eq: + forall r r', freg_of r = OK r' -> preg_of r = FR r'. +Proof. + unfold freg_of; intros. destruct (preg_of r); inv H; auto. +Qed. + +Lemma preg_of_injective: + forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. +Proof. + destruct r1; destruct r2; simpl; intros; reflexivity || discriminate. +Qed. + +Lemma preg_of_data: + forall r, data_preg (preg_of r) = true. +Proof. + intros. destruct r; reflexivity. +Qed. +Hint Resolve preg_of_data: asmgen. + +Lemma data_diff: + forall r r', + data_preg r = true -> data_preg r' = false -> r <> r'. +Proof. + congruence. +Qed. +Hint Resolve data_diff: asmgen. + +Lemma preg_of_not_SP: + forall r, preg_of r <> SP. +Proof. + intros. unfold preg_of; destruct r; simpl; congruence. +Qed. + +Lemma preg_of_not_PC: + forall r, preg_of r <> PC. +Proof. + intros. apply data_diff; auto with asmgen. +Qed. + +Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. + +Lemma nontemp_diff: + forall r r', + nontemp_preg r = true -> nontemp_preg r' = false -> r <> r'. +Proof. + congruence. +Qed. +Hint Resolve nontemp_diff: asmgen. + +Lemma temporaries_temp_preg: + forall r, In r temporary_regs -> nontemp_preg (preg_of r) = false. +Proof. + assert (List.forallb (fun r => negb (nontemp_preg (preg_of r))) temporary_regs = true) by reflexivity. + rewrite List.forallb_forall in H. intros. generalize (H r H0). + destruct (nontemp_preg (preg_of r)); simpl; congruence. +Qed. + +Lemma nontemp_data_preg: + forall r, nontemp_preg r = true -> data_preg r = true. +Proof. + destruct r; try (destruct i); try (destruct f); simpl; congruence. +Qed. +Hint Resolve nontemp_data_preg: asmgen. + +Lemma nextinstr_pc: + forall rs, (nextinstr rs)#PC = Val.add rs#PC Vone. +Proof. + intros. apply Pregmap.gss. +Qed. + +Lemma nextinstr_inv: + forall r rs, r <> PC -> (nextinstr rs)#r = rs#r. +Proof. + intros. unfold nextinstr. apply Pregmap.gso. red; intro; subst. auto. +Qed. + +Lemma nextinstr_inv1: + forall r rs, data_preg r = true -> (nextinstr rs)#r = rs#r. +Proof. + intros. apply nextinstr_inv. red; intro; subst; discriminate. +Qed. + +Lemma nextinstr_inv2: + forall r rs, nontemp_preg r = true -> (nextinstr rs)#r = rs#r. +Proof. + intros. apply nextinstr_inv1; auto with asmgen. +Qed. + +Lemma nextinstr_set_preg: + forall rs m v, + (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone. +Proof. + intros. unfold nextinstr. rewrite Pregmap.gss. + rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC. +Qed. + +(** * Agreement between Mach registers and processor registers *) + +Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree { + agree_sp: rs#SP = sp; + agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r)) +}. + +Lemma preg_val: + forall ms sp rs r, agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r). +Proof. + intros. destruct H. auto. +Qed. + +Lemma preg_vals: + forall ms sp rs, agree ms sp rs -> + forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)). +Proof. + induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto. +Qed. + +Lemma sp_val: + forall ms sp rs, agree ms sp rs -> sp = rs#SP. +Proof. + intros. destruct H; auto. +Qed. + +Lemma ireg_val: + forall ms sp rs r r', + agree ms sp rs -> + ireg_of r = OK r' -> + Val.lessdef (ms r) rs#r'. +Proof. + intros. rewrite <- (ireg_of_eq _ _ H0). eapply preg_val; eauto. +Qed. + +Lemma freg_val: + forall ms sp rs r r', + agree ms sp rs -> + freg_of r = OK r' -> + Val.lessdef (ms r) (rs#r'). +Proof. + intros. rewrite <- (freg_of_eq _ _ H0). eapply preg_val; eauto. +Qed. + +Lemma agree_exten: + forall ms sp rs rs', + agree ms sp rs -> + (forall r, data_preg r = true -> rs'#r = rs#r) -> + agree ms sp rs'. +Proof. + intros. destruct H. split. + rewrite H0; auto. auto. + intros. rewrite H0; auto. apply preg_of_data. +Qed. + +(** Preservation of register agreement under various assignments. *) + +Lemma agree_set_mreg: + forall ms sp rs r v rs', + agree ms sp rs -> + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v ms) sp rs'. +Proof. + intros. destruct H. split. + rewrite H1; auto. apply sym_not_equal. apply preg_of_not_SP. + auto. + intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. + rewrite H1. auto. apply preg_of_data. + red; intros; elim n. eapply preg_of_injective; eauto. +Qed. + +Lemma agree_set_other: + forall ms sp rs r v, + agree ms sp rs -> + data_preg r = false -> + agree ms sp (rs#r <- v). +Proof. + intros. apply agree_exten with rs. auto. + intros. apply Pregmap.gso. congruence. +Qed. + +Lemma agree_nextinstr: + forall ms sp rs, + agree ms sp rs -> agree ms sp (nextinstr rs). +Proof. + intros. unfold nextinstr. apply agree_set_other. auto. auto. +Qed. + +Lemma agree_undef_regs: + forall ms sp rl rs, + agree ms sp rs -> + (forall r, In r rl -> data_preg r = false) -> + agree ms sp (undef_regs rl rs). +Proof. + induction rl; simpl; intros. auto. + apply IHrl. apply agree_exten with rs; auto. + intros. apply Pregmap.gso. red; intros; subst. + assert (data_preg a = false) by auto. congruence. + intros. apply H0; auto. +Qed. + +Lemma agree_exten_temps: + forall ms sp rs rs', + agree ms sp rs -> + (forall r, nontemp_preg r = true -> rs'#r = rs#r) -> + agree (undef_temps ms) sp rs'. +Proof. + intros. destruct H. split. + rewrite H0; auto. auto. + intros. unfold undef_temps. + destruct (In_dec mreg_eq r temporary_regs). + rewrite Mach.undef_regs_same; auto. + rewrite Mach.undef_regs_other; auto. rewrite H0; auto. + simpl in n. destruct r; auto; intuition. +Qed. + +Lemma agree_set_undef_mreg: + forall ms sp rs r v rs', + agree ms sp rs -> + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', nontemp_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v (undef_temps ms)) sp rs'. +Proof. + intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto. + eapply agree_exten_temps; eauto. + intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). + congruence. auto. + intros. rewrite Pregmap.gso; auto. +Qed. + +Lemma agree_change_sp: + forall ms sp rs sp', + agree ms sp rs -> sp' <> Vundef -> + agree ms sp' (rs#SP <- sp'). +Proof. + intros. inv H. split. apply Pregmap.gss. auto. + intros. rewrite Pregmap.gso; auto with asmgen. +Qed. + +(** Connection between Mach and Asm calling conventions for external + functions. *) + +Lemma extcall_arg_match: + forall ms sp rs m m' l v, + agree ms sp rs -> + Mem.extends m m' -> + Mach.extcall_arg ms m sp l v -> + exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'. +Proof. + intros. inv H1. + exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto. + unfold load_stack in H2. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ H) in A. + exists v'; split; auto. + destruct ty; econstructor. + reflexivity. assumption. + reflexivity. assumption. +Qed. + +Lemma extcall_args_match: + forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> + forall ll vl, + list_forall2 (Mach.extcall_arg ms m sp) ll vl -> + exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'. +Proof. + induction 3; intros. + exists (@nil val); split. constructor. constructor. + exploit extcall_arg_match; eauto. intros [v1' [A B]]. + destruct IHlist_forall2 as [vl' [C D]]. + exists (v1' :: vl'); split; constructor; auto. +Qed. + +Lemma extcall_arguments_match: + forall ms m m' sp rs sg args, + agree ms sp rs -> Mem.extends m m' -> + Mach.extcall_arguments ms m sp sg args -> + exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'. +Proof. + unfold Mach.extcall_arguments, Asm.extcall_arguments; intros. + eapply extcall_args_match; eauto. +Qed. + +(** Translation of arguments to annotations. *) + +Lemma annot_arg_match: + forall ms sp rs m m' p v, + agree ms sp rs -> + Mem.extends m m' -> + Mach.annot_arg ms m sp p v -> + exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'. +Proof. + intros. inv H1; simpl. +(* reg *) + exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto. +(* stack *) + exploit Mem.load_extends; eauto. intros [v' [A B]]. + exists v'; split; auto. + inv H. econstructor; eauto. +Qed. + +Lemma annot_arguments_match: + forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> + forall pl vl, + Mach.annot_arguments ms m sp pl vl -> + exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl' + /\ Val.lessdef_list vl vl'. +Proof. + induction 3; intros. + exists (@nil val); split. constructor. constructor. + exploit annot_arg_match; eauto. intros [v1' [A B]]. + destruct IHlist_forall2 as [vl' [C D]]. + exists (v1' :: vl'); split; constructor; auto. +Qed. + +(** * Correspondence between Mach code and Asm code *) + +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]. *) + +Inductive code_tail: Z -> code -> code -> Prop := + | code_tail_0: forall c, + code_tail 0 c c + | code_tail_S: forall pos i c1 c2, + code_tail pos c1 c2 -> + code_tail (pos + 1) (i :: c1) c2. + +Lemma code_tail_pos: + forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. +Proof. + induction 1. omega. omega. +Qed. + +Lemma find_instr_tail: + forall c1 i c2 pos, + code_tail pos c1 (i :: c2) -> + find_instr pos c1 = Some i. +Proof. + induction c1; simpl; intros. + inv H. + destruct (zeq pos 0). subst pos. + inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction. + inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega. + eauto. +Qed. + +Remark code_tail_bounds: + forall fn ofs i c, + code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn. +Proof. + assert (forall ofs fn c, code_tail ofs fn c -> + forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn). + induction 1; intros; simpl. + rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega. + rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega. + eauto. +Qed. + +Lemma code_tail_next: + forall fn ofs i c, + code_tail ofs fn (i :: c) -> + code_tail (ofs + 1) fn c. +Proof. + assert (forall ofs fn c, code_tail ofs fn c -> + forall i c', c = i :: c' -> code_tail (ofs + 1) fn c'). + induction 1; intros. + subst c. constructor. constructor. + constructor. eauto. + eauto. +Qed. + +Lemma code_tail_next_int: + forall fn ofs i c, + list_length_z fn <= Int.max_unsigned -> + code_tail (Int.unsigned ofs) fn (i :: c) -> + code_tail (Int.unsigned (Int.add ofs Int.one)) fn c. +Proof. + intros. rewrite Int.add_unsigned. + change (Int.unsigned Int.one) with 1. + rewrite Int.unsigned_repr. apply code_tail_next with i; auto. + generalize (code_tail_bounds _ _ _ _ H0). omega. +Qed. + +(** [transl_code_at_pc pc f c ep tf tc] holds if the code pointer [pc] points + within the Asm code generated by translating Mach function [f], + and [tc] is the tail of the generated code at the position corresponding + to the code pointer [pc]. *) + +Inductive transl_code_at_pc (ge: Mach.genv): + val -> Mach.function -> Mach.code -> bool -> Asm.function -> Asm.code -> Prop := + transl_code_at_pc_intro: + forall b ofs f c ep tf tc, + Genv.find_funct_ptr ge b = Some(Internal f) -> + transf_function f = Errors.OK tf -> + transl_code f c ep = OK tc -> + code_tail (Int.unsigned ofs) (fn_code tf) tc -> + transl_code_at_pc ge (Vptr b ofs) f c ep tf tc. + +(** * Execution of straight-line code *) + +Section STRAIGHTLINE. + +Variable ge: genv. +Variable fn: function. + +(** Straight-line code is composed of processor instructions that execute + in sequence (no branches, no function calls and returns). + The following inductive predicate relates the machine states + before and after executing a straight-line sequence of instructions. + Instructions are taken from the first list instead of being fetched + from memory. *) + +Inductive exec_straight: code -> regset -> mem -> + code -> regset -> mem -> Prop := + | exec_straight_one: + forall i1 c rs1 m1 rs2 m2, + exec_instr ge fn i1 rs1 m1 = Next rs2 m2 -> + rs2#PC = Val.add rs1#PC Vone -> + exec_straight (i1 :: c) rs1 m1 c rs2 m2 + | exec_straight_step: + forall i c rs1 m1 rs2 m2 c' rs3 m3, + exec_instr ge fn i rs1 m1 = Next rs2 m2 -> + rs2#PC = Val.add rs1#PC Vone -> + exec_straight c rs2 m2 c' rs3 m3 -> + exec_straight (i :: c) rs1 m1 c' rs3 m3. + +Lemma exec_straight_trans: + forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, + exec_straight c1 rs1 m1 c2 rs2 m2 -> + exec_straight c2 rs2 m2 c3 rs3 m3 -> + exec_straight c1 rs1 m1 c3 rs3 m3. +Proof. + induction 1; intros. + apply exec_straight_step with rs2 m2; auto. + apply exec_straight_step with rs2 m2; auto. +Qed. + +Lemma exec_straight_two: + forall i1 i2 c rs1 m1 rs2 m2 rs3 m3, + exec_instr ge fn i1 rs1 m1 = Next rs2 m2 -> + exec_instr ge fn i2 rs2 m2 = Next rs3 m3 -> + rs2#PC = Val.add rs1#PC Vone -> + rs3#PC = Val.add rs2#PC Vone -> + exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3. +Proof. + intros. apply exec_straight_step with rs2 m2; auto. + apply exec_straight_one; auto. +Qed. + +Lemma exec_straight_three: + forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4, + exec_instr ge fn i1 rs1 m1 = Next rs2 m2 -> + exec_instr ge fn i2 rs2 m2 = Next rs3 m3 -> + exec_instr ge fn i3 rs3 m3 = Next rs4 m4 -> + rs2#PC = Val.add rs1#PC Vone -> + rs3#PC = Val.add rs2#PC Vone -> + rs4#PC = Val.add rs3#PC Vone -> + exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4. +Proof. + intros. apply exec_straight_step with rs2 m2; auto. + eapply exec_straight_two; eauto. +Qed. + +(** The following lemmas show that straight-line executions + (predicate [exec_straight]) correspond to correct Asm executions. *) + +Lemma exec_straight_steps_1: + forall c rs m c' rs' m', + exec_straight c rs m c' rs' m' -> + list_length_z (fn_code fn) <= Int.max_unsigned -> + forall b ofs, + rs#PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal fn) -> + code_tail (Int.unsigned ofs) (fn_code fn) c -> + plus step ge (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 c rs m c' rs' m', + exec_straight c rs m c' rs' m' -> + list_length_z (fn_code fn) <= Int.max_unsigned -> + forall b ofs, + rs#PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal fn) -> + code_tail (Int.unsigned ofs) (fn_code fn) c -> + exists ofs', + rs'#PC = Vptr b ofs' + /\ code_tail (Int.unsigned ofs') (fn_code fn) c'. +Proof. + induction 1; intros. + exists (Int.add ofs Int.one). split. + rewrite H0. rewrite H2. auto. + apply code_tail_next_int with i1; auto. + apply IHexec_straight with (Int.add ofs Int.one). + auto. rewrite H0. rewrite H3. reflexivity. auto. + apply code_tail_next_int with i; auto. +Qed. + +End STRAIGHTLINE. + +(** * Stack invariants *) + +(** ** Stored return addresses *) + +(** [retaddr_stored_at m m' sp pos ra] holds if Asm memory [m'] + contains value [ra] (a return address) at offset [pos] in block [sp]. *) + +Record retaddr_stored_at (m m': mem) (sp: block) (pos: Z) (ra: val) : Prop := { + rsa_noperm: + forall ofs k p, pos <= ofs < pos + 4 -> ~Mem.perm m sp ofs k p; + rsa_allperm: + forall ofs k p, pos <= ofs < pos + 4 -> Mem.perm m' sp ofs k p; + rsa_contains: + Mem.load Mint32 m' sp pos = Some ra +}. + +Lemma retaddr_stored_at_invariant: + forall m m' sp pos ra m1 m1', + retaddr_stored_at m m' sp pos ra -> + (forall ofs p, pos <= ofs < pos + 4 -> Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> + (forall ofs k p, pos <= ofs < pos + 4 -> Mem.perm m' sp ofs k p -> Mem.perm m1' sp ofs k p) -> + (Mem.load Mint32 m' sp pos = Some ra -> Mem.load Mint32 m1' sp pos = Some ra) -> + retaddr_stored_at m1 m1' sp pos ra. +Proof. + intros. inv H. constructor; intros. + red; intros. eelim rsa_noperm0. eauto. apply H0. auto. eapply Mem.perm_max; eauto. + eauto. + eauto. +Qed. + +Lemma retaddr_stored_at_store: + forall chunk m m' b ofs v v' m1 m1' sp pos ra, + retaddr_stored_at m m' sp pos ra -> + Mem.store chunk m b ofs v = Some m1 -> + Mem.store chunk m' b ofs v' = Some m1' -> + retaddr_stored_at m1 m1' sp pos ra. +Proof. + intros. eapply retaddr_stored_at_invariant; eauto; intros. +- eapply Mem.perm_store_2; eauto. +- eapply Mem.perm_store_1; eauto. +- rewrite <- H2. eapply Mem.load_store_other; eauto. + destruct (eq_block sp b); auto. subst b. + right. exploit Mem.store_valid_access_3. eexact H0. intros [A B]. + apply (Intv.range_disjoint' (pos, pos + size_chunk Mint32) (ofs, ofs + size_chunk chunk)). + red; intros; red; intros. + elim (rsa_noperm _ _ _ _ _ H x Cur Writable). assumption. apply A. assumption. + simpl; omega. + simpl; generalize (size_chunk_pos chunk); omega. +Qed. + +Lemma retaddr_stored_at_storev: + forall chunk m m' a a' v v' m1 m1' sp pos ra, + retaddr_stored_at m m' sp pos ra -> + Mem.storev chunk m a v = Some m1 -> + Mem.storev chunk m' a' v' = Some m1' -> + Val.lessdef a a' -> + retaddr_stored_at m1 m1' sp pos ra. +Proof. + intros. destruct a; simpl in H0; try discriminate. inv H2. simpl in H1. + eapply retaddr_stored_at_store; eauto. +Qed. + +Lemma retaddr_stored_at_valid': + forall m m' sp pos ra, + retaddr_stored_at m m' sp pos ra -> + Mem.valid_block m' sp. +Proof. + intros. + eapply Mem.valid_access_valid_block. + apply Mem.valid_access_implies with Readable; auto with mem. + eapply Mem.load_valid_access. + eapply rsa_contains; eauto. +Qed. + +Lemma retaddr_stored_at_valid: + forall m m' sp pos ra, + retaddr_stored_at m m' sp pos ra -> + Mem.extends m m' -> + Mem.valid_block m sp. +Proof. + intros. + erewrite Mem.valid_block_extends; eauto. + eapply retaddr_stored_at_valid'; eauto. +Qed. + +Lemma retaddr_stored_at_extcall: + forall m1 m1' sp pos ra m2 m2', + retaddr_stored_at m1 m1' sp pos ra -> + (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> + mem_unchanged_on (loc_out_of_bounds m1) m1' m2' -> + Mem.extends m1 m1' -> + retaddr_stored_at m2 m2' sp pos ra. +Proof. + intros. + assert (B: forall ofs, pos <= ofs < pos + 4 -> loc_out_of_bounds m1 sp ofs). + intros; red; intros. eapply rsa_noperm; eauto. + eapply retaddr_stored_at_invariant; eauto. +- intros. apply H0; auto. eapply retaddr_stored_at_valid; eauto. +- intros. destruct H1. eauto. +- intros. destruct H1. apply H4; auto. +Qed. + +Lemma retaddr_stored_at_can_alloc: + forall m lo hi m1 sp pos m2 a v m3 m' m1' a' v' m2' ra, + Mem.alloc m lo hi = (m1, sp) -> + Mem.free m1 sp pos (pos + 4) = Some m2 -> + Mem.storev Mint32 m2 a v = Some m3 -> + Mem.alloc m' lo hi = (m1', sp) -> + Mem.storev Mint32 m1' a' v' = Some m2' -> + (4 | pos) -> + Mem.extends m3 m2' -> + Val.has_type ra Tint -> + exists m3', + Mem.store Mint32 m2' sp pos ra = Some m3' + /\ retaddr_stored_at m3 m3' sp pos ra + /\ Mem.extends m3 m3'. +Proof. + intros. destruct a; simpl in H1; try discriminate. destruct a'; simpl in H3; try discriminate. + assert (POS: forall ofs, pos <= ofs < pos + 4 -> lo <= ofs < hi). + intros. eapply Mem.perm_alloc_3. eexact H. eapply Mem.free_range_perm; eauto. + assert (ST: { m3' | Mem.store Mint32 m2' sp pos ra = Some m3' }). + { + apply Mem.valid_access_store. split. + red; intros. eapply Mem.perm_store_1; eauto. + apply Mem.perm_implies with Freeable; auto with mem. + eapply Mem.perm_alloc_2; eauto. + assumption. + } + destruct ST as [m3' ST]. exists m3'; split; auto. + split. constructor. + intros; red; intros. eelim Mem.perm_free_2; eauto. eapply Mem.perm_store_2; eauto. + intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. + apply Mem.perm_implies with Freeable; auto with mem. + eapply Mem.perm_alloc_2; eauto. + replace ra with (Val.load_result Mint32 ra). eapply Mem.load_store_same; eauto. + destruct ra; reflexivity || contradiction. + eapply Mem.store_outside_extends; eauto. + intros. eelim Mem.perm_free_2; eauto. eapply Mem.perm_store_2; eauto. +Qed. + +Lemma retaddr_stored_at_can_free: + forall m m' sp pos ra lo m1 hi m2, + retaddr_stored_at m m' sp pos ra -> + Mem.free m sp lo pos = Some m1 -> + Mem.free m1 sp (pos + 4) hi = Some m2 -> + Mem.extends m m' -> + exists m1', Mem.free m' sp lo hi = Some m1' /\ Mem.extends m2 m1'. +Proof. + intros. inv H. + assert (F: { m1' | Mem.free m' sp lo hi = Some m1' }). + { + apply Mem.range_perm_free. red; intros. + assert (EITHER: lo <= ofs < pos \/ pos <= ofs < pos + 4 \/ pos + 4 <= ofs < hi) by omega. + destruct EITHER as [A | [A | A]]. + eapply Mem.perm_extends; eauto. eapply Mem.free_range_perm; eauto. + auto. + eapply Mem.perm_extends; eauto. + eapply Mem.perm_free_3; eauto. eapply Mem.free_range_perm; eauto. + } + destruct F as [m1' F]. exists m1'; split; auto. + eapply Mem.free_right_extends; eauto. + eapply Mem.free_left_extends. eapply Mem.free_left_extends. eauto. eauto. eauto. + intros. + exploit Mem.perm_free_3. eexact H1. eauto. intros P1. + exploit Mem.perm_free_3. eexact H0. eauto. intros P0. + assert (EITHER: lo <= ofs < pos \/ pos <= ofs < pos + 4 \/ pos + 4 <= ofs < hi) by omega. + destruct EITHER as [A | [A | A]]. + eelim Mem.perm_free_2. eexact H0. eexact A. eauto. + eelim rsa_noperm0; eauto. + eelim Mem.perm_free_2. eexact H1. eexact A. eauto. +Qed. + +Lemma retaddr_stored_at_type: + forall m m' sp pos ra, retaddr_stored_at m m' sp pos ra -> Val.has_type ra Tint. +Proof. + intros. change Tint with (type_of_chunk Mint32). + eapply Mem.load_type. eapply rsa_contains; eauto. +Qed. + +(** Matching a Mach stack against an Asm memory state. *) + +Section MATCH_STACK. + +Variable ge: Mach.genv. + +Inductive match_stack: + list Mach.stackframe -> mem -> mem -> val -> block -> Prop := + | match_stack_nil: forall m m' bound, + match_stack nil m m' Vzero bound + | match_stack_cons: forall f sp c s m m' ra tf tc ra' bound + (AT: transl_code_at_pc ge ra f c false tf tc) + (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra') + (BELOW: sp < bound), + match_stack s m m' ra' sp -> + match_stack (Stackframe f (Vptr sp Int.zero) c :: s) m m' ra bound. + +Lemma match_stack_invariant: + forall m2 m2' s m1 m1' ra bound, + match_stack s m1 m1' ra bound -> + (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> + (forall b ofs k p, b < bound -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) -> + (forall b ofs v, b < bound -> Mem.load Mint32 m1' b ofs = Some v -> Mem.load Mint32 m2' b ofs = Some v) -> + match_stack s m2 m2' ra bound. +Proof. + induction 1; intros; econstructor; eauto. + eapply retaddr_stored_at_invariant; eauto. + apply IHmatch_stack; intros. + eapply H0; eauto. omega. + eapply H1; eauto. omega. + eapply H2; eauto. omega. +Qed. + +Lemma match_stack_change_bound: + forall s m m' ra bound1 bound2, + match_stack s m m' ra bound1 -> + bound1 <= bound2 -> + match_stack s m m' ra bound2. +Proof. + intros. inv H; econstructor; eauto. omega. +Qed. + +Lemma match_stack_storev: + forall chunk a v m1 a' v' m1' s m m' ra bound, + match_stack s m m' ra bound -> + Mem.storev chunk m a v = Some m1 -> + Mem.storev chunk m' a' v' = Some m1' -> + Val.lessdef a a' -> + match_stack s m1 m1' ra bound. +Proof. + induction 1; intros; econstructor; eauto. + eapply retaddr_stored_at_storev; eauto. +Qed. + +Lemma match_stack_extcall: + forall m2 m2' s m1 m1' ra bound, + match_stack s m1 m1' ra bound -> + (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> + mem_unchanged_on (loc_out_of_bounds m1) m1' m2' -> + Mem.extends m1 m1' -> + match_stack s m2 m2' ra bound. +Proof. + induction 1; intros; econstructor; eauto. + eapply retaddr_stored_at_extcall; eauto. +Qed. + +Lemma match_stack_free_left: + forall s m m' ra bound b lo hi m1, + match_stack s m m' ra bound -> + Mem.free m b lo hi = Some m1 -> + match_stack s m1 m' ra bound. +Proof. + intros. eapply match_stack_invariant; eauto. + intros. eapply Mem.perm_free_3; eauto. +Qed. + +Lemma match_stack_free_right: + forall s m m' ra bound b lo hi m1', + match_stack s m m' ra bound -> + Mem.free m' b lo hi = Some m1' -> + bound <= b -> + match_stack s m m1' ra bound. +Proof. + intros. eapply match_stack_invariant; eauto. + intros. eapply Mem.perm_free_1; eauto. left. unfold block; omega. + intros. rewrite <- H3. eapply Mem.load_free; eauto. left. unfold block; omega. +Qed. + +Lemma parent_sp_def: + forall s m m' ra bound, + match_stack s m m' ra bound -> parent_sp s <> Vundef. +Proof. + intros. inv H; simpl; congruence. +Qed. + +Lemma lessdef_parent_sp: + forall s m m' ra bound v, + match_stack s m m' ra bound -> Val.lessdef (parent_sp s) v -> v = parent_sp s. +Proof. + intros. inv H0; auto. exfalso. eelim parent_sp_def; eauto. +Qed. + +End MATCH_STACK. + + -- cgit