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 --- backend/Stackingproof.v | 79 +++++++++++++++++++++++++++---------------------- 1 file changed, 43 insertions(+), 36 deletions(-) (limited to 'backend/Stackingproof.v') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 2ec14aa6..be5e4b97 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -423,13 +423,13 @@ Definition frame_perm_freeable (m: mem) (sp: block): Prop := forall ofs, 0 <= ofs < fe.(fe_size) -> ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> - Mem.perm m sp ofs Freeable. + Mem.perm m sp ofs Cur Freeable. Lemma offset_of_index_perm: forall m sp idx, index_valid idx -> frame_perm_freeable m sp -> - Mem.range_perm m sp (offset_of_index fe idx) (offset_of_index fe idx + AST.typesize (type_of_index idx)) Freeable. + Mem.range_perm m sp (offset_of_index fe idx) (offset_of_index fe idx + AST.typesize (type_of_index idx)) Cur Freeable. Proof. intros. exploit offset_of_index_valid; eauto. intros [A B]. @@ -612,7 +612,7 @@ Record agree_frame (j: meminj) (ls ls0: locset) (** Bounds of the Linear stack data block *) agree_bounds: - Mem.bounds m sp = (0, f.(Linear.fn_stacksize)); + forall ofs p, Mem.perm m sp ofs Max p -> 0 <= ofs < f.(Linear.fn_stacksize); (** Permissions on the frame part of the Mach stack block *) agree_perm: @@ -928,16 +928,16 @@ Lemma agree_frame_invariant: forall j ls ls0 m sp m' sp' parent retaddr m1 m1', agree_frame j ls ls0 m sp m' sp' parent retaddr -> (Mem.valid_block m sp -> Mem.valid_block m1 sp) -> - (Mem.bounds m1 sp = Mem.bounds m sp) -> + (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') -> (forall chunk ofs v, ofs + size_chunk chunk <= fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> Mem.load chunk m' sp' ofs = Some v -> Mem.load chunk m1' sp' ofs = Some v) -> - (forall ofs p, + (forall ofs k p, ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> - Mem.perm m' sp' ofs p -> Mem.perm m1' sp' ofs p) -> + Mem.perm m' sp' ofs k p -> Mem.perm m1' sp' ofs k p) -> agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. Proof. intros. @@ -950,7 +950,7 @@ Proof. index_contains_inj j m' sp' idx v -> index_contains_inj j m1' sp' idx v). intros. destruct H5 as [v' [A B]]. exists v'; split; auto. inv H; constructor; auto; intros. - rewrite H1; auto. + eauto. red; intros. apply H4; auto. Qed. @@ -960,7 +960,7 @@ Lemma agree_frame_extcall_invariant: forall j ls ls0 m sp m' sp' parent retaddr m1 m1', agree_frame j ls ls0 m sp m' sp' parent retaddr -> (Mem.valid_block m sp -> Mem.valid_block m1 sp) -> - (Mem.bounds m1 sp = Mem.bounds m sp) -> + (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') -> mem_unchanged_on (loc_out_of_reach j m) m' m1' -> agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. @@ -970,7 +970,7 @@ Proof. ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> loc_out_of_reach j m sp' ofs). intros; red; intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst. - rewrite (agree_bounds _ _ _ _ _ _ _ _ _ H). unfold fst, snd. omega. + red; intros. exploit agree_bounds; eauto. omega. eapply agree_frame_invariant; eauto. intros. apply H3. intros. apply REACH. omega. auto. intros. apply H3; auto. @@ -992,17 +992,23 @@ Opaque Int.add. inv VINJ; simpl in *; try discriminate. eapply agree_frame_invariant; eauto. eauto with mem. - eapply Mem.bounds_store; eauto. + eauto with mem. eauto with mem. intros. rewrite <- H1. eapply Mem.load_store_other; eauto. destruct (zeq sp' b2); auto. subst b2. right. exploit agree_inj_unique; eauto. intros [P Q]. subst b1 delta. exploit Mem.store_valid_access_3. eexact STORE1. intros [A B]. - exploit Mem.range_perm_in_bounds. eexact A. generalize (size_chunk_pos chunk); omega. - rewrite (agree_bounds _ _ _ _ _ _ _ _ _ AG). unfold fst,snd. intros [C D]. - rewrite shifted_stack_offset_no_overflow. omega. - generalize (size_chunk_pos chunk); omega. + rewrite shifted_stack_offset_no_overflow. + exploit agree_bounds. eauto. apply Mem.perm_cur_max. apply A. + instantiate (1 := Int.unsigned ofs1). generalize (size_chunk_pos chunk). omega. + intros C. + exploit agree_bounds. eauto. apply Mem.perm_cur_max. apply A. + instantiate (1 := Int.unsigned ofs1 + size_chunk chunk - 1). generalize (size_chunk_pos chunk). omega. + intros D. + omega. + eapply agree_bounds. eauto. apply Mem.perm_cur_max. apply A. + generalize (size_chunk_pos chunk). omega. intros; eauto with mem. Qed. @@ -1325,7 +1331,7 @@ Qed. Lemma stores_in_frame_inject: forall j sp sp' m, (forall b delta, j b = Some(sp', delta) -> b = sp /\ delta = fe.(fe_stack_data)) -> - Mem.bounds m sp = (0, f.(Linear.fn_stacksize)) -> + (forall ofs k p, Mem.perm m sp ofs k p -> 0 <= ofs < f.(Linear.fn_stacksize)) -> forall m1 m2, stores_in_frame sp' m1 m2 -> Mem.inject j m m1 -> Mem.inject j m m2. Proof. induction 3; intros. @@ -1333,7 +1339,7 @@ Proof. apply IHstores_in_frame. intros. eapply Mem.store_outside_inject; eauto. intros. exploit H; eauto. intros [A B]; subst. - rewrite H0; unfold fst, snd. omega. + exploit H0; eauto. omega. Qed. Lemma stores_in_frame_valid: @@ -1343,7 +1349,7 @@ Proof. Qed. Lemma stores_in_frame_perm: - forall b ofs p sp m m', stores_in_frame sp m m' -> Mem.perm m b ofs p -> Mem.perm m' b ofs p. + forall b ofs k p sp m m', stores_in_frame sp m m' -> Mem.perm m b ofs k p -> Mem.perm m' b ofs k p. Proof. induction 1; intros. auto. apply IHstores_in_frame. eauto with mem. Qed. @@ -1396,8 +1402,9 @@ Proof. instantiate (1 := sp'). eauto with mem. instantiate (1 := fe_stack_data fe). generalize stack_data_offset_valid (bound_stack_data_pos b) size_no_overflow; omega. - right. rewrite (Mem.bounds_alloc_same _ _ _ _ _ ALLOC'). unfold fst, snd. - split. omega. apply size_no_overflow. + intros; right. + exploit Mem.perm_alloc_inv. eexact ALLOC'. eauto. rewrite zeq_true. + generalize size_no_overflow. omega. intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. generalize stack_data_offset_valid bound_stack_data_stacksize; omega. @@ -1495,7 +1502,7 @@ Proof. (* valid sp' *) eapply stores_in_frame_valid with (m := m2'); eauto with mem. (* bounds *) - eapply Mem.bounds_alloc_same; eauto. + exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto. (* perms *) auto. (* wt *) @@ -1506,7 +1513,7 @@ Proof. split. eapply inject_alloc_separated; eauto with mem. (* inject *) split. eapply stores_in_frame_inject; eauto. - eapply Mem.bounds_alloc_same; eauto. + intros. exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto. (* stores in frame *) auto. Qed. @@ -1690,8 +1697,7 @@ Proof. simpl. rewrite H2. auto. intros. exploit agree_inj_unique; eauto. intros [P Q]; subst b1 delta. exists 0; exists (Linear.fn_stacksize f); split. auto with coqlib. - exploit Mem.perm_in_bounds; eauto. - rewrite (agree_bounds _ _ _ _ _ _ _ _ _ H0). auto. + eapply agree_bounds. eauto. eapply Mem.perm_max. eauto. (* can execute epilogue *) exploit restore_callee_save_correct; eauto. instantiate (1 := rs). red; intros. @@ -1775,7 +1781,7 @@ Lemma match_stacks_change_linear_mem: forall j m1 m2 m' cs cs' sg bound bound', match_stacks j m1 m' cs cs' sg bound bound' -> (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) -> - (forall b, b < bound -> Mem.bounds m2 b = Mem.bounds m1 b) -> + (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> match_stacks j m2 m' cs cs' sg bound bound'. Proof. induction 1; intros. @@ -1784,7 +1790,7 @@ Proof. eapply agree_frame_invariant; eauto. apply IHmatch_stacks. intros. apply H0; auto. omega. - intros. apply H1. omega. + intros. apply H1. omega. auto. Qed. (** Invariance with respect to change of [m']. *) @@ -1793,7 +1799,7 @@ Lemma match_stacks_change_mach_mem: forall j m m1' m2' cs cs' sg bound bound', match_stacks j m m1' cs cs' sg bound bound' -> (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) -> - (forall b ofs p, b < bound' -> Mem.perm m1' b ofs p -> Mem.perm m2' b ofs p) -> + (forall b ofs k p, b < bound' -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) -> (forall chunk b ofs v, b < bound' -> Mem.load chunk m1' b ofs = Some v -> Mem.load chunk m2' b ofs = Some v) -> match_stacks j m m2' cs cs' sg bound bound'. Proof. @@ -1813,7 +1819,7 @@ Lemma match_stacks_change_mem_extcall: forall j m1 m2 m1' m2' cs cs' sg bound bound', match_stacks j m1 m1' cs cs' sg bound bound' -> (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) -> - (forall b, b < bound -> Mem.bounds m2 b = Mem.bounds m1 b) -> + (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) -> mem_unchanged_on (loc_out_of_reach j m1) m1' m2' -> match_stacks j m2 m2' cs cs' sg bound bound'. @@ -1824,7 +1830,7 @@ Proof. eapply agree_frame_extcall_invariant; eauto. apply IHmatch_stacks. intros; apply H0; auto; omega. - intros; apply H1; omega. + intros; apply H1. omega. auto. intros; apply H2; auto; omega. auto. Qed. @@ -1888,7 +1894,7 @@ Proof. eapply match_stacks_change_meminj; eauto. eapply match_stacks_change_mem_extcall; eauto. intros; eapply external_call_valid_block; eauto. - intros; eapply external_call_bounds; eauto. red; omega. + intros; eapply external_call_max_perm; eauto. red; omega. intros; eapply external_call_valid_block; eauto. Qed. @@ -2435,9 +2441,9 @@ Proof. econstructor; eauto with coqlib. eapply Mem.store_outside_inject; eauto. intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta. - rewrite (agree_bounds _ _ _ _ _ _ _ _ _ _ AGFRAME). unfold fst, snd. rewrite Zplus_0_l. - rewrite size_type_chunk. + rewrite size_type_chunk in H5. exploit offset_of_index_disj_stack_data_2; eauto. + exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. omega. apply match_stacks_change_mach_mem with m'; auto. eauto with mem. eauto with mem. intros. rewrite <- H4; eapply Mem.load_store_other; eauto. left; unfold block; omega. @@ -2546,7 +2552,7 @@ Proof. auto. eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. intros. rewrite <- H2. eapply Mem.load_free; eauto. left; unfold block; omega. - eauto with mem. intros. eapply Mem.bounds_free; eauto. + eauto with mem. intros. eapply Mem.perm_free_3; eauto. apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. eapply find_function_well_typed; eauto. @@ -2570,7 +2576,7 @@ Proof. eapply agree_frame_inject_incr; eauto. apply agree_frame_extcall_invariant with m m'0; auto. eapply external_call_valid_block; eauto. - eapply external_call_bounds; eauto. eapply agree_valid_linear; eauto. + intros. eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto. eapply external_call_valid_block; eauto. eapply agree_valid_mach; eauto. inv WTI. simpl; rewrite H4. eapply external_call_well_typed; eauto. @@ -2594,7 +2600,7 @@ Proof. eapply agree_frame_inject_incr; eauto. apply agree_frame_extcall_invariant with m m'0; auto. eapply external_call_valid_block; eauto. - eapply external_call_bounds; eauto. eapply agree_valid_linear; eauto. + intros. eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto. eapply external_call_valid_block; eauto. eapply agree_valid_mach; eauto. @@ -2652,7 +2658,7 @@ Proof. eauto. eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. intros. rewrite <- H1. eapply Mem.load_free; eauto. left; unfold block; omega. - eauto with mem. intros. eapply Mem.bounds_free; eauto. + eauto with mem. intros. eapply Mem.perm_free_3; eauto. apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto. @@ -2677,7 +2683,8 @@ Proof. apply match_stacks_change_linear_mem with m. rewrite SP_EQ; rewrite SP'_EQ. eapply match_stacks_change_meminj; eauto. omega. - eauto with mem. intros. eapply Mem.bounds_alloc_other; eauto. unfold block; omega. + eauto with mem. intros. exploit Mem.perm_alloc_inv. eexact H. eauto. + rewrite zeq_false. auto. omega. intros. eapply stores_in_frame_valid; eauto with mem. intros. eapply stores_in_frame_perm; eauto with mem. intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto. -- cgit