From aaa49526068f528f2233de0dace43549432fba52 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 12 Apr 2008 12:55:21 +0000 Subject: Revu gestion retaddr et link dans Stacking git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Bounds.v | 2 +- backend/Conventions.v | 41 ++- backend/Lineartyping.v | 2 +- backend/Mach.v | 7 +- backend/Machabstr.v | 114 ++++--- backend/Machabstr2concr.v | 735 ++++++++++++++++++++++------------------------ backend/Machconcr.v | 55 ++-- backend/Machtyping.v | 46 +-- backend/PPC.v | 32 +- backend/PPCgen.v | 29 +- backend/PPCgenproof.v | 137 ++++----- backend/PPCgenretaddr.v | 8 +- backend/RTLtyping.v | 5 +- backend/Reloadtyping.v | 13 +- backend/Stacking.v | 26 +- backend/Stackingproof.v | 689 +++++++++++++++++++++++-------------------- backend/Stackingtyping.v | 25 +- 17 files changed, 1032 insertions(+), 934 deletions(-) (limited to 'backend') diff --git a/backend/Bounds.v b/backend/Bounds.v index 0e8b9faf..415a85f0 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -63,7 +63,7 @@ Definition slot_within_bounds (s: slot) := | Local ofs Tint => 0 <= ofs < bound_int_local b | Local ofs Tfloat => 0 <= ofs < bound_float_local b | Outgoing ofs ty => 14 <= ofs /\ ofs + typesize ty <= bound_outgoing b - | Incoming ofs ty => 14 <= ofs /\ ofs + typesize ty <= size_arguments funct.(fn_sig) + | Incoming ofs ty => In (S s) (loc_parameters funct.(fn_sig)) end. Definition instr_within_bounds (i: instruction) := diff --git a/backend/Conventions.v b/backend/Conventions.v index ea7d448e..2ab2ca91 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -710,28 +710,25 @@ Proof. destruct s; try tauto. destruct s0; tauto. Qed. -(** A tailcall is possible if and only if the size of arguments is 14. *) - -Lemma tailcall_possible_size: - forall s, tailcall_possible s <-> size_arguments s = 14. -Proof. - intro; split; intro. - assert (forall tyl iregl fregl ofs, - (forall l, In l (loc_arguments_rec tyl iregl fregl ofs) -> - match l with R _ => True | S _ => False end) -> - size_arguments_rec tyl iregl fregl ofs = ofs). - induction tyl; simpl; intros. - auto. - destruct a. destruct iregl. elim (H0 _ (in_eq _ _)). - apply IHtyl; intros. apply H0. auto with coqlib. - destruct fregl. elim (H0 _ (in_eq _ _)). - apply IHtyl; intros. apply H0. auto with coqlib. - unfold size_arguments. apply H0. assumption. - red; intros. - generalize (loc_arguments_acceptable s l H0). - destruct l; simpl. auto. destruct s0; intro; auto. - generalize (loc_arguments_bounded _ _ _ H0). - generalize (typesize_pos t). omega. +(** Decide whether a tailcall is possible. *) + +Definition tailcall_is_possible (sg: signature) : bool := + let fix tcisp (l: list loc) := + match l with + | nil => true + | R _ :: l' => tcisp l' + | S _ :: l' => false + end + in tcisp (loc_arguments sg). + +Lemma tailcall_is_possible_correct: + forall s, tailcall_is_possible s = true -> tailcall_possible s. +Proof. + intro s. unfold tailcall_is_possible, tailcall_possible. + generalize (loc_arguments s). induction l; simpl; intros. + elim H0. + destruct a. + destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate. Qed. (** ** Location of function parameters *) diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 0f5a1ec9..551462c8 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -36,7 +36,7 @@ Definition slot_valid (s: slot) := match s with | Local ofs ty => 0 <= ofs | Outgoing ofs ty => 14 <= ofs - | Incoming ofs ty => 14 <= ofs /\ ofs + typesize ty <= size_arguments funct.(fn_sig) + | Incoming ofs ty => In (S s) (loc_parameters funct.(fn_sig)) end. Definition slot_writable (s: slot) := diff --git a/backend/Mach.v b/backend/Mach.v index f7275041..c64903b8 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -70,7 +70,9 @@ Record function: Set := mkfunction { fn_sig: signature; fn_code: code; fn_stacksize: Z; - fn_framesize: Z }. + fn_framesize: Z; + fn_link_ofs: int; + fn_retaddr_ofs: int }. Definition fundef := AST.fundef function. @@ -137,6 +139,3 @@ Definition find_function_ptr Genv.find_symbol ge symb end. -Definition align_16_top (lo hi: Z) := - Zmax 0 (((hi - lo + 15) / 16) * 16 + lo). - diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 32a316ae..76e37e8e 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -46,54 +46,87 @@ Require Import Mach. (** * Structure of abstract stack frames *) -(** An abstract stack frame comprises a low bound [fr_low] (the high bound - is implicitly 0) and a mapping from (type, offset) pairs to values. *) +(** An abstract stack frame is a mapping from (type, offset) pairs to + values. Like location sets (see module [Locations]), overlap + can occur. *) -Record frame : Set := mkframe { - fr_low: Z; - fr_contents: typ -> Z -> val -}. +Definition frame : Set := typ -> Z -> val. Definition typ_eq: forall (ty1 ty2: typ), {ty1=ty2} + {ty1<>ty2}. Proof. decide equality. Defined. Definition update (ty: typ) (ofs: Z) (v: val) (f: frame) : frame := - mkframe f.(fr_low) - (fun ty' ofs' => - if zeq ofs ofs' then - if typ_eq ty ty' then v else Vundef - else - if zle (ofs' + AST.typesize ty') ofs then f.(fr_contents) ty' ofs' - else if zle (ofs + AST.typesize ty) ofs' then f.(fr_contents) ty' ofs' - else Vundef). - -Definition empty_frame := mkframe 0 (fun ty ofs => Vundef). - -(** [get_slot fr ty ofs v] holds if the frame [fr] contains value [v] + fun ty' ofs' => + if zeq ofs ofs' then + if typ_eq ty ty' then v else Vundef + else + if zle (ofs' + AST.typesize ty') ofs then f ty' ofs' + else if zle (ofs + AST.typesize ty) ofs' then f ty' ofs' + else Vundef. + +Lemma update_same: + forall ty ofs v fr, + update ty ofs v fr ty ofs = v. +Proof. + unfold update; intros. + rewrite zeq_true. rewrite dec_eq_true. auto. +Qed. + +Lemma update_other: + forall ty ofs v fr ty' ofs', + ofs + AST.typesize ty <= ofs' \/ ofs' + AST.typesize ty' <= ofs -> + update ty ofs v fr ty' ofs' = fr ty' ofs'. +Proof. + unfold update; intros. + generalize (AST.typesize_pos ty). + generalize (AST.typesize_pos ty'). intros. + rewrite zeq_false. + destruct H. rewrite zle_false. apply zle_true. auto. omega. + apply zle_true. auto. + omega. +Qed. + +Definition empty_frame : frame := fun ty ofs => Vundef. + +Section FRAME_ACCESSES. + +Variable f: function. + +(** A slot [(ty, ofs)] within a frame is valid in function [f] if it lies + within the bounds of [f]'s frame, and it does not overlap with + the slots reserved for the return address and the back link. *) + +Inductive slot_valid: typ -> Z -> Prop := + slot_valid_intro: + forall ty ofs, + 0 <= ofs -> + ofs + AST.typesize ty <= f.(fn_framesize) -> + (ofs + AST.typesize ty <= Int.signed f.(fn_link_ofs) + \/ Int.signed f.(fn_link_ofs) + 4 <= ofs) -> + (ofs + AST.typesize ty <= Int.signed f.(fn_retaddr_ofs) + \/ Int.signed f.(fn_retaddr_ofs) + 4 <= ofs) -> + slot_valid ty ofs. + +(** [get_slot f fr ty ofs v] holds if the frame [fr] contains value [v] with type [ty] at word offset [ofs]. *) Inductive get_slot: frame -> typ -> Z -> val -> Prop := | get_slot_intro: forall fr ty ofs v, - 24 <= ofs -> - fr.(fr_low) + ofs + AST.typesize ty <= 0 -> - v = fr.(fr_contents) ty (fr.(fr_low) + ofs) -> + slot_valid ty ofs -> + v = fr ty (ofs - f.(fn_framesize)) -> get_slot fr ty ofs v. -(** [set_slot fr ty ofs v fr'] holds if frame [fr'] is obtained from +(** [set_slot f fr ty ofs v fr'] holds if frame [fr'] is obtained from frame [fr] by storing value [v] with type [ty] at word offset [ofs]. *) Inductive set_slot: frame -> typ -> Z -> val -> frame -> Prop := | set_slot_intro: forall fr ty ofs v fr', - 24 <= ofs -> - fr.(fr_low) + ofs + AST.typesize ty <= 0 -> - fr' = update ty (fr.(fr_low) + ofs) v fr -> + slot_valid ty ofs -> + fr' = update ty (ofs - f.(fn_framesize)) v fr -> set_slot fr ty ofs v fr'. -Definition init_frame (f: function) := - mkframe (- f.(fn_framesize)) (fun ty ofs => Vundef). - (** Extract the values of the arguments of an external call. *) Inductive extcall_arg: regset -> frame -> loc -> val -> Prop := @@ -114,6 +147,8 @@ Definition extcall_arguments (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop := extcall_args rs fr (Conventions.loc_arguments sg) args. +End FRAME_ACCESSES. + (** Mach execution states. *) Inductive stackframe: Set := @@ -148,7 +183,9 @@ Inductive state: Set := (** [parent_frame s] returns the frame of the calling function. It is used to access function parameters that are passed on the stack - (the [Mgetparent] instruction). *) + (the [Mgetparent] instruction). + [parent_function s] returns the calling function itself. + Suitable defaults are used if there are no calling function. *) Definition parent_frame (s: list stackframe) : frame := match s with @@ -156,6 +193,15 @@ Definition parent_frame (s: list stackframe) : frame := | Stackframe f sp c fr :: s => fr end. +Definition empty_function := + mkfunction (mksignature nil None) nil 0 0 Int.zero Int.zero. + +Definition parent_function (s: list stackframe) : function := + match s with + | nil => empty_function + | Stackframe f sp c fr :: s => f + end. + Section RELSEM. Variable ge: genv. @@ -177,17 +223,17 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp c rs fr m) | exec_Mgetstack: forall s f sp ofs ty dst c rs fr m v, - get_slot fr ty (Int.signed ofs) v -> + get_slot f fr ty (Int.signed ofs) v -> step (State s f sp (Mgetstack ofs ty dst :: c) rs fr m) E0 (State s f sp c (rs#dst <- v) fr m) | exec_Msetstack: forall s f sp src ofs ty c rs fr m fr', - set_slot fr ty (Int.signed ofs) (rs src) fr' -> + set_slot f fr ty (Int.signed ofs) (rs src) fr' -> step (State s f sp (Msetstack src ofs ty :: c) rs fr m) E0 (State s f sp c rs fr' m) | exec_Mgetparam: forall s f sp ofs ty dst c rs fr m v, - get_slot (parent_frame s) ty (Int.signed ofs) v -> + get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v -> step (State s f sp (Mgetparam ofs ty dst :: c) rs fr m) E0 (State s f sp c (rs#dst <- v) fr m) | exec_Mop: @@ -251,11 +297,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> step (Callstate s (Internal f) rs m) E0 (State s f (Vptr stk (Int.repr (-f.(fn_framesize)))) - f.(fn_code) rs (init_frame f) m') + f.(fn_code) rs empty_frame m') | exec_function_external: forall s ef args res rs1 rs2 m t, event_match ef args t res -> - extcall_arguments rs1 (parent_frame s) ef.(ef_sig) args -> + extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args -> rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> step (Callstate s (External ef) rs1 m) t (Returnstate s rs2 m) diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index ffdfb336..2dd3134f 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -27,7 +27,6 @@ Require Import Mach. Require Import Machtyping. Require Import Machabstr. Require Import Machconcr. -Require Import Stackingproof. Require Import PPCgenretaddr. (** Two semantics were defined for the Mach intermediate language: @@ -48,27 +47,6 @@ Require Import PPCgenretaddr. Mach semantics as input). *) -Remark align_16_top_ge: - forall lo hi, - hi <= align_16_top lo hi. -Proof. - intros. unfold align_16_top. apply Zmax_bound_r. - assert (forall x, x <= (x + 15) / 16 * 16). - intro. assert (16 > 0). omega. - generalize (Z_div_mod_eq (x + 15) 16 H). intro. - replace ((x + 15) / 16 * 16) with ((x + 15) - (x + 15) mod 16). - generalize (Z_mod_lt (x + 15) 16 H). omega. - rewrite Zmult_comm. omega. - generalize (H (hi - lo)). omega. -Qed. - -Remark align_16_top_pos: - forall lo hi, - 0 <= align_16_top lo hi. -Proof. - intros. unfold align_16_top. apply Zmax_bound_l. omega. -Qed. - Remark size_type_chunk: forall ty, size_chunk (chunk_of_type ty) = AST.typesize ty. Proof. @@ -79,11 +57,16 @@ Qed. (** ** Agreement for one frame *) +Section FRAME_MATCH. + +Variable f: function. +Hypothesis wt_f: wt_function f. + (** The core idea of the simulation proof is that for all active functions, the memory-allocated activation record, in the concrete semantics, contains the same data as the Cminor stack block (at positive offsets) and the frame of the function (at negative - offsets) in the abstract semantics. + offsets) in the abstract semantics This intuition (activation record = Cminor stack data + frame) is formalized by the following predicate [frame_match fr sp base mm ms]. @@ -91,19 +74,18 @@ Qed. semantics. [ms] is the current memory state in the concrete semantics. The stack pointer is [Vptr sp base] in both semantics. *) -Inductive frame_match (fr: frame) (sp: block) (base: int) +Inductive frame_match (fr: frame) + (sp: block) (base: int) (mm ms: mem) : Prop := frame_match_intro: valid_block ms sp -> low_bound mm sp = 0 -> - low_bound ms sp = fr.(fr_low) -> + low_bound ms sp = -f.(fn_framesize) -> high_bound ms sp >= 0 -> - fr.(fr_low) <= -24 -> - Int.min_signed <= fr.(fr_low) -> - base = Int.repr fr.(fr_low) -> + base = Int.repr (-f.(fn_framesize)) -> (forall ty ofs, - fr.(fr_low) + 24 <= ofs -> ofs + AST.typesize ty <= 0 -> - load (chunk_of_type ty) ms sp ofs = Some(fr.(fr_contents) ty ofs)) -> + -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> + load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) -> frame_match fr sp base mm ms. (** The following two innocuous-looking lemmas are the key results @@ -140,22 +122,36 @@ Qed. to reading the corresponding slot from the frame (in the abstract semantics). *) +Lemma frame_match_load_stack: + forall fr sp base mm ms ty ofs, + frame_match fr sp base mm ms -> + 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> + load_stack ms (Vptr sp base) ty ofs = + Some (fr ty (Int.signed ofs - f.(fn_framesize))). +Proof. + intros. inv H. + unfold load_stack, Val.add, loadv. + replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs)) + with (Int.signed ofs - fn_framesize f). + apply H6. omega. omega. + inv wt_f. + assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f). + apply Int.signed_repr. + assert (0 <= Int.max_signed). compute; congruence. omega. + rewrite int_add_no_overflow. rewrite H. omega. + rewrite H. split. omega. + apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. + compute; congruence. +Qed. + Lemma frame_match_get_slot: forall fr sp base mm ms ty ofs v, frame_match fr sp base mm ms -> - get_slot fr ty (Int.signed ofs) v -> + get_slot f fr ty (Int.signed ofs) v -> load_stack ms (Vptr sp base) ty ofs = Some v. Proof. - intros. inv H. inv H0. - unfold load_stack, Val.add, loadv. - assert (Int.signed (Int.repr (fr_low fr)) = fr_low fr). - apply Int.signed_repr. - split. auto. apply Zle_trans with (-24). auto. compute; congruence. - assert (Int.signed (Int.add (Int.repr (fr_low fr)) ofs) = fr_low fr + Int.signed ofs). - rewrite int_add_no_overflow. rewrite H0. auto. - rewrite H0. split. omega. apply Zle_trans with 0. - generalize (AST.typesize_pos ty). omega. compute; congruence. - rewrite H9. apply H8. omega. auto. + intros. inversion H. inv H0. eapply frame_match_load_stack; eauto. + inv H7. auto. Qed. (** Assigning a value to a frame slot (in the abstract semantics) @@ -163,41 +159,42 @@ Qed. (in the concrete semantics). Moreover, agreement between frames and activation records is preserved. *) -Lemma frame_match_set_slot: - forall fr sp base mm ms ty ofs v fr', +Lemma frame_match_store_stack: + forall fr sp base mm ms ty ofs v, frame_match fr sp base mm ms -> - set_slot fr ty (Int.signed ofs) v fr' -> + 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> Val.has_type v ty -> Mem.extends mm ms -> exists ms', store_stack ms (Vptr sp base) ty ofs v = Some ms' /\ - frame_match fr' sp base mm ms' /\ - Mem.extends mm ms' /\ - Int.signed base + 24 <= Int.signed (Int.add base ofs). + frame_match (update ty (Int.signed ofs - f.(fn_framesize)) v fr) sp base mm ms' /\ + Mem.extends mm ms'. Proof. - intros. inv H. inv H0. + intros. inv H. inv wt_f. unfold store_stack, Val.add, storev. - assert (Int.signed (Int.repr (fr_low fr)) = fr_low fr). - apply Int.signed_repr. - split. auto. apply Zle_trans with (-24). auto. compute; congruence. - assert (Int.signed (Int.add (Int.repr (fr_low fr)) ofs) = fr_low fr + Int.signed ofs). - rewrite int_add_no_overflow. congruence. - rewrite H0. split. omega. apply Zle_trans with 0. - generalize (AST.typesize_pos ty). omega. compute; congruence. - rewrite H11. - assert (exists ms', store (chunk_of_type ty) ms sp (fr_low fr + Int.signed ofs) v = Some ms'). + assert (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs) = + Int.signed ofs - fn_framesize f). + assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f). + apply Int.signed_repr. + assert (0 <= Int.max_signed). compute; congruence. omega. + rewrite int_add_no_overflow. rewrite H. omega. + rewrite H. split. omega. + apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. + compute; congruence. + rewrite H. + assert (exists ms', store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v = Some ms'). apply valid_access_store. constructor. auto. omega. rewrite size_type_chunk. omega. - destruct H12 as [ms' STORE]. + destruct H7 as [ms' STORE]. generalize (low_bound_store _ _ _ _ _ _ STORE sp). intro LB. generalize (high_bound_store _ _ _ _ _ _ STORE sp). intro HB. exists ms'. split. exact STORE. (* frame match *) - split. constructor; simpl fr_low; try congruence. - eauto with mem. intros. simpl. - destruct (zeq (fr_low fr + Int.signed ofs) ofs0). subst ofs0. + split. constructor; try congruence. + eauto with mem. intros. unfold update. + destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0. destruct (typ_eq ty ty0). subst ty0. (* same *) transitivity (Some (Val.load_result (chunk_of_type ty) v)). @@ -206,33 +203,45 @@ Proof. (* mismatch *) eapply load_store_mismatch'; eauto with mem. destruct ty; destruct ty0; simpl; congruence. - destruct (zle (ofs0 + AST.typesize ty0) (fr_low fr + Int.signed ofs)). + destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)). (* disjoint *) - rewrite <- H10; auto. eapply load_store_other; eauto. + rewrite <- H8; auto. eapply load_store_other; eauto. right; left. rewrite size_type_chunk; auto. - destruct (zle (fr_low fr + Int.signed ofs + AST.typesize ty)). - rewrite <- H10; auto. eapply load_store_other; eauto. + destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)). + rewrite <- H8; auto. eapply load_store_other; eauto. right; right. rewrite size_type_chunk; auto. (* overlap *) eapply load_store_overlap'; eauto with mem. rewrite size_type_chunk; auto. rewrite size_type_chunk; auto. (* extends *) - split. eapply store_outside_extends; eauto. + eapply store_outside_extends; eauto. left. rewrite size_type_chunk. omega. - (* bound *) - omega. +Qed. + +Lemma frame_match_set_slot: + forall fr sp base mm ms ty ofs v fr', + frame_match fr sp base mm ms -> + set_slot f fr ty (Int.signed ofs) v fr' -> + Val.has_type v ty -> + Mem.extends mm ms -> + exists ms', + store_stack ms (Vptr sp base) ty ofs v = Some ms' /\ + frame_match fr' sp base mm ms' /\ + Mem.extends mm ms'. +Proof. + intros. inv H0. eapply frame_match_store_stack; eauto. + inv H3. auto. Qed. (** Agreement is preserved by stores within blocks other than the - one pointed to by [sp], or to the low 24 bytes - of the [sp] block. *) + one pointed to by [sp]. *) Lemma frame_match_store_other: forall fr sp base mm ms chunk b ofs v ms', frame_match fr sp base mm ms -> store chunk ms b ofs v = Some ms' -> - sp <> b \/ ofs + size_chunk chunk <= fr_low fr + 24 -> + sp <> b -> frame_match fr sp base mm ms'. Proof. intros. inv H. @@ -242,11 +251,13 @@ Proof. eauto with mem. congruence. congruence. - intros. rewrite <- H9; auto. + intros. rewrite <- H7; auto. eapply load_store_other; eauto. - elim H1; intro. auto. right. rewrite size_type_chunk. omega. Qed. +(** Agreement is preserved by parallel stores in the Machabstr + and the Machconcr semantics. *) + Lemma frame_match_store: forall fr sp base mm ms chunk b ofs v mm' ms', frame_match fr sp base mm ms -> @@ -262,31 +273,11 @@ Proof. apply frame_match_intro; auto. eauto with mem. congruence. congruence. congruence. - intros. rewrite <- H9; auto. eapply load_store_other; eauto. + intros. rewrite <- H7; auto. eapply load_store_other; eauto. destruct (zeq sp b). subst b. right. rewrite size_type_chunk. assert (valid_access mm chunk sp ofs) by eauto with mem. - inv H10. left. omega. - auto. -Qed. - -(** The low 24 bytes of a frame are preserved by a parallel - store in the two memory states. *) - -Lemma frame_match_store_link_invariant: - forall fr sp base mm ms chunk b ofs v mm' ms' ofs', - frame_match fr sp base mm ms -> - store chunk mm b ofs v = Some mm' -> - store chunk ms b ofs v = Some ms' -> - ofs' <= fr_low fr + 20 -> - load Mint32 ms' sp ofs' = load Mint32 ms sp ofs'. -Proof. - intros. inv H. - eapply load_store_other; eauto. - destruct (eq_block sp b). subst b. - right; left. change (size_chunk Mint32) with 4. - assert (valid_access mm chunk sp ofs) by eauto with mem. - inv H. omega. + inv H8. left. omega. auto. Qed. @@ -297,14 +288,12 @@ Qed. remain true. *) Lemma frame_match_new: - forall mm ms mm' ms' sp sp' f, + forall mm ms mm' ms' sp sp', mm.(nextblock) = ms.(nextblock) -> alloc mm 0 f.(fn_stacksize) = (mm', sp) -> - alloc ms (- f.(fn_framesize)) (align_16_top (- f.(fn_framesize)) f.(fn_stacksize)) = (ms', sp') -> - f.(fn_framesize) >= 24 -> - f.(fn_framesize) <= -Int.min_signed -> + alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp') -> sp = sp' /\ - frame_match (init_frame f) sp (Int.repr (-f.(fn_framesize))) mm' ms'. + frame_match empty_frame sp (Int.repr (-f.(fn_framesize))) mm' ms'. Proof. intros. assert (sp = sp'). @@ -315,13 +304,12 @@ Proof. generalize (low_bound_alloc_same _ _ _ _ _ H1). intro LBs. generalize (high_bound_alloc_same _ _ _ _ _ H0). intro HBm. generalize (high_bound_alloc_same _ _ _ _ _ H1). intro HBs. + inv wt_f. constructor; simpl; eauto with mem. - rewrite HBs. apply Zle_ge. apply align_16_top_pos. - omega. omega. + rewrite HBs. auto. intros. - eapply load_alloc_same'; eauto. omega. - rewrite size_type_chunk. apply Zle_trans with 0. auto. - apply align_16_top_pos. + eapply load_alloc_same'; eauto. + rewrite size_type_chunk. omega. Qed. Lemma frame_match_alloc: @@ -334,13 +322,13 @@ Lemma frame_match_alloc: Proof. intros. inversion H0. assert (valid_block mm sp). red. rewrite H. auto. - exploit low_bound_alloc_other. eexact H1. eexact H11. intro LBm. - exploit high_bound_alloc_other. eexact H1. eexact H11. intro HBm. + exploit low_bound_alloc_other. eexact H1. eexact H9. intro LBm. + exploit high_bound_alloc_other. eexact H1. eexact H9. intro HBm. exploit low_bound_alloc_other. eexact H2. eexact H3. intro LBs. exploit high_bound_alloc_other. eexact H2. eexact H3. intro HBs. apply frame_match_intro. eapply valid_block_alloc; eauto. - congruence. congruence. congruence. auto. auto. auto. + congruence. congruence. congruence. auto. auto. intros. eapply load_alloc_other; eauto. Qed. @@ -360,9 +348,138 @@ Proof. generalize (high_bound_free ms _ _ H0); intro HBs. apply frame_match_intro; auto. congruence. congruence. congruence. - intros. rewrite <- H8; auto. apply load_free. auto. + intros. rewrite <- H6; auto. apply load_free. auto. +Qed. + +End FRAME_MATCH. + +(** ** Accounting for the return address and back link *) + +Section EXTEND_FRAME. + +Variable f: function. +Hypothesis wt_f: wt_function f. +Variable cs: list Machconcr.stackframe. + +Definition extend_frame (fr: frame) : frame := + update Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize)) (parent_ra cs) + (update Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize)) (parent_sp cs) + fr). + +Lemma get_slot_extends: + forall fr ty ofs v, + get_slot f fr ty ofs v -> + get_slot f (extend_frame fr) ty ofs v. +Proof. + intros. inv H. constructor. auto. + inv H0. inv wt_f. generalize (AST.typesize_pos ty); intro. + unfold extend_frame. rewrite update_other. rewrite update_other. auto. + simpl; omega. simpl; omega. +Qed. + +Lemma update_commut: + forall ty1 ofs1 v1 ty2 ofs2 v2 fr, + ofs1 + AST.typesize ty1 <= ofs2 \/ + ofs2 + AST.typesize ty2 <= ofs1 -> + update ty1 ofs1 v1 (update ty2 ofs2 v2 fr) = + update ty2 ofs2 v2 (update ty1 ofs1 v1 fr). +Proof. + intros. unfold frame. + apply extensionality. intro ty. apply extensionality. intro ofs. + generalize (AST.typesize_pos ty1). + generalize (AST.typesize_pos ty2). + generalize (AST.typesize_pos ty); intros. + unfold update. + set (sz1 := AST.typesize ty1) in *. + set (sz2 := AST.typesize ty2) in *. + set (sz := AST.typesize ty) in *. + destruct (zeq ofs1 ofs). + rewrite zeq_false. + destruct (zle (ofs + sz) ofs2). auto. + destruct (zle (ofs2 + sz2) ofs). auto. + destruct (typ_eq ty1 ty); auto. + replace sz with sz1 in z. omegaContradiction. unfold sz1, sz; congruence. + omega. + + destruct (zle (ofs + sz) ofs1). + auto. + destruct (zle (ofs1 + sz1) ofs). + auto. + + destruct (zeq ofs2 ofs). + destruct (typ_eq ty2 ty); auto. + replace sz with sz2 in z. omegaContradiction. unfold sz2, sz; congruence. + destruct (zle (ofs + sz) ofs2); auto. + destruct (zle (ofs2 + sz2) ofs); auto. +Qed. + +Lemma set_slot_extends: + forall fr ty ofs v fr', + set_slot f fr ty ofs v fr' -> + set_slot f (extend_frame fr) ty ofs v (extend_frame fr'). +Proof. + intros. inv H. constructor. auto. + inv H0. inv wt_f. generalize (AST.typesize_pos ty); intro. + unfold extend_frame. + rewrite (update_commut ty). rewrite (update_commut ty). auto. + simpl. omega. + simpl. omega. +Qed. + +Lemma frame_match_load_link: + forall fr sp base mm ms, + frame_match f (extend_frame fr) sp base mm ms -> + load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some (parent_sp cs). +Proof. + intros. inversion wt_f. + replace (parent_sp cs) with + (extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))). + eapply frame_match_load_stack; eauto. + unfold extend_frame. rewrite update_other. apply update_same. simpl. omega. +Qed. + +Lemma frame_match_load_retaddr: + forall fr sp base mm ms, + frame_match f (extend_frame fr) sp base mm ms -> + load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some (parent_ra cs). +Proof. + intros. inversion wt_f. + replace (parent_ra cs) with + (extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))). + eapply frame_match_load_stack; eauto. + unfold extend_frame. apply update_same. +Qed. + +Lemma frame_match_function_entry: + forall mm ms mm' ms1 sp sp', + extends mm ms -> + alloc mm 0 f.(fn_stacksize) = (mm', sp) -> + alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp') -> + Val.has_type (parent_sp cs) Tint -> + Val.has_type (parent_ra cs) Tint -> + let base := Int.repr (-f.(fn_framesize)) in + exists ms2, exists ms3, + sp = sp' /\ + store_stack ms1 (Vptr sp base) Tint f.(fn_link_ofs) (parent_sp cs) = Some ms2 /\ + store_stack ms2 (Vptr sp base) Tint f.(fn_retaddr_ofs) (parent_ra cs) = Some ms3 /\ + frame_match f (extend_frame empty_frame) sp base mm' ms3 /\ + extends mm' ms3. +Proof. + intros. inversion wt_f. + exploit alloc_extends; eauto. omega. omega. intros [A EXT0]. + exploit frame_match_new. eauto. inv H. eexact H4. eauto. eauto. eauto. + fold base. intros [C FM0]. + destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ + FM0 wt_function_link H2 EXT0) + as [ms2 [STORE1 [FM1 EXT1]]]. + destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ + FM1 wt_function_retaddr H3 EXT1) + as [ms3 [STORE2 [FM3 EXT3]]]. + exists ms2; exists ms3; auto. Qed. +End EXTEND_FRAME. + (** ** Invariant for stacks *) Section SIMULATION. @@ -380,31 +497,27 @@ Let ge := Genv.globalenv p. their addresses increase strictly from caller to callee. *) +Definition stack_below (ts: list Machconcr.stackframe) (b: block) : Prop := + match parent_sp ts with + | Vptr sp base' => sp < b + | _ => False + end. + Inductive match_stacks: list Machabstr.stackframe -> list Machconcr.stackframe -> - block -> int -> mem -> mem -> Prop := - | match_stacks_nil: forall sp base mm ms, - load Mint32 ms sp (Int.signed base) = Some (Vptr Mem.nullptr Int.zero) -> - load Mint32 ms sp (Int.signed base + 12) = Some Vzero -> - match_stacks nil nil sp base mm ms - | match_stacks_cons: forall f sp' base' c fr s fb ra ts sp base mm ms, - frame_match fr sp' base' mm ms -> - sp' < sp -> - load Mint32 ms sp (Int.signed base) = Some (Vptr sp' base') -> - load Mint32 ms sp (Int.signed base + 12) = Some ra -> + mem -> mem -> Prop := + | match_stacks_nil: forall mm ms, + match_stacks nil nil mm ms + | match_stacks_cons: forall fb sp base c fr s f ra ts mm ms, Genv.find_funct_ptr ge fb = Some (Internal f) -> - match_stacks s ts sp' base' mm ms -> - match_stacks (Machabstr.Stackframe f (Vptr sp' base') c fr :: s) - (Machconcr.Stackframe fb (Vptr sp' base') ra c :: ts) - sp base mm ms. - -Remark frame_match_base_eq: - forall fr sp base mm ms, - frame_match fr sp base mm ms -> Int.signed base = fr_low fr. -Proof. - intros. inv H. apply Int.signed_repr. split; auto. - apply Zle_trans with (-24); auto. compute; congruence. -Qed. + wt_function f -> + frame_match f (extend_frame f ts fr) sp base mm ms -> + stack_below ts sp -> + Val.has_type ra Tint -> + match_stacks s ts mm ms -> + match_stacks (Machabstr.Stackframe f (Vptr sp base) c fr :: s) + (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts) + mm ms. (** If [match_stacks] holds, a lookup in the parent frame in the Machabstr semantics corresponds to two memory loads in the @@ -412,230 +525,128 @@ Qed. activation record, the second to read within this record. *) Lemma match_stacks_get_parent: - forall s ts sp base mm ms ty ofs v, - match_stacks s ts sp base mm ms -> - get_slot (parent_frame s) ty (Int.signed ofs) v -> - exists parent, - load_stack ms (Vptr sp base) Tint (Int.repr 0) = Some parent - /\ load_stack ms parent ty ofs = Some v. + forall s ts mm ms ty ofs v, + match_stacks s ts mm ms -> + get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v -> + load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v. Proof. intros. inv H; simpl in H0. - inv H0. simpl in H3. elimtype False. generalize (AST.typesize_pos ty). omega. - exists (Vptr sp' base'); split. - unfold load_stack. simpl. rewrite Int.add_zero. auto. - eapply frame_match_get_slot; eauto. + inv H0. inv H. simpl in H1. elimtype False. generalize (AST.typesize_pos ty). omega. + simpl. eapply frame_match_get_slot; eauto. + eapply get_slot_extends; eauto. Qed. -(** If [match_stacks] holds, reading memory at offsets 0 and 12 - from the stack pointer returns the stack pointer and return - address of the caller, respectively. *) +(** Preservation of the [match_stacks] invariant + by various kinds of memory stores. *) -Lemma match_stacks_load_links: - forall fr s ts sp base mm ms, - frame_match fr sp base mm ms -> - match_stacks s ts sp base mm ms -> - load_stack ms (Vptr sp base) Tint (Int.repr 0) = Some (parent_sp ts) /\ - load_stack ms (Vptr sp base) Tint (Int.repr 12) = Some (parent_ra ts). -Proof. - intros. unfold load_stack. simpl. rewrite Int.add_zero. - replace (Int.signed (Int.add base (Int.repr 12))) - with (Int.signed base + 12). - inv H0; simpl; auto. - inv H. rewrite Int.add_signed. - change (Int.signed (Int.repr 12)) with 12. - repeat rewrite Int.signed_repr. auto. - split. omega. apply Zle_trans with (-12). omega. compute; congruence. - split. auto. apply Zle_trans with (-24). auto. compute; congruence. -Qed. - -(** The [match_stacks] invariant is preserved by memory stores - outside the 24-byte reserved area at the bottom of activation records. -*) +Remark stack_below_trans: + forall ts b b', + stack_below ts b -> b <= b' -> stack_below ts b'. +Proof. + unfold stack_below; intros. + destruct (parent_sp ts); auto. omega. +Qed. Lemma match_stacks_store_other: - forall s ts sp base ms mm, - match_stacks s ts sp base mm ms -> + forall s ts ms mm, + match_stacks s ts mm ms -> forall chunk b ofs v ms', store chunk ms b ofs v = Some ms' -> - sp < b -> - match_stacks s ts sp base mm ms'. + stack_below ts b -> + match_stacks s ts mm ms'. Proof. induction 1; intros. - assert (sp <> b). unfold block; omega. constructor. - rewrite <- H. eapply load_store_other; eauto. - rewrite <- H0. eapply load_store_other; eauto. - assert (sp <> b). unfold block; omega. + red in H6; simpl in H6. econstructor; eauto. eapply frame_match_store_other; eauto. - left. unfold block; omega. - rewrite <- H1. eapply load_store_other; eauto. - rewrite <- H2. eapply load_store_other; eauto. - eapply IHmatch_stacks; eauto. omega. + unfold block; omega. + eapply IHmatch_stacks; eauto. + eapply stack_below_trans; eauto. omega. Qed. Lemma match_stacks_store_slot: - forall s ts sp base ms mm, - match_stacks s ts sp base mm ms -> - forall ty ofs v ms', - store_stack ms (Vptr sp base) ty ofs v = Some ms' -> - Int.signed base + 24 <= Int.signed (Int.add base ofs) -> - match_stacks s ts sp base mm ms'. + forall s ts ms mm, + match_stacks s ts mm ms -> + forall ty ofs v ms' b i, + stack_below ts b -> + store_stack ms (Vptr b i) ty ofs v = Some ms' -> + match_stacks s ts mm ms'. Proof. intros. - unfold store_stack in H0. simpl in H0. - assert (load Mint32 ms' sp (Int.signed base) = load Mint32 ms sp (Int.signed base)). - eapply load_store_other; eauto. - right; left. change (size_chunk Mint32) with 4; omega. - assert (load Mint32 ms' sp (Int.signed base + 12) = load Mint32 ms sp (Int.signed base + 12)). - eapply load_store_other; eauto. - right; left. change (size_chunk Mint32) with 4; omega. + unfold store_stack in H1. simpl in H1. inv H. - constructor; congruence. - constructor; auto. + constructor. + red in H0; simpl in H0. + econstructor; eauto. eapply frame_match_store_other; eauto. - left; unfold block; omega. - congruence. congruence. + unfold block; omega. eapply match_stacks_store_other; eauto. + eapply stack_below_trans; eauto. omega. Qed. Lemma match_stacks_store: - forall s ts sp base ms mm, - match_stacks s ts sp base mm ms -> - forall fr chunk b ofs v mm' ms', - frame_match fr sp base mm ms -> + forall s ts ms mm, + match_stacks s ts mm ms -> + forall chunk b ofs v mm' ms', store chunk mm b ofs v = Some mm' -> store chunk ms b ofs v = Some ms' -> - match_stacks s ts sp base mm' ms'. + match_stacks s ts mm' ms'. Proof. induction 1; intros. - assert (Int.signed base = fr_low fr) by (eapply frame_match_base_eq; eauto). constructor. - rewrite <- H. eapply frame_match_store_link_invariant; eauto. omega. - rewrite <- H0. eapply frame_match_store_link_invariant; eauto. omega. - assert (Int.signed base = fr_low fr0) by (eapply frame_match_base_eq; eauto). econstructor; eauto. - eapply frame_match_store; eauto. - rewrite <- H1. eapply frame_match_store_link_invariant; eauto. omega. - rewrite <- H2. eapply frame_match_store_link_invariant; eauto. omega. + eapply frame_match_store; eauto. Qed. Lemma match_stacks_alloc: - forall s ts sp base ms mm, - match_stacks s ts sp base mm ms -> + forall s ts ms mm, + match_stacks s ts mm ms -> forall lom him mm' bm los his ms' bs, mm.(nextblock) = ms.(nextblock) -> alloc mm lom him = (mm', bm) -> alloc ms los his = (ms', bs) -> - match_stacks s ts sp base mm' ms'. + match_stacks s ts mm' ms'. Proof. induction 1; intros. constructor. - rewrite <- H; eapply load_alloc_unchanged; eauto with mem. - rewrite <- H0; eapply load_alloc_unchanged; eauto with mem. econstructor; eauto. eapply frame_match_alloc; eauto. - rewrite <- H1; eapply load_alloc_unchanged; eauto with mem. - rewrite <- H2; eapply load_alloc_unchanged; eauto with mem. Qed. Lemma match_stacks_free: - forall s ts sp base ms mm, - match_stacks s ts sp base mm ms -> + forall s ts ms mm, + match_stacks s ts mm ms -> forall b, - sp < b -> - match_stacks s ts sp base (Mem.free mm b) (Mem.free ms b). + stack_below ts b -> + match_stacks s ts (Mem.free mm b) (Mem.free ms b). Proof. induction 1; intros. - assert (sp <> b). unfold block; omega. constructor. - rewrite <- H. apply load_free; auto. - rewrite <- H0. apply load_free; auto. - assert (sp <> b). unfold block; omega. + red in H5; simpl in H5. econstructor; eauto. eapply frame_match_free; eauto. unfold block; omega. - rewrite <- H1. apply load_free; auto. - rewrite <- H2. apply load_free; auto. - eapply IHmatch_stacks; eauto. omega. -Qed. - -(** Invocation of a function temporarily violates the [mach_stacks] - invariant: the return address and back link are not yet stored - in the appropriate parts of the activation record. - The following [match_stacks_partial] predicate is a weaker version - of [match_stacks] that captures this situation. *) - -Inductive match_stacks_partial: - list Machabstr.stackframe -> list Machconcr.stackframe -> - mem -> mem -> Prop := - | match_stacks_partial_nil: forall mm ms, - match_stacks_partial nil nil mm ms - | match_stacks_partial_cons: forall f sp base c fr s fb ra ts mm ms, - frame_match fr sp base mm ms -> - sp < ms.(nextblock) -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - match_stacks s ts sp base mm ms -> - Val.has_type ra Tint -> - match_stacks_partial (Machabstr.Stackframe f (Vptr sp base) c fr :: s) - (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts) - mm ms. - -Lemma match_stacks_match_stacks_partial: - forall s ts sp base mm ms, - match_stacks s ts sp base mm ms -> - match_stacks_partial s ts (free mm sp) (free ms sp). -Proof. - intros. inv H. constructor. - econstructor. - eapply frame_match_free; eauto. unfold block; omega. - simpl. inv H0; auto. - auto. - apply match_stacks_free; auto. - generalize (Mem.load_inv _ _ _ _ _ H3). intros [A B]. - rewrite B. - destruct (getN (pred_size_chunk Mint32) (Int.signed base + 12) - (contents (blocks ms sp))); exact I. + eapply IHmatch_stacks; eauto. + eapply stack_below_trans; eauto. omega. Qed. Lemma match_stacks_function_entry: - forall s ts mm ms lom him mm' los his ms' stk ms'' ms''' base, - match_stacks_partial s ts mm ms -> + forall s ts mm ms lom him mm' los his ms' stk, + match_stacks s ts mm ms -> alloc mm lom him = (mm', stk) -> alloc ms los his = (ms', stk) -> - store Mint32 ms' stk (Int.signed base) (parent_sp ts) = Some ms'' -> - store Mint32 ms'' stk (Int.signed base + 12) (parent_ra ts) = Some ms''' -> - match_stacks s ts stk base mm' ms'''. + match_stacks s ts mm' ms' /\ stack_below ts stk. Proof. - intros. - assert (WT_SP: Val.has_type (parent_sp ts) Tint). - inv H; simpl; auto. - assert (WT_RA: Val.has_type (parent_ra ts) Tint). - inv H; simpl; auto. - assert (load Mint32 ms''' stk (Int.signed base) = Some (parent_sp ts)). - transitivity (load Mint32 ms'' stk (Int.signed base)). - eapply load_store_other; eauto. right; left. simpl. omega. - transitivity (Some (Val.load_result (chunk_of_type Tint) (parent_sp ts))). - simpl chunk_of_type. eapply load_store_same; eauto. - decEq. apply load_result_ty. auto. - assert (load Mint32 ms''' stk (Int.signed base + 12) = Some (parent_ra ts)). - transitivity (Some (Val.load_result (chunk_of_type Tint) (parent_ra ts))). - simpl chunk_of_type. eapply load_store_same; eauto. - decEq. apply load_result_ty. auto. - inv H; simpl in *. - constructor; auto. - assert (sp < stk). rewrite (alloc_result _ _ _ _ _ H1). auto. - assert (sp <> stk). unfold block; omega. - assert (nextblock mm = nextblock ms). - rewrite <- (alloc_result _ _ _ _ _ H0). - rewrite <- (alloc_result _ _ _ _ _ H1). auto. - econstructor; eauto. - eapply frame_match_store_other; eauto. - eapply frame_match_store_other; eauto. - eapply frame_match_alloc with (mm := mm) (ms := ms); eauto. - eapply match_stacks_store_other; eauto. - eapply match_stacks_store_other; eauto. - eapply match_stacks_alloc with (mm := mm) (ms := ms); eauto. - Qed. + intros. + assert (stk = nextblock mm). eapply Mem.alloc_result; eauto. + assert (stk = nextblock ms). eapply Mem.alloc_result; eauto. + split. + eapply match_stacks_alloc; eauto. congruence. + red. + inv H; simpl. + unfold nullptr. apply Zgt_lt. apply nextblock_pos. + inv H6. red in H. rewrite H3. auto. +Qed. (** ** Invariant between states. *) @@ -651,27 +662,27 @@ Inductive match_states: Machabstr.state -> Machconcr.state -> Prop := | match_states_intro: forall s f sp base c rs fr mm ts fb ms - (STACKS: match_stacks s ts sp base mm ms) - (FM: frame_match fr sp base mm ms) + (STACKS: match_stacks s ts mm ms) + (FM: frame_match f (extend_frame f ts fr) sp base mm ms) + (BELOW: stack_below ts sp) (MEXT: Mem.extends mm ms) (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)), match_states (Machabstr.State s f (Vptr sp base) c rs fr mm) (Machconcr.State ts fb (Vptr sp base) c rs ms) | match_states_call: forall s f rs mm ts fb ms - (STACKS: match_stacks_partial s ts mm ms) + (STACKS: match_stacks s ts mm ms) (MEXT: Mem.extends mm ms) (FIND: Genv.find_funct_ptr ge fb = Some f), match_states (Machabstr.Callstate s f rs mm) (Machconcr.Callstate ts fb rs ms) | match_states_return: forall s rs mm ts ms - (STACKS: match_stacks_partial s ts mm ms) + (STACKS: match_stacks s ts mm ms) (MEXT: Mem.extends mm ms), match_states (Machabstr.Returnstate s rs mm) (Machconcr.Returnstate ts rs ms). - (** * The proof of simulation *) (** The proof of simulation relies on diagrams of the following form: @@ -710,29 +721,23 @@ Qed. Lemma transl_extcall_arguments: forall rs s sg args ts m ms, - Machabstr.extcall_arguments rs (parent_frame s) sg args -> - match_stacks_partial s ts m ms -> + Machabstr.extcall_arguments (parent_function s) rs (parent_frame s) sg args -> + match_stacks s ts m ms -> extcall_arguments rs ms (parent_sp ts) sg args. Proof. unfold Machabstr.extcall_arguments, extcall_arguments; intros. - assert (forall ty ofs v, - get_slot (parent_frame s) ty (Int.signed ofs) v -> - load_stack ms (parent_sp ts) ty ofs = Some v). - inv H0; simpl; intros. - inv H0. simpl in H2. elimtype False. generalize (AST.typesize_pos ty). omega. - eapply frame_match_get_slot; eauto. assert (forall locs vals, - Machabstr.extcall_args rs (parent_frame s) locs vals -> + Machabstr.extcall_args (parent_function s) rs (parent_frame s) locs vals -> extcall_args rs ms (parent_sp ts) locs vals). - induction locs; intros; inversion H2; subst; clear H2. + induction locs; intros; inv H1. constructor. constructor; auto. - inversion H7; subst; clear H7. - constructor. - constructor. auto. + inv H6. constructor. constructor. eapply match_stacks_get_parent; eauto. auto. Qed. +Hypothesis wt_prog: wt_program p. + Theorem step_equiv: forall s1 t s2, Machabstr.step ge s1 t s2 -> forall s1' (MS: match_states s1 s1') (WTS: wt_state s1), @@ -746,27 +751,33 @@ Proof. econstructor; eauto with coqlib. (* Mgetstack *) + assert (WTF: wt_function f) by (inv WTS; auto). exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split. - apply exec_Mgetstack; auto. eapply frame_match_get_slot; eauto. + constructor; auto. + eapply frame_match_get_slot; eauto. + eapply get_slot_extends; eauto. econstructor; eauto with coqlib. (* Msetstack *) + assert (WTF: wt_function f) by (inv WTS; auto). assert (Val.has_type (rs src) ty). inv WTS. generalize (wt_function_instrs _ WTF _ (is_tail_in TAIL)); intro WTI. inv WTI. apply WTRS. - exploit frame_match_set_slot; eauto. - intros [ms' [STORE [FM' [EXT' BOUND]]]]. + exploit frame_match_set_slot; eauto. + eapply set_slot_extends; eauto. + intros [ms' [STORE [FM' EXT']]]. exists (State ts fb (Vptr sp0 base) c rs ms'); split. apply exec_Msetstack; auto. econstructor; eauto. eapply match_stacks_store_slot; eauto. (* Mgetparam *) - exploit match_stacks_get_parent; eauto. - intros [parent [LOAD1 LOAD2]]. + assert (WTF: wt_function f) by (inv WTS; auto). exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split. - eapply exec_Mgetparam; eauto. + eapply exec_Mgetparam; eauto. + eapply frame_match_load_link; eauto. + eapply match_stacks_get_parent; eauto. econstructor; eauto with coqlib. (* Mop *) @@ -802,16 +813,17 @@ Proof. econstructor; split. eapply exec_Mcall; eauto. econstructor; eauto. - econstructor; eauto. inv FM; auto. exact I. + econstructor; eauto. inv WTS; auto. exact I. (* Mtailcall *) + assert (WTF: wt_function f) by (inv WTS; auto). exploit find_function_find_function_ptr; eauto. intros [fb' [FIND' FINDFUNCT]]. - exploit match_stacks_load_links; eauto. intros [LOAD1 LOAD2]. econstructor; split. eapply exec_Mtailcall; eauto. - econstructor; eauto. - eapply match_stacks_match_stacks_partial; eauto. + eapply frame_match_load_link; eauto. + eapply frame_match_load_retaddr; eauto. + econstructor; eauto. eapply match_stacks_free; auto. apply free_extends; auto. (* Malloc *) @@ -841,67 +853,32 @@ Proof. econstructor; eauto. (* Mreturn *) - exploit match_stacks_load_links; eauto. intros [LOAD1 LOAD2]. + assert (WTF: wt_function f) by (inv WTS; auto). econstructor; split. eapply exec_Mreturn; eauto. - econstructor; eauto. - eapply match_stacks_match_stacks_partial; eauto. + eapply frame_match_load_link; eauto. + eapply frame_match_load_retaddr; eauto. + econstructor; eauto. eapply match_stacks_free; eauto. apply free_extends; auto. (* internal function *) - assert (WTF: wt_function f). inv WTS. inv H5. auto. inv WTF. - caseEq (alloc ms (- f.(fn_framesize)) - (align_16_top (- f.(fn_framesize)) f.(fn_stacksize))). + assert (WTF: wt_function f). inv WTS. inv H5. auto. + caseEq (alloc ms (- f.(fn_framesize)) f.(fn_stacksize)). intros ms' stk' ALLOC. - exploit (alloc_extends m ms m' ms' 0 (fn_stacksize f) - (- fn_framesize f) - (align_16_top (- fn_framesize f) (fn_stacksize f))); eauto. - omega. apply align_16_top_ge. - intros [EQ EXT']. subst stk'. - exploit (frame_match_new m ms); eauto. inv MEXT; auto. - intros [EQ FM]. clear EQ. - set (sp := Vptr stk (Int.repr (- fn_framesize f))). - assert (exists ms'', store Mint32 ms' stk (- fn_framesize f) (parent_sp ts) = Some ms''). - apply valid_access_store. constructor. - eauto with mem. - rewrite (low_bound_alloc_same _ _ _ _ _ ALLOC). omega. - rewrite (high_bound_alloc_same _ _ _ _ _ ALLOC). - change (size_chunk Mint32) with 4. - apply Zle_trans with 0. omega. apply align_16_top_pos. - destruct H0 as [ms'' STORE1]. - assert (exists ms''', store Mint32 ms'' stk (- fn_framesize f + 12) (parent_ra ts) = Some ms'''). - apply valid_access_store. constructor. - eauto with mem. - rewrite (low_bound_store _ _ _ _ _ _ STORE1 stk). - rewrite (low_bound_alloc_same _ _ _ _ _ ALLOC). omega. - rewrite (high_bound_store _ _ _ _ _ _ STORE1 stk). - rewrite (high_bound_alloc_same _ _ _ _ _ ALLOC). - change (size_chunk Mint32) with 4. - apply Zle_trans with 0. omega. apply align_16_top_pos. - destruct H0 as [ms''' STORE2]. - assert (RANGE1: Int.min_signed <= - fn_framesize f <= Int.max_signed). - split. omega. apply Zle_trans with (-24). omega. compute;congruence. - assert (RANGE2: Int.min_signed <= - fn_framesize f + 12 <= Int.max_signed). - split. omega. apply Zle_trans with (-12). omega. compute;congruence. + assert (Val.has_type (parent_sp ts) Tint). + inv STACKS; simpl; auto. + assert (Val.has_type (parent_ra ts) Tint). + inv STACKS; simpl; auto. + destruct (frame_match_function_entry _ WTF _ _ _ _ _ _ _ + MEXT H ALLOC H0 H1) + as [ms2 [ms3 [EQ [STORE1 [STORE2 [FM MEXT']]]]]]. + subst stk'. econstructor; split. eapply exec_function_internal; eauto. - unfold store_stack. simpl. rewrite Int.add_zero. - rewrite Int.signed_repr. eauto. auto. - unfold store_stack. simpl. rewrite Int.add_signed. - change (Int.signed (Int.repr 12)) with 12. - repeat rewrite Int.signed_repr; eauto. - (* match states *) - unfold sp; econstructor; eauto. - eapply match_stacks_function_entry; eauto. - rewrite Int.signed_repr; eauto. - rewrite Int.signed_repr; eauto. - eapply frame_match_store_other with (ms := ms''); eauto. - eapply frame_match_store_other with (ms := ms'); eauto. - simpl. right; omega. simpl. right; omega. - eapply store_outside_extends with (m2 := ms''); eauto. - eapply store_outside_extends with (m2 := ms'); eauto. - rewrite (low_bound_alloc_same _ _ _ _ _ H). simpl; omega. - rewrite (low_bound_alloc_same _ _ _ _ _ H). simpl; omega. + exploit match_stacks_function_entry; eauto. intros [STACKS' BELOW]. + econstructor; eauto. + eapply match_stacks_store_slot with (ms := ms2); eauto. + eapply match_stacks_store_slot with (ms := ms'); eauto. (* external function *) econstructor; split. @@ -916,8 +893,6 @@ Proof. econstructor; eauto. Qed. -Hypothesis wt_prog: wt_program p. - Lemma equiv_initial_states: forall st1, Machabstr.initial_state p st1 -> exists st2, Machconcr.initial_state p st2 /\ match_states st1 st2 /\ wt_state st1. diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 2eb3d478..0cfd8f11 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -41,17 +41,17 @@ Require PPCgenretaddr. caller function at offset 0. In addition to this linking of activation records, the concrete -semantics also make provisions for storing a return address -at offset 12 from the stack pointer. This stack location will -be used by the PPC code generated by [PPCgen] 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. The Mach concrete -semantics does not attach any particular meaning to the pointer -stored in this reserved location, but makes sure that it is preserved -during execution of a function. The [return_address_offset] predicate -from module [PPCgenretaddr] is used to guess the value of the return -address that the PPC code generated later will store in the -reserved location. +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 PPC code generated by [PPCgen] 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. The Mach concrete semantics does not +attach any particular meaning to the pointer stored in this reserved +location, but makes sure that it is preserved during execution of a +function. The [return_address_offset] predicate from module +[PPCgenretaddr] is used to guess the value of the return address that +the PPC code generated later will store in the reserved location. *) Definition chunk_of_type (ty: typ) := @@ -146,11 +146,12 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Msetstack src ofs ty :: c) rs m) E0 (State s f sp c rs m') | exec_Mgetparam: - forall s f sp parent ofs ty dst c rs m v, - load_stack m sp Tint (Int.repr 0) = Some parent -> + forall s fb f sp parent ofs ty dst c rs m v, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m sp Tint f.(fn_link_ofs) = Some parent -> load_stack m parent ty ofs = Some v -> - step (State s f sp (Mgetparam ofs ty dst :: c) rs m) - E0 (State s f sp c (rs#dst <- v) m) + step (State s fb sp (Mgetparam ofs ty dst :: c) rs m) + E0 (State s fb sp c (rs#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 -> @@ -177,10 +178,11 @@ Inductive step: state -> trace -> state -> Prop := E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' rs m) | exec_Mtailcall: - forall s fb stk soff sig ros c rs m f', + forall s fb stk soff sig ros c rs m f f', find_function_ptr ge ros rs = Some f' -> - load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) E0 (Callstate s f' rs (Mem.free m stk)) | exec_Malloc: @@ -210,20 +212,19 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Mcond cond args lbl :: c) rs m) E0 (State s f sp c rs m) | exec_Mreturn: - forall s f stk soff c rs m, - load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) -> - step (State s f (Vptr stk soff) (Mreturn :: c) rs m) + forall s fb stk soff c rs m f, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + step (State s fb (Vptr stk soff) (Mreturn :: c) rs m) E0 (Returnstate s rs (Mem.free m stk)) | exec_function_internal: forall s fb rs m f m1 m2 m3 stk, Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mem.alloc m (- f.(fn_framesize)) - (align_16_top (- f.(fn_framesize)) f.(fn_stacksize)) - = (m1, stk) -> + Mem.alloc m (- f.(fn_framesize)) f.(fn_stacksize) = (m1, stk) -> let sp := Vptr stk (Int.repr (-f.(fn_framesize))) in - store_stack m1 sp Tint (Int.repr 0) (parent_sp s) = Some m2 -> - store_stack m2 sp Tint (Int.repr 12) (parent_ra s) = Some m3 -> + 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) rs m3) | exec_function_external: diff --git a/backend/Machtyping.v b/backend/Machtyping.v index 5e5f03c4..f9f76d82 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -90,9 +90,16 @@ Record wt_function (f: function) : Prop := mk_wt_function { wt_function_stacksize: f.(fn_stacksize) >= 0; wt_function_framesize: - f.(fn_framesize) >= 24; - wt_function_no_overflow: - f.(fn_framesize) <= -Int.min_signed + 0 <= f.(fn_framesize) <= -Int.min_signed; + wt_function_link: + 0 <= Int.signed f.(fn_link_ofs) + /\ Int.signed f.(fn_link_ofs) + 4 <= f.(fn_framesize); + wt_function_retaddr: + 0 <= Int.signed f.(fn_retaddr_ofs) + /\ Int.signed f.(fn_retaddr_ofs) + 4 <= f.(fn_framesize); + wt_function_link_retaddr: + Int.signed f.(fn_retaddr_ofs) + 4 <= Int.signed f.(fn_link_ofs) + \/ Int.signed f.(fn_link_ofs) + 4 <= Int.signed f.(fn_retaddr_ofs) }. Inductive wt_fundef: fundef -> Prop := @@ -122,7 +129,7 @@ Definition wt_regset (rs: regset) : Prop := forall r, Val.has_type (rs r) (mreg_type r). Definition wt_frame (fr: frame) : Prop := - forall ty ofs, Val.has_type (fr.(fr_contents) ty ofs) ty. + forall ty ofs, Val.has_type (fr ty ofs) ty. Lemma wt_setreg: forall (rs: regset) (r: mreg) (v: val), @@ -136,28 +143,28 @@ Proof. Qed. Lemma wt_get_slot: - forall fr ty ofs v, - get_slot fr ty ofs v -> + forall f fr ty ofs v, + get_slot f fr ty ofs v -> wt_frame fr -> Val.has_type v ty. Proof. induction 1; intros. - subst v. apply H2. + subst v. apply H1. Qed. Lemma wt_set_slot: - forall fr ty ofs v fr', - set_slot fr ty ofs v fr' -> + forall f fr ty ofs v fr', + set_slot f fr ty ofs v fr' -> wt_frame fr -> Val.has_type v ty -> wt_frame fr'. Proof. - intros. induction H. subst fr'; red; intros; simpl. - destruct (zeq (fr_low fr + ofs) ofs0). + intros. induction H. subst fr'; red; intros. unfold update. + destruct (zeq (ofs - f.(fn_framesize)) ofs0). destruct (typ_eq ty ty0). congruence. exact I. - destruct (zle (ofs0 + AST.typesize ty0) (fr_low fr + ofs)). + destruct (zle (ofs0 + AST.typesize ty0) (ofs - f.(fn_framesize))). apply H0. - destruct (zle (fr_low fr + ofs + AST.typesize ty) ofs0). + destruct (zle (ofs - f.(fn_framesize) + AST.typesize ty) ofs0). apply H0. exact I. Qed. @@ -168,13 +175,6 @@ Proof. intros; red; intros; exact I. Qed. -Lemma wt_init_frame: - forall f, - wt_frame (init_frame f). -Proof. - intros; red; intros; exact I. -Qed. - Lemma is_tail_find_label: forall lbl c c', find_label lbl c = Some c' -> is_tail c' c. Proof. @@ -235,7 +235,7 @@ Proof. eapply wt_state_intro; eauto with coqlib). apply wt_setreg; auto. - inversion H0. rewrite H2. apply wt_get_slot with fr (Int.signed ofs); auto. + inversion H0. rewrite H2. eapply wt_get_slot; eauto. inversion H0. eapply wt_set_slot; eauto. rewrite <- H2. apply WTRS. @@ -244,7 +244,7 @@ Proof. destruct s; simpl. apply wt_empty_frame. generalize (STK s (in_eq _ _)); intro. inv H1. auto. inversion H0. apply wt_setreg; auto. - rewrite H3. apply wt_get_slot with (parent_frame s) (Int.signed ofs); auto. + rewrite H3. eapply wt_get_slot; eauto. apply wt_setreg; auto. inv H0. simpl in H. @@ -280,7 +280,7 @@ Proof. econstructor; eauto. econstructor; eauto with coqlib. inv H5; auto. exact I. - apply wt_init_frame. + apply wt_empty_frame. econstructor; eauto. apply wt_setreg; auto. generalize (wt_event_match _ _ _ _ H). diff --git a/backend/PPC.v b/backend/PPC.v index 8af2c9be..7a330639 100644 --- a/backend/PPC.v +++ b/backend/PPC.v @@ -98,7 +98,7 @@ Inductive instruction : Set := | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) | Paddze: ireg -> ireg -> instruction (**r add Carry bit *) | Pallocblock: instruction (**r allocate new heap block *) - | Pallocframe: Z -> Z -> instruction (**r allocate new stack frame *) + | Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *) | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) @@ -121,7 +121,7 @@ Inductive instruction : Set := | Peqv: ireg -> ireg -> ireg -> instruction (**r bitwise not-xor *) | Pextsb: ireg -> ireg -> instruction (**r 8-bit sign extension *) | Pextsh: ireg -> ireg -> instruction (**r 16-bit sign extension *) - | Pfreeframe: instruction (**r deallocate stack frame and restore previous frame *) + | Pfreeframe: int -> instruction (**r deallocate stack frame and restore previous frame *) | Pfabs: freg -> freg -> instruction (**r float absolute value *) | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) | Pfcmpu: freg -> freg -> instruction (**r float comparison *) @@ -243,25 +243,25 @@ lbl: .long 0x43300000, 0x80000000 lbl: .long 0x43300000, 0x00000000 .text >> -- [Pallocframe lo hi]: in the formal semantics, this pseudo-instruction +- [Pallocframe lo hi ofs]: in the formal semantics, this pseudo-instruction allocates a memory block with bounds [lo] and [hi], stores the value - of register [r1] (the stack pointer, by convention) at the bottom - of this block, and sets [r1] to a pointer to the bottom of this + of register [r1] (the stack pointer, by convention) at offset [ofs] + in this block, and sets [r1] to a pointer to the bottom of this block. In the printed PowerPC assembly code, this allocation - is just a store-decrement of register [r1]: + is just a store-decrement of register [r1], assuming that [ofs = 0]: << stwu r1, (lo - hi)(r1) >> This cannot be expressed in our memory model, which does not reflect the fact that stack frames are adjacent and allocated/freed following a stack discipline. -- [Pfreeframe]: in the formal semantics, this pseudo-instruction - reads the bottom word of the block pointed by [r1] (the stack pointer), - frees this block, and sets [r1] to the value of the bottom word. - In the printed PowerPC assembly code, this freeing - is just a load of register [r1] relative to [r1] itself: +- [Pfreeframe ofs]: in the formal semantics, this pseudo-instruction + reads the word at offset [ofs] in the block pointed by [r1] (the + stack pointer), frees this block, and sets [r1] to the value of the + word at offset [ofs]. In the printed PowerPC assembly code, this + freeing is just a load of register [r1] relative to [r1] itself: << - lwz r1, 0(r1) + lwz r1, ofs(r1) >> Again, our memory model cannot comprehend that this operation frees (logically) the current stack frame. @@ -534,10 +534,10 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome #LR <- (Val.add rs#PC Vone))) m' | _ => Error end - | Pallocframe lo hi => + | Pallocframe lo hi ofs => let (m1, stk) := Mem.alloc m lo hi in let sp := Vptr stk (Int.repr lo) in - match Mem.storev Mint32 m1 sp rs#GPR1 with + match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with | None => Error | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR2 <- Vundef)) m2 end @@ -594,8 +594,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr (rs#rd <- (Val.cast8signed rs#r1))) m | Pextsh rd r1 => OK (nextinstr (rs#rd <- (Val.cast16signed rs#r1))) m - | Pfreeframe => - match Mem.loadv Mint32 m rs#GPR1 with + | Pfreeframe ofs => + match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with | None => Error | Some v => match rs#GPR1 with diff --git a/backend/PPCgen.v b/backend/PPCgen.v index 805d039b..1789fb13 100644 --- a/backend/PPCgen.v +++ b/backend/PPCgen.v @@ -419,14 +419,14 @@ Definition transl_load_store (** Translation of a Mach instruction. *) -Definition transl_instr (i: Mach.instruction) (k: code) := +Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := match i with | Mgetstack ofs ty dst => loadind GPR1 ofs ty dst k | Msetstack src ofs ty => storeind src GPR1 ofs ty k | Mgetparam ofs ty dst => - Plwz GPR2 (Cint (Int.repr 0)) GPR1 :: loadind GPR2 ofs ty dst k + Plwz GPR2 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR2 ofs ty dst k | Mop op args res => transl_op op args res k | Mload chunk addr args dst => @@ -484,14 +484,14 @@ Definition transl_instr (i: Mach.instruction) (k: code) := Pbl symb :: k | Mtailcall sig (inl r) => Pmtctr (ireg_of r) :: - Plwz GPR2 (Cint (Int.repr 12)) GPR1 :: + Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR2 :: - Pfreeframe :: + Pfreeframe f.(fn_link_ofs) :: Pbctr :: k | Mtailcall sig (inr symb) => - Plwz GPR2 (Cint (Int.repr 12)) GPR1 :: + Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR2 :: - Pfreeframe :: + Pfreeframe f.(fn_link_ofs) :: Pbs symb :: k | Malloc => Pallocblock :: k @@ -504,12 +504,14 @@ Definition transl_instr (i: Mach.instruction) (k: code) := transl_cond cond args (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k) | Mreturn => - Plwz GPR2 (Cint (Int.repr 12)) GPR1 :: - Pmtlr GPR2 :: Pfreeframe :: Pblr :: k + Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR2 :: + Pfreeframe f.(fn_link_ofs) :: + Pblr :: k end. -Definition transl_code (il: list Mach.instruction) := - List.fold_right transl_instr nil il. +Definition transl_code (f: Mach.function) (il: list Mach.instruction) := + List.fold_right (transl_instr f) nil il. (** Translation of a whole function. Note that we must check that the generated code contains less than [2^32] instructions, @@ -517,11 +519,10 @@ Definition transl_code (il: list Mach.instruction) := around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - Pallocframe (- f.(fn_framesize)) - (align_16_top (-f.(fn_framesize)) f.(fn_stacksize)) :: + Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pmflr GPR2 :: - Pstw GPR2 (Cint (Int.repr 12)) GPR1 :: - transl_code f.(fn_code). + Pstw GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 :: + transl_code f f.(fn_code). Fixpoint code_size (c: code) : Z := match c with diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v index 2b00cfc0..932f7dea 100644 --- a/backend/PPCgenproof.v +++ b/backend/PPCgenproof.v @@ -157,7 +157,7 @@ Inductive transl_code_at_pc: val -> block -> Mach.function -> Mach.code -> Prop transl_code_at_pc_intro: forall b ofs f c, Genv.find_funct_ptr ge b = Some (Internal f) -> - code_tail (Int.unsigned ofs) (transl_function f) (transl_code c) -> + code_tail (Int.unsigned ofs) (transl_function f) (transl_code f c) -> transl_code_at_pc (Vptr b ofs) b f c. (** The following lemmas show that straight-line executions @@ -213,7 +213,7 @@ Lemma exec_straight_exec: forall fb f c c' rs m rs' m', transl_code_at_pc (rs PC) fb f c -> exec_straight tge (transl_function f) - (transl_code c) rs m c' rs' m' -> + (transl_code f c) rs m c' rs' m' -> plus step tge (State rs m) E0 (State rs' m'). Proof. intros. inversion H. subst. @@ -226,7 +226,7 @@ Lemma exec_straight_at: forall fb f c c' rs m rs' m', transl_code_at_pc (rs PC) fb f c -> exec_straight tge (transl_function f) - (transl_code c) rs m (transl_code c') rs' m' -> + (transl_code f c) rs m (transl_code f c') rs' m' -> transl_code_at_pc (rs' PC) fb f c'. Proof. intros. inversion H. subst. @@ -471,8 +471,8 @@ Qed. Hint Rewrite transl_load_store_label: labels. Lemma transl_instr_label: - forall i k, - find_label lbl (transl_instr i k) = + forall f i k, + find_label lbl (transl_instr f i k) = if Mach.is_label lbl i then Some k else find_label lbl k. Proof. intros. generalize (Mach.is_label_correct lbl i). @@ -488,9 +488,9 @@ Proof. Qed. Lemma transl_code_label: - forall c, - find_label lbl (transl_code c) = - option_map transl_code (Mach.find_label lbl c). + forall f c, + find_label lbl (transl_code f c) = + option_map (transl_code f) (Mach.find_label lbl c). Proof. induction c; simpl; intros. auto. rewrite transl_instr_label. @@ -501,7 +501,7 @@ Qed. Lemma transl_find_label: forall f, find_label lbl (transl_function f) = - option_map transl_code (Mach.find_label lbl f.(fn_code)). + option_map (transl_code f) (Mach.find_label lbl f.(fn_code)). Proof. intros. unfold transl_function. simpl. apply transl_code_label. Qed. @@ -525,7 +525,7 @@ Proof. generalize (transl_find_label lbl f). rewrite H1; simpl. intro. generalize (label_pos_code_tail lbl (transl_function f) 0 - (transl_code c') H2). + (transl_code f c') H2). intros [pos' [A [B C]]]. exists (rs#PC <- (Vptr b (Int.repr pos'))). split. unfold goto_label. rewrite A. rewrite H0. auto. @@ -663,7 +663,7 @@ Lemma exec_straight_steps: incl c2 f.(fn_code) -> transl_code_at_pc (rs1 PC) fb f c1 -> (exists rs2, - exec_straight tge (transl_function f) (transl_code c1) rs1 m1 (transl_code c2) rs2 m2 + exec_straight tge (transl_function f) (transl_code f c1) rs1 m1 (transl_code f c2) rs2 m2 /\ agree ms2 sp rs2) -> exists st', plus step tge (State rs1 m1) E0 st' /\ @@ -729,7 +729,7 @@ Proof. rewrite (sp_val _ _ _ AG) in H. assert (NOTE: GPR1 <> GPR0). congruence. generalize (loadind_correct tge (transl_function f) GPR1 ofs ty - dst (transl_code c) rs m v H H1 NOTE). + dst (transl_code f c) rs m v H H1 NOTE). intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. simpl. exists rs2; split. auto. @@ -756,7 +756,7 @@ Proof. rewrite (preg_val ms sp rs) in H; auto. assert (NOTE: GPR1 <> GPR0). congruence. generalize (storeind_correct tge (transl_function f) GPR1 ofs ty - src (transl_code c) rs m m' H H1 NOTE). + src (transl_code f c) rs m m' H H1 NOTE). intros [rs2 [EX OTH]]. left; eapply exec_straight_steps; eauto with coqlib. exists rs2; split; auto. @@ -764,30 +764,32 @@ Proof. Qed. Lemma exec_Mgetparam_prop: - forall (s : list stackframe) (fb : block) (sp parent : val) + forall (s : list stackframe) (fb : block) (f: Mach.function) (sp parent : val) (ofs : int) (ty : typ) (dst : mreg) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (v : val), - load_stack m sp Tint (Int.repr 0) = Some parent -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m sp Tint f.(fn_link_ofs) = Some parent -> load_stack m parent ty ofs = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0 (Machconcr.State s fb sp c (Regmap.set dst v ms) m). Proof. intros; red; intros; inv MS. + assert (f0 = f) by congruence. subst f0. set (rs2 := nextinstr (rs#GPR2 <- parent)). assert (EX1: exec_straight tge (transl_function f) - (transl_code (Mgetparam ofs ty dst :: c)) rs m - (loadind GPR2 ofs ty dst (transl_code c)) rs2 m). + (transl_code f (Mgetparam ofs ty dst :: c)) rs m + (loadind GPR2 ofs ty dst (transl_code f c)) rs2 m). simpl. apply exec_straight_one. simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto with ppcgen. unfold const_low. rewrite <- (sp_val ms sp rs); auto. - unfold load_stack in H. simpl chunk_of_type in H. - rewrite H. reflexivity. reflexivity. + unfold load_stack in H0. simpl chunk_of_type in H0. + rewrite H0. reflexivity. reflexivity. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inversion WTI. - unfold load_stack in H0. change parent with rs2#GPR2 in H0. + unfold load_stack in H1. change parent with rs2#GPR2 in H1. assert (NOTE: GPR2 <> GPR0). congruence. generalize (loadind_correct tge (transl_function f) GPR2 ofs ty - dst (transl_code c) rs2 m v H0 H2 NOTE). + dst (transl_code f c) rs2 m v H1 H3 NOTE). intros [rs3 [EX2 [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. exists rs3; split; simpl. @@ -852,7 +854,7 @@ Proof. generalize (transl_load_correct tge (transl_function f) (Plbz (ireg_of dst)) (Plbzx (ireg_of dst)) Mint8unsigned addr args - (Pextsb (ireg_of dst) (ireg_of dst) :: transl_code c) + (Pextsb (ireg_of dst) (ireg_of dst) :: transl_code f c) ms sp rs m dst a v' X1 X2 AG H3 H7 LOAD'). intros [rs2 [EX1 AG1]]. @@ -965,21 +967,23 @@ Qed. Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (sig : signature) (ros : mreg + ident) (c : list Mach.instruction) - (ms : Mach.regset) (m : mem) (f' : block), + (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block), find_function_ptr ge ros ms = Some f' -> - load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 (Callstate s f' ms (free m stk)). Proof. intros; red; intros; inv MS. + assert (f0 = f) by congruence. subst f0. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inversion WTI. inversion AT. subst b f0 c0. assert (NOOV: code_size (transl_function f) <= Int.max_unsigned). eapply functions_transl_no_overflow; eauto. - destruct ros; simpl in H; simpl in H8. + destruct ros; simpl in H; simpl in H9. (* Indirect call *) set (rs2 := nextinstr (rs#CTR <- (ms m0))). set (rs3 := nextinstr (rs2#GPR2 <- (parent_ra s))). @@ -987,27 +991,27 @@ Proof. set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))). set (rs6 := rs5#PC <- (rs5 CTR)). assert (exec_straight tge (transl_function f) - (transl_code (Mtailcall sig (inl ident m0) :: c)) rs m - (Pbctr :: transl_code c) rs5 (free m stk)). + (transl_code f (Mtailcall sig (inl ident m0) :: c)) rs m + (Pbctr :: transl_code f c) rs5 (free m stk)). simpl. apply exec_straight_step with rs2 m. - simpl. rewrite <- (ireg_val _ _ _ _ AG H5). reflexivity. reflexivity. + simpl. rewrite <- (ireg_val _ _ _ _ AG H6). reflexivity. reflexivity. apply exec_straight_step with rs3 m. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. change (rs2 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. unfold load_stack in H1. simpl in H1. rewrite H1. + simpl. unfold load_stack in H2. simpl in H2. rewrite H2. reflexivity. discriminate. reflexivity. apply exec_straight_step with rs4 m. simpl. reflexivity. reflexivity. apply exec_straight_one. simpl. change (rs4 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - unfold load_stack in H0; simpl in H0. rewrite Int.add_zero in H0. - simpl. rewrite H0. reflexivity. reflexivity. + unfold load_stack in H1; simpl in H1. + simpl. rewrite H1. reflexivity. reflexivity. left; exists (State rs6 (free m stk)); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone) Vone). - rewrite <- H6; simpl. eauto. + rewrite <- H7; simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. repeat (eapply code_tail_next_int; auto). eauto. @@ -1018,7 +1022,7 @@ Proof. unfold rs4, rs3, rs2; auto 10 with ppcgen. assert (AG5: agree ms (parent_sp s) rs5). unfold rs5. apply agree_nextinstr. - split. reflexivity. intros. inv AG4. rewrite H11. + split. reflexivity. intros. inv AG4. rewrite H12. rewrite Pregmap.gso; auto with ppcgen. unfold rs6; auto with ppcgen. change (rs6 PC) with (ms m0). @@ -1030,25 +1034,25 @@ Proof. set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). set (rs5 := rs4#PC <- (Vptr f' Int.zero)). assert (exec_straight tge (transl_function f) - (transl_code (Mtailcall sig (inr mreg i) :: c)) rs m - (Pbs i :: transl_code c) rs4 (free m stk)). + (transl_code f (Mtailcall sig (inr mreg i) :: c)) rs m + (Pbs i :: transl_code f c) rs4 (free m stk)). simpl. apply exec_straight_step with rs2 m. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. rewrite <- (sp_val _ _ _ AG). - simpl. unfold load_stack in H1. simpl in H1. rewrite H1. + simpl. unfold load_stack in H2. simpl in H2. rewrite H2. reflexivity. discriminate. reflexivity. apply exec_straight_step with rs3 m. simpl. reflexivity. reflexivity. apply exec_straight_one. simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). - unfold load_stack in H0; simpl in H0. rewrite Int.add_zero in H0. - simpl. rewrite H0. reflexivity. reflexivity. + unfold load_stack in H1; simpl in H1. + simpl. rewrite H1. reflexivity. reflexivity. left; exists (State rs5 (free m stk)); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). - rewrite <- H6; simpl. eauto. + rewrite <- H7; simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. repeat (eapply code_tail_next_int; auto). eauto. @@ -1060,7 +1064,7 @@ Proof. unfold rs3, rs2; auto 10 with ppcgen. assert (AG4: agree ms (parent_sp s) rs4). unfold rs4. apply agree_nextinstr. - split. reflexivity. intros. inv AG3. rewrite H11. + split. reflexivity. intros. inv AG3. rewrite H12. rewrite Pregmap.gso; auto with ppcgen. unfold rs5; auto with ppcgen. Qed. @@ -1120,8 +1124,8 @@ Proof. intro WTI. inv WTI. pose (k1 := if snd (crbit_for_cond cond) - then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code c - else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code c). + then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c + else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c). generalize (transl_cond_correct tge (transl_function f) cond args k1 ms sp rs m true H3 AG H). simpl. intros [rs2 [EX [RES AG2]]]. @@ -1161,8 +1165,8 @@ Proof. intro WTI. inversion WTI. pose (k1 := if snd (crbit_for_cond cond) - then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code c - else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code c). + then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c + else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c). generalize (transl_cond_correct tge (transl_function f) cond args k1 ms sp rs m false H1 AG H). simpl. intros [rs2 [EX [RES AG2]]]. @@ -1181,30 +1185,32 @@ Qed. Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : int) - (c : list Mach.instruction) (ms : Mach.regset) (m : mem), - load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) -> + (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function), + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 (Returnstate s ms (free m stk)). Proof. intros; red; intros; inv MS. + assert (f0 = f) by congruence. subst f0. set (rs2 := nextinstr (rs#GPR2 <- (parent_ra s))). set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). set (rs5 := rs4#PC <- (parent_ra s)). assert (exec_straight tge (transl_function f) - (transl_code (Mreturn :: c)) rs m - (Pblr :: transl_code c) rs4 (free m stk)). + (transl_code f (Mreturn :: c)) rs m + (Pblr :: transl_code f c) rs4 (free m stk)). simpl. apply exec_straight_three with rs2 m rs3 m. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - unfold load_stack in H0. simpl in H0. - rewrite <- (sp_val _ _ _ AG). simpl. rewrite H0. + unfold load_stack in H1. simpl in H1. + rewrite <- (sp_val _ _ _ AG). simpl. rewrite H1. reflexivity. discriminate. unfold rs3. change (parent_ra s) with rs2#GPR2. reflexivity. simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). simpl. - unfold load_stack in H. simpl in H. rewrite Int.add_zero in H. - rewrite H. reflexivity. + unfold load_stack in H0. simpl in H0. + rewrite H0. reflexivity. reflexivity. reflexivity. reflexivity. left; exists (State rs5 (free m stk)); split. (* execution *) @@ -1212,10 +1218,10 @@ Proof. eapply exec_straight_exec; eauto. inv AT. econstructor. change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). - rewrite <- H2. simpl. eauto. + rewrite <- H3. simpl. eauto. apply functions_transl; eauto. - generalize (functions_transl_no_overflow _ _ H3); intro NOOV. - simpl in H4. eapply find_instr_tail. + generalize (functions_transl_no_overflow _ _ H4); intro NOOV. + simpl in H5. eapply find_instr_tail. eapply code_tail_next_int; auto. eapply code_tail_next_int; auto. eapply code_tail_next_int; eauto. @@ -1237,11 +1243,10 @@ Lemma exec_function_internal_prop: forall (s : list stackframe) (fb : block) (ms : Mach.regset) (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block), Genv.find_funct_ptr ge fb = Some (Internal f) -> - alloc m (- fn_framesize f) - (align_16_top (- fn_framesize f) (fn_stacksize f)) = (m1, stk) -> + alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) -> let sp := Vptr stk (Int.repr (- fn_framesize f)) in - store_stack m1 sp Tint (Int.repr 0) (parent_sp s) = Some m2 -> - store_stack m2 sp Tint (Int.repr 12) (parent_ra s) = Some m3 -> + store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 -> + store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> exec_instr_prop (Machconcr.Callstate s fb ms m) E0 (Machconcr.State s fb sp (fn_code f) ms m3). Proof. @@ -1258,14 +1263,12 @@ Proof. assert (EXEC_PROLOGUE: exec_straight tge (transl_function f) (transl_function f) rs m - (transl_code (fn_code f)) rs4 m3). + (transl_code f (fn_code f)) rs4 m3). unfold transl_function at 2. apply exec_straight_three with rs2 m2 rs3 m2. - unfold exec_instr. rewrite H0. fold sp. - generalize H1. unfold store_stack. change (Vint (Int.repr 0)) with Vzero. - replace (Val.add sp Vzero) with sp. simpl chunk_of_type. - rewrite (sp_val _ _ _ AG). intro EQ; rewrite EQ; clear EQ. - reflexivity. unfold sp. simpl. rewrite Int.add_zero. reflexivity. + unfold exec_instr. rewrite H0. fold sp. + unfold store_stack in H1. simpl chunk_of_type in H1. + rewrite <- (sp_val _ _ _ AG). rewrite H1. reflexivity. simpl. change (rs2 LR) with (rs LR). rewrite ATLR. reflexivity. simpl. unfold store1. rewrite gpr_or_zero_not_zero. unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR2) with (parent_ra s). diff --git a/backend/PPCgenretaddr.v b/backend/PPCgenretaddr.v index 3526865e..eab8599e 100644 --- a/backend/PPCgenretaddr.v +++ b/backend/PPCgenretaddr.v @@ -68,7 +68,7 @@ Qed. Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop := | return_address_offset_intro: forall c f ofs, - code_tail ofs (transl_function f) (transl_code c) -> + code_tail ofs (transl_function f) (transl_code f c) -> return_address_offset f c (Int.repr ofs). (** We now show that such an offset always exists if the Mach code [c] @@ -159,7 +159,7 @@ Proof. unfold transl_load_store; intros; destruct addr; IsTail. Qed. Hint Resolve transl_load_store_tail: ppcretaddr. Lemma transl_instr_tail: - forall i k, is_tail k (transl_instr i k). + forall f i k, is_tail k (transl_instr f i k). Proof. unfold transl_instr; intros; destruct i; IsTail. destruct m; IsTail. @@ -170,7 +170,7 @@ Qed. Hint Resolve transl_instr_tail: ppcretaddr. Lemma transl_code_tail: - forall c1 c2, is_tail c1 c2 -> is_tail (transl_code c1) (transl_code c2). + forall f c1 c2, is_tail c1 c2 -> is_tail (transl_code f c1) (transl_code f c2). Proof. induction 1; simpl. constructor. eapply is_tail_trans; eauto with ppcretaddr. Qed. @@ -179,7 +179,7 @@ Lemma return_address_exists: forall f c, is_tail c f.(fn_code) -> exists ra, return_address_offset f c ra. Proof. - intros. assert (is_tail (transl_code c) (transl_function f)). + intros. assert (is_tail (transl_code f c) (transl_function f)). unfold transl_function. IsTail. apply transl_code_tail; auto. destruct (is_tail_code_tail _ _ H0) as [ofs A]. exists (Int.repr ofs). constructor. auto. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index a30f9e50..fa9dd210 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -224,7 +224,7 @@ Definition check_instr (i: instruction) : bool := match ros with inl r => check_reg r Tint | inr s => true end && check_regs args sig.(sig_args) && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res) - && zeq (Conventions.size_arguments sig) 14 + && Conventions.tailcall_is_possible sig | Ialloc arg res s => check_reg arg Tint && check_reg res Tint @@ -330,8 +330,7 @@ Proof. destruct s0; auto. apply check_reg_correct; auto. eapply proj_sumbool_true; eauto. apply check_regs_correct; auto. - rewrite Conventions.tailcall_possible_size. - eapply proj_sumbool_true; eauto. + apply Conventions.tailcall_is_possible_correct; auto. (* alloc *) constructor. apply check_reg_correct; auto. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 3f0ff1ee..2edb4827 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -300,12 +300,13 @@ Proof. inv H. inv H1. constructor. unfold wt_function. simpl. apply wt_parallel_move; auto with reloadty. rewrite loc_parameters_type. auto. - unfold loc_parameters; red; intros. - destruct (list_in_map_inv _ _ _ H) as [r [A B]]. rewrite A. - generalize (loc_arguments_acceptable _ _ B). - destruct r; simpl; auto. destruct s; try tauto. - intros; simpl. split. omega. - apply loc_arguments_bounded; auto. + red; intros. + destruct (list_in_map_inv _ _ _ H) as [r [A B]]. + generalize (loc_arguments_acceptable _ _ B). + destruct r; intro. + rewrite A. simpl. auto. + red in H0. destruct s; try tauto. + simpl in A. subst l. simpl. auto. apply wt_transf_code; auto. constructor. Qed. diff --git a/backend/Stacking.v b/backend/Stacking.v index 16595e54..a1310aa1 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -45,9 +45,8 @@ Require Import Conventions. To facilitate some of the proofs, the Cminor stack-allocated data starts at offset 0; the preceding areas in the activation record therefore have negative offsets. This part (with negative offsets) -is called the ``frame'' (see the [Machabstr] semantics for the Mach -language), by opposition with the ``Cminor stack data'' which is the part -with positive offsets. +is called the ``frame'', by opposition with the ``Cminor stack data'' +which is the part with positive offsets. The [frame_env] compilation environment records the positions of the boundaries between areas in the frame part. @@ -55,6 +54,8 @@ the boundaries between areas in the frame part. Record frame_env : Set := mk_frame_env { fe_size: Z; + fe_ofs_link: Z; + fe_ofs_retaddr: Z; fe_ofs_int_local: Z; fe_ofs_int_callee_save: Z; fe_num_int_callee_save: Z; @@ -67,19 +68,22 @@ Record frame_env : Set := mk_frame_env { function. *) Definition make_env (b: bounds) := - let oil := 4 * b.(bound_outgoing) in (* integer locals *) + let oil := 4 * b.(bound_outgoing) in (* integer locals *) let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *) let oendi := oics + 4 * b.(bound_int_callee_save) in let ofl := align oendi 8 in (* float locals *) let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *) let sz := ofcs + 8 * b.(bound_float_callee_save) in (* total frame size *) - mk_frame_env sz oil oics b.(bound_int_callee_save) + mk_frame_env sz 0 12 + oil oics b.(bound_int_callee_save) ofl ofcs b.(bound_float_callee_save). (** Computation the frame offset for the given component of the frame. The component is expressed by the following [frame_index] sum type. *) Inductive frame_index: Set := + | FI_link: frame_index + | FI_retaddr: frame_index | FI_local: Z -> typ -> frame_index | FI_arg: Z -> typ -> frame_index | FI_saved_int: Z -> frame_index @@ -87,6 +91,8 @@ Inductive frame_index: Set := Definition offset_of_index (fe: frame_env) (idx: frame_index) := match idx with + | FI_link => fe.(fe_ofs_link) + | FI_retaddr => fe.(fe_ofs_retaddr) | FI_local x Tint => fe.(fe_ofs_int_local) + 4 * x | FI_local x Tfloat => fe.(fe_ofs_float_local) + 8 * x | FI_arg x ty => 4 * x @@ -218,7 +224,8 @@ Definition transl_instr | Lcall sig ros => Mcall sig ros :: k | Ltailcall sig ros => - restore_callee_save fe (Mtailcall sig ros :: k) + restore_callee_save fe + (Mtailcall sig ros :: k) | Lalloc => Malloc :: k | Llabel lbl => @@ -228,7 +235,8 @@ Definition transl_instr | Lcond cond args lbl => Mcond cond args lbl :: k | Lreturn => - restore_callee_save fe (Mreturn :: k) + restore_callee_save fe + (Mreturn :: k) end. (** Translation of a function. Code that saves the values of used @@ -260,7 +268,9 @@ Definition transf_function (f: Linear.function) : res Mach.function := f.(Linear.fn_sig) (transl_body f fe) f.(Linear.fn_stacksize) - fe.(fe_size)). + fe.(fe_size) + (Int.repr fe.(fe_ofs_link)) + (Int.repr fe.(fe_ofs_retaddr))). Definition transf_fundef (f: Linear.fundef) : res Mach.fundef := AST.transf_partial_fundef transf_function f. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 46e19ca9..fc2b63a1 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -50,6 +50,7 @@ Proof. destruct ty; auto. Qed. +(* Lemma get_slot_ok: forall fr ty ofs, 24 <= ofs -> fr.(fr_low) + ofs + 4 * typesize ty <= 0 -> @@ -133,6 +134,7 @@ Lemma slot_gi: Proof. intros. rewrite <- typesize_typesize in H0. constructor; auto. Qed. +*) Section PRESERVATION. @@ -157,7 +159,9 @@ Lemma unfold_transf_function: f.(Linear.fn_sig) (transl_body f fe) f.(Linear.fn_stacksize) - fe.(fe_size). + fe.(fe_size) + (Int.repr fe.(fe_ofs_link)) + (Int.repr fe.(fe_ofs_retaddr)). Proof. generalize TRANSF_F. unfold transf_function. case (zlt (Linear.fn_stacksize f) 0). intros; discriminate. @@ -180,6 +184,8 @@ Qed. Definition index_valid (idx: frame_index) := match idx with + | FI_link => True + | FI_retaddr => True | FI_local x Tint => 0 <= x < b.(bound_int_local) | FI_local x Tfloat => 0 <= x < b.(bound_float_local) | FI_arg x ty => 14 <= x /\ x + typesize ty <= b.(bound_outgoing) @@ -189,6 +195,8 @@ Definition index_valid (idx: frame_index) := Definition type_of_index (idx: frame_index) := match idx with + | FI_link => Tint + | FI_retaddr => Tint | FI_local x ty => ty | FI_arg x ty => ty | FI_saved_int x => Tint @@ -200,6 +208,8 @@ Definition type_of_index (idx: frame_index) := Definition index_diff (idx1 idx2: frame_index) : Prop := match idx1, idx2 with + | FI_link, FI_link => False + | FI_retaddr, FI_retaddr => False | FI_local x1 ty1, FI_local x2 ty2 => x1 <> x2 \/ ty1 <> ty2 | FI_arg x1 ty1, FI_arg x2 ty2 => @@ -224,7 +234,7 @@ Ltac AddPosProps := generalize (bound_outgoing_pos b); intro; generalize align_float_part; intro. -Lemma size_pos: fe.(fe_size) >= 24. +Lemma size_pos: fe.(fe_size) >= 0. Proof. AddPosProps. unfold fe, make_env, fe_size. omega. @@ -246,6 +256,7 @@ Proof. unfold offset_of_index, fe, make_env, fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, fe_ofs_float_local, fe_ofs_float_callee_save, + fe_ofs_link, fe_ofs_retaddr, type_of_index, typesize; simpl in H5; simpl in H6; simpl in H7; try omega. @@ -302,7 +313,7 @@ Hint Resolve index_local_valid index_arg_valid Lemma offset_of_index_valid: forall idx, index_valid idx -> - 24 <= offset_of_index fe idx /\ + 0 <= offset_of_index fe idx /\ offset_of_index fe idx + 4 * typesize (type_of_index idx) <= fe.(fe_size). Proof. AddPosProps. @@ -311,6 +322,7 @@ Proof. unfold offset_of_index, fe, make_env, fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, fe_ofs_float_local, fe_ofs_float_callee_save, + fe_ofs_link, fe_ofs_retaddr, type_of_index, typesize; simpl in H5; omega. @@ -327,7 +339,7 @@ Proof. intros. generalize (offset_of_index_valid idx H). intros [A B]. apply Int.signed_repr. - split. apply Zle_trans with 24; auto. compute; intro; discriminate. + split. apply Zle_trans with 0; auto. compute; intro; discriminate. assert (offset_of_index fe idx < fe_size fe). generalize (typesize_pos (type_of_index idx)); intro. omega. apply Zlt_succ_le. @@ -335,102 +347,111 @@ Proof. generalize size_no_overflow. omega. Qed. -(** Admissible evaluation rules for the [Mgetstack] and [Msetstack] - instructions, in case the offset is computed with [offset_of_index]. *) +(** Characterization of the [get_slot] and [set_slot] + operations in terms of the following [index_val] and [set_index_val] + frame access functions. *) -Lemma exec_Mgetstack': - forall sp idx ty c rs fr dst m v, - index_valid idx -> - get_slot fr ty (offset_of_index fe idx) v -> - step tge - (State stack tf sp - (Mgetstack (Int.repr (offset_of_index fe idx)) ty dst :: c) - rs fr m) - E0 (State stack tf sp c (rs#dst <- v) fr m). -Proof. - intros. apply exec_Mgetstack. - rewrite offset_of_index_no_overflow. auto. auto. -Qed. +Definition index_val (idx: frame_index) (fr: frame) := + fr (type_of_index idx) (offset_of_index fe idx - tf.(fn_framesize)). -Lemma exec_Msetstack': - forall sp idx ty c rs fr src m fr', - index_valid idx -> - set_slot fr ty (offset_of_index fe idx) (rs src) fr' -> - step tge - (State stack tf sp - (Msetstack src (Int.repr (offset_of_index fe idx)) ty :: c) - rs fr m) - E0 (State stack tf sp c rs fr' m). +Definition set_index_val (idx: frame_index) (v: val) (fr: frame) := + update (type_of_index idx) (offset_of_index fe idx - tf.(fn_framesize)) v fr. + +Lemma slot_valid_index: + forall idx, + index_valid idx -> idx <> FI_link -> idx <> FI_retaddr -> + slot_valid tf (type_of_index idx) (offset_of_index fe idx). Proof. - intros. apply exec_Msetstack. - rewrite offset_of_index_no_overflow. auto. auto. + intros. + destruct (offset_of_index_valid idx H) as [A B]. + rewrite <- typesize_typesize in B. + rewrite unfold_transf_function; constructor. + auto. unfold fn_framesize. auto. + unfold fn_link_ofs. change (fe_ofs_link fe) with (offset_of_index fe FI_link). + rewrite offset_of_index_no_overflow. + exploit (offset_of_index_disj idx FI_link). + auto. exact I. red. destruct idx; auto || congruence. + intro. rewrite typesize_typesize. assumption. + exact I. + unfold fn_retaddr_ofs. change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr). + rewrite offset_of_index_no_overflow. + exploit (offset_of_index_disj idx FI_retaddr). + auto. exact I. red. destruct idx; auto || congruence. + intro. rewrite typesize_typesize. assumption. + exact I. Qed. -(** An alternate characterization of the [get_slot] and [set_slot] - operations in terms of the following [index_val] frame access - function. *) - -Definition index_val (idx: frame_index) (fr: frame) := - fr.(fr_contents) (type_of_index idx) (fr.(fr_low) + offset_of_index fe idx). - Lemma get_slot_index: forall fr idx ty v, - index_valid idx -> - fr.(fr_low) = -fe.(fe_size) -> + index_valid idx -> idx <> FI_link -> idx <> FI_retaddr -> ty = type_of_index idx -> v = index_val idx fr -> - get_slot fr ty (offset_of_index fe idx) v. + get_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe idx))) v. Proof. - intros. subst v; subst ty. - generalize (offset_of_index_valid idx H); intros [A B]. - rewrite <- typesize_typesize in B. + intros. subst v; subst ty. rewrite offset_of_index_no_overflow; auto. unfold index_val. apply get_slot_intro; auto. - rewrite H0. omega. + apply slot_valid_index; auto. Qed. Lemma set_slot_index: forall fr idx v, - index_valid idx -> - fr.(fr_low) = -fe.(fe_size) -> - exists fr', set_slot fr (type_of_index idx) (offset_of_index fe idx) v fr'. -Proof. - intros. - generalize (offset_of_index_valid idx H); intros [A B]. - apply set_slot_ok; auto. rewrite H0. omega. + index_valid idx -> idx <> FI_link -> idx <> FI_retaddr -> + set_slot tf fr (type_of_index idx) (Int.signed (Int.repr (offset_of_index fe idx))) + v (set_index_val idx v fr). +Proof. + intros. rewrite offset_of_index_no_overflow; auto. + apply set_slot_intro. + apply slot_valid_index; auto. + unfold set_index_val. auto. Qed. -(** Alternate ``good variable'' properties for [get_slot] and [set_slot]. *) +(** ``Good variable'' properties for [index_val] and [set_index_val]. *) -Lemma slot_iss: - forall fr idx v fr', - set_slot fr (type_of_index idx) (offset_of_index fe idx) v fr' -> - index_val idx fr' = v. +Lemma get_set_index_val_same: + forall fr idx v, + index_val idx (set_index_val idx v fr) = v. Proof. - intros. exploit slot_gss; eauto. intro. inv H0. auto. + intros. unfold index_val, set_index_val. apply update_same. Qed. -Lemma slot_iso: - forall fr idx v fr' idx', - set_slot fr (type_of_index idx) (offset_of_index fe idx) v fr' -> - index_diff idx idx' -> - index_valid idx -> index_valid idx' -> - index_val idx' fr' = index_val idx' fr. +Lemma get_set_index_val_other: + forall fr idx idx' v, + index_valid idx -> index_valid idx' -> index_diff idx idx' -> + index_val idx' (set_index_val idx v fr) = index_val idx' fr. Proof. - intros. generalize (offset_of_index_disj idx idx' H1 H2 H0). intro. - inv H. unfold index_val. simpl fr_low. apply frame_update_gso. - omega. + intros. unfold index_val, set_index_val. apply update_other. + repeat rewrite typesize_typesize. + exploit (offset_of_index_disj idx idx'); auto. omega. +Qed. + +Lemma get_set_index_val_overlap: + forall ofs1 ty1 ofs2 ty2 v fr, + S (Outgoing ofs1 ty1) <> S (Outgoing ofs2 ty2) -> + Loc.overlap (S (Outgoing ofs1 ty1)) (S (Outgoing ofs2 ty2)) = true -> + index_val (FI_arg ofs2 ty2) (set_index_val (FI_arg ofs1 ty1) v fr) = Vundef. +Proof. + intros. unfold index_val, set_index_val, offset_of_index, type_of_index. + assert (~(ofs1 + typesize ty1 <= ofs2 \/ ofs2 + typesize ty2 <= ofs1)). + destruct (orb_prop _ _ H0). apply Loc.overlap_aux_true_1. auto. + apply Loc.overlap_aux_true_2. auto. + unfold update. + destruct (zeq (4 * ofs1 - fn_framesize tf) (4 * ofs2 - fn_framesize tf)). + destruct (typ_eq ty1 ty2). + elim H. decEq. decEq. omega. auto. + auto. + repeat rewrite typesize_typesize. + rewrite zle_false. apply zle_false. omega. omega. Qed. (** * Agreement between location sets and Mach environments *) (** The following [agree] predicate expresses semantic agreement between: - on the Linear side, the current location set [ls] and the location - set at function entry [ls0]; -- on the Mach side, a register set [rs] plus the current and parent frames - [fr] and [parent]. + set of the caller [ls0]; +- on the Mach side, a register set [rs], a frame [fr] and a call stack [cs]. *) -Record agree (ls: locset) (rs: regset) (fr parent: frame) (ls0: locset) : Prop := +Record agree (ls ls0: locset) (rs: regset) (fr: frame) (cs: list stackframe): Prop := mk_agree { (** Machine registers have the same values on the Linear and Mach sides. *) agree_reg: @@ -442,10 +463,6 @@ Record agree (ls: locset) (rs: regset) (fr parent: frame) (ls0: locset) : Prop : agree_unused_reg: forall r, ~(mreg_within_bounds b r) -> rs r = ls0 (R r); - (** The low bound of the current frame is [- fe.(fe_size)]. *) - agree_size: - fr.(fr_low) = -fe.(fe_size); - (** Local and outgoing stack slots (on the Linear side) have the same values as the one loaded from the current Mach frame at the corresponding offsets. *) @@ -463,8 +480,9 @@ Record agree (ls: locset) (rs: regset) (fr parent: frame) (ls0: locset) : Prop : at the corresponding offsets. *) agree_incoming: forall ofs ty, - slot_within_bounds f b (Incoming ofs ty) -> - get_slot parent ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Incoming ofs ty))); + In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) -> + get_slot (parent_function cs) (parent_frame cs) + ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Incoming ofs ty))); (** The areas of the frame reserved for saving used callee-save registers always contain the values that those registers had @@ -481,22 +499,22 @@ Record agree (ls: locset) (rs: regset) (fr parent: frame) (ls0: locset) : Prop : index_val (FI_saved_float (index_float_callee_save r)) fr = ls0 (R r) }. -Hint Resolve agree_reg agree_unused_reg agree_size +Hint Resolve agree_reg agree_unused_reg agree_locals agree_outgoing agree_incoming agree_saved_int agree_saved_float: stacking. (** Values of registers and register lists. *) Lemma agree_eval_reg: - forall ls rs fr parent ls0 r, - agree ls rs fr parent ls0 -> rs r = ls (R r). + forall ls ls0 rs fr cs r, + agree ls ls0 rs fr cs -> rs r = ls (R r). Proof. intros. symmetry. eauto with stacking. Qed. Lemma agree_eval_regs: - forall ls rs fr parent ls0 rl, - agree ls rs fr parent ls0 -> rs##rl = reglist ls rl. + forall ls ls0 rs fr cs rl, + agree ls ls0 rs cs fr -> rs##rl = reglist ls rl. Proof. induction rl; simpl; intros. auto. f_equal. eapply agree_eval_reg; eauto. auto. @@ -508,10 +526,10 @@ Hint Resolve agree_eval_reg agree_eval_regs: stacking. of machine registers, of local slots, of outgoing slots. *) Lemma agree_set_reg: - forall ls rs fr parent ls0 r v, - agree ls rs fr parent ls0 -> + forall ls ls0 rs fr cs r v, + agree ls ls0 rs fr cs -> mreg_within_bounds b r -> - agree (Locmap.set (R r) v ls) (Regmap.set r v rs) fr parent ls0. + agree (Locmap.set (R r) v ls) ls0 (Regmap.set r v rs) fr cs. Proof. intros. constructor; eauto with stacking. intros. case (mreg_eq r r0); intro. @@ -526,131 +544,176 @@ Proof. Qed. Lemma agree_set_local: - forall ls rs fr parent ls0 v ofs ty, - agree ls rs fr parent ls0 -> + forall ls ls0 rs fr cs v ofs ty, + agree ls ls0 rs fr cs -> slot_within_bounds f b (Local ofs ty) -> exists fr', - set_slot fr ty (offset_of_index fe (FI_local ofs ty)) v fr' /\ - agree (Locmap.set (S (Local ofs ty)) v ls) rs fr' parent ls0. + set_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe (FI_local ofs ty)))) v fr' /\ + agree (Locmap.set (S (Local ofs ty)) v ls) ls0 rs fr' cs. Proof. intros. - generalize (set_slot_index fr _ v (index_local_valid _ _ H0) - (agree_size _ _ _ _ _ H)). - intros [fr' SET]. - exists fr'. split. auto. constructor; eauto with stacking. + exists (set_index_val (FI_local ofs ty) v fr); split. + set (idx := FI_local ofs ty). + change ty with (type_of_index idx). + apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. + constructor; eauto with stacking. (* agree_reg *) intros. rewrite Locmap.gso. eauto with stacking. red; auto. - (* agree_size *) - inversion SET. rewrite H3; simpl fr_low. eauto with stacking. (* agree_local *) intros. case (slot_eq (Local ofs ty) (Local ofs0 ty0)); intro. rewrite <- e. rewrite Locmap.gss. replace (FI_local ofs0 ty0) with (FI_local ofs ty). - symmetry. eapply slot_iss; eauto. congruence. + symmetry. apply get_set_index_val_same. congruence. assert (ofs <> ofs0 \/ ty <> ty0). case (zeq ofs ofs0); intro. compare ty ty0; intro. congruence. tauto. tauto. - rewrite Locmap.gso. transitivity (index_val (FI_local ofs0 ty0) fr). - eauto with stacking. symmetry. eapply slot_iso; eauto. - simpl. auto. + rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. + red. auto. (* agree_outgoing *) - intros. rewrite Locmap.gso. transitivity (index_val (FI_arg ofs0 ty0) fr). - eauto with stacking. symmetry. eapply slot_iso; eauto. - red; auto. red; auto. + intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. + red; auto. red; auto. (* agree_incoming *) intros. rewrite Locmap.gso. eauto with stacking. red. auto. (* agree_saved_int *) - intros. rewrite <- (agree_saved_int _ _ _ _ _ H r H1 H2). - eapply slot_iso; eauto with stacking. red; auto. + intros. rewrite get_set_index_val_other; eauto with stacking. + red; auto. (* agree_saved_float *) - intros. rewrite <- (agree_saved_float _ _ _ _ _ H r H1 H2). - eapply slot_iso; eauto with stacking. red; auto. + intros. rewrite get_set_index_val_other; eauto with stacking. + red; auto. Qed. Lemma agree_set_outgoing: - forall ls rs fr parent ls0 v ofs ty, - agree ls rs fr parent ls0 -> + forall ls ls0 rs fr cs v ofs ty, + agree ls ls0 rs fr cs -> slot_within_bounds f b (Outgoing ofs ty) -> exists fr', - set_slot fr ty (offset_of_index fe (FI_arg ofs ty)) v fr' /\ - agree (Locmap.set (S (Outgoing ofs ty)) v ls) rs fr' parent ls0. -Proof. - intros. - generalize (set_slot_index fr _ v (index_arg_valid _ _ H0) - (agree_size _ _ _ _ _ H)). - intros [fr' SET]. - exists fr'. split. exact SET. constructor; eauto with stacking. + set_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe (FI_arg ofs ty)))) v fr' /\ + agree (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 rs fr' cs. +Proof. + intros. + exists (set_index_val (FI_arg ofs ty) v fr); split. + set (idx := FI_arg ofs ty). + change ty with (type_of_index idx). + apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. + constructor; eauto with stacking. (* agree_reg *) intros. rewrite Locmap.gso. eauto with stacking. red; auto. - (* agree_size *) - inversion SET. subst fr'; simpl fr_low. eauto with stacking. (* agree_local *) - intros. rewrite Locmap.gso. - transitivity (index_val (FI_local ofs0 ty0) fr). - eauto with stacking. symmetry. eapply slot_iso; eauto. - red; auto. red; auto. + intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. + red; auto. red; auto. (* agree_outgoing *) intros. unfold Locmap.set. case (Loc.eq (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))); intro. (* same location *) - replace ofs0 with ofs. replace ty0 with ty. - symmetry. eapply slot_iss; eauto. - congruence. congruence. + replace ofs0 with ofs by congruence. replace ty0 with ty by congruence. + symmetry. apply get_set_index_val_same. (* overlapping locations *) caseEq (Loc.overlap (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))); intros. - inv SET. unfold index_val, type_of_index, offset_of_index. - destruct (zeq ofs ofs0). - subst ofs0. symmetry. apply frame_update_mismatch. - destruct ty; destruct ty0; simpl; congruence. - generalize (Loc.overlap_not_diff _ _ H2). intro. simpl in H5. - simpl fr_low. symmetry. apply frame_update_overlap. omega. omega. omega. - (* different locations *) - transitivity (index_val (FI_arg ofs0 ty0) fr). - eauto with stacking. - symmetry. eapply slot_iso; eauto. - simpl. eapply Loc.overlap_aux_false_1; eauto. + symmetry. apply get_set_index_val_overlap; auto. + (* disjoint locations *) + rewrite get_set_index_val_other; eauto with stacking. + red. eapply Loc.overlap_aux_false_1; eauto. (* agree_incoming *) intros. rewrite Locmap.gso. eauto with stacking. red. auto. (* saved ints *) - intros. rewrite <- (agree_saved_int _ _ _ _ _ H r H1 H2). - eapply slot_iso; eauto with stacking. red; auto. + intros. rewrite get_set_index_val_other; eauto with stacking. red; auto. (* saved floats *) - intros. rewrite <- (agree_saved_float _ _ _ _ _ H r H1 H2). - eapply slot_iso; eauto with stacking. red; auto. + intros. rewrite get_set_index_val_other; eauto with stacking. red; auto. Qed. + (* -Lemma agree_return_regs: - forall ls rs fr parent ls0 ls' rs', - agree ls rs fr parent ls0 -> - (forall r, - In (R r) temporaries \/ In (R r) destroyed_at_call -> - rs' r = ls' (R r)) -> - (forall r, - In r int_callee_save_regs \/ In r float_callee_save_regs -> - rs' r = rs r) -> - agree (LTL.return_regs ls ls') rs' fr parent ls0. +Lemma agree_set_int_callee_save: + forall ls ls0 rs fr r v, + agree ls ls0 rs fr -> + In r int_callee_save_regs -> + index_int_callee_save r < fe.(fe_num_int_callee_save) -> + exists fr', + set_slot tf fr Tint + (Int.signed (Int.repr + (offset_of_index fe (FI_saved_int (index_int_callee_save r))))) + v fr' /\ + agree ls (Locmap.set (R r) v ls0) rs fr'. Proof. - intros. constructor; unfold LTL.return_regs; eauto with stacking. - (* agree_reg *) - intros. case (In_dec Loc.eq (R r) temporaries); intro. - symmetry. apply H0. tauto. - case (In_dec Loc.eq (R r) destroyed_at_call); intro. - symmetry. apply H0. tauto. - rewrite H1. eauto with stacking. - generalize (register_classification r); tauto. + intros. + set (idx := FI_saved_int (index_int_callee_save r)). + exists (set_index_val idx v fr); split. + change Tint with (type_of_index idx). + apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. + constructor; eauto with stacking. (* agree_unused_reg *) - intros. rewrite H1. eauto with stacking. - generalize H2; unfold mreg_within_bounds; case (mreg_type r); intro. - left. apply index_int_callee_save_pos2. - generalize (bound_int_callee_save_pos b); intro. omega. - right. apply index_float_callee_save_pos2. - generalize (bound_float_callee_save_pos b); intro. omega. -Qed. + intros. rewrite Locmap.gso. eauto with stacking. + red; red; intro. subst r0. elim H2. red. + rewrite (int_callee_save_type r H0). auto. + (* agree_local *) + intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. + red; auto. + (* agree_outgoing *) + intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. + red; auto. + (* agree_incoming *) + intros. rewrite Locmap.gso. eauto with stacking. red. auto. + (* saved ints *) + intros. destruct (mreg_eq r r0). + subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. + rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking. + unfold idx. auto with stacking. auto with stacking. + unfold idx; red. apply index_int_callee_save_inj; auto. + red; auto. + (* saved floats *) + intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. + unfold idx. auto with stacking. + unfold idx; red; auto. + red. apply int_float_callee_save_disjoint; auto. +Qed. + +Lemma agree_set_float_callee_save: + forall ls ls0 rs fr r v, + agree ls ls0 rs fr -> + In r float_callee_save_regs -> + index_float_callee_save r < fe.(fe_num_float_callee_save) -> + exists fr', + set_slot tf fr Tfloat + (Int.signed (Int.repr + (offset_of_index fe (FI_saved_float (index_float_callee_save r))))) + v fr' /\ + agree ls (Locmap.set (R r) v ls0) rs fr'. +Proof. + intros. + set (idx := FI_saved_float (index_float_callee_save r)). + exists (set_index_val idx v fr); split. + change Tfloat with (type_of_index idx). + apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. + constructor; eauto with stacking. + (* agree_unused_reg *) + intros. rewrite Locmap.gso. eauto with stacking. + red; red; intro. subst r0. elim H2. red. + rewrite (float_callee_save_type r H0). auto. + (* agree_local *) + intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. + red; auto. + (* agree_outgoing *) + intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. + red; auto. + (* agree_incoming *) + intros. rewrite Locmap.gso. eauto with stacking. red. auto. + (* saved ints *) + intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. + unfold idx. auto with stacking. + unfold idx; red; auto. + red. apply sym_not_equal. apply int_float_callee_save_disjoint; auto. + (* saved floats *) + intros. destruct (mreg_eq r r0). + subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. + rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking. + unfold idx. auto with stacking. auto with stacking. + unfold idx; red. apply index_float_callee_save_inj; auto. + red; auto. +Qed. *) Lemma agree_return_regs: - forall ls rs fr parent ls0 rs', - agree ls rs fr parent ls0 -> + forall ls ls0 rs fr cs rs', + agree ls ls0 rs fr cs -> (forall r, ~In r int_callee_save_regs -> ~In r float_callee_save_regs -> rs' r = rs r) -> @@ -695,10 +758,10 @@ Proof. Qed. Lemma agree_callee_save_agree: - forall ls rs fr parent ls1 ls2, - agree ls rs fr parent ls1 -> + forall ls ls1 ls2 rs fr cs, + agree ls ls1 rs fr cs -> agree_callee_save ls1 ls2 -> - agree ls rs fr parent ls2. + agree ls ls2 rs fr cs. Proof. intros. inv H. constructor; auto. intros. rewrite agree_unused_reg0; auto. @@ -732,15 +795,15 @@ Qed. (** A variant of [agree] used for return frames. *) -Definition agree_frame (ls: locset) (fr parent: frame) (ls0: locset) : Prop := - exists rs, agree ls rs fr parent ls0. +Definition agree_frame (ls ls0: locset) (fr: frame) (cs: list stackframe): Prop := + exists rs, agree ls ls0 rs fr cs. Lemma agree_frame_agree: - forall ls1 ls2 rs fr parent ls0, - agree_frame ls1 fr parent ls0 -> + forall ls1 ls2 rs fr cs ls0, + agree_frame ls1 ls0 fr cs -> agree_callee_save ls2 ls1 -> (forall r, rs r = ls2 (R r)) -> - agree ls2 rs fr parent ls0. + agree ls2 ls0 rs fr cs. Proof. intros. destruct H as [rs' AG]. inv AG. constructor; auto. @@ -767,10 +830,15 @@ Variable mkindex: Z -> frame_index. Variable ty: typ. Variable sp: val. Variable csregs: list mreg. + Hypothesis number_inj: forall r1 r2, In r1 csregs -> In r2 csregs -> r1 <> r2 -> number r1 <> number r2. Hypothesis mkindex_valid: forall r, In r csregs -> number r < bound fe -> index_valid (mkindex (number r)). +Hypothesis mkindex_not_link: + forall z, mkindex z <> FI_link. +Hypothesis mkindex_not_retaddr: + forall z, mkindex z <> FI_retaddr. Hypothesis mkindex_typ: forall z, type_of_index (mkindex z) = ty. Hypothesis mkindex_inj: @@ -783,13 +851,11 @@ Lemma save_callee_save_regs_correct: forall l k rs fr m, incl l csregs -> list_norepet l -> - fr.(fr_low) = -fe.(fe_size) -> exists fr', star step tge (State stack tf sp (save_callee_save_regs bound number mkindex ty fe l k) rs fr m) E0 (State stack tf sp k rs fr' m) - /\ fr'.(fr_low) = - fe.(fe_size) /\ (forall r, In r l -> number r < bound fe -> index_val (mkindex (number r)) fr' = rs r) @@ -801,8 +867,9 @@ Lemma save_callee_save_regs_correct: Proof. induction l; intros; simpl save_callee_save_regs. (* base case *) - exists fr. split. apply star_refl. split. auto. - split. intros. elim H2. auto. + exists fr. split. apply star_refl. + split. intros. elim H1. + auto. (* inductive case *) set (k1 := save_callee_save_regs bound number mkindex ty fe l k). assert (R1: incl l csregs). eauto with coqlib. @@ -810,49 +877,42 @@ Proof. unfold save_callee_save_reg. destruct (zlt (number a) (bound fe)). (* a store takes place *) - assert (VALID: index_valid (mkindex (number a))). - apply mkindex_valid. auto with coqlib. auto. - exploit set_slot_index; eauto. - intros [fr1 SET]. - exploit (IHl k rs fr1 m); auto. inv SET; auto. - fold k1. intros [fr' [A [B [C D]]]]. + set (fr1 := set_index_val (mkindex (number a)) (rs a) fr). + exploit (IHl k rs fr1 m); auto. + fold k1. intros [fr' [A [B C]]]. exists fr'. - split. eapply star_left. - apply exec_Msetstack'; eauto with stacking. rewrite <- (mkindex_typ (number a)). eauto. - eexact A. traceEq. - split. auto. - split. intros. elim H2; intros. subst r. - rewrite D. eapply slot_iss; eauto. - apply mkindex_valid; auto. + split. eapply star_left. + apply exec_Msetstack. instantiate (1 := fr1). + unfold fr1. rewrite <- (mkindex_typ (number a)). + eapply set_slot_index; eauto with coqlib. + eexact A. + traceEq. + split. intros. simpl in H1. destruct H1. subst r. + rewrite C. unfold fr1. apply get_set_index_val_same. + apply mkindex_valid; auto with coqlib. intros. apply mkindex_inj. apply number_inj; auto with coqlib. - inversion H0. red; intro; subst r; contradiction. - apply C; auto. - intros. transitivity (index_val idx fr1). - apply D; auto. - intros. apply H3; eauto with coqlib. - eapply slot_iso; eauto. - apply mkindex_diff. apply H3. auto with coqlib. - auto. + inversion H0. congruence. + apply B; auto. + intros. rewrite C; auto with coqlib. + unfold fr1. apply get_set_index_val_other; auto with coqlib. (* no store takes place *) - exploit (IHl k rs fr m); auto. intros [fr' [A [B [C D]]]]. - exists fr'. split. exact A. split. exact B. - split. intros. elim H2; intros. subst r. omegaContradiction. - apply C; auto. - intros. apply D; auto. - intros. apply H3; auto with coqlib. + exploit (IHl k rs fr m); auto. intros [fr' [A [B C]]]. + exists fr'. + split. exact A. + split. intros. simpl in H1; destruct H1. subst r. omegaContradiction. + apply B; auto. + intros. apply C; auto with coqlib. Qed. End SAVE_CALLEE_SAVE. Lemma save_callee_save_int_correct: forall k sp rs fr m, - fr.(fr_low) = - fe.(fe_size) -> exists fr', star step tge (State stack tf sp (save_callee_save_int fe k) rs fr m) E0 (State stack tf sp k rs fr' m) - /\ fr'.(fr_low) = - fe.(fe_size) /\ (forall r, In r int_callee_save_regs -> index_int_callee_save r < bound_int_callee_save b -> @@ -866,26 +926,26 @@ Proof. exploit (save_callee_save_regs_correct fe_num_int_callee_save index_int_callee_save FI_saved_int Tint sp int_callee_save_regs). exact index_int_callee_save_inj. - intros. red. split; auto. generalize (index_int_callee_save_pos r H0). omega. + intros. red. split; auto. generalize (index_int_callee_save_pos r H). omega. + intro; congruence. + intro; congruence. auto. intros; congruence. intros until idx. destruct idx; simpl; auto. congruence. apply incl_refl. - apply int_callee_save_norepet. eauto. - intros [fr' [A [B [C D]]]]. + apply int_callee_save_norepet. + intros [fr' [A [B C]]]. exists fr'; intuition. unfold save_callee_save_int; eauto. - apply D. auto. intros; subst idx. auto. + apply C. auto. intros; subst idx. auto. Qed. Lemma save_callee_save_float_correct: forall k sp rs fr m, - fr.(fr_low) = - fe.(fe_size) -> exists fr', star step tge (State stack tf sp (save_callee_save_float fe k) rs fr m) E0 (State stack tf sp k rs fr' m) - /\ fr'.(fr_low) = - fe.(fe_size) /\ (forall r, In r float_callee_save_regs -> index_float_callee_save r < bound_float_callee_save b -> @@ -899,55 +959,57 @@ Proof. exploit (save_callee_save_regs_correct fe_num_float_callee_save index_float_callee_save FI_saved_float Tfloat sp float_callee_save_regs). exact index_float_callee_save_inj. - intros. red. split; auto. generalize (index_float_callee_save_pos r H0). omega. + intros. red. split; auto. generalize (index_float_callee_save_pos r H). omega. + intro; congruence. + intro; congruence. auto. intros; congruence. intros until idx. destruct idx; simpl; auto. congruence. apply incl_refl. apply float_callee_save_norepet. eauto. - intros [fr' [A [B [C D]]]]. + intros [fr' [A [B C]]]. exists fr'; intuition. unfold save_callee_save_float; eauto. - apply D. auto. intros; subst idx. auto. + apply C. auto. intros; subst idx. auto. Qed. Lemma save_callee_save_correct: - forall sp k rs fr m ls, + forall sp k rs m ls cs, (forall r, rs r = ls (R r)) -> - (forall ofs ty, - 14 <= ofs -> - ofs + typesize ty <= size_arguments f.(Linear.fn_sig) -> - get_slot (parent_frame stack) ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Outgoing ofs ty)))) -> - fr.(fr_low) = - fe.(fe_size) -> - (forall idx, index_valid idx -> index_val idx fr = Vundef) -> + (forall ofs ty, + In (S (Outgoing ofs ty)) (loc_arguments f.(Linear.fn_sig)) -> + get_slot (parent_function cs) (parent_frame cs) + ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Outgoing ofs ty)))) -> exists fr', star step tge - (State stack tf sp (save_callee_save fe k) rs fr m) + (State stack tf sp (save_callee_save fe k) rs empty_frame m) E0 (State stack tf sp k rs fr' m) - /\ agree (LTL.call_regs ls) rs fr' (parent_frame stack) ls. + /\ agree (LTL.call_regs ls) ls rs fr' cs. Proof. intros. unfold save_callee_save. exploit save_callee_save_int_correct; eauto. - intros [fr1 [A1 [B1 [C1 D1]]]]. - exploit save_callee_save_float_correct. eexact B1. - intros [fr2 [A2 [B2 [C2 D2]]]]. + intros [fr1 [A1 [B1 C1]]]. + exploit save_callee_save_float_correct. + intros [fr2 [A2 [B2 C2]]]. exists fr2. split. eapply star_trans. eexact A1. eexact A2. traceEq. constructor; unfold LTL.call_regs; auto. (* agree_local *) - intros. rewrite D2; auto with stacking. - rewrite D1; auto with stacking. - symmetry. auto with stacking. + intros. rewrite C2; auto with stacking. + rewrite C1; auto with stacking. (* agree_outgoing *) - intros. rewrite D2; auto with stacking. - rewrite D1; auto with stacking. - symmetry. auto with stacking. + intros. rewrite C2; auto with stacking. + rewrite C1; auto with stacking. (* agree_incoming *) - intros. simpl in H3. apply H0. tauto. tauto. + intros. apply H0. unfold loc_parameters in H1. + exploit list_in_map_inv; eauto. intros [l [A B]]. + exploit loc_arguments_acceptable; eauto. intro C. + destruct l; simpl in A. discriminate. + simpl in C. destruct s; try contradiction. inv A. auto. (* agree_saved_int *) - intros. rewrite D2; auto with stacking. - rewrite C1; auto with stacking. + intros. rewrite C2; auto with stacking. + rewrite B1; auto with stacking. (* agree_saved_float *) - intros. rewrite C2; auto with stacking. + intros. rewrite B2; auto with stacking. Qed. (** The following lemmas show the correctness of the register reloading @@ -965,21 +1027,25 @@ Variable sp: val. Variable csregs: list mreg. Hypothesis mkindex_valid: forall r, In r csregs -> number r < bound fe -> index_valid (mkindex (number r)). +Hypothesis mkindex_not_link: + forall z, mkindex z <> FI_link. +Hypothesis mkindex_not_retaddr: + forall z, mkindex z <> FI_retaddr. Hypothesis mkindex_typ: forall z, type_of_index (mkindex z) = ty. Hypothesis number_within_bounds: forall r, In r csregs -> (number r < bound fe <-> mreg_within_bounds b r). Hypothesis mkindex_val: - forall ls rs fr ls0 r, - agree ls rs fr (parent_frame stack) ls0 -> In r csregs -> number r < bound fe -> + forall ls ls0 rs fr cs r, + agree ls ls0 rs fr cs -> In r csregs -> number r < bound fe -> index_val (mkindex (number r)) fr = ls0 (R r). Lemma restore_callee_save_regs_correct: - forall k fr m ls0 l ls rs, + forall k fr m ls0 l ls rs cs, incl l csregs -> list_norepet l -> - agree ls rs fr (parent_frame stack) ls0 -> + agree ls ls0 rs fr cs -> exists ls', exists rs', star step tge (State stack tf sp @@ -987,7 +1053,7 @@ Lemma restore_callee_save_regs_correct: E0 (State stack tf sp k rs' fr m) /\ (forall r, In r l -> rs' r = ls0 (R r)) /\ (forall r, ~(In r l) -> rs' r = rs r) - /\ agree ls' rs' fr (parent_frame stack) ls0. + /\ agree ls' ls0 rs' fr cs. Proof. induction l; intros; simpl restore_callee_save_regs. (* base case *) @@ -1004,15 +1070,14 @@ Proof. destruct (zlt (number a) (bound fe)). set (ls1 := Locmap.set (R a) (ls0 (R a)) ls). set (rs1 := Regmap.set a (ls0 (R a)) rs). - assert (R3: agree ls1 rs1 fr (parent_frame stack) ls0). + assert (R3: agree ls1 ls0 rs1 fr cs). unfold ls1, rs1. apply agree_set_reg. auto. rewrite <- number_within_bounds; auto. - generalize (IHl ls1 rs1 R1 R2 R3). + generalize (IHl ls1 rs1 cs R1 R2 R3). intros [ls' [rs' [A [B [C D]]]]]. exists ls'. exists rs'. split. apply star_left with E0 (State stack tf sp k1 rs1 fr m) E0. - unfold rs1; apply exec_Mgetstack'; eauto with stacking. - apply get_slot_index; eauto with stacking. + unfold rs1; apply exec_Mgetstack. apply get_slot_index; auto. symmetry. eapply mkindex_val; eauto. auto. traceEq. split. intros. elim H2; intros. @@ -1022,7 +1087,7 @@ Proof. apply sym_not_eq; tauto. tauto. assumption. (* no load takes place *) - generalize (IHl ls rs R1 R2 H1). + generalize (IHl ls rs cs R1 R2 H1). intros [ls' [rs' [A [B [C D]]]]]. exists ls'; exists rs'. split. assumption. split. intros. elim H2; intros. @@ -1035,8 +1100,8 @@ Qed. End RESTORE_CALLEE_SAVE. Lemma restore_int_callee_save_correct: - forall sp k fr m ls0 ls rs, - agree ls rs fr (parent_frame stack) ls0 -> + forall sp k fr m ls0 ls rs cs, + agree ls ls0 rs fr cs -> exists ls', exists rs', star step tge (State stack tf sp @@ -1044,11 +1109,13 @@ Lemma restore_int_callee_save_correct: E0 (State stack tf sp k rs' fr m) /\ (forall r, In r int_callee_save_regs -> rs' r = ls0 (R r)) /\ (forall r, ~(In r int_callee_save_regs) -> rs' r = rs r) - /\ agree ls' rs' fr (parent_frame stack) ls0. + /\ agree ls' ls0 rs' fr cs. Proof. intros. unfold restore_callee_save_int. apply restore_callee_save_regs_correct with int_callee_save_regs ls. intros; simpl. split; auto. generalize (index_int_callee_save_pos r H0). omega. + intros; congruence. + intros; congruence. auto. intros. unfold mreg_within_bounds. rewrite (int_callee_save_type r H0). tauto. @@ -1059,8 +1126,8 @@ Proof. Qed. Lemma restore_float_callee_save_correct: - forall sp k fr m ls0 ls rs, - agree ls rs fr (parent_frame stack) ls0 -> + forall sp k fr m ls0 ls rs cs, + agree ls ls0 rs fr cs -> exists ls', exists rs', star step tge (State stack tf sp @@ -1068,11 +1135,13 @@ Lemma restore_float_callee_save_correct: E0 (State stack tf sp k rs' fr m) /\ (forall r, In r float_callee_save_regs -> rs' r = ls0 (R r)) /\ (forall r, ~(In r float_callee_save_regs) -> rs' r = rs r) - /\ agree ls' rs' fr (parent_frame stack) ls0. + /\ agree ls' ls0 rs' fr cs. Proof. intros. unfold restore_callee_save_float. apply restore_callee_save_regs_correct with float_callee_save_regs ls. intros; simpl. split; auto. generalize (index_float_callee_save_pos r H0). omega. + intros; congruence. + intros; congruence. auto. intros. unfold mreg_within_bounds. rewrite (float_callee_save_type r H0). tauto. @@ -1083,8 +1152,8 @@ Proof. Qed. Lemma restore_callee_save_correct: - forall sp k fr m ls0 ls rs, - agree ls rs fr (parent_frame stack) ls0 -> + forall sp k fr m ls0 ls rs cs, + agree ls ls0 rs fr cs -> exists rs', star step tge (State stack tf sp (restore_callee_save fe k) rs fr m) @@ -1235,15 +1304,15 @@ Proof. Qed. Lemma find_function_translated: - forall f0 ls rs fr parent ls0 ros f, - agree f0 ls rs fr parent ls0 -> + forall f0 tf0 ls ls0 rs fr cs ros f, + agree f0 tf0 ls ls0 rs fr cs -> Linear.find_function ge ros ls = Some f -> exists tf, find_function tge ros rs = Some tf /\ transf_fundef f = OK tf. Proof. intros until f; intro AG. destruct ros; simpl. - rewrite (agree_eval_reg _ _ _ _ _ _ m AG). intro. + rewrite (agree_eval_reg _ _ _ _ _ _ _ m AG). intro. apply functions_translated; auto. rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try congruence. intro. apply function_ptr_translated; auto. @@ -1321,42 +1390,40 @@ Qed. Section EXTERNAL_ARGUMENTS. +Variable f: function. Variable ls: locset. Variable fr: frame. Variable rs: regset. Variable sg: signature. Hypothesis AG1: forall r, rs r = ls (R r). Hypothesis AG2: forall (ofs : Z) (ty : typ), - 14 <= ofs -> - ofs + typesize ty <= size_arguments sg -> - get_slot fr ty (Int.signed (Int.repr (4 * ofs))) - (ls (S (Outgoing ofs ty))). + In (S (Outgoing ofs ty)) (loc_arguments sg) -> + get_slot f fr ty (Int.signed (Int.repr (4 * ofs))) + (ls (S (Outgoing ofs ty))). Lemma transl_external_arguments_rec: forall locs, - (forall l, In l locs -> loc_argument_acceptable l) -> - (forall ofs ty, In (S (Outgoing ofs ty)) locs -> - ofs + typesize ty <= size_arguments sg) -> - extcall_args rs fr locs ls##locs. + incl locs (loc_arguments sg) -> + extcall_args f rs fr locs ls##locs. Proof. induction locs; simpl; intros. constructor. constructor. - assert (loc_argument_acceptable a). apply H; auto. - destruct a; red in H1. + assert (loc_argument_acceptable a). + apply loc_arguments_acceptable with sg; auto with coqlib. + destruct a; red in H0. rewrite <- AG1. constructor. destruct s; try contradiction. - constructor. apply AG2. omega. apply H0. auto. - apply IHlocs; auto. + constructor. apply AG2. auto with coqlib. + apply IHlocs; eauto with coqlib. Qed. Lemma transl_external_arguments: - extcall_arguments rs fr sg (ls ## (loc_arguments sg)). + extcall_arguments f rs fr sg (ls ## (loc_arguments sg)). Proof. unfold extcall_arguments. - apply transl_external_arguments_rec. - exact (Conventions.loc_arguments_acceptable sg). - exact (Conventions.loc_arguments_bounded sg). + apply transl_external_arguments_rec. + auto with coqlib. Qed. End EXTERNAL_ARGUMENTS. @@ -1390,7 +1457,7 @@ Inductive match_stacks: list Linear.stackframe -> list Machabstr.stackframe -> P match_stacks s ts -> transf_function f = OK tf -> wt_function f -> - agree_frame f ls fr (parent_frame ts) (parent_locset s) -> + agree_frame f tf ls (parent_locset s) fr ts -> incl c (Linear.fn_code f) -> match_stacks (Linear.Stackframe f sp ls c :: s) @@ -1402,7 +1469,7 @@ Inductive match_states: Linear.state -> Machabstr.state -> Prop := (STACKS: match_stacks s ts) (TRANSL: transf_function f = OK tf) (WTF: wt_function f) - (AG: agree f ls rs fr (parent_frame ts) (parent_locset s)) + (AG: agree f tf ls (parent_locset s) rs fr ts) (INCL: incl c (Linear.fn_code f)), match_states (Linear.State s f sp c ls m) (Machabstr.State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) c) rs fr m) @@ -1413,9 +1480,8 @@ Inductive match_states: Linear.state -> Machabstr.state -> Prop := (WTF: wt_fundef f) (AG1: forall r, rs r = ls (R r)) (AG2: forall ofs ty, - 14 <= ofs -> - ofs + typesize ty <= size_arguments (Linear.funsig f) -> - get_slot (parent_frame ts) ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Outgoing ofs ty)))) + In (S (Outgoing ofs ty)) (loc_arguments (Linear.funsig f)) -> + get_slot (parent_function ts) (parent_frame ts) ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Outgoing ofs ty)))) (AG3: agree_callee_save ls (parent_locset s)), match_states (Linear.Callstate s f ls m) (Machabstr.Callstate ts tf rs m) @@ -1450,17 +1516,15 @@ Proof. (rs0#r <- (rs (S sl))) fr m). split. destruct sl. (* Lgetstack, local *) - apply plus_one. eapply exec_Mgetstack'; eauto. - apply get_slot_index. apply index_local_valid. auto. - eapply agree_size; eauto. reflexivity. + apply plus_one. apply exec_Mgetstack. + apply get_slot_index. auto. apply index_local_valid. auto. congruence. congruence. auto. eapply agree_locals; eauto. (* Lgetstack, incoming *) apply plus_one; apply exec_Mgetparam. unfold offset_of_index. eapply agree_incoming; eauto. (* Lgetstack, outgoing *) - apply plus_one; apply exec_Mgetstack'; eauto. - apply get_slot_index. apply index_arg_valid. auto. - eapply agree_size; eauto. reflexivity. + apply plus_one; apply exec_Mgetstack. + apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto. eapply agree_outgoing; eauto. (* Lgetstack, common *) econstructor; eauto with coqlib. @@ -1470,20 +1534,20 @@ Proof. inv WTI. destruct sl. (* Lsetstack, local *) - generalize (agree_set_local _ _ _ _ _ _ (rs0 r) _ _ AG BOUND). + generalize (agree_set_local _ _ TRANSL _ _ _ _ _ (rs0 r) _ _ AG BOUND). intros [fr' [SET AG']]. econstructor; split. - apply plus_one. eapply exec_Msetstack'; eauto. + apply plus_one. eapply exec_Msetstack; eauto. econstructor; eauto with coqlib. replace (rs (R r)) with (rs0 r). auto. symmetry. eapply agree_reg; eauto. (* Lsetstack, incoming *) contradiction. (* Lsetstack, outgoing *) - generalize (agree_set_outgoing _ _ _ _ _ _ (rs0 r) _ _ AG BOUND). + generalize (agree_set_outgoing _ _ TRANSL _ _ _ _ _ (rs0 r) _ _ AG BOUND). intros [fr' [SET AG']]. econstructor; split. - apply plus_one. eapply exec_Msetstack'; eauto. + apply plus_one. eapply exec_Msetstack; eauto. econstructor; eauto with coqlib. replace (rs (R r)) with (rs0 r). auto. symmetry. eapply agree_reg; eauto. @@ -1493,7 +1557,7 @@ Proof. apply plus_one. apply exec_Mop. apply shift_eval_operation. auto. change mreg with RegEq.t. - rewrite (agree_eval_regs _ _ _ _ _ _ args AG). auto. + rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). auto. econstructor; eauto with coqlib. apply agree_set_reg; auto. @@ -1502,7 +1566,7 @@ Proof. apply plus_one; eapply exec_Mload; eauto. apply shift_eval_addressing; auto. change mreg with RegEq.t. - rewrite (agree_eval_regs _ _ _ _ _ _ args AG). eauto. + rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eauto. econstructor; eauto with coqlib. apply agree_set_reg; auto. @@ -1511,8 +1575,8 @@ Proof. apply plus_one; eapply exec_Mstore; eauto. apply shift_eval_addressing; eauto. change mreg with RegEq.t. - rewrite (agree_eval_regs _ _ _ _ _ _ args AG). eauto. - rewrite (agree_eval_reg _ _ _ _ _ _ src AG). eauto. + rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eauto. + rewrite (agree_eval_reg _ _ _ _ _ _ _ src AG). eauto. econstructor; eauto with coqlib. (* Lcall *) @@ -1525,24 +1589,24 @@ Proof. econstructor; eauto with coqlib. exists rs0; auto. intro. symmetry. eapply agree_reg; eauto. - intros. + intros. unfold parent_function, parent_frame. assert (slot_within_bounds f (function_bounds f) (Outgoing ofs ty)). - red. simpl. omega. + red. simpl. generalize (loc_arguments_bounded _ _ _ H0). + generalize (loc_arguments_acceptable _ _ H0). unfold loc_argument_acceptable. + omega. change (4 * ofs) with (offset_of_index (make_env (function_bounds f)) (FI_arg ofs ty)). - rewrite (offset_of_index_no_overflow f tf); auto. - apply get_slot_index. apply index_arg_valid. auto. - eapply agree_size; eauto. reflexivity. + apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto. eapply agree_outgoing; eauto. simpl. red; auto. (* Ltailcall *) assert (WTF': wt_fundef f'). eapply find_function_well_typed; eauto. - generalize (find_function_translated _ _ _ _ _ _ _ _ AG H). + exploit find_function_translated; eauto. intros [tf' [FIND' TRANSL']]. generalize (restore_callee_save_correct ts _ _ TRANSL (shift_sp tf (Vptr stk Int.zero)) (Mtailcall (Linear.funsig f') ros :: transl_code (make_env (function_bounds f)) b) - _ m _ _ _ AG). + _ m _ _ _ _ AG). intros [rs2 [A [B C]]]. assert (FIND'': find_function tge ros rs2 = Some tf'). rewrite <- FIND'. destruct ros; simpl; auto. @@ -1553,15 +1617,14 @@ Proof. simpl shift_sp. eapply exec_Mtailcall; eauto. traceEq. econstructor; eauto. intros; symmetry; eapply agree_return_regs; eauto. - intros. inv WTI. rewrite tailcall_possible_size in H4. - rewrite H4 in H1. elimtype False. generalize (typesize_pos ty). omega. + intros. inv WTI. generalize (H3 _ H0). tauto. apply agree_callee_save_return_regs. (* Lalloc *) exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) (rs0#loc_alloc_result <- (Vptr blk Int.zero)) fr m'); split. apply plus_one; eapply exec_Malloc; eauto. - rewrite (agree_eval_reg _ _ _ _ _ _ loc_alloc_argument AG). auto. + rewrite (agree_eval_reg _ _ _ _ _ _ _ loc_alloc_argument AG). auto. econstructor; eauto with coqlib. apply agree_set_reg; auto. red. simpl. generalize (max_over_regs_of_funct_pos f int_callee_save). omega. @@ -1581,7 +1644,7 @@ Proof. (* Lcond, true *) econstructor; split. apply plus_one; apply exec_Mcond_true. - rewrite <- (agree_eval_regs _ _ _ _ _ _ args AG) in H; eauto. + rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; eauto. apply transl_find_label; eauto. econstructor; eauto. eapply find_label_incl; eauto. @@ -1589,7 +1652,7 @@ Proof. (* Lcond, false *) econstructor; split. apply plus_one; apply exec_Mcond_false. - rewrite <- (agree_eval_regs _ _ _ _ _ _ args AG) in H; auto. + rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; auto. econstructor; eauto with coqlib. (* Lreturn *) @@ -1611,15 +1674,6 @@ Proof. set (sp := Vptr stk Int.zero) in *. set (tsp := shift_sp tfn sp). set (fe := make_env (function_bounds f)). - assert (fr_low (init_frame tfn) = - fe.(fe_size)). - simpl fr_low. rewrite (unfold_transf_function _ _ TRANSL). - reflexivity. - assert (UNDEF: forall idx, index_valid f idx -> index_val f idx (init_frame tfn) = Vundef). - intros. - assert (get_slot (init_frame tfn) (type_of_index idx) (offset_of_index fe idx) Vundef). - generalize (offset_of_index_valid _ _ H1). fold fe. intros [XX YY]. - apply slot_gi; auto. omega. - inv H2; auto. exploit save_callee_save_correct; eauto. intros [fr [EXP AG]]. econstructor; split. @@ -1671,10 +1725,7 @@ Proof. rewrite (Genv.init_mem_transf_partial _ _ TRANSF). econstructor; eauto. constructor. eapply Genv.find_funct_ptr_prop; eauto. - intros. - replace (size_arguments (Linear.funsig f)) with 14 in H5. - elimtype False. generalize (typesize_pos ty). omega. - rewrite H2; auto. + intros. rewrite H2 in H4. simpl in H4. contradiction. simpl; red; auto. Qed. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index aa534ff0..f3fe24f2 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -205,18 +205,33 @@ Proof. case (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))); intro. intros; discriminate. intro EQ. generalize (unfold_transf_function f tf H); intro. - assert (fn_framesize tf = fe_size (make_env (function_bounds f))). + set (b := function_bounds f) in *. + set (fe := make_env b) in *. + assert (fn_framesize tf = fe_size fe). subst tf; reflexivity. + assert (Int.signed tf.(fn_link_ofs) = offset_of_index fe FI_link). + rewrite H1; unfold fn_link_ofs. + change (fe_ofs_link fe) with (offset_of_index fe FI_link). + unfold fe, b; eapply offset_of_index_no_overflow. eauto. red; auto. + assert (Int.signed tf.(fn_retaddr_ofs) = offset_of_index fe FI_retaddr). + rewrite H1; unfold fn_retaddr_ofs. + change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr). + unfold fe, b; eapply offset_of_index_no_overflow. eauto. red; auto. constructor. change (wt_instrs (fn_code tf)). rewrite H1; simpl; unfold transl_body. - apply wt_save_callee_save; auto. + 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 H3. + red; intros. elim H5. subst tf; simpl; auto. - rewrite H2. eapply size_pos; eauto. - rewrite H2. eapply size_no_overflow; eauto. + rewrite H2. generalize (size_pos f). fold b; fold fe; omega. + rewrite H3; rewrite H2. change 4 with (4 * typesize (type_of_index FI_link)). + unfold fe, b; apply offset_of_index_valid. red; auto. + rewrite H4; rewrite H2. change 4 with (4 * typesize (type_of_index FI_retaddr)). + unfold fe, b; apply offset_of_index_valid. red; auto. + rewrite H3; rewrite H4. + apply (offset_of_index_disj f FI_retaddr FI_link); red; auto. Qed. Lemma wt_transf_fundef: -- cgit