From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 6 + cfrontend/Cminorgenproof.v | 266 +++++++++++++++++++----------------------- cfrontend/Initializersproof.v | 4 +- 3 files changed, 126 insertions(+), 150 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 508c414..0d29a23 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -956,3 +956,9 @@ let atom_is_small_data a ofs = (Hashtbl.find decl_atom a).a_small_data with Not_found -> false + +let atom_is_inline a = + try + (Hashtbl.find decl_atom a).a_inline + with Not_found -> + false diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 1a66ec9..f94e081 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -150,10 +150,10 @@ Proof. Qed. Lemma perm_freelist: - forall fbl m m' b ofs p, + forall fbl m m' b ofs k p, Mem.free_list m fbl = Some m' -> - Mem.perm m' b ofs p -> - Mem.perm m b ofs p. + Mem.perm m' b ofs k p -> + Mem.perm m b ofs k p. Proof. induction fbl; simpl; intros until p. congruence. @@ -177,7 +177,7 @@ Lemma free_list_freeable: forall l m m', Mem.free_list m l = Some m' -> forall b lo hi, - In (b, lo, hi) l -> Mem.range_perm m b lo hi Freeable. + In (b, lo, hi) l -> Mem.range_perm m b lo hi Cur Freeable. Proof. induction l; simpl; intros. contradiction. @@ -189,18 +189,6 @@ Proof. red; intros. eapply Mem.perm_free_3; eauto. exploit IHl; eauto. Qed. -Lemma bounds_freelist: - forall b l m m', - Mem.free_list m l = Some m' -> Mem.bounds m' b = Mem.bounds m b. -Proof. - induction l; simpl; intros. - inv H; auto. - revert H. destruct a as [[b' lo'] hi']. - caseEq (Mem.free m b' lo' hi'); try congruence. - intros m1 FREE1 FREE2. - transitivity (Mem.bounds m1 b). eauto. eapply Mem.bounds_free; eauto. -Qed. - Lemma nextblock_storev: forall chunk m addr v m', Mem.storev chunk m addr v = Some m' -> Mem.nextblock m' = Mem.nextblock m. @@ -324,8 +312,8 @@ Record match_env (f: meminj) (cenv: compilenv) (** The sizes of blocks appearing in [e] agree with their types *) me_bounds: - forall id b lv, - PTree.get id e = Some(b, lv) -> Mem.bounds m b = (0, sizeof lv) + forall id b lv ofs p, + PTree.get id e = Some(b, lv) -> Mem.perm m b ofs Max p -> 0 <= ofs < sizeof lv }. Hint Resolve me_low_high. @@ -351,7 +339,7 @@ Proof. rewrite <- H4. eapply Mem.load_store_other; eauto. left. congruence. (* bounds *) - intros. rewrite (Mem.bounds_store _ _ _ _ _ _ H0). eauto. + intros. eauto with mem. Qed. (** Preservation by assignment to a Csharpminor variable that is @@ -403,7 +391,7 @@ Proof. (* temps *) intros. rewrite PTree.gso. auto. unfold for_temp, for_var; congruence. (* bounds *) - intros. rewrite (Mem.bounds_store _ _ _ _ _ _ H2). eauto. + intros. eauto with mem. Qed. (** Preservation by assignment to a Csharpminor temporary and the @@ -442,16 +430,14 @@ Lemma match_env_invariant: (forall b ofs chunk v, lo <= b < hi -> Mem.load chunk m1 b ofs = Some v -> Mem.load chunk m2 b ofs = Some v) -> - (forall b, - lo <= b < hi -> Mem.bounds m2 b = Mem.bounds m1 b) -> + (forall b ofs p, + lo <= b < hi -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> match_env f cenv e le m1 te sp lo hi -> match_env f cenv e le m2 te sp lo hi. Proof. intros. inv H1. constructor; eauto. (* vars *) intros. geninv (me_vars0 id); econstructor; eauto. - (* bounds *) - intros. rewrite H0. eauto. eauto. Qed. (** [match_env] is insensitive to the Cminor values of stack-allocated data. *) @@ -551,10 +537,10 @@ Proof. exploit Mem.alloc_result; eauto. unfold block; omega. (* bounds *) intros. rewrite PTree.gsspec in H. - rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). + exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. destruct (peq id0 id). - inv H. apply dec_eq_true. - rewrite dec_eq_false. eauto. + inv H. rewrite zeq_true. auto. + rewrite zeq_false. eauto. apply Mem.valid_not_valid_diff with m1. exploit me_bounded0; eauto. intros [A B]. auto. eauto with mem. @@ -599,7 +585,8 @@ Proof. intros. eapply me_incr0; eauto. rewrite <- OTHER; eauto. exploit Mem.alloc_result; eauto. unfold block in *; omega. (* bounds *) - intros. rewrite (Mem.bounds_alloc_other _ _ _ _ _ ALLOC). eauto. + intros. exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. + rewrite zeq_false. eauto. exploit me_bounded0; eauto. Qed. @@ -634,7 +621,7 @@ Lemma match_env_external_call: mem_unchanged_on (loc_unmapped f1) m1 m2 -> inject_incr f1 f2 -> inject_separated f1 f2 m1 m1' -> - (forall b, Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b) -> + (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> hi <= Mem.nextblock m1 -> sp < Mem.nextblock m1' -> match_env f2 cenv e le m2 te sp lo hi. Proof. @@ -661,7 +648,7 @@ Proof. instantiate (1 := b). red; omega. intros. apply me_incr0 with b delta. congruence. auto. (* bounds *) - intros. rewrite BOUNDS; eauto. + intros. eapply me_bounds0; eauto. eapply BOUNDS; eauto. red. exploit me_bounded0; eauto. omega. Qed. @@ -704,13 +691,12 @@ Inductive match_globalenvs (f: meminj) (bound: Z): Prop := that are not images of C#minor local variable blocks. *) -Definition padding_freeable (f: meminj) (m: mem) (tm: mem) (sp: block) (sz: Z) : Prop := +Definition padding_freeable (f: meminj) (e: Csharpminor.env) (tm: mem) (sp: block) (sz: Z) : Prop := forall ofs, 0 <= ofs < sz -> - Mem.perm tm sp ofs Freeable - \/ exists b, exists delta, - f b = Some(sp, delta) - /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta. + Mem.perm tm sp ofs Cur Freeable + \/ exists id, exists b, exists lv, exists delta, + e!id = Some(b, lv) /\ f b = Some(sp, delta) /\ delta <= ofs < delta + sizeof lv. Inductive match_callstack (f: meminj) (m: mem) (tm: mem): callstack -> Z -> Z -> Prop := @@ -724,7 +710,7 @@ Inductive match_callstack (f: meminj) (m: mem) (tm: mem): (BOUND: hi <= bound) (TBOUND: sp < tbound) (MENV: match_env f cenv e le m te sp lo hi) - (PERM: padding_freeable f m tm sp tf.(fn_stackspace)) + (PERM: padding_freeable f e tm sp tf.(fn_stackspace)) (MCS: match_callstack f m tm cs lo sp), match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) bound tbound. @@ -742,22 +728,20 @@ Qed. generalize those for [match_env]. *) Lemma padding_freeable_invariant: - forall f1 m1 tm1 sp sz cenv e le te lo hi f2 m2 tm2, - padding_freeable f1 m1 tm1 sp sz -> + forall f1 m1 tm1 sp sz cenv e le te lo hi f2 tm2, + padding_freeable f1 e tm1 sp sz -> match_env f1 cenv e le m1 te sp lo hi -> - (forall ofs, Mem.perm tm1 sp ofs Freeable -> Mem.perm tm2 sp ofs Freeable) -> - (forall b, b < hi -> Mem.bounds m2 b = Mem.bounds m1 b) -> + (forall ofs, Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) -> (forall b, b < hi -> f2 b = f1 b) -> - padding_freeable f2 m2 tm2 sp sz. + padding_freeable f2 e tm2 sp sz. Proof. intros; red; intros. - exploit H; eauto. intros [A | [b [delta [A B]]]]. + exploit H; eauto. intros [A | [id [b [lv [delta [A [B C]]]]]]]. left; auto. - exploit me_inv; eauto. intros [id [lv C]]. - exploit me_bounded; eauto. intros [D E]. - right; exists b; exists delta. split. - rewrite H3; auto. - rewrite H2; auto. + exploit me_bounded; eauto. intros [D E]. + right; exists id; exists b; exists lv; exists delta; split. + auto. + rewrite H2; auto. Qed. Lemma match_callstack_store_mapped: @@ -775,7 +759,6 @@ Proof. eapply match_env_store_mapped; eauto. congruence. eapply padding_freeable_invariant; eauto. intros; eauto with mem. - intros. eapply Mem.bounds_store; eauto. Qed. Lemma match_callstack_storev_mapped: @@ -800,21 +783,17 @@ Lemma match_callstack_invariant: hi <= bound -> match_env f cenv e le m te sp lo hi -> match_env f cenv e le m' te sp lo hi) -> - (forall b, - b < bound -> Mem.bounds m' b = Mem.bounds m b) -> - (forall b ofs p, - b < tbound -> Mem.perm tm b ofs p -> Mem.perm tm' b ofs p) -> + (forall b ofs k p, + b < tbound -> Mem.perm tm b ofs k p -> Mem.perm tm' b ofs k p) -> match_callstack f m' tm' cs bound tbound. Proof. induction 1; intros. econstructor; eauto. constructor; auto. - eapply padding_freeable_invariant; eauto. - intros. apply H1. omega. + eapply padding_freeable_invariant; eauto. eapply IHmatch_callstack; eauto. intros. eapply H0; eauto. inv MENV; omega. intros. apply H1; auto. inv MENV; omega. - intros. apply H2; auto. omega. Qed. Lemma match_callstack_store_local: @@ -828,14 +807,11 @@ Lemma match_callstack_store_local: Proof. intros. inv H3. constructor; auto. eapply match_env_store_local; eauto. - eapply padding_freeable_invariant; eauto. - intros. eapply Mem.bounds_store; eauto. eapply match_callstack_invariant; eauto. intros. apply match_env_invariant with m1; auto. intros. rewrite <- H6. eapply Mem.load_store_other; eauto. - left. inv MENV. exploit me_bounded0; eauto. unfold block in *; omega. - intros. eapply Mem.bounds_store; eauto. - intros. eapply Mem.bounds_store; eauto. + left. inv MENV. exploit me_bounded0; eauto. unfold block in *; omega. + intros. eauto with mem. Qed. (** A variant of [match_callstack_store_local] where the Cminor environment @@ -923,11 +899,9 @@ Proof. assert ({tm' | Mem.free tm sp 0 (fn_stackspace tf) = Some tm'}). apply Mem.range_perm_free. red; intros. - exploit PERM; eauto. intros [A | [b [delta [A B]]]]. + exploit PERM; eauto. intros [A | [id [b [lv [delta [A [B C]]]]]]]. auto. - exploit me_inv0; eauto. intros [id [lv C]]. - exploit me_bounds0; eauto. intro D. rewrite D in B; simpl in B. - assert (Mem.range_perm m b 0 (sizeof lv) Freeable). + assert (Mem.range_perm m b 0 (sizeof lv) Cur Freeable). eapply free_list_freeable; eauto. eapply in_blocks_of_env; eauto. replace ofs with ((ofs - delta) + delta) by omega. eapply Mem.perm_inject; eauto. apply H0. omega. @@ -943,15 +917,13 @@ Proof. intros. exploit in_blocks_of_env_inv; eauto. intros [id [lv [A [B C]]]]. exploit me_bounded0; eauto. unfold block; omega. - intros. eapply bounds_freelist; eauto. - intros. eapply bounds_freelist; eauto. + intros. eapply perm_freelist; eauto. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. eapply Mem.free_inject; eauto. intros. exploit me_inv0; eauto. intros [id [lv A]]. exists 0; exists (sizeof lv); split. eapply in_blocks_of_env; eauto. - exploit me_bounds0; eauto. intro B. - exploit Mem.perm_in_bounds; eauto. rewrite B; simpl. auto. + eapply me_bounds0; eauto. eapply Mem.perm_max. eauto. Qed. (** Preservation of [match_callstack] by allocations. *) @@ -975,7 +947,6 @@ Proof. constructor; auto. eapply match_env_alloc_other; eauto. omega. destruct (f2 b); auto. destruct p; omega. eapply padding_freeable_invariant; eauto. - intros. eapply Mem.bounds_alloc_other; eauto. unfold block; omega. intros. apply H1. unfold block; omega. apply IHmatch_callstack. inv MENV; omega. @@ -1004,9 +975,12 @@ Proof. constructor. omega. auto. eapply match_env_alloc_same; eauto. - eapply padding_freeable_invariant; eauto. - intros. eapply Mem.bounds_alloc_other; eauto. unfold block in *; omega. - intros. apply OTHER. unfold block in *; omega. + red; intros. exploit PERM; eauto. intros [A | [id' [b' [lv' [delta' [A [B C]]]]]]]. + left; auto. + right; exists id'; exists b'; exists lv'; exists delta'. + split. rewrite PTree.gso; auto. congruence. + split. apply INCR; auto. + auto. eapply match_callstack_alloc_below; eauto. inv MENV. unfold block in *; omega. inv ACOND. auto. omega. omega. @@ -1059,43 +1033,42 @@ Qed. (** Decidability of the predicate "this is not a padding location" *) -Definition is_reachable (f: meminj) (m: mem) (sp: block) (ofs: Z) : Prop := - exists b, exists delta, - f b = Some(sp, delta) - /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta. +Definition is_reachable (f: meminj) (e: Csharpminor.env) (sp: block) (ofs: Z) : Prop := + exists id, exists b, exists lv, exists delta, + e!id = Some(b, lv) /\ f b = Some(sp, delta) /\ delta <= ofs < delta + sizeof lv. Lemma is_reachable_dec: - forall f cenv e le m te sp lo hi ofs, - match_env f cenv e le m te sp lo hi -> - {is_reachable f m sp ofs} + {~is_reachable f m sp ofs}. + forall f e sp ofs, is_reachable f e sp ofs \/ ~is_reachable f e sp ofs. Proof. - intros. - set (P := fun (b: block) => - match f b with - | None => False - | Some(b', delta) => - b' = sp /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta - end). - assert ({forall b, Intv.In b (lo, hi) -> ~P b} + {exists b, Intv.In b (lo, hi) /\ P b}). - apply Intv.forall_dec. intro b. unfold P. - destruct (f b) as [[b' delta] | ]. - destruct (eq_block b' sp). - destruct (zle (Mem.low_bound m b + delta) ofs). - destruct (zlt ofs (Mem.high_bound m b + delta)). - right; auto. - left; intuition. - left; intuition. - left; intuition. - left; intuition. - inv H. destruct H0. - right; red; intros [b [delta [A [B C]]]]. - elim (n b). - exploit me_inv0; eauto. intros [id [lv D]]. exploit me_bounded0; eauto. - red. rewrite A. auto. - left. destruct e0 as [b [A B]]. red in B; revert B. - case_eq (f b). intros [b' delta] EQ [C [D E]]. subst b'. - exists b; exists delta. auto. - tauto. + intros. + set (pred := fun id_b_lv : ident * (block * var_kind) => + match id_b_lv with + | (id, (b, lv)) => + match f b with + | None => false + | Some(sp', delta) => + if eq_block sp sp' + then zle delta ofs && zlt ofs (delta + sizeof lv) + else false + end + end). + destruct (List.existsb pred (PTree.elements e)) as []_eqn. + rewrite List.existsb_exists in Heqb. + destruct Heqb as [[id [b lv]] [A B]]. + simpl in B. destruct (f b) as [[sp' delta] |]_eqn; try discriminate. + destruct (eq_block sp sp'); try discriminate. + destruct (andb_prop _ _ B). + left; red. exists id; exists b; exists lv; exists delta. + split. apply PTree.elements_complete; auto. + split. congruence. + split; eapply proj_sumbool_true; eauto. + right; red. intros [id [b [lv [delta [A [B C]]]]]]. + assert (existsb pred (PTree.elements e) = true). + rewrite List.existsb_exists. exists (id, (b, lv)); split. + apply PTree.elements_correct; auto. + simpl. rewrite B. rewrite dec_eq_true. + unfold proj_sumbool. destruct C. rewrite zle_true; auto. rewrite zlt_true; auto. + congruence. Qed. (** Preservation of [match_callstack] by external calls. *) @@ -1106,14 +1079,14 @@ Lemma match_callstack_external_call: mem_unchanged_on (loc_out_of_reach f1 m1) m1' m2' -> inject_incr f1 f2 -> inject_separated f1 f2 m1 m1' -> - (forall b, Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b) -> + (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> forall cs bound tbound, match_callstack f1 m1 m1' cs bound tbound -> bound <= Mem.nextblock m1 -> tbound <= Mem.nextblock m1' -> match_callstack f2 m2 m2' cs bound tbound. Proof. intros until m2'. - intros UNMAPPED OUTOFREACH INCR SEPARATED BOUNDS. + intros UNMAPPED OUTOFREACH INCR SEPARATED MAXPERMS. destruct OUTOFREACH as [OUTOFREACH1 OUTOFREACH2]. induction 1; intros. (* base case *) @@ -1127,18 +1100,16 @@ Proof. eapply match_env_external_call; eauto. omega. omega. (* padding-freeable *) red; intros. - destruct (is_reachable_dec _ _ _ _ _ _ _ _ _ ofs MENV). - destruct i as [b [delta [A B]]]. - right; exists b; exists delta; split. - apply INCR; auto. rewrite BOUNDS. auto. - exploit me_inv; eauto. intros [id [lv C]]. - exploit me_bounded; eauto. intros. red; omega. + destruct (is_reachable_dec f1 e sp ofs). + destruct H3 as [id [b [lv [delta [A [B C]]]]]]. + right; exists id; exists b; exists lv; exists delta. + split. auto. split. apply INCR; auto. auto. exploit PERM; eauto. intros [A|A]; try contradiction. left. - apply OUTOFREACH1; auto. red; intros. - assert ((ofs < Mem.low_bound m1 b0 + delta \/ ofs >= Mem.high_bound m1 b0 + delta) - \/ Mem.low_bound m1 b0 + delta <= ofs < Mem.high_bound m1 b0 + delta) - by omega. destruct H4; auto. - elim n. exists b0; exists delta; auto. + apply OUTOFREACH1; auto. red; intros. + red; intros; elim H3. + exploit me_inv; eauto. intros [id [lv B]]. + exploit me_bounds; eauto. intros C. + red. exists id; exists b0; exists lv; exists delta. intuition omega. (* induction *) eapply IHmatch_callstack; eauto. inv MENV; omega. omega. Qed. @@ -2091,7 +2062,7 @@ Proof. split. auto. split. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. - intros. eapply external_call_bounds; eauto. + intros. eapply external_call_max_perm; eauto. omega. omega. eapply external_call_nextblock_incr; eauto. eapply external_call_nextblock_incr; eauto. @@ -2189,8 +2160,9 @@ Lemma match_callstack_alloc_variable: forall atk id lv cenv sz cenv' sz' tm sp e tf m m' b te le lo cs f tv, assign_variable atk (id, lv) (cenv, sz) = (cenv', sz') -> Mem.valid_block tm sp -> - Mem.bounds tm sp = (0, tf.(fn_stackspace)) -> - Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable -> + (forall ofs k p, + Mem.perm tm sp ofs k p -> 0 <= ofs < tf.(fn_stackspace)) -> + Mem.range_perm tm sp 0 tf.(fn_stackspace) Cur Freeable -> tf.(fn_stackspace) <= Int.max_unsigned -> Mem.alloc m 0 (sizeof lv) = (m', b) -> match_callstack f m tm @@ -2198,7 +2170,8 @@ Lemma match_callstack_alloc_variable: (Mem.nextblock m) (Mem.nextblock tm) -> Mem.inject f m tm -> 0 <= sz -> sz' <= tf.(fn_stackspace) -> - (forall b delta, f b = Some(sp, delta) -> Mem.high_bound m b + delta <= sz) -> + (forall b delta ofs k p, + f b = Some(sp, delta) -> Mem.perm m b ofs k p -> ofs + delta < sz) -> e!id = None -> te!(for_var id) = Some tv -> exists f', @@ -2207,8 +2180,8 @@ Lemma match_callstack_alloc_variable: /\ match_callstack f' m' tm (Frame cenv' tf (PTree.set id (b, lv) e) le te sp lo (Mem.nextblock m') :: cs) (Mem.nextblock m') (Mem.nextblock tm) - /\ (forall b delta, - f' b = Some(sp, delta) -> Mem.high_bound m' b + delta <= sz'). + /\ (forall b delta ofs k p, + f' b = Some(sp, delta) -> Mem.perm m' b ofs k p -> ofs + delta < sz'). Proof. intros until tv. intros ASV VALID BOUNDS PERMS NOOV ALLOC MCS INJ LO HI RANGE E TE. generalize ASV. unfold assign_variable. @@ -2222,23 +2195,22 @@ Proof. generalize (align_le sz (size_chunk chunk) SIZEPOS). fold ofs. intro SZOFS. exploit Mem.alloc_left_mapped_inject. eauto. eauto. eauto. - instantiate (1 := ofs). omega. - right; rewrite BOUNDS; simpl. omega. - intros. apply Mem.perm_implies with Freeable; auto with mem. + instantiate (1 := ofs). omega. + intros. exploit BOUNDS; eauto. omega. + intros. apply Mem.perm_implies with Freeable; auto with mem. apply Mem.perm_cur. apply PERMS. rewrite LV in H1. simpl in H1. omega. rewrite LV; simpl. rewrite Zminus_0_r. unfold ofs. apply inj_offset_aligned_var. - intros. generalize (RANGE _ _ H1). omega. + intros. generalize (RANGE _ _ _ _ _ H1 H2). omega. intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]]. exists f1; split. auto. split. auto. split. eapply match_callstack_alloc_left; eauto. rewrite <- LV; auto. rewrite SAME; constructor. - intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). - destruct (eq_block b0 b); simpl. + intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b0 b). subst b0. assert (delta = ofs) by congruence. subst delta. rewrite LV. simpl. omega. - rewrite OTHER in H1; eauto. generalize (RANGE _ _ H1). omega. + intro. rewrite OTHER in H1; eauto. generalize (RANGE _ _ _ _ _ H1 H3). omega. (* 1.2 info = Var_local chunk *) intro EQ; injection EQ; intros; clear EQ. subst sz'. rewrite <- H0. exploit Mem.alloc_left_unmapped_inject; eauto. @@ -2247,8 +2219,7 @@ Proof. eapply match_callstack_alloc_left; eauto. rewrite <- LV; auto. rewrite SAME; constructor. - intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). - destruct (eq_block b0 b); simpl. + intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b0 b). subst b0. congruence. rewrite OTHER in H; eauto. (* 2 info = Var_stack_array ofs *) @@ -2259,29 +2230,29 @@ Proof. exploit Mem.alloc_left_mapped_inject. eauto. eauto. eauto. instantiate (1 := ofs). generalize Int.min_signed_neg. omega. - right; rewrite BOUNDS; simpl. generalize Int.min_signed_neg. omega. - intros. apply Mem.perm_implies with Freeable; auto with mem. + intros. exploit BOUNDS; eauto. generalize Int.min_signed_neg. omega. + intros. apply Mem.perm_implies with Freeable; auto with mem. apply Mem.perm_cur. apply PERMS. rewrite LV in H3. simpl in H3. omega. rewrite LV; simpl. rewrite Zminus_0_r. unfold ofs. apply inj_offset_aligned_array'. - intros. generalize (RANGE _ _ H3). omega. + intros. generalize (RANGE _ _ _ _ _ H3 H4). omega. intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]]. exists f1; split. auto. split. auto. split. subst cenv'. eapply match_callstack_alloc_left; eauto. rewrite <- LV; auto. rewrite SAME; constructor. - intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). - destruct (eq_block b0 b); simpl. + intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b0 b). subst b0. assert (delta = ofs) by congruence. subst delta. rewrite LV. simpl. omega. - rewrite OTHER in H3; eauto. generalize (RANGE _ _ H3). omega. + intro. rewrite OTHER in H3; eauto. generalize (RANGE _ _ _ _ _ H3 H5). omega. Qed. Lemma match_callstack_alloc_variables_rec: forall tm sp cenv' tf le te lo cs atk, Mem.valid_block tm sp -> - Mem.bounds tm sp = (0, tf.(fn_stackspace)) -> - Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable -> + (forall ofs k p, + Mem.perm tm sp ofs k p -> 0 <= ofs < tf.(fn_stackspace)) -> + Mem.range_perm tm sp 0 tf.(fn_stackspace) Cur Freeable -> tf.(fn_stackspace) <= Int.max_unsigned -> forall e m vars e' m', alloc_variables e m vars e' m' -> @@ -2292,8 +2263,8 @@ Lemma match_callstack_alloc_variables_rec: (Mem.nextblock m) (Mem.nextblock tm) -> Mem.inject f m tm -> 0 <= sz -> - (forall b delta, - f b = Some(sp, delta) -> Mem.high_bound m b + delta <= sz) -> + (forall b delta ofs k p, + f b = Some(sp, delta) -> Mem.perm m b ofs k p -> ofs + delta < sz) -> (forall id lv, In (id, lv) vars -> te!(for_var id) <> None) -> list_norepet (List.map (@fst ident var_kind) vars) -> (forall id lv, In (id, lv) vars -> e!id = None) -> @@ -2395,8 +2366,7 @@ Proof. intros. unfold build_compilenv in H. eapply match_callstack_alloc_variables_rec; eauto with mem. - eapply Mem.bounds_alloc_same; eauto. - red; intros; eauto with mem. + red; intros. eapply Mem.perm_alloc_2; eauto. eapply match_callstack_alloc_right; eauto. eapply Mem.alloc_right_inject; eauto. omega. intros. elim (Mem.valid_not_valid_diff tm sp sp); eauto with mem. @@ -3257,7 +3227,7 @@ Proof. (Mem.nextblock m') (Mem.nextblock tm')). apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. - intros. eapply external_call_bounds; eauto. + intros. eapply external_call_max_perm; eauto. omega. omega. eapply external_call_nextblock_incr; eauto. eapply external_call_nextblock_incr; eauto. @@ -3414,7 +3384,7 @@ Opaque PTree.set. econstructor; eauto. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. - intros. eapply external_call_bounds; eauto. + intros. eapply external_call_max_perm; eauto. omega. omega. eapply external_call_nextblock_incr; eauto. eapply external_call_nextblock_incr; eauto. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 627db89..37f15cf 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -327,8 +327,8 @@ Qed. Lemma mem_empty_not_valid_pointer: forall b ofs, Mem.valid_pointer Mem.empty b ofs = false. Proof. - intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Nonempty); auto. - red in p. simpl in p. contradiction. + intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Cur Nonempty); auto. + eelim Mem.perm_empty; eauto. Qed. Lemma sem_cmp_match: -- cgit v1.2.3