diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-21 07:34:06 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-21 07:34:06 +0000 |
commit | f7270a57205abd7314203eaef9b752a7abd13ed7 (patch) | |
tree | 21e31e9608e4af96125a0f4f8afa0e0c96859030 /common/Globalenvs.v | |
parent | 30fbbdb86d2a2989062a9c82dc770a923fb19643 (diff) | |
download | compcert-f7270a57205abd7314203eaef9b752a7abd13ed7.tar.gz compcert-f7270a57205abd7314203eaef9b752a7abd13ed7.zip |
Memory.v: added drop_perm operation
Globalenvs.v: used drop_perm to set appropriate permissions on global variables
(Notempty if volatile; Readable if readonly; Writable otherwise)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1510 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Globalenvs.v')
-rw-r--r-- | common/Globalenvs.v | 86 |
1 files changed, 62 insertions, 24 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index a29c2496..4a57a375 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -523,10 +523,18 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := | i :: il' => init_data_size i + init_data_list_size il' end. +Definition perm_globvar (gv: globvar V) : permission := + if gv.(gvar_volatile) then Nonempty + else if gv.(gvar_readonly) then Readable + else Writable. + Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem := let init := idv#2.(gvar_init) in let (m', b) := Mem.alloc m 0 (init_data_list_size init) in - store_init_data_list m' b 0 init. + match store_init_data_list m' b 0 init with + | None => None + | Some m'' => Mem.drop_perm m'' b 0 (init_data_list_size init) (perm_globvar idv#2) + end. Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V)) {struct vl} : option mem := @@ -564,8 +572,11 @@ Proof. unfold alloc_variable. set (init := gvar_init a#2). caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE REC. - rewrite (IHvl _ _ REC). + caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE. + caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. + intros m3 DROP REC. + rewrite (IHvl _ _ REC). + rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). rewrite (store_init_data_list_nextblock _ _ _ _ STORE). rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega. @@ -595,8 +606,12 @@ Proof. intros until m'. simpl. unfold alloc_variable. set (init := gvar_init a#2). caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE REC PERM. - eapply IHvl; eauto. + caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE. + caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. + intros m3 DROP REC PERM. + assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem. + eapply IHvl; eauto. + eapply Mem.perm_drop_3; eauto. eapply store_init_data_list_perm; eauto. eauto with mem. Qed. @@ -685,13 +700,19 @@ Proof. unfold alloc_variable. set (init := gvar_init a#2). caseEq (Mem.alloc m 0 (init_data_list_size init)); intros m1 b1 ALLOC. - caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO REC VAL. + caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO. + caseEq (Mem.drop_perm m2 b1 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. + intros m3 DROP RED VALID. + assert (b <> b1). apply Mem.valid_not_valid_diff with m; eauto with mem. + transitivity (Mem.load chunk m3 b p). + apply IHvl; auto. red. + rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). + rewrite (store_init_data_list_nextblock _ _ _ _ STO). + change (Mem.valid_block m1 b). eauto with mem. transitivity (Mem.load chunk m2 b p). - apply IHvl; auto. red. rewrite (store_init_data_list_nextblock _ _ _ _ STO). - change (Mem.valid_block m1 b). eauto with mem. + eapply Mem.load_drop; eauto. transitivity (Mem.load chunk m1 b p). - eapply store_init_data_list_outside; eauto. left. - apply Mem.valid_not_valid_diff with m; eauto with mem. + eapply store_init_data_list_outside; eauto. eapply Mem.load_alloc_unchanged; eauto. Qed. @@ -714,8 +735,8 @@ Lemma alloc_variables_charact: In (id, gv) vl -> exists b, find_symbol (add_variables g vl) id = Some b /\ find_var_info (add_variables g vl) b = Some gv - /\ Mem.range_perm m' b 0 (init_data_list_size gv.(gvar_init)) Writable - /\ load_store_init_data m' b 0 gv.(gvar_init). + /\ Mem.range_perm m' b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv) + /\ (gv.(gvar_volatile) = false -> load_store_init_data m' b 0 gv.(gvar_init)). Proof. induction vl; simpl. contradiction. @@ -724,7 +745,9 @@ Proof. caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init gv'))); try congruence. intros m1 b ALLOC. caseEq (store_init_data_list m1 b 0 (gvar_init gv')); try congruence. - intros m2 STORE REC NOREPET IN. inv NOREPET. + intros m2 STORE. + caseEq (Mem.drop_perm m2 b 0 (init_data_list_size (gvar_init gv')) (perm_globvar gv')); try congruence. + intros m3 DROP REC NOREPET IN. inv NOREPET. exploit Mem.alloc_result; eauto. intro BEQ. destruct IN. inv H. exists (Mem.nextblock m); split. @@ -733,17 +756,24 @@ Proof. split. rewrite add_variables_same_address. unfold find_var_info; simpl. rewrite NEXT. apply ZMap.gss. simpl. rewrite <- NEXT; omega. - split. red; intros. eapply alloc_variables_perm; eauto. - eapply store_init_data_list_perm; eauto. - apply Mem.perm_implies with Freeable; eauto with mem. + split. red; intros. + eapply alloc_variables_perm; eauto. + eapply Mem.perm_drop_1; eauto. + intros NOVOL. apply load_store_init_data_invariant with m2. - intros. eapply load_alloc_variables; eauto. - red. rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + intros. transitivity (Mem.load chunk m3 (Mem.nextblock m) ofs). + eapply load_alloc_variables; eauto. + red. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). + rewrite (store_init_data_list_nextblock _ _ _ _ STORE). change (Mem.valid_block m1 (Mem.nextblock m)). eauto with mem. + eapply Mem.load_drop; eauto. repeat right. + unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv); auto with mem. eapply store_init_data_list_charact; eauto. - apply IHvl with m2; auto. - simpl. rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + apply IHvl with m3; auto. + simpl. + rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). + rewrite (store_init_data_list_nextblock _ _ _ _ STORE). rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega. Qed. @@ -785,8 +815,8 @@ Theorem find_var_exists: init_mem p = Some m -> exists b, find_symbol (globalenv p) id = Some b /\ find_var_info (globalenv p) b = Some gv - /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Writable - /\ load_store_init_data (globalenv p) m b 0 gv.(gvar_init). + /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv) + /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)). Proof. intros. exploit alloc_variables_charact; eauto. instantiate (1 := Mem.empty). rewrite add_functions_nextvar. rewrite Mem.nextblock_empty; auto. @@ -839,11 +869,15 @@ Lemma alloc_variable_neutral: Mem.inject_neutral thr m'. Proof. intros until m'. unfold alloc_variable. - caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b; intros. + caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b ALLOC. + caseEq (store_init_data_list ge m1 b 0 (gvar_init id#2)); try congruence. + intros m2 STORE DROP NEUTRAL NEXT. + eapply Mem.drop_inject_neutral; eauto. eapply store_init_data_list_neutral with (b := b). eapply Mem.alloc_inject_neutral; eauto. - rewrite (Mem.alloc_result _ _ _ _ _ H). auto. + rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. eauto. + rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. Qed. Lemma alloc_variables_neutral: @@ -1067,6 +1101,10 @@ Proof. destruct (Mem.alloc m 0 (init_data_list_size init)). rewrite store_init_data_list_match. destruct (store_init_data_list (globalenv p) m0 b 0 init); auto. + change (perm_globvar (mkglobvar info2 init ro vo)) + with (perm_globvar (mkglobvar info1 init ro vo)). + destruct (Mem.drop_perm m1 b 0 (init_data_list_size init) + (perm_globvar (mkglobvar info1 init ro vo))); auto. Qed. Theorem init_mem_match: |