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 +++++++++++++++++++++++++++++++++++++++++++++++ backend/Mach.v | 247 +++++++++++++- backend/Machsem.v | 108 +++--- backend/Stackingproof.v | 445 ++++++++++++++----------- backend/Stackingtyping.v | 250 -------------- 5 files changed, 1371 insertions(+), 523 deletions(-) create mode 100644 backend/Asmgenproof0.v delete mode 100644 backend/Stackingtyping.v (limited to 'backend') diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v new file mode 100644 index 0000000..06b5407 --- /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. + + diff --git a/backend/Mach.v b/backend/Mach.v index 56c0369..12c6c9d 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -21,10 +21,14 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. +Require Import Memory. Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. Require Import Op. Require Import Locations. Require Import Conventions. +Require Stacklayout. (** * Abstract syntax *) @@ -89,13 +93,39 @@ Definition funsig (fd: fundef) := Definition genv := Genv.t fundef unit. -(** * Elements of dynamic semantics *) - -(** The operational semantics is in module [Machsem]. *) +(** * Operational semantics *) + +(** The semantics for Mach is close to that of [Linear]: they differ only + on the interpretation of stack slot accesses. In Mach, these + accesses are interpreted as memory accesses relative to the + stack pointer. More precisely: +- [Mgetstack ofs ty r] is a memory load at offset [ofs * 4] relative + to the stack pointer. +- [Msetstack r ofs ty] is a memory store at offset [ofs * 4] relative + to the stack pointer. +- [Mgetparam ofs ty r] is a memory load at offset [ofs * 4] + relative to the pointer found at offset 0 from the stack pointer. + The semantics maintain a linked structure of activation records, + with the current record containing a pointer to the record of the + caller function at offset 0. + +In addition to this linking of activation records, the +semantics also make provisions for storing a back link at offset +[f.(fn_link_ofs)] from the stack pointer, and a return address at +offset [f.(fn_retaddr_ofs)]. The latter stack location will be used +by the Asm code generated by [Asmgen] to save the return address into +the caller at the beginning of a function, then restore it and jump to +it at the end of a function. *) Definition chunk_of_type (ty: typ) := match ty with Tint => Mint32 | Tfloat => Mfloat64al32 end. +Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) := + Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)). + +Definition store_stack (m: mem) (sp: val) (ty: typ) (ofs: int) (v: val) := + Mem.storev (chunk_of_type ty) m (Val.add sp (Vint ofs)) v. + Module RegEq. Definition t := mreg. Definition eq := mreg_eq. @@ -170,15 +200,210 @@ Proof. destruct (is_label lbl a). inv H. auto with coqlib. eauto with coqlib. Qed. -Definition find_function_ptr - (ge: genv) (ros: mreg + ident) (rs: regset) : option block := +Section RELSEM. + +Variable ge: genv. + +Definition find_function (ros: mreg + ident) (rs: regset) : option fundef := match ros with - | inl r => - match rs r with - | Vptr b ofs => if Int.eq ofs Int.zero then Some b else None - | _ => None - end + | inl r => Genv.find_funct ge (rs r) | inr symb => - Genv.find_symbol ge symb + match Genv.find_symbol ge symb with + | None => None + | Some b => Genv.find_funct_ptr ge b + end + end. + +(** Extract the values of the arguments to an external call. *) + +Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop := + | extcall_arg_reg: forall rs m sp r, + extcall_arg rs m sp (R r) (rs r) + | extcall_arg_stack: forall rs m sp ofs ty v, + load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = Some v -> + extcall_arg rs m sp (S (Outgoing ofs ty)) v. + +Definition extcall_arguments + (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := + list_forall2 (extcall_arg rs m sp) (loc_arguments sg) args. + +(** Extract the values of the arguments to an annotation. *) + +Inductive annot_arg: regset -> mem -> val -> annot_param -> val -> Prop := + | annot_arg_reg: forall rs m sp r, + annot_arg rs m sp (APreg r) (rs r) + | annot_arg_stack: forall rs m stk base chunk ofs v, + Mem.load chunk m stk (Int.unsigned base + ofs) = Some v -> + annot_arg rs m (Vptr stk base) (APstack chunk ofs) v. + +Definition annot_arguments + (rs: regset) (m: mem) (sp: val) (params: list annot_param) (args: list val) : Prop := + list_forall2 (annot_arg rs m sp) params args. + +(** Mach execution states. *) + +Inductive stackframe: Type := + | Stackframe: + forall (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (c: code), (**r program point in calling function *) + stackframe. + +Inductive state: Type := + | State: + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r current function *) + (sp: val) (**r stack pointer *) + (c: code) (**r current program point *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Callstate: + forall (stack: list stackframe) (**r call stack *) + (fd: fundef) (**r function to call *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Returnstate: + forall (stack: list stackframe) (**r call stack *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state. + +Definition parent_sp (s: list stackframe) : val := + match s with + | nil => Vptr Mem.nullptr Int.zero + | Stackframe f sp c :: s' => sp end. +Inductive step: state -> trace -> state -> Prop := + | exec_Mlabel: + forall s f sp lbl c rs m, + step (State s f sp (Mlabel lbl :: c) rs m) + E0 (State s f sp c rs m) + | exec_Mgetstack: + forall s f sp ofs ty dst c rs m v, + load_stack m sp ty ofs = Some v -> + step (State s f sp (Mgetstack ofs ty dst :: c) rs m) + E0 (State s f sp c (rs#dst <- v) m) + | exec_Msetstack: + forall s f sp src ofs ty c rs m m', + store_stack m sp ty ofs (rs src) = Some m' -> + step (State s f sp (Msetstack src ofs ty :: c) rs m) + E0 (State s f sp c (undef_setstack rs) m') + | exec_Mgetparam: + forall s f sp ofs ty dst c rs m v, + load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (parent_sp s) ty ofs = Some v -> + step (State s f sp (Mgetparam ofs ty dst :: c) rs m) + E0 (State s f sp c (rs # IT1 <- Vundef # dst <- v) m) + | exec_Mop: + forall s f sp op args res c rs m v, + eval_operation ge sp op rs##args m = Some v -> + step (State s f sp (Mop op args res :: c) rs m) + E0 (State s f sp c ((undef_op op rs)#res <- v) m) + | exec_Mload: + forall s f sp chunk addr args dst c rs m a v, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + step (State s f sp (Mload chunk addr args dst :: c) rs m) + E0 (State s f sp c ((undef_temps rs)#dst <- v) m) + | exec_Mstore: + forall s f sp chunk addr args src c rs m m' a, + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a (rs src) = Some m' -> + step (State s f sp (Mstore chunk addr args src :: c) rs m) + E0 (State s f sp c (undef_temps rs) m') + | exec_Mcall: + forall s f sp sig ros c rs m fd, + find_function ros rs = Some fd -> + step (State s f sp (Mcall sig ros :: c) rs m) + E0 (Callstate (Stackframe f sp c :: s) + fd rs m) + | exec_Mtailcall: + forall s f stk soff sig ros c rs m fd m' m'', + find_function ros rs = Some fd -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' -> + Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' -> + step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs m) + E0 (Callstate s fd rs m'') + | exec_Mbuiltin: + forall s f sp rs m ef args res b t v m', + external_call ef ge rs##args m t v m' -> + step (State s f sp (Mbuiltin ef args res :: b) rs m) + t (State s f sp b ((undef_temps rs)#res <- v) m') + | exec_Mannot: + forall s f sp rs m ef args b vargs t v m', + annot_arguments rs m sp args vargs -> + external_call ef ge vargs m t v m' -> + step (State s f sp (Mannot ef args :: b) rs m) + t (State s f sp b rs m') + | exec_Mgoto: + forall s f sp lbl c rs m c', + find_label lbl f.(fn_code) = Some c' -> + step (State s f sp (Mgoto lbl :: c) rs m) + E0 (State s f sp c' rs m) + | exec_Mcond_true: + forall s f sp cond args lbl c rs m c', + eval_condition cond rs##args m = Some true -> + find_label lbl f.(fn_code) = Some c' -> + step (State s f sp (Mcond cond args lbl :: c) rs m) + E0 (State s f sp c' (undef_temps rs) m) + | exec_Mcond_false: + forall s f sp cond args lbl c rs m, + eval_condition cond rs##args m = Some false -> + step (State s f sp (Mcond cond args lbl :: c) rs m) + E0 (State s f sp c (undef_temps rs) m) + | exec_Mjumptable: + forall s f sp arg tbl c rs m n lbl c', + rs arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some lbl -> + find_label lbl f.(fn_code) = Some c' -> + step (State s f sp (Mjumptable arg tbl :: c) rs m) + E0 (State s f sp c' (undef_temps rs) m) + | exec_Mreturn: + forall s f stk soff c rs m m' m'', + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' -> + Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' -> + step (State s f (Vptr stk soff) (Mreturn :: c) rs m) + E0 (Returnstate s rs m'') + | exec_function_internal: + forall s f rs m m1 m2 m3 stk, + Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> + Mem.free m1 stk (Int.unsigned f.(fn_retaddr_ofs)) (Int.unsigned f.(fn_retaddr_ofs) + 4) = Some m2 -> + let sp := Vptr stk Int.zero in + store_stack m2 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m3 -> + (4 | Int.unsigned f.(fn_retaddr_ofs)) -> + step (Callstate s (Internal f) rs m) + E0 (State s f sp f.(fn_code) (undef_temps rs) m3) + | exec_function_external: + forall s ef rs m t rs' args res m', + external_call ef ge args m t res m' -> + extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> + rs' = (rs#(loc_result (ef_sig ef)) <- res) -> + step (Callstate s (External ef) rs m) + t (Returnstate s rs' m') + | exec_return: + forall s f sp c rs m, + step (Returnstate (Stackframe f sp c :: s) rs m) + E0 (State s f sp c rs m). + +End RELSEM. + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b fd m0, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some fd -> + initial_state p (Callstate nil fd (Regmap.init Vundef) m0). + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall rs m r, + rs (loc_result (mksignature nil (Some Tint))) = Vint r -> + final_state (Returnstate nil rs m) r. + +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). diff --git a/backend/Machsem.v b/backend/Machsem.v index 6d5f1cf..60762c0 100644 --- a/backend/Machsem.v +++ b/backend/Machsem.v @@ -25,7 +25,6 @@ Require Import Locations. Require Import Conventions. Require Import Mach. Require Stacklayout. -Require Asmgenretaddr. (** The semantics for Mach is close to that of [Linear]: they differ only on the interpretation of stack slot accesses. In Mach, these @@ -91,16 +90,15 @@ Definition annot_arguments Inductive stackframe: Type := | Stackframe: - forall (f: block) (**r pointer to calling function *) + forall (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) - (retaddr: val) (**r Asm return address in calling function *) (c: code), (**r program point in calling function *) stackframe. Inductive state: Type := | State: forall (stack: list stackframe) (**r call stack *) - (f: block) (**r pointer to current function *) + (f: function) (**r current function *) (sp: val) (**r stack pointer *) (c: code) (**r current program point *) (rs: regset) (**r register state *) @@ -108,7 +106,7 @@ Inductive state: Type := state | Callstate: forall (stack: list stackframe) (**r call stack *) - (f: block) (**r pointer to function to call *) + (fd: fundef) (**r function to call *) (rs: regset) (**r register state *) (m: mem), (**r memory state *) state @@ -121,13 +119,7 @@ Inductive state: Type := Definition parent_sp (s: list stackframe) : val := match s with | nil => Vptr Mem.nullptr Int.zero - | Stackframe f sp ra c :: s' => sp - end. - -Definition parent_ra (s: list stackframe) : val := - match s with - | nil => Vzero - | Stackframe f sp ra c :: s' => ra + | Stackframe f sp c :: s' => sp end. Section RELSEM. @@ -150,12 +142,11 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Msetstack src ofs ty :: c) rs m) E0 (State s f sp c (undef_setstack rs) m') | exec_Mgetparam: - forall s fb f sp ofs ty dst c rs m v, - Genv.find_funct_ptr ge fb = Some (Internal f) -> + forall s f sp ofs ty dst c rs m v, load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (parent_sp s) ty ofs = Some v -> - step (State s fb sp (Mgetparam ofs ty dst :: c) rs m) - E0 (State s fb sp c (rs # IT1 <- Vundef # dst <- v) m) + step (State s f sp (Mgetparam ofs ty dst :: c) rs m) + E0 (State s f sp c (rs # IT1 <- Vundef # dst <- v) m) | exec_Mop: forall s f sp op args res c rs m v, eval_operation ge sp op rs##args m = Some v -> @@ -174,22 +165,19 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Mstore chunk addr args src :: c) rs m) E0 (State s f sp c (undef_temps rs) m') | exec_Mcall: - forall s fb sp sig ros c rs m f f' ra, - find_function_ptr ge ros rs = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Asmgenretaddr.return_address_offset f c ra -> - step (State s fb sp (Mcall sig ros :: c) rs m) - E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) - f' rs m) + forall s f sp sig ros c rs m fd, + find_function ge ros rs = Some fd -> + step (State s f sp (Mcall sig ros :: c) rs m) + E0 (Callstate (Stackframe f sp c :: s) + fd rs m) | exec_Mtailcall: - forall s fb stk soff sig ros c rs m f f' m', - find_function_ptr ge ros rs = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> + forall s f stk soff sig ros c rs m fd m' m'', + find_function ge ros rs = Some fd -> 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' -> - step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) - E0 (Callstate s f' rs m') + Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' -> + Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' -> + step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs m) + E0 (Callstate s fd rs m'') | exec_Mbuiltin: forall s f sp rs m ef args res b t v m', external_call ef ge rs##args m t v m' -> @@ -202,69 +190,65 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Mannot ef args :: b) rs m) t (State s f sp b rs m') | exec_Mgoto: - forall s fb f sp lbl c rs m c', - Genv.find_funct_ptr ge fb = Some (Internal f) -> + forall s f sp lbl c rs m c', find_label lbl f.(fn_code) = Some c' -> - step (State s fb sp (Mgoto lbl :: c) rs m) - E0 (State s fb sp c' rs m) + step (State s f sp (Mgoto lbl :: c) rs m) + E0 (State s f sp c' rs m) | exec_Mcond_true: - forall s fb f sp cond args lbl c rs m c', + forall s f sp cond args lbl c rs m c', eval_condition cond rs##args m = Some true -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> find_label lbl f.(fn_code) = Some c' -> - step (State s fb sp (Mcond cond args lbl :: c) rs m) - E0 (State s fb sp c' (undef_temps rs) m) + step (State s f sp (Mcond cond args lbl :: c) rs m) + E0 (State s f sp c' (undef_temps rs) m) | exec_Mcond_false: forall s f sp cond args lbl c rs m, eval_condition cond rs##args m = Some false -> step (State s f sp (Mcond cond args lbl :: c) rs m) E0 (State s f sp c (undef_temps rs) m) | exec_Mjumptable: - forall s fb f sp arg tbl c rs m n lbl c', + forall s f sp arg tbl c rs m n lbl c', rs arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some lbl -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> find_label lbl f.(fn_code) = Some c' -> - step (State s fb sp (Mjumptable arg tbl :: c) rs m) - E0 (State s fb sp c' (undef_temps rs) m) + step (State s f sp (Mjumptable arg tbl :: c) rs m) + E0 (State s f sp c' (undef_temps rs) m) | exec_Mreturn: - forall s fb stk soff c rs m f m', - Genv.find_funct_ptr ge fb = Some (Internal f) -> + forall s f stk soff c rs m m' m'', 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' -> - step (State s fb (Vptr stk soff) (Mreturn :: c) rs m) - E0 (Returnstate s rs m') + Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' -> + Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' -> + step (State s f (Vptr stk soff) (Mreturn :: c) rs m) + E0 (Returnstate s rs m'') | exec_function_internal: - forall s fb rs m f m1 m2 m3 stk, - Genv.find_funct_ptr ge fb = Some (Internal f) -> + forall s f rs m m1 m2 m3 stk, Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> + Mem.free m1 stk (Int.unsigned f.(fn_retaddr_ofs)) (Int.unsigned f.(fn_retaddr_ofs) + 4) = Some m2 -> 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 -> - step (Callstate s fb rs m) - E0 (State s fb sp f.(fn_code) (undef_temps rs) m3) + store_stack m2 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m3 -> + (4 | Int.unsigned f.(fn_retaddr_ofs)) -> + step (Callstate s (Internal f) rs m) + E0 (State s f sp f.(fn_code) (undef_temps rs) m3) | exec_function_external: - forall s fb rs m t rs' ef args res m', - Genv.find_funct_ptr ge fb = Some (External ef) -> + forall s ef rs m t rs' args res m', external_call ef ge args m t res m' -> extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> rs' = (rs#(loc_result (ef_sig ef)) <- res) -> - step (Callstate s fb rs m) + step (Callstate s (External ef) rs m) t (Returnstate s rs' m') | exec_return: - forall s f sp ra c rs m, - step (Returnstate (Stackframe f sp ra c :: s) rs m) + forall s f sp c rs m, + step (Returnstate (Stackframe f sp c :: s) rs m) E0 (State s f sp c rs m). End RELSEM. Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall fb m0, + | initial_state_intro: forall b fd m0, let ge := Genv.globalenv p in Genv.init_mem p = Some m0 -> - Genv.find_symbol ge p.(prog_main) = Some fb -> - initial_state p (Callstate nil fb (Regmap.init Vundef) m0). + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some fd -> + initial_state p (Callstate nil fd (Regmap.init Vundef) m0). Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index b731487..cd01beb 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -29,7 +29,6 @@ Require LTL. Require Import Linear. Require Import Lineartyping. Require Import Mach. -Require Import Machsem. Require Import Bounds. Require Import Conventions. Require Import Stacklayout. @@ -422,23 +421,31 @@ Definition frame_perm_freeable (m: mem) (sp: block): Prop := forall ofs, 0 <= ofs < fe.(fe_size) -> ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> + ofs < fe.(fe_ofs_retaddr) \/ fe.(fe_ofs_retaddr) + 4 <= ofs -> Mem.perm m sp ofs Cur Freeable. Lemma offset_of_index_perm: forall m sp idx, - index_valid idx -> + index_valid idx -> idx <> FI_retaddr -> frame_perm_freeable m sp -> Mem.range_perm m sp (offset_of_index fe idx) (offset_of_index fe idx + AST.typesize (type_of_index idx)) Cur Freeable. Proof. intros. exploit offset_of_index_valid; eauto. intros [A B]. - exploit offset_of_index_disj_stack_data_2; eauto. intros. - red; intros. apply H0. omega. omega. + exploit offset_of_index_disj. + instantiate (1 := FI_retaddr); exact I. + eexact H. + red. destruct idx; auto || congruence. + change (AST.typesize (type_of_index FI_retaddr)) with 4. + change (offset_of_index fe FI_retaddr) with fe.(fe_ofs_retaddr). + intros C. + exploit offset_of_index_disj_stack_data_2; eauto. intros D. + red; intros. apply H1. omega. omega. omega. Qed. Lemma store_index_succeeds: forall m sp idx v, - index_valid idx -> + index_valid idx -> idx <> FI_retaddr -> frame_perm_freeable m sp -> exists m', Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m'. @@ -520,7 +527,7 @@ Qed. Lemma index_contains_inj_undef: forall j m sp idx, - index_valid idx -> + index_valid idx -> idx <> FI_retaddr -> frame_perm_freeable m sp -> index_contains_inj j m sp idx Vundef. Proof. @@ -550,7 +557,7 @@ Definition agree_regs (j: meminj) (ls: locset) (rs: regset) : Prop := Record agree_frame (j: meminj) (ls ls0: locset) (m: mem) (sp: block) (m': mem) (sp': block) - (parent retaddr: val) : Prop := + (parent: val) : Prop := mk_agree_frame { (** Unused registers have the same value as in the caller *) @@ -576,12 +583,9 @@ Record agree_frame (j: meminj) (ls ls0: locset) In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) -> ls (S (Incoming ofs ty)) = ls0 (S (Outgoing ofs ty)); - (** The back link and return address slots of the Mach frame contain - the [parent] and [retaddr] values, respectively. *) + (** The back link contains the [parent] value. *) agree_link: index_contains m' sp' FI_link parent; - agree_retaddr: - index_contains m' sp' FI_retaddr retaddr; (** The areas of the frame reserved for saving used callee-save registers always contain the values that those registers had @@ -623,7 +627,7 @@ Record agree_frame (j: meminj) (ls ls0: locset) }. Hint Resolve agree_unused_reg agree_locals agree_outgoing agree_incoming - agree_link agree_retaddr agree_saved_int agree_saved_float + agree_link agree_saved_int agree_saved_float agree_valid_linear agree_valid_mach agree_perm agree_wt_ls: stacking. @@ -763,11 +767,11 @@ Qed. (** Preservation under assignment of machine register. *) Lemma agree_frame_set_reg: - forall j ls ls0 m sp m' sp' parent ra r v, - agree_frame j ls ls0 m sp m' sp' parent ra -> + forall j ls ls0 m sp m' sp' parent r v, + agree_frame j ls ls0 m sp m' sp' parent -> mreg_within_bounds b r -> Val.has_type v (Loc.type (R r)) -> - agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent ra. + agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent. Proof. intros. inv H; constructor; auto; intros. rewrite Locmap.gso. auto. red. intuition congruence. @@ -794,10 +798,10 @@ Proof. Qed. Lemma agree_frame_undef_locs: - forall j ls0 m sp m' sp' parent ra regs ls, - agree_frame j ls ls0 m sp m' sp' parent ra -> + forall j ls0 m sp m' sp' parent regs ls, + agree_frame j ls ls0 m sp m' sp' parent -> incl (List.map R regs) temporaries -> - agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent ra. + agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent. Proof. induction regs; simpl; intros. auto. @@ -808,17 +812,17 @@ Proof. Qed. Lemma agree_frame_undef_temps: - forall j ls ls0 m sp m' sp' parent ra, - agree_frame j ls ls0 m sp m' sp' parent ra -> - agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent ra. + forall j ls ls0 m sp m' sp' parent, + agree_frame j ls ls0 m sp m' sp' parent -> + agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent. Proof. intros. unfold temporaries. apply agree_frame_undef_locs; auto. apply incl_refl. Qed. Lemma agree_frame_undef_setstack: - forall j ls ls0 m sp m' sp' parent ra, - agree_frame j ls ls0 m sp m' sp' parent ra -> - agree_frame j (Linear.undef_setstack ls) ls0 m sp m' sp' parent ra. + forall j ls ls0 m sp m' sp' parent, + agree_frame j ls ls0 m sp m' sp' parent -> + agree_frame j (Linear.undef_setstack ls) ls0 m sp m' sp' parent. Proof. intros. unfold Linear.undef_setstack, destroyed_at_move. apply agree_frame_undef_locs; auto. @@ -826,9 +830,9 @@ Proof. Qed. Lemma agree_frame_undef_op: - forall j ls ls0 m sp m' sp' parent ra op, - agree_frame j ls ls0 m sp m' sp' parent ra -> - agree_frame j (Linear.undef_op op ls) ls0 m sp m' sp' parent ra. + forall j ls ls0 m sp m' sp' parent op, + agree_frame j ls ls0 m sp m' sp' parent -> + agree_frame j (Linear.undef_op op ls) ls0 m sp m' sp' parent. Proof. intros. exploit agree_frame_undef_temps; eauto. @@ -838,13 +842,13 @@ Qed. (** Preservation by assignment to local slot *) Lemma agree_frame_set_local: - forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'', - agree_frame j ls ls0 m sp m' sp' parent retaddr -> + forall j ls ls0 m sp m' sp' parent ofs ty v v' m'', + agree_frame j ls ls0 m sp m' sp' parent -> slot_within_bounds f b (Local ofs ty) -> val_inject j v v' -> Val.has_type v ty -> Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_local ofs ty)) v' = Some m'' -> - agree_frame j (Locmap.set (S (Local ofs ty)) v ls) ls0 m sp m'' sp' parent retaddr. + agree_frame j (Locmap.set (S (Local ofs ty)) v ls) ls0 m sp m'' sp' parent. Proof. intros. inv H. change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3. @@ -863,8 +867,6 @@ Proof. rewrite Locmap.gso; auto. red; auto. (* parent *) eapply gso_index_contains; eauto. red; auto. -(* retaddr *) - eapply gso_index_contains; eauto. red; auto. (* int callee save *) eapply gso_index_contains_inj; eauto. simpl; auto. (* float callee save *) @@ -880,13 +882,13 @@ Qed. (** Preservation by assignment to outgoing slot *) Lemma agree_frame_set_outgoing: - forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'', - agree_frame j ls ls0 m sp m' sp' parent retaddr -> + forall j ls ls0 m sp m' sp' parent ofs ty v v' m'', + agree_frame j ls ls0 m sp m' sp' parent -> slot_within_bounds f b (Outgoing ofs ty) -> val_inject j v v' -> Val.has_type v ty -> Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_arg ofs ty)) v' = Some m'' -> - agree_frame j (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 m sp m'' sp' parent retaddr. + agree_frame j (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 m sp m'' sp' parent. Proof. intros. inv H. change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3. @@ -899,7 +901,7 @@ Proof. unfold Locmap.set. simpl. destruct (Loc.eq (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))). inv e. eapply gss_index_contains_inj; eauto. case_eq (Loc.overlap_aux ty ofs ofs0 || Loc.overlap_aux ty0 ofs0 ofs); intros. - apply index_contains_inj_undef. auto. + apply index_contains_inj_undef. auto. congruence. red; intros. eapply Mem.perm_store_1; eauto. eapply gso_index_contains_inj; eauto. red. eapply Loc.overlap_aux_false_1; eauto. @@ -907,8 +909,6 @@ Proof. rewrite Locmap.gso; auto. red; auto. (* parent *) eapply gso_index_contains; eauto with stacking. red; auto. -(* retaddr *) - eapply gso_index_contains; eauto with stacking. red; auto. (* int callee save *) eapply gso_index_contains_inj; eauto with stacking. simpl; auto. (* float callee save *) @@ -924,8 +924,8 @@ Qed. (** General invariance property with respect to memory changes. *) Lemma agree_frame_invariant: - forall j ls ls0 m sp m' sp' parent retaddr m1 m1', - agree_frame j ls ls0 m sp m' sp' parent retaddr -> + forall j ls ls0 m sp m' sp' parent m1 m1', + agree_frame j ls ls0 m sp m' sp' parent -> (Mem.valid_block m sp -> Mem.valid_block m1 sp) -> (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') -> @@ -937,7 +937,7 @@ Lemma agree_frame_invariant: (forall ofs k p, ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> Mem.perm m' sp' ofs k p -> Mem.perm m1' sp' ofs k p) -> - agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. + agree_frame j ls ls0 m1 sp m1' sp' parent. Proof. intros. assert (IC: forall idx v, @@ -956,13 +956,13 @@ Qed. (** A variant of the latter, for use with external calls *) Lemma agree_frame_extcall_invariant: - forall j ls ls0 m sp m' sp' parent retaddr m1 m1', - agree_frame j ls ls0 m sp m' sp' parent retaddr -> + forall j ls ls0 m sp m' sp' parent m1 m1', + agree_frame j ls ls0 m sp m' sp' parent -> (Mem.valid_block m sp -> Mem.valid_block m1 sp) -> (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') -> mem_unchanged_on (loc_out_of_reach j m) m' m1' -> - agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. + agree_frame j ls ls0 m1 sp m1' sp' parent. Proof. intros. assert (REACH: forall ofs, @@ -978,13 +978,13 @@ Qed. (** Preservation by parallel stores in the Linear and Mach codes *) Lemma agree_frame_parallel_stores: - forall j ls ls0 m sp m' sp' parent retaddr chunk addr addr' v v' m1 m1', - agree_frame j ls ls0 m sp m' sp' parent retaddr -> + forall j ls ls0 m sp m' sp' parent chunk addr addr' v v' m1 m1', + agree_frame j ls ls0 m sp m' sp' parent -> Mem.inject j m m' -> val_inject j addr addr' -> Mem.storev chunk m addr v = Some m1 -> Mem.storev chunk m' addr' v' = Some m1' -> - agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. + agree_frame j ls ls0 m1 sp m1' sp' parent. Proof. Opaque Int.add. intros until m1'. intros AG MINJ VINJ STORE1 STORE2. @@ -1014,11 +1014,11 @@ Qed. (** Preservation by increasing memory injections (allocations and external calls) *) Lemma agree_frame_inject_incr: - forall j ls ls0 m sp m' sp' parent retaddr m1 m1' j', - agree_frame j ls ls0 m sp m' sp' parent retaddr -> + forall j ls ls0 m sp m' sp' parent m1 m1' j', + agree_frame j ls ls0 m sp m' sp' parent -> inject_incr j j' -> inject_separated j j' m1 m1' -> Mem.valid_block m1' sp' -> - agree_frame j' ls ls0 m sp m' sp' parent retaddr. + agree_frame j' ls ls0 m sp m' sp' parent. Proof. intros. inv H. constructor; auto; intros; eauto with stacking. case_eq (j b0). @@ -1054,11 +1054,11 @@ Proof. Qed. Lemma agree_frame_return: - forall j ls ls0 m sp m' sp' parent retaddr ls', - agree_frame j ls ls0 m sp m' sp' parent retaddr -> + forall j ls ls0 m sp m' sp' parent ls', + agree_frame j ls ls0 m sp m' sp' parent -> agree_callee_save ls' ls -> wt_locset ls' -> - agree_frame j ls' ls0 m sp m' sp' parent retaddr. + agree_frame j ls' ls0 m sp m' sp' parent. Proof. intros. red in H0. inv H; constructor; auto; intros. rewrite H0; auto. apply mreg_not_within_bounds_callee_save; auto. @@ -1070,10 +1070,10 @@ Qed. (** Preservation at tailcalls (when [ls0] is changed but not [ls]). *) Lemma agree_frame_tailcall: - forall j ls ls0 m sp m' sp' parent retaddr ls0', - agree_frame j ls ls0 m sp m' sp' parent retaddr -> + forall j ls ls0 m sp m' sp' parent ls0', + agree_frame j ls ls0 m sp m' sp' parent -> agree_callee_save ls0 ls0' -> - agree_frame j ls ls0' m sp m' sp' parent retaddr. + agree_frame j ls ls0' m sp m' sp' parent. Proof. intros. red in H0. inv H; constructor; auto; intros. rewrite <- H0; auto. apply mreg_not_within_bounds_callee_save; auto. @@ -1082,7 +1082,6 @@ Proof. rewrite <- H0; auto. Qed. - (** Properties of [agree_callee_save]. *) Lemma agree_callee_save_return_regs: @@ -1123,7 +1122,6 @@ Variable mkindex: Z -> frame_index. Variable ty: typ. Variable j: meminj. Variable cs: list stackframe. -Variable fb: block. Variable sp: block. Variable csregs: list mreg. Variable ls: locset. @@ -1156,6 +1154,8 @@ Hypothesis mkindex_inj: Hypothesis mkindex_diff: forall r idx, idx <> mkindex (number r) -> index_diff (mkindex (number r)) idx. +Hypothesis mkindex_not_retaddr: + forall r, mkindex (number r) <> FI_retaddr. Hypothesis csregs_typ: forall r, In r csregs -> mreg_type r = ty. @@ -1172,9 +1172,9 @@ Lemma save_callee_save_regs_correct: agree_regs j ls rs -> exists rs', exists m', star step tge - (State cs fb (Vptr sp Int.zero) + (State cs tf (Vptr sp Int.zero) (save_callee_save_regs bound number mkindex ty fe l k) rs m) - E0 (State cs fb (Vptr sp Int.zero) k rs' m') + E0 (State cs tf (Vptr sp Int.zero) k rs' m') /\ (forall r, In r l -> number r < bound fe -> index_contains_inj j m' sp (mkindex (number r)) (ls (R r))) @@ -1201,7 +1201,7 @@ Proof. unfold save_callee_save_reg. destruct (zlt (number a) (bound fe)). (* a store takes place *) - exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. + exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. auto. eauto. instantiate (1 := rs a). intros [m1 ST]. exploit (IHl k (undef_setstack rs) m1). auto with coqlib. auto. red; eauto with mem. @@ -1244,13 +1244,13 @@ Qed. End SAVE_CALLEE_SAVE. Lemma save_callee_save_correct: - forall j ls rs sp cs fb k m, + forall j ls rs sp cs k m, agree_regs j (call_regs ls) rs -> wt_locset (call_regs ls) -> frame_perm_freeable m sp -> exists rs', exists m', star step tge - (State cs fb (Vptr sp Int.zero) (save_callee_save fe k) rs m) - E0 (State cs fb (Vptr sp Int.zero) k rs' m') + (State cs tf (Vptr sp Int.zero) (save_callee_save fe k) rs m) + E0 (State cs tf (Vptr sp Int.zero) k rs' m') /\ (forall r, In r int_callee_save_regs -> index_int_callee_save r < b.(bound_int_callee_save) -> index_contains_inj j m' sp (FI_saved_int (index_int_callee_save r)) (call_regs ls (R r))) @@ -1275,12 +1275,13 @@ Transparent destroyed_at_move_regs. fe_num_int_callee_save index_int_callee_save FI_saved_int Tint - j cs fb sp int_callee_save_regs (call_regs ls)). + j cs sp int_callee_save_regs (call_regs ls)). intros. apply index_int_callee_save_inj; auto. intros. simpl. split. apply Zge_le. apply index_int_callee_save_pos; auto. assumption. auto. intros; congruence. intros; simpl. destruct idx; auto. congruence. + intros; congruence. intros. apply int_callee_save_type. auto. auto. auto. @@ -1293,12 +1294,13 @@ Transparent destroyed_at_move_regs. fe_num_float_callee_save index_float_callee_save FI_saved_float Tfloat - j cs fb sp float_callee_save_regs (call_regs ls)). + j cs sp float_callee_save_regs (call_regs ls)). intros. apply index_float_callee_save_inj; auto. intros. simpl. split. apply Zge_le. apply index_float_callee_save_pos; auto. assumption. simpl; auto. intros; congruence. intros; simpl. destruct idx; auto. congruence. + intros; congruence. intros. apply float_callee_save_type. auto. auto. auto. @@ -1369,28 +1371,28 @@ Qed. saving of the used callee-save registers). *) Lemma function_prologue_correct: - forall j ls ls0 rs m1 m1' m2 sp parent ra cs fb k, + forall j ls ls0 rs m1 m1' m2 sp parent cs k, agree_regs j ls rs -> agree_callee_save ls ls0 -> wt_locset ls -> Mem.inject j m1 m1' -> Mem.alloc m1 0 f.(Linear.fn_stacksize) = (m2, sp) -> - Val.has_type parent Tint -> Val.has_type ra Tint -> + Val.has_type parent Tint -> exists j', exists rs', exists m2', exists sp', exists m3', exists m4', exists m5', Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp') - /\ store_stack m2' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m3' - /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) ra = Some m4' + /\ Mem.free m2' sp' (Int.unsigned tf.(fn_retaddr_ofs)) (Int.unsigned tf.(fn_retaddr_ofs) + 4) = Some m3' + /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m4' /\ star step tge - (State cs fb (Vptr sp' Int.zero) (save_callee_save fe k) (undef_temps rs) m4') - E0 (State cs fb (Vptr sp' Int.zero) k rs' m5') + (State cs tf (Vptr sp' Int.zero) (save_callee_save fe k) (undef_temps rs) m4') + E0 (State cs tf (Vptr sp' Int.zero) k rs' m5') /\ agree_regs j' (call_regs ls) rs' - /\ agree_frame j' (call_regs ls) ls0 m2 sp m5' sp' parent ra + /\ agree_frame j' (call_regs ls) ls0 m2 sp m5' sp' parent /\ inject_incr j j' /\ inject_separated j j' m1 m1' /\ Mem.inject j' m2 m5' - /\ stores_in_frame sp' m2' m5'. + /\ stores_in_frame sp' m3' m5'. Proof. - intros until k; intros AGREGS AGCS WTREGS INJ1 ALLOC TYPAR TYRA. + intros until k; intros AGREGS AGCS WTREGS INJ1 ALLOC TYPAR. rewrite unfold_transf_function. unfold fn_stacksize, fn_link_ofs, fn_retaddr_ofs. (* Allocation step *) @@ -1415,14 +1417,37 @@ Proof. assert (~Mem.valid_block m1' sp') by eauto with mem. contradiction. intros [j' [INJ2 [INCR [MAP1 MAP2]]]]. - assert (PERM: frame_perm_freeable m2' sp'). - red; intros. eapply Mem.perm_alloc_2; eauto. + (* separation *) + assert (SEP: forall b0 delta, j' b0 = Some(sp', delta) -> b0 = sp /\ delta = fe_stack_data fe). + intros. destruct (zeq b0 sp). + subst b0. rewrite MAP1 in H; inv H; auto. + rewrite MAP2 in H; auto. + assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto. + assert (~Mem.valid_block m1' sp') by eauto with mem. + contradiction. + (* Freeing step *) + assert (OFSRA: Int.unsigned (Int.repr (fe_ofs_retaddr fe)) = fe_ofs_retaddr fe). + apply (offset_of_index_no_overflow FI_retaddr). exact I. + rewrite OFSRA. + assert (FREE: { m3' | Mem.free m2' sp' (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + 4) = Some m3'}). + apply Mem.range_perm_free. + exploit (offset_of_index_valid FI_retaddr). exact I. + unfold offset_of_index. simpl AST.typesize. intros [A B]. + red; intros. eapply Mem.perm_alloc_2; eauto. omega. + destruct FREE as [m3' FREE]. + assert (INJ3: Mem.inject j' m2 m3'). + eapply Mem.free_right_inject; eauto. + intros. exploit SEP; eauto. intros [A B]. subst b1 delta. + exploit (offset_of_index_disj_stack_data_1 FI_retaddr). exact I. + unfold offset_of_index. simpl AST.typesize. intros. + exploit Mem.perm_alloc_3. eexact ALLOC. eauto. intros. + generalize bound_stack_data_stacksize; intros. + omega. + assert (PERM: frame_perm_freeable m3' sp'). + red; intros. eapply Mem.perm_free_1; eauto. eapply Mem.perm_alloc_2; eauto. (* Store of parent *) - exploit (store_index_succeeds m2' sp' FI_link parent). red; auto. auto. - intros [m3' STORE2]. - (* Store of retaddr *) - exploit (store_index_succeeds m3' sp' FI_retaddr ra). red; auto. red; eauto with mem. - intros [m4' STORE3]. + exploit (store_index_succeeds m3' sp' FI_link parent). red; auto. congruence. auto. + intros [m4' STORE]. (* Saving callee-save registers *) assert (PERM4: frame_perm_freeable m4' sp'). red; intros. eauto with mem. @@ -1432,32 +1457,21 @@ Proof. eexact PERM4. intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]]. (* stores in frames *) - assert (SIF: stores_in_frame sp' m2' m5'). + assert (SIF: stores_in_frame sp' m3' m5'). econstructor; eauto. rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; auto. red; auto. - econstructor; eauto. - rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; auto. red; auto. - (* separation *) - assert (SEP: forall b0 delta, j' b0 = Some(sp', delta) -> b0 = sp /\ delta = fe_stack_data fe). - intros. destruct (zeq b0 sp). - subst b0. rewrite MAP1 in H; inv H; auto. - rewrite MAP2 in H; auto. - assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto. - assert (~Mem.valid_block m1' sp') by eauto with mem. - contradiction. (* Conclusions *) exists j'; exists rs'; exists m2'; exists sp'; exists m3'; exists m4'; exists m5'. + (* alloc *) + split. auto. + (* free *) split. auto. (* store parent *) split. change Tint with (type_of_index FI_link). change (fe_ofs_link fe) with (offset_of_index fe FI_link). apply store_stack_succeeds; auto. red; auto. - (* store retaddr *) - split. change Tint with (type_of_index FI_retaddr). - change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr). - apply store_stack_succeeds; auto. red; auto. (* saving of registers *) - split. eexact STEPS. + split. rewrite <- unfold_transf_function. eexact STEPS. (* agree_regs *) split. auto. (* agree frame *) @@ -1467,18 +1481,13 @@ Proof. elim H. apply temporary_within_bounds; auto. apply AGCS. apply mreg_not_within_bounds_callee_save; auto. (* locals *) - simpl. apply index_contains_inj_undef; auto. + simpl. apply index_contains_inj_undef; auto. congruence. (* outgoing *) - simpl. apply index_contains_inj_undef; auto. + simpl. apply index_contains_inj_undef; auto. congruence. (* incoming *) unfold call_regs. apply AGCS. auto. (* parent *) apply OTHERS; auto. red; auto. - eapply gso_index_contains; eauto. red; auto. - eapply gss_index_contains; eauto. red; auto. - red; auto. - (* retaddr *) - apply OTHERS; auto. red; auto. eapply gss_index_contains; eauto. red; auto. (* int callee save *) rewrite <- AGCS. replace (ls (R r)) with (call_regs ls (R r)). @@ -1499,7 +1508,7 @@ Proof. (* valid sp *) eauto with mem. (* valid sp' *) - eapply stores_in_frame_valid with (m := m2'); eauto with mem. + eapply stores_in_frame_valid with (m := m3'); eauto with mem. (* bounds *) exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto. (* perms *) @@ -1531,7 +1540,6 @@ Variable ty: typ. Variable csregs: list mreg. Variable j: meminj. Variable cs: list stackframe. -Variable fb: block. Variable sp: block. Variable ls0: locset. Variable m: mem. @@ -1558,9 +1566,9 @@ Lemma restore_callee_save_regs_correct: agree_unused ls0 rs -> exists rs', star step tge - (State cs fb (Vptr sp Int.zero) + (State cs tf (Vptr sp Int.zero) (restore_callee_save_regs bound number mkindex ty fe l k) rs m) - E0 (State cs fb (Vptr sp Int.zero) k rs' m) + E0 (State cs tf (Vptr sp Int.zero) k rs' m) /\ (forall r, In r l -> val_inject j (ls0 (R r)) (rs' r)) /\ (forall r, ~(In r l) -> rs' r = rs r) /\ agree_unused ls0 rs'. @@ -1605,13 +1613,13 @@ Qed. End RESTORE_CALLEE_SAVE. Lemma restore_callee_save_correct: - forall j ls ls0 m sp m' sp' pa ra cs fb rs k, - agree_frame j ls ls0 m sp m' sp' pa ra -> + forall j ls ls0 m sp m' sp' pa cs rs k, + agree_frame j ls ls0 m sp m' sp' pa -> agree_unused j ls0 rs -> exists rs', star step tge - (State cs fb (Vptr sp' Int.zero) (restore_callee_save fe k) rs m') - E0 (State cs fb (Vptr sp' Int.zero) k rs' m') + (State cs tf (Vptr sp' Int.zero) (restore_callee_save fe k) rs m') + E0 (State cs tf (Vptr sp' Int.zero) k rs' m') /\ (forall r, In r int_callee_save_regs \/ In r float_callee_save_regs -> val_inject j (ls0 (R r)) (rs' r)) @@ -1627,7 +1635,7 @@ Proof. FI_saved_int Tint int_callee_save_regs - j cs fb sp' ls0 m'); auto. + j cs sp' ls0 m'); auto. intros. unfold mreg_within_bounds. rewrite (int_callee_save_type r H1). tauto. eapply agree_saved_int; eauto. apply incl_refl. @@ -1640,7 +1648,7 @@ Proof. FI_saved_float Tfloat float_callee_save_regs - j cs fb sp' ls0 m'); auto. + j cs sp' ls0 m'); auto. intros. unfold mreg_within_bounds. rewrite (float_callee_save_type r H1). tauto. eapply agree_saved_float; eauto. apply incl_refl. @@ -1660,57 +1668,94 @@ Qed. registers + reloading of the link and return address + freeing of the frame). *) +Remark mem_range_perm_free_twice: + forall m blk lo1 hi1 lo2 hi2, + (forall ofs, lo1 <= ofs < hi2 -> ofs < hi1 \/ lo2 <= ofs -> Mem.perm m blk ofs Cur Freeable) -> + lo1 <= hi1 /\ lo2 <= hi2 -> hi1 < lo2 -> + exists m', exists m'', + Mem.free m blk lo1 hi1 = Some m' /\ Mem.free m' blk lo2 hi2 = Some m''. +Proof. + intros. + destruct (Mem.range_perm_free m blk lo1 hi1) as [m' FREE1]. + red; intros. apply H. omega. omega. + destruct (Mem.range_perm_free m' blk lo2 hi2) as [m'' FREE2]. + red; intros. eapply Mem.perm_free_1; eauto. right. omega. + apply H. omega. omega. + exists m'; exists m''; auto. +Qed. + Lemma function_epilogue_correct: - forall j ls ls0 m sp m' sp' pa ra cs fb rs k m1, + forall j ls ls0 m sp m' sp' pa cs rs k m1, agree_regs j ls rs -> - agree_frame j ls ls0 m sp m' sp' pa ra -> + agree_frame j ls ls0 m sp m' sp' pa -> Mem.inject j m m' -> Mem.free m sp 0 f.(Linear.fn_stacksize) = Some m1 -> - exists rs1, exists m1', + exists rs1, exists m1', exists m2', load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) = Some pa - /\ load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) = Some ra - /\ Mem.free m' sp' 0 tf.(fn_stacksize) = Some m1' + /\ Mem.free m' sp' 0 (Int.unsigned tf.(fn_retaddr_ofs)) = Some m1' + /\ Mem.free m1' sp' (Int.unsigned tf.(fn_retaddr_ofs) + 4) tf.(fn_stacksize) = Some m2' /\ star step tge - (State cs fb (Vptr sp' Int.zero) (restore_callee_save fe k) rs m') - E0 (State cs fb (Vptr sp' Int.zero) k rs1 m') + (State cs tf (Vptr sp' Int.zero) (restore_callee_save fe k) rs m') + E0 (State cs tf (Vptr sp' Int.zero) k rs1 m') /\ agree_regs j (return_regs ls0 ls) rs1 /\ agree_callee_save (return_regs ls0 ls) ls0 /\ rs1 IT1 = rs IT1 - /\ Mem.inject j m1 m1'. + /\ Mem.inject j m1 m2'. Proof. intros. + assert (RETADDR: Int.unsigned tf.(fn_retaddr_ofs) = fe.(fe_ofs_retaddr)). + rewrite unfold_transf_function. unfold fn_retaddr_ofs. + apply (offset_of_index_no_overflow FI_retaddr). exact I. + rewrite RETADDR. (* can free *) - destruct (Mem.range_perm_free m' sp' 0 (fn_stacksize tf)) as [m1' FREE]. - rewrite unfold_transf_function; unfold fn_stacksize. red; intros. + destruct (mem_range_perm_free_twice m' sp' + 0 (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + 4) (fe_size fe)) + as [m1' [m2' [FREE1 FREE2]]]. + intros. assert (EITHER: fe_stack_data fe <= ofs < fe_stack_data fe + Linear.fn_stacksize f - \/ (ofs < fe_stack_data fe \/ fe_stack_data fe + Linear.fn_stacksize f <= ofs)) + \/ (ofs < fe_stack_data fe \/ fe_stack_data fe + Linear.fn_stacksize f <= ofs)) by omega. destruct EITHER. replace ofs with ((ofs - fe_stack_data fe) + fe_stack_data fe) by omega. eapply Mem.perm_inject with (f := j). eapply agree_inj; eauto. eauto. eapply Mem.free_range_perm; eauto. omega. - eapply agree_perm; eauto. + eapply agree_perm; eauto. + apply (offset_of_index_valid FI_retaddr). exact I. + omega. (* inject after free *) - assert (INJ1: Mem.inject j m1 m1'). - eapply Mem.free_inject with (l := (sp, 0, f.(Linear.fn_stacksize)) :: nil); eauto. - simpl. rewrite H2. auto. - intros. exploit agree_inj_unique; eauto. intros [P Q]; subst b1 delta. - exists 0; exists (Linear.fn_stacksize f); split. auto with coqlib. - eapply agree_bounds. eauto. eapply Mem.perm_max. eauto. + assert (UNMAPPED: forall b1 delta ofs k0 p, + j b1 = Some (sp', delta) -> + Mem.perm m1 b1 ofs k0 p -> + False). + { + intros. + exploit agree_inj_unique; eauto. intros [P Q]; subst b1 delta. + eelim Mem.perm_free_2. eexact H2. eapply agree_bounds; eauto. + eapply Mem.perm_free_3; eauto. apply Mem.perm_max with k0. eauto. eauto. + } + assert (INJ1: Mem.inject j m1 m2'). + { + eapply Mem.free_right_inject. + eapply Mem.free_right_inject. + eapply Mem.free_left_inject. eauto. eauto. + eauto. + intros; eapply UNMAPPED; eauto. + eauto. + intros; eapply UNMAPPED; eauto. + } (* can execute epilogue *) exploit restore_callee_save_correct; eauto. instantiate (1 := rs). red; intros. - rewrite <- (agree_unused_reg _ _ _ _ _ _ _ _ _ H0). auto. auto. + rewrite <- (agree_unused_reg _ _ _ _ _ _ _ _ H0). auto. auto. intros [rs1 [A [B C]]]. (* conclusions *) - exists rs1; exists m1'. + exists rs1; exists m1'; exists m2'. split. rewrite unfold_transf_function; unfold fn_link_ofs. eapply index_contains_load_stack with (idx := FI_link); eauto with stacking. - split. rewrite unfold_transf_function; unfold fn_retaddr_ofs. - eapply index_contains_load_stack with (idx := FI_retaddr); eauto with stacking. - split. auto. + split. exact FREE1. + split. rewrite unfold_transf_function; unfold fn_stacksize. exact FREE2. split. eexact A. - split. red;intros. unfold return_regs. + split. red; intros. unfold return_regs. generalize (register_classification r) (int_callee_save_not_destroyed r) (float_callee_save_not_destroyed r); intros. destruct (in_dec Loc.eq (R r) temporaries). rewrite C; auto. @@ -1742,14 +1787,12 @@ Inductive match_stacks (j: meminj) (m m': mem): hi <= bound -> hi <= bound' -> match_globalenvs j hi -> tailcall_possible sg -> match_stacks j m m' nil nil sg bound bound' - | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg bound bound' trf + | match_stacks_cons: forall f sp ls c cs sp' c' cs' sg bound bound' tf (TAIL: is_tail c (Linear.fn_code f)) (WTF: wt_function f) - (FINDF: Genv.find_funct_ptr tge fb = Some (Internal trf)) - (TRF: transf_function f = OK trf) + (TRF: transf_function f = OK tf) (TRC: transl_code (make_env (function_bounds f)) c = c') - (TY_RA: Val.has_type ra Tint) - (FRM: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs')) + (FRM: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs')) (ARGS: forall ofs ty, In (S (Outgoing ofs ty)) (loc_arguments sg) -> slot_within_bounds f (function_bounds f) (Outgoing ofs ty)) @@ -1758,7 +1801,7 @@ Inductive match_stacks (j: meminj) (m m': mem): (BELOW': sp' < bound'), match_stacks j m m' (Linear.Stackframe f (Vptr sp Int.zero) ls c :: cs) - (Stackframe fb (Vptr sp' Int.zero) ra c' :: cs') + (Stackframe tf (Vptr sp' Int.zero) c' :: cs') sg bound bound'. (** Invariance with respect to change of bounds. *) @@ -1949,14 +1992,6 @@ Proof. induction 1; simpl; auto. Qed. -Lemma match_stacks_type_retaddr: - forall j m m' cs cs' sg bound bound', - match_stacks j m m' cs cs' sg bound bound' -> - Val.has_type (parent_ra cs') Tint. -Proof. - induction 1; simpl; auto. -Qed. - (** * Syntactic properties of the translation *) (** Preservation of code labels through the translation. *) @@ -2157,9 +2192,8 @@ Lemma find_function_translated: agree_regs j ls rs -> match_stacks j m m' cs cs' sg bound bound' -> Linear.find_function ge ros ls = Some f -> - exists bf, exists tf, - find_function_ptr tge ros rs = Some bf - /\ Genv.find_funct_ptr tge bf = Some tf + exists tf, + find_function tge ros rs = Some tf /\ transf_fundef f = OK tf. Proof. intros until f; intros AG MS FF. @@ -2168,13 +2202,14 @@ Proof. exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in FF. rewrite Genv.find_funct_find_funct_ptr in FF. exploit function_ptr_translated; eauto. intros [tf [A B]]. - exists b; exists tf; split; auto. simpl. + exists tf; split; auto. simpl. generalize (AG m0). rewrite EQ. intro INJ. inv INJ. - inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. - destruct (Genv.find_symbol ge i) as [b|] eqn:?; try discriminate. + rewrite Int.add_zero_l. + inv MG. rewrite DOMAIN in H2. inv H2. simpl. rewrite A. apply dec_eq_true. + eapply FUNCTIONS; eauto. + destruct (Genv.find_symbol ge i) as [b|] eqn:FS; try discriminate. exploit function_ptr_translated; eauto. intros [tf [A B]]. - exists b; exists tf; split; auto. simpl. - rewrite symbols_preserved. auto. + exists tf; split; auto. simpl. rewrite symbols_preserved. rewrite FS. auto. Qed. Hypothesis wt_prog: wt_program prog. @@ -2262,9 +2297,9 @@ Variables m m': mem. Variables ls ls0: locset. Variable rs: regset. Variables sp sp': block. -Variables parent retaddr: val. +Variables parent: val. Hypothesis AGR: agree_regs j ls rs. -Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent retaddr. +Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent. Lemma transl_annot_param_correct: forall l, @@ -2327,31 +2362,29 @@ End ANNOT_ARGUMENTS. - Well-typedness of [f]. *) -Inductive match_states: Linear.state -> Machsem.state -> Prop := +Inductive match_states: Linear.state -> Mach.state -> Prop := | match_states_intro: - forall cs f sp c ls m cs' fb sp' rs m' j tf + forall cs f sp c ls m cs' sp' rs m' j tf (MINJ: Mem.inject j m m') (STACKS: match_stacks j m m' cs cs' f.(Linear.fn_sig) sp sp') (TRANSL: transf_function f = OK tf) - (FIND: Genv.find_funct_ptr tge fb = Some (Internal tf)) (WTF: wt_function f) (AGREGS: agree_regs j ls rs) - (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs')) + (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs')) (TAIL: is_tail c (Linear.fn_code f)), match_states (Linear.State cs f (Vptr sp Int.zero) c ls m) - (Machsem.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m') + (Mach.State cs' tf (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m') | match_states_call: - forall cs f ls m cs' fb rs m' j tf + forall cs f ls m cs' rs m' j tf (MINJ: Mem.inject j m m') (STACKS: match_stacks j m m' cs cs' (Linear.funsig f) (Mem.nextblock m) (Mem.nextblock m')) (TRANSL: transf_fundef f = OK tf) - (FIND: Genv.find_funct_ptr tge fb = Some tf) (WTF: wt_fundef f) (WTLS: wt_locset ls) (AGREGS: agree_regs j ls rs) (AGLOCS: agree_callee_save ls (parent_locset cs)), match_states (Linear.Callstate cs f ls m) - (Machsem.Callstate cs' fb rs m') + (Mach.Callstate cs' tf rs m') | match_states_return: forall cs ls m cs' rs m' j sg (MINJ: Mem.inject j m m') @@ -2360,12 +2393,12 @@ Inductive match_states: Linear.state -> Machsem.state -> Prop := (AGREGS: agree_regs j ls rs) (AGLOCS: agree_callee_save ls (parent_locset cs)), match_states (Linear.Returnstate cs ls m) - (Machsem.Returnstate cs' rs m'). + (Mach.Returnstate cs' rs m'). Theorem transf_step_correct: forall s1 t s2, Linear.step ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), - exists s2', plus Machsem.step tge s1' t s2' /\ match_states s2 s2'. + exists s2', plus Mach.step tge s1' t s2' /\ match_states s2 s2'. Proof. assert (RED: forall f i c, transl_code (make_env (function_bounds f)) (i :: c) = @@ -2430,6 +2463,7 @@ Proof. apply index_local_valid; auto. red; auto. apply index_arg_valid; auto. + assert (idx <> FI_retaddr) by (unfold idx; destruct sl; congruence). exploit store_index_succeeds; eauto. eapply agree_perm; eauto. instantiate (1 := rs0 r). intros [m1' STORE]. econstructor; split. @@ -2440,12 +2474,12 @@ Proof. econstructor; eauto with coqlib. eapply Mem.store_outside_inject; eauto. intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta. - rewrite size_type_chunk in H5. + rewrite size_type_chunk in H6. exploit offset_of_index_disj_stack_data_2; eauto. exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. omega. apply match_stacks_change_mach_mem with m'; auto. - eauto with mem. eauto with mem. intros. rewrite <- H4; eapply Mem.load_store_other; eauto. left; unfold block; omega. + eauto with mem. eauto with mem. intros. rewrite <- H5; eapply Mem.load_store_other; eauto. left; unfold block; omega. apply agree_regs_set_slot. apply agree_regs_undef_setstack; auto. destruct sl. eapply agree_frame_set_local. eapply agree_frame_undef_setstack; eauto. auto. auto. @@ -2514,15 +2548,11 @@ Proof. eapply agree_frame_parallel_stores; eauto. (* Lcall *) - exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. - exploit is_tail_transf_function; eauto. intros IST. simpl in IST. - exploit Asmgenretaddr.return_address_exists. eexact IST. - intros [ra D]. + exploit find_function_translated; eauto. intros [tf' [A B]]. econstructor; split. apply plus_one. econstructor; eauto. econstructor; eauto. econstructor; eauto with coqlib. - simpl; auto. intros; red. split. generalize (loc_arguments_acceptable _ _ H0). simpl. omega. apply Zle_trans with (size_arguments (Linear.funsig f')); auto. @@ -2534,13 +2564,13 @@ Proof. simpl; red; auto. (* Ltailcall *) - exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. + exploit find_function_translated; eauto. intros [tf' [A B]]. exploit function_epilogue_correct; eauto. - intros [rs1 [m1' [P [Q [R [S [T [U [V W]]]]]]]]]. + intros [rs1 [m1' [m2' [P [Q [R [S [T [U [V W ]]]]]]]]]]. econstructor; split. eapply plus_right. eexact S. econstructor; eauto. - replace (find_function_ptr tge ros rs1) - with (find_function_ptr tge ros rs0). eauto. + replace (find_function tge ros rs1) + with (find_function tge ros rs0). eauto. destruct ros; simpl; auto. inv WTI. rewrite V; auto. traceEq. econstructor; eauto. @@ -2549,11 +2579,15 @@ Proof. apply match_stacks_change_linear_mem with m. apply match_stacks_change_mach_mem with m'0. auto. - eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. - intros. rewrite <- H2. eapply Mem.load_free; eauto. left; unfold block; omega. - eauto with mem. intros. eapply Mem.perm_free_3; eauto. + eauto with mem. + intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. + eapply Mem.perm_free_1; eauto. left; unfold block; omega. + intros. erewrite Mem.load_free. erewrite Mem.load_free; eauto. + left; unfold block; omega. eauto. left; unfold block; omega. + eauto with mem. + intros. eapply Mem.perm_free_3; eauto. apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. - apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. + apply Zlt_le_weak. change (Mem.valid_block m2' sp'). eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. eapply find_function_well_typed; eauto. apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto. @@ -2646,7 +2680,7 @@ Proof. (* Lreturn *) exploit function_epilogue_correct; eauto. - intros [rs1 [m1' [P [Q [R [S [T [U [V W]]]]]]]]]. + intros [rs1 [m1' [m2' [P [Q [R [S [T [U [V W]]]]]]]]]]. econstructor; split. eapply plus_right. eexact S. econstructor; eauto. traceEq. @@ -2655,11 +2689,15 @@ Proof. apply match_stacks_change_linear_mem with m. apply match_stacks_change_mach_mem with m'0. eauto. - eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. - intros. rewrite <- H1. eapply Mem.load_free; eauto. left; unfold block; omega. - eauto with mem. intros. eapply Mem.perm_free_3; eauto. + eauto with mem. + intros. eapply Mem.perm_free_1. eauto. left; unfold block; omega. + eapply Mem.perm_free_1; eauto. left; unfold block; omega. + intros. erewrite Mem.load_free. erewrite Mem.load_free; eauto. + left; unfold block; omega. eauto. left; unfold block; omega. + eauto with mem. + intros. eapply Mem.perm_free_3; eauto. apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. - apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. + apply Zlt_le_weak. change (Mem.valid_block m2' sp'). eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto. (* internal function *) @@ -2669,11 +2707,14 @@ Proof. inversion WTF as [|f' WTFN]. subst f'. exploit function_prologue_correct; eauto. eapply match_stacks_type_sp; eauto. - eapply match_stacks_type_retaddr; eauto. intros [j' [rs' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]]. econstructor; split. - eapply plus_left. econstructor; eauto. - rewrite (unfold_transf_function _ _ TRANSL). unfold fn_code. unfold transl_body. + eapply plus_left. econstructor; eauto. + rewrite (unfold_transf_function _ _ TRANSL). unfold fn_retaddr_ofs. + generalize (offset_of_index_no_overflow _ _ TRANSL FI_retaddr I). + unfold offset_of_index. intros EQ; rewrite EQ. + apply (offset_of_index_aligned f FI_retaddr). + rewrite (unfold_transf_function _ _ TRANSL) at 2. unfold fn_code. unfold transl_body. eexact D. traceEq. generalize (Mem.alloc_result _ _ _ _ _ H). intro SP_EQ. generalize (Mem.alloc_result _ _ _ _ _ A). intro SP'_EQ. @@ -2686,7 +2727,10 @@ Proof. rewrite zeq_false. auto. omega. intros. eapply stores_in_frame_valid; eauto with mem. intros. eapply stores_in_frame_perm; eauto with mem. - intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto. + eapply Mem.perm_free_1; eauto. left; unfold block; omega. eauto with mem. + intros. rewrite <- H1. + transitivity (Mem.load chunk m3' b ofs). eapply stores_in_frame_contents; eauto. + transitivity (Mem.load chunk m2' b ofs). eapply Mem.load_free; eauto. left; unfold block; omega. eapply Mem.load_alloc_unchanged; eauto. red. congruence. auto with coqlib. @@ -2724,7 +2768,7 @@ Qed. Lemma transf_initial_states: forall st1, Linear.initial_state prog st1 -> - exists st2, Machsem.initial_state tprog st2 /\ match_states st1 st2. + exists st2, Mach.initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inv H. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. @@ -2733,6 +2777,7 @@ Proof. eapply Genv.init_mem_transf_partial; eauto. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. eauto. + eexact FIND. econstructor; eauto. eapply Genv.initmem_inject; eauto. apply match_stacks_empty with (Mem.nextblock m0). omega. omega. @@ -2753,7 +2798,7 @@ Qed. Lemma transf_final_states: forall st1 st2 r, - match_states st1 st2 -> Linear.final_state st1 r -> Machsem.final_state st2 r. + match_states st1 st2 -> Linear.final_state st1 r -> Mach.final_state st2 r. Proof. intros. inv H0. inv H. inv STACKS. constructor. @@ -2762,7 +2807,7 @@ Proof. Qed. Theorem transf_program_correct: - forward_simulation (Linear.semantics prog) (Machsem.semantics tprog). + forward_simulation (Linear.semantics prog) (Mach.semantics tprog). Proof. eapply forward_simulation_plus. eexact symbols_preserved. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v deleted file mode 100644 index 2324cd5..0000000 --- a/backend/Stackingtyping.v +++ /dev/null @@ -1,250 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Type preservation for the [Stacking] pass. *) - -Require Import Coqlib. -Require Import Errors. -Require Import Integers. -Require Import AST. -Require Import Op. -Require Import Locations. -Require Import Conventions. -Require Import Linear. -Require Import Lineartyping. -Require Import Mach. -Require Import Machtyping. -Require Import Bounds. -Require Import Stacklayout. -Require Import Stacking. -Require Import Stackingproof. - -(** We show that the Mach code generated by the [Stacking] pass - is well-typed if the original LTLin code is. *) - -Definition wt_instrs (k: Mach.code) : Prop := - forall i, In i k -> wt_instr i. - -Lemma wt_instrs_cons: - forall i k, - wt_instr i -> wt_instrs k -> wt_instrs (i :: k). -Proof. - unfold wt_instrs; intros. elim H1; intro. - subst i0; auto. auto. -Qed. - -Section TRANSL_FUNCTION. - -Variable f: Linear.function. -Let fe := make_env (function_bounds f). -Variable tf: Mach.function. -Hypothesis TRANSF_F: transf_function f = OK tf. - -Lemma wt_fold_right: - forall (A: Type) (f: A -> code -> code) (k: code) (l: list A), - (forall x k', In x l -> wt_instrs k' -> wt_instrs (f x k')) -> - wt_instrs k -> - wt_instrs (List.fold_right f k l). -Proof. - induction l; intros; simpl. - auto. - apply H. apply in_eq. apply IHl. - intros. apply H. auto with coqlib. auto. - auto. -Qed. - -Lemma wt_save_callee_save_int: - forall k, - wt_instrs k -> - wt_instrs (save_callee_save_int fe k). -Proof. - intros. unfold save_callee_save_int, save_callee_save_regs. - apply wt_fold_right; auto. - intros. unfold save_callee_save_reg. - case (zlt (index_int_callee_save x) (fe_num_int_callee_save fe)); intro. - apply wt_instrs_cons; auto. - apply wt_Msetstack. apply int_callee_save_type; auto. - auto. -Qed. - -Lemma wt_save_callee_save_float: - forall k, - wt_instrs k -> - wt_instrs (save_callee_save_float fe k). -Proof. - intros. unfold save_callee_save_float, save_callee_save_regs. - apply wt_fold_right; auto. - intros. unfold save_callee_save_reg. - case (zlt (index_float_callee_save x) (fe_num_float_callee_save fe)); intro. - apply wt_instrs_cons; auto. - apply wt_Msetstack. apply float_callee_save_type; auto. - auto. -Qed. - -Lemma wt_restore_callee_save_int: - forall k, - wt_instrs k -> - wt_instrs (restore_callee_save_int fe k). -Proof. - intros. unfold restore_callee_save_int, restore_callee_save_regs. - apply wt_fold_right; auto. - intros. unfold restore_callee_save_reg. - case (zlt (index_int_callee_save x) (fe_num_int_callee_save fe)); intro. - apply wt_instrs_cons; auto. - constructor. apply int_callee_save_type; auto. - auto. -Qed. - -Lemma wt_restore_callee_save_float: - forall k, - wt_instrs k -> - wt_instrs (restore_callee_save_float fe k). -Proof. - intros. unfold restore_callee_save_float, restore_callee_save_regs. - apply wt_fold_right; auto. - intros. unfold restore_callee_save_reg. - case (zlt (index_float_callee_save x) (fe_num_float_callee_save fe)); intro. - apply wt_instrs_cons; auto. - constructor. apply float_callee_save_type; auto. - auto. -Qed. - -Lemma wt_save_callee_save: - forall k, - wt_instrs k -> wt_instrs (save_callee_save fe k). -Proof. - intros. unfold save_callee_save. - apply wt_save_callee_save_int. apply wt_save_callee_save_float. auto. -Qed. - -Lemma wt_restore_callee_save: - forall k, - wt_instrs k -> wt_instrs (restore_callee_save fe k). -Proof. - intros. unfold restore_callee_save. - apply wt_restore_callee_save_int. apply wt_restore_callee_save_float. auto. -Qed. - -Lemma wt_transl_instr: - forall instr k, - In instr f.(Linear.fn_code) -> - Lineartyping.wt_instr f instr -> - wt_instrs k -> - wt_instrs (transl_instr fe instr k). -Proof. - intros. - generalize (instr_is_within_bounds f instr H H0); intro BND. - destruct instr; unfold transl_instr; inv H0; simpl in BND. - (* getstack *) - destruct BND. - destruct s; simpl in *; apply wt_instrs_cons; auto; - constructor; auto. - (* setstack *) - destruct s. - apply wt_instrs_cons; auto. apply wt_Msetstack. auto. - auto. - apply wt_instrs_cons; auto. apply wt_Msetstack. auto. - (* op, move *) - simpl. apply wt_instrs_cons. constructor; auto. auto. - (* op, others *) - apply wt_instrs_cons; auto. - constructor. - destruct o; simpl; congruence. - rewrite H6. symmetry. apply type_shift_stack_operation. - (* load *) - apply wt_instrs_cons; auto. - constructor; auto. - rewrite H4. destruct a; reflexivity. - (* store *) - apply wt_instrs_cons; auto. - constructor; auto. - rewrite H4. destruct a; reflexivity. - (* call *) - apply wt_instrs_cons; auto. - constructor; auto. - (* tailcall *) - apply wt_restore_callee_save. apply wt_instrs_cons; auto. - constructor; auto. - destruct s0; auto. rewrite H5; auto. - (* builtin *) - apply wt_instrs_cons; auto. - constructor; auto. - (* annot *) - apply wt_instrs_cons; auto. - constructor; auto. - (* label *) - apply wt_instrs_cons; auto. - constructor. - (* goto *) - apply wt_instrs_cons; auto. - constructor; auto. - (* cond *) - apply wt_instrs_cons; auto. - constructor; auto. - (* jumptable *) - apply wt_instrs_cons; auto. - constructor; auto. - (* return *) - apply wt_restore_callee_save. apply wt_instrs_cons. constructor. auto. -Qed. - -End TRANSL_FUNCTION. - -Lemma wt_transf_function: - forall f tf, - transf_function f = OK tf -> - Lineartyping.wt_function f -> - wt_function tf. -Proof. - intros. - exploit unfold_transf_function; eauto. intro EQ. - set (b := function_bounds f) in *. - set (fe := make_env b) in *. - constructor. - change (wt_instrs (fn_code tf)). - rewrite EQ; simpl; unfold transl_body. - unfold fe, b; apply wt_save_callee_save; auto. - unfold transl_code. apply wt_fold_right. - intros. eapply wt_transl_instr; eauto. - red; intros. elim H1. - rewrite EQ; unfold fn_stacksize. - generalize (size_pos f). - generalize (size_no_overflow _ _ H). - unfold fe, b. omega. -Qed. - -Lemma wt_transf_fundef: - forall f tf, - Lineartyping.wt_fundef f -> - transf_fundef f = OK tf -> - wt_fundef tf. -Proof. - intros f tf WT. inversion WT; subst. - simpl; intros; inversion H. constructor. - unfold transf_fundef, transf_partial_fundef. - caseEq (transf_function f0); simpl; try congruence. - intros tfn TRANSF EQ. inversion EQ; subst tf. - constructor; eapply wt_transf_function; eauto. -Qed. - -Lemma program_typing_preserved: - forall (p: Linear.program) (tp: Mach.program), - transf_program p = OK tp -> - Lineartyping.wt_program p -> - Machtyping.wt_program tp. -Proof. - intros; red; intros. - generalize (transform_partial_program_function transf_fundef p i f H H1). - intros [f0 [IN TRANSF]]. - apply wt_transf_fundef with f0; auto. - eapply H0; eauto. -Qed. -- cgit v1.2.3