From a74f6b45d72834b5b8417297017bd81424123d98 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 7 Mar 2010 15:52:58 +0000 Subject: Merge of the newmem and newextcalls branches: - Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Tailcallproof.v | 280 +++++++++++++----------------------------------- 1 file changed, 77 insertions(+), 203 deletions(-) (limited to 'backend/Tailcallproof.v') diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 8681d84a..0ca4c028 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -17,7 +17,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Op. Require Import Events. Require Import Globalenvs. @@ -227,66 +227,6 @@ Proof. apply regset_set. auto. auto. Qed. -(** ** Agreement between the size of a stack block and a function *) - -(** To reason over deallocation of empty stack blocks, we need to - maintain the invariant that the bounds of a stack block - for function [f] are always [0, f.(fn_stacksize)]. *) - -Inductive match_stacksize: function -> block -> mem -> Z -> Prop := - | match_stacksize_intro: forall f sp m bound, - sp < bound -> - low_bound m sp = 0 -> - high_bound m sp = f.(fn_stacksize) -> - match_stacksize f sp m bound. - -Lemma match_stacksize_store: - forall m m' chunk b ofs v f sp bound, - store chunk m b ofs v = Some m' -> - match_stacksize f sp m bound -> - match_stacksize f sp m' bound. -Proof. - intros. inv H0. constructor. auto. - rewrite <- H2. eapply Mem.low_bound_store; eauto. - rewrite <- H3. eapply Mem.high_bound_store; eauto. -Qed. - -Lemma match_stacksize_alloc_other: - forall m m' lo hi b f sp bound, - alloc m lo hi = (m', b) -> - match_stacksize f sp m bound -> - bound <= m.(nextblock) -> - match_stacksize f sp m' bound. -Proof. - intros. inv H0. - assert (valid_block m sp). red. omega. - constructor. auto. - rewrite <- H3. eapply low_bound_alloc_other; eauto. - rewrite <- H4. eapply high_bound_alloc_other; eauto. -Qed. - -Lemma match_stacksize_alloc_same: - forall m f m' sp, - alloc m 0 f.(fn_stacksize) = (m', sp) -> - match_stacksize f sp m' m'.(nextblock). -Proof. - intros. constructor. - unfold alloc in H. inv H. simpl. omega. - eapply low_bound_alloc_same; eauto. - eapply high_bound_alloc_same; eauto. -Qed. - -Lemma match_stacksize_free: - forall f sp m b bound, - match_stacksize f sp m bound -> - bound <= b -> - match_stacksize f sp (free m b) bound. -Proof. - intros. inv H. constructor. auto. - rewrite <- H2. apply low_bound_free. unfold block; omega. - rewrite <- H3. apply high_bound_free. unfold block; omega. -Qed. - (** * Proof of semantic preservation *) Section PRESERVATION. @@ -319,6 +259,13 @@ Proof. destruct (zeq (fn_stacksize f) 0); auto. Qed. +Lemma stacksize_preserved: + forall f, fn_stacksize (transf_function f) = fn_stacksize f. +Proof. + unfold transf_function. intros. + destruct (zeq (fn_stacksize f) 0); auto. +Qed. + Lemma find_function_translated: forall ros rs rs' f, find_function ge ros rs = Some f -> @@ -370,131 +317,58 @@ We first define the simulation invariant between call stacks. The first two cases are standard, but the third case corresponds to a frame that was eliminated by the transformation. *) -Inductive match_stackframes: mem -> Z -> list stackframe -> list stackframe -> Prop := - | match_stackframes_nil: forall m bound, - match_stackframes m bound nil nil - | match_stackframes_normal: forall m bound stk stk' res sp pc rs rs' f, - match_stackframes m sp stk stk' -> - match_stacksize f sp m bound -> +Inductive match_stackframes: list stackframe -> list stackframe -> Prop := + | match_stackframes_nil: + match_stackframes nil nil + | match_stackframes_normal: forall stk stk' res sp pc rs rs' f, + match_stackframes stk stk' -> regset_lessdef rs rs' -> - match_stackframes m bound - (Stackframe res f.(fn_code) (Vptr sp Int.zero) pc rs :: stk) - (Stackframe res (transf_function f).(fn_code) (Vptr sp Int.zero) pc rs' :: stk') - | match_stackframes_tail: forall m bound stk stk' res sp pc rs f, - match_stackframes m sp stk stk' -> - match_stacksize f sp m bound -> + match_stackframes + (Stackframe res f (Vptr sp Int.zero) pc rs :: stk) + (Stackframe res (transf_function f) (Vptr sp Int.zero) pc rs' :: stk') + | match_stackframes_tail: forall stk stk' res sp pc rs f, + match_stackframes stk stk' -> is_return_spec f pc res -> f.(fn_stacksize) = 0 -> - match_stackframes m bound - (Stackframe res f.(fn_code) (Vptr sp Int.zero) pc rs :: stk) + match_stackframes + (Stackframe res f (Vptr sp Int.zero) pc rs :: stk) stk'. -(** In [match_stackframes m bound s s'], the memory state [m] is used - to check that the sizes of the stack blocks agree with what was - declared by the corresponding functions. The [bound] parameter - is used to enforce separation between the stack blocks. *) - -Lemma match_stackframes_incr: - forall m bound s s' bound', - match_stackframes m bound s s' -> - bound <= bound' -> - match_stackframes m bound' s s'. -Proof. - intros. inv H; econstructor; eauto. - inv H2. constructor; auto. omega. - inv H2. constructor; auto. omega. -Qed. - -Lemma match_stackframes_store: - forall m bound s s', - match_stackframes m bound s s' -> - forall chunk b ofs v m', - store chunk m b ofs v = Some m' -> - match_stackframes m' bound s s'. -Proof. - induction 1; intros. - constructor. - econstructor; eauto. eapply match_stacksize_store; eauto. - econstructor; eauto. eapply match_stacksize_store; eauto. -Qed. - -Lemma match_stackframes_alloc: - forall m lo hi m' sp s s', - match_stackframes m (nextblock m) s s' -> - alloc m lo hi = (m', sp) -> - match_stackframes m' sp s s'. -Proof. - intros. - assert (forall bound s s', - match_stackframes m bound s s' -> - bound <= m.(nextblock) -> - match_stackframes m' bound s s'). - induction 1; intros. constructor. - constructor; auto. apply IHmatch_stackframes; auto. inv H2. omega. - eapply match_stacksize_alloc_other; eauto. - econstructor; eauto. apply IHmatch_stackframes; auto. inv H2. omega. - eapply match_stacksize_alloc_other; eauto. - exploit alloc_result; eauto. intro. rewrite H2. - eapply H1; eauto. omega. -Qed. - -Lemma match_stackframes_free: - forall f sp m s s', - match_stacksize f sp m (nextblock m) -> - match_stackframes m sp s s' -> - match_stackframes (free m sp) (nextblock (free m sp)) s s'. -Proof. - intros. simpl. - assert (forall bound s s', - match_stackframes m bound s s' -> - bound <= sp -> - match_stackframes (free m sp) bound s s'). - induction 1; intros. constructor. - constructor; auto. apply IHmatch_stackframes; auto. inv H2; omega. - apply match_stacksize_free; auto. - econstructor; eauto. apply IHmatch_stackframes; auto. inv H2; omega. - apply match_stacksize_free; auto. - - apply match_stackframes_incr with sp. apply H1; auto. omega. - inv H. omega. -Qed. - (** Here is the invariant relating two states. The first three cases are standard. Note the ``less defined than'' conditions - over values, register states, and memory states. *) + over values and register states, and the corresponding ``extends'' + relation over memory states. *) Inductive match_states: state -> state -> Prop := | match_states_normal: forall s sp pc rs m s' rs' m' f - (STKSZ: match_stacksize f sp m m.(nextblock)) - (STACKS: match_stackframes m sp s s') + (STACKS: match_stackframes s s') (RLD: regset_lessdef rs rs') - (MLD: Mem.lessdef m m'), - match_states (State s f.(fn_code) (Vptr sp Int.zero) pc rs m) - (State s' (transf_function f).(fn_code) (Vptr sp Int.zero) pc rs' m') + (MLD: Mem.extends m m'), + match_states (State s f (Vptr sp Int.zero) pc rs m) + (State s' (transf_function f) (Vptr sp Int.zero) pc rs' m') | match_states_call: forall s f args m s' args' m', - match_stackframes m m.(nextblock) s s' -> + match_stackframes s s' -> Val.lessdef_list args args' -> - Mem.lessdef m m' -> + Mem.extends m m' -> match_states (Callstate s f args m) (Callstate s' (transf_fundef f) args' m') | match_states_return: forall s v m s' v' m', - match_stackframes m m.(nextblock) s s' -> + match_stackframes s s' -> Val.lessdef v v' -> - Mem.lessdef m m' -> + Mem.extends m m' -> match_states (Returnstate s v m) (Returnstate s' v' m') | match_states_interm: forall s sp pc rs m s' m' f r v' - (STKSZ: match_stacksize f sp m m.(nextblock)) - (STACKS: match_stackframes m sp s s') - (MLD: Mem.lessdef m m'), + (STACKS: match_stackframes s s') + (MLD: Mem.extends m m'), is_return_spec f pc r -> f.(fn_stacksize) = 0 -> Val.lessdef (rs#r) v' -> - match_states (State s f.(fn_code) (Vptr sp Int.zero) pc rs m) + match_states (State s f (Vptr sp Int.zero) pc rs m) (Returnstate s' v' m'). (** The last case of [match_states] corresponds to the execution @@ -516,7 +390,7 @@ Inductive match_states: state -> state -> Prop := Definition measure (st: state) : nat := match st with - | State s c sp pc rs m => (List.length s * (niter + 2) + return_measure c pc + 1)%nat + | State s f sp pc rs m => (List.length s * (niter + 2) + return_measure f.(fn_code) pc + 1)%nat | Callstate s f args m => 0%nat | Returnstate s v m => (List.length s * (niter + 2))%nat end. @@ -557,7 +431,7 @@ Proof. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. exploit eval_operation_lessdef; eauto. intros [v' [EVAL' VLD]]. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'); split. eapply exec_Iop; eauto. rewrite <- EVAL'. apply eval_operation_preserved. exact symbols_preserved. econstructor; eauto. apply regset_set; auto. @@ -571,9 +445,9 @@ Proof. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. exploit eval_addressing_lessdef; eauto. intros [a' [ADDR' ALD]]. - exploit loadv_lessdef; eauto. + exploit Mem.loadv_extends; eauto. intros [v' [LOAD' VLD]]. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split. eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'. apply eval_addressing_preserved. exact symbols_preserved. eauto. econstructor; eauto. apply regset_set; auto. @@ -583,88 +457,91 @@ Proof. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. exploit eval_addressing_lessdef; eauto. intros [a' [ADDR' ALD]]. - exploit storev_lessdef. 4: eexact H1. eauto. eauto. apply RLD. + exploit Mem.storev_extends. 2: eexact H1. eauto. eauto. apply RLD. intros [m'1 [STORE' MLD']]. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'1); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' rs' m'1); split. eapply exec_Istore with (a := a'). eauto. rewrite <- ADDR'. apply eval_addressing_preserved. exact symbols_preserved. eauto. destruct a; simpl in H1; try discriminate. econstructor; eauto. - eapply match_stacksize_store; eauto. - rewrite (nextblock_store _ _ _ _ _ _ H1). auto. - eapply match_stackframes_store; eauto. (* call *) exploit find_function_translated; eauto. intro FIND'. TransfInstr. (* call turned tailcall *) - left. exists (Callstate s' (transf_fundef f) (rs'##args) (Mem.free m' sp0)); split. + assert ({ m'' | Mem.free m' sp0 0 (fn_stacksize (transf_function f)) = Some m''}). + apply Mem.range_perm_free. rewrite stacksize_preserved. rewrite H7. + red; intros; omegaContradiction. + destruct X as [m'' FREE]. + left. exists (Callstate s' (transf_fundef fd) (rs'##args) m''); split. eapply exec_Itailcall; eauto. apply sig_preserved. constructor. eapply match_stackframes_tail; eauto. apply regset_get_list; auto. - apply Mem.free_right_lessdef; auto. inv STKSZ. omega. + eapply Mem.free_right_extends; eauto. + rewrite stacksize_preserved. rewrite H7. intros. omegaContradiction. (* call that remains a call *) - left. exists (Callstate (Stackframe res (fn_code (transf_function f0)) (Vptr sp0 Int.zero) pc' rs' :: s') - (transf_fundef f) (rs'##args) m'); split. + left. exists (Callstate (Stackframe res (transf_function f) (Vptr sp0 Int.zero) pc' rs' :: s') + (transf_fundef fd) (rs'##args) m'); split. eapply exec_Icall; eauto. apply sig_preserved. constructor. constructor; auto. apply regset_get_list; auto. auto. (* tailcall *) - exploit find_function_translated; eauto. intro FIND'. + exploit find_function_translated; eauto. intro FIND'. + exploit Mem.free_parallel_extends; eauto. intros [m'1 [FREE EXT]]. TransfInstr. - left. exists (Callstate s' (transf_fundef f) (rs'##args) (Mem.free m' stk)); split. - eapply exec_Itailcall; eauto. apply sig_preserved. - constructor. eapply match_stackframes_free; eauto. - apply regset_get_list; auto. apply Mem.free_lessdef; auto. + left. exists (Callstate s' (transf_fundef fd) (rs'##args) m'1); split. + eapply exec_Itailcall; eauto. apply sig_preserved. + rewrite stacksize_preserved; auto. + constructor. auto. apply regset_get_list; auto. auto. (* cond true *) TransfInstr. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) ifso rs' m'); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifso rs' m'); split. eapply exec_Icond_true; eauto. apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto. constructor; auto. (* cond false *) TransfInstr. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) ifnot rs' m'); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifnot rs' m'); split. eapply exec_Icond_false; eauto. apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto. constructor; auto. (* jumptable *) TransfInstr. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' rs' m'); split. eapply exec_Ijumptable; eauto. generalize (RLD arg). rewrite H0. intro. inv H2. auto. constructor; auto. (* return *) + exploit Mem.free_parallel_extends; eauto. intros [m'1 [FREE EXT]]. TransfInstr. - left. exists (Returnstate s' (regmap_optget or Vundef rs') (free m' stk)); split. - apply exec_Ireturn; auto. - constructor. - eapply match_stackframes_free; eauto. + left. exists (Returnstate s' (regmap_optget or Vundef rs') m'1); split. + apply exec_Ireturn; auto. rewrite stacksize_preserved; auto. + constructor. auto. destruct or; simpl. apply RLD. constructor. - apply Mem.free_lessdef; auto. + auto. (* eliminated return None *) assert (or = None) by congruence. subst or. right. split. simpl. omega. split. auto. - constructor. - eapply match_stackframes_free; eauto. + constructor. auto. simpl. constructor. - apply Mem.free_left_lessdef; auto. + eapply Mem.free_left_extends; eauto. (* eliminated return Some *) assert (or = Some r) by congruence. subst or. right. split. simpl. omega. split. auto. - constructor. - eapply match_stackframes_free; eauto. + constructor. auto. simpl. auto. - apply Mem.free_left_lessdef; auto. + eapply Mem.free_left_extends; eauto. (* internal call *) - caseEq (alloc m'0 0 (fn_stacksize f)). intros m'1 stk' ALLOC'. - exploit alloc_lessdef; eauto. intros [EQ1 LD']. subst stk'. + exploit Mem.alloc_extends; eauto. + instantiate (1 := 0). omega. + instantiate (1 := fn_stacksize f). omega. + intros [m'1 [ALLOC EXT]]. assert (fn_stacksize (transf_function f) = fn_stacksize f /\ fn_entrypoint (transf_function f) = fn_entrypoint f /\ fn_params (transf_function f) = fn_params f). @@ -673,13 +550,12 @@ Proof. left. econstructor; split. simpl. eapply exec_function_internal; eauto. rewrite EQ1; eauto. rewrite EQ2. rewrite EQ3. constructor; auto. - eapply match_stacksize_alloc_same; eauto. - eapply match_stackframes_alloc; eauto. apply regset_init_regs. auto. (* external call *) - exploit event_match_lessdef; eauto. intros [res' [EVM' VLD']]. - left. exists (Returnstate s' res' m'); split. + exploit external_call_mem_extends; eauto. + intros [res' [m2' [A [B [C D]]]]]. + left. exists (Returnstate s' res' m2'); split. simpl. econstructor; eauto. constructor; auto. @@ -705,15 +581,13 @@ Lemma transf_initial_states: Proof. intros. inv H. exploit funct_ptr_translated; eauto. intro FIND. - exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. - econstructor; eauto. + exists (Callstate nil (transf_fundef f) nil m0); split. + econstructor; eauto. apply Genv.init_mem_transf. auto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. reflexivity. - rewrite <- H2. apply sig_preserved. - replace (Genv.init_mem tprog) with (Genv.init_mem prog). - constructor. constructor. constructor. apply lessdef_refl. - symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. + rewrite <- H3. apply sig_preserved. + constructor. constructor. constructor. apply Mem.extends_refl. Qed. Lemma transf_final_states: -- cgit