From 4af1682d04244bab9f793e00eb24090153a36a0f Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 28 Jul 2011 12:51:16 +0000 Subject: Added animation of the CompCert C semantics (ccomp -interp) test/regression: int main() so that interpretation works Revised once more implementation of __builtin_memcpy (to check for PPC & ARM) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Globalenvs.v | 208 ++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 163 insertions(+), 45 deletions(-) (limited to 'common/Globalenvs.v') diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 4a57a375..a9db51ec 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -33,6 +33,8 @@ place during program linking and program loading in a real operating system. *) +Require Recdef. +Require Import Zwf. Require Import Axioms. Require Import Coqlib. Require Import Errors. @@ -99,6 +101,13 @@ Definition find_funct (ge: t) (v: val) : option F := | _ => None end. +(** [invert_symbol ge b] returns the name associated with the given block, if any *) + +Definition invert_symbol (ge: t) (b: block) : option ident := + PTree.fold + (fun res id b' => if eq_block b b' then Some id else res) + ge.(genv_symb) None. + (** [find_var_info ge b] returns the information attached to the variable at address [b]. *) @@ -468,6 +477,39 @@ Proof. intros. red; intros; subst. elim H. destruct ge. eauto. Qed. +Theorem invert_find_symbol: + forall ge id b, + invert_symbol ge b = Some id -> find_symbol ge id = Some b. +Proof. + intros until b; unfold find_symbol, invert_symbol. + apply PTree_Properties.fold_rec. + intros. rewrite H in H0; auto. + congruence. + intros. destruct (eq_block b v). inv H2. apply PTree.gss. + rewrite PTree.gsspec. destruct (peq id k). + subst. assert (m!k = Some b) by auto. congruence. + auto. +Qed. + +Theorem find_invert_symbol: + forall ge id b, + find_symbol ge id = Some b -> invert_symbol ge b = Some id. +Proof. + intros until b. + assert (find_symbol ge id = Some b -> exists id', invert_symbol ge b = Some id'). + unfold find_symbol, invert_symbol. + apply PTree_Properties.fold_rec. + intros. rewrite H in H0; auto. + rewrite PTree.gempty; congruence. + intros. destruct (eq_block b v). exists k; auto. + rewrite PTree.gsspec in H2. destruct (peq id k). + inv H2. congruence. auto. + + intros; exploit H; eauto. intros [id' A]. + assert (id = id'). eapply genv_vars_inj; eauto. apply invert_find_symbol; auto. + congruence. +Qed. + (** * Construction of the initial memory state *) Section INITMEM. @@ -517,6 +559,18 @@ Fixpoint store_init_data_list (m: mem) (b: block) (p: Z) (idl: list init_data) end end. +Function store_zeros (m: mem) (b: block) (n: Z) {wf (Zwf 0) n}: option mem := + if zle n 0 then Some m else + let n' := n - 1 in + match Mem.store Mint8unsigned m b n' Vzero with + | Some m' => store_zeros m' b n' + | None => None + end. +Proof. + intros. red. omega. + apply Zwf_well_founded. +Qed. + Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := match il with | nil => 0 @@ -530,10 +584,15 @@ Definition perm_globvar (gv: globvar V) : permission := 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 - match store_init_data_list m' b 0 init with + let sz := init_data_list_size init in + let (m1, b) := Mem.alloc m 0 sz in + match store_zeros m1 b sz with | None => None - | Some m'' => Mem.drop_perm m'' b 0 (init_data_list_size init) (perm_globvar idv#2) + | Some m2 => + match store_init_data_list m2 b 0 init with + | None => None + | Some m3 => Mem.drop_perm m3 b 0 sz (perm_globvar idv#2) + end end. Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V)) @@ -561,6 +620,15 @@ Proof. destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto. Qed. +Remark store_zeros_nextblock: + forall m b n m', store_zeros m b n = Some m' -> Mem.nextblock m' = Mem.nextblock m. +Proof. + intros until n. functional induction (store_zeros m b n); intros. + inv H; auto. + rewrite IHo; eauto with mem. + congruence. +Qed. + Remark alloc_variables_nextblock: forall vl m m', alloc_variables m vl = Some m' -> @@ -571,17 +639,31 @@ Proof. simpl length; rewrite inj_S; simpl. intros m m'. 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. - caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. - intros m3 DROP REC. + set (sz := init_data_list_size init). + caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC. + caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. + caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. + caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC. rewrite (IHvl _ _ REC). rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + rewrite (store_zeros_nextblock _ _ _ STZ). rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega. Qed. + +Remark store_zeros_perm: + forall prm b' q m b n m', + store_zeros m b n = Some m' -> + Mem.perm m b' q prm -> Mem.perm m' b' q prm. +Proof. + intros until n. functional induction (store_zeros m b n); intros. + inv H; auto. + eauto with mem. + congruence. +Qed. + Remark store_init_data_list_perm: forall prm b' q idl b m p m', store_init_data_list m b p idl = Some m' -> @@ -605,17 +687,31 @@ Proof. simpl; intros. congruence. 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. - caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. - intros m3 DROP REC PERM. + set (sz := init_data_list_size init). + caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC. + caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. + caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. + caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 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. + eapply store_init_data_list_perm; eauto. + eapply store_zeros_perm; eauto. eauto with mem. Qed. +Remark store_zeros_outside: + forall m b n m', + store_zeros m b n = Some m' -> + forall chunk b' p, + b' <> b -> Mem.load chunk m' b' p = Mem.load chunk m b' p. +Proof. + intros until n. functional induction (store_zeros m b n); intros. + inv H; auto. + rewrite IHo; auto. eapply Mem.load_store_other; eauto. + inv H. +Qed. + Remark store_init_data_list_outside: forall b il m p m', store_init_data_list m b p il = Some m' -> @@ -699,20 +795,24 @@ Proof. congruence. 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. - caseEq (Mem.drop_perm m2 b1 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. - intros m3 DROP RED VALID. + set (sz := init_data_list_size init). + caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC. + caseEq (store_zeros m1 b1 sz); try congruence. intros m2 STZ. + caseEq (store_init_data_list m2 b1 0 init); try congruence. intros m3 STORE. + caseEq (Mem.drop_perm m3 b1 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID. assert (b <> b1). apply Mem.valid_not_valid_diff with m; eauto with mem. - transitivity (Mem.load chunk m3 b p). + transitivity (Mem.load chunk m4 b p). apply IHvl; auto. red. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ STO). + rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + rewrite (store_zeros_nextblock _ _ _ STZ). change (Mem.valid_block m1 b). eauto with mem. - transitivity (Mem.load chunk m2 b p). + transitivity (Mem.load chunk m3 b p). eapply Mem.load_drop; eauto. + transitivity (Mem.load chunk m2 b p). + eapply store_init_data_list_outside; eauto. transitivity (Mem.load chunk m1 b p). - eapply store_init_data_list_outside; eauto. + eapply store_zeros_outside; eauto. eapply Mem.load_alloc_unchanged; eauto. Qed. @@ -742,14 +842,15 @@ Proof. contradiction. intros until m'; intro NEXT. unfold alloc_variable. destruct a as [id' gv']. simpl. - 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. - 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. + set (init := gvar_init gv'). + set (sz := init_data_list_size init). + caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC. + caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. + caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. + caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar gv')); try congruence. + intros m4 DROP REC NOREPET IN. inv NOREPET. exploit Mem.alloc_result; eauto. intro BEQ. - destruct IN. inv H. + destruct IN. inversion H; subst id gv. exists (Mem.nextblock m); split. rewrite add_variables_same_symb; auto. unfold find_symbol; simpl. rewrite PTree.gss. congruence. @@ -757,23 +858,24 @@ Proof. rewrite NEXT. apply ZMap.gss. simpl. rewrite <- NEXT; omega. split. red; intros. - eapply alloc_variables_perm; eauto. - eapply Mem.perm_drop_1; eauto. + rewrite <- BEQ. eapply alloc_variables_perm; eauto. eapply Mem.perm_drop_1; eauto. intros NOVOL. - apply load_store_init_data_invariant with m2. - intros. transitivity (Mem.load chunk m3 (Mem.nextblock m) ofs). + apply load_store_init_data_invariant with m3. + intros. transitivity (Mem.load chunk m4 (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. + rewrite (store_zeros_nextblock _ _ _ STZ). + change (Mem.valid_block m1 (Mem.nextblock m)). rewrite <- BEQ. 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. + unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv'); auto with mem. + rewrite <- BEQ. eapply store_init_data_list_charact; eauto. - apply IHvl with m3; auto. + apply IHvl with m4; auto. simpl. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + rewrite (store_zeros_nextblock _ _ _ STZ). rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega. Qed. @@ -861,6 +963,19 @@ Proof. eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto. Qed. +Lemma store_zeros_neutral: + forall m b n m', + Mem.inject_neutral thr m -> + b < thr -> + store_zeros m b n = Some m' -> + Mem.inject_neutral thr m'. +Proof. + intros until n. functional induction (store_zeros m b n); intros. + inv H1; auto. + apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor. + inv H1. +Qed. + Lemma alloc_variable_neutral: forall id m m', alloc_variable ge m id = Some m' -> @@ -868,16 +983,18 @@ Lemma alloc_variable_neutral: Mem.nextblock m < thr -> 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 ALLOC. - caseEq (store_init_data_list ge m1 b 0 (gvar_init id#2)); try congruence. - intros m2 STORE DROP NEUTRAL NEXT. + intros until m'. unfold alloc_variable. + set (init := gvar_init id#2). + set (sz := init_data_list_size init). + caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC. + caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. + caseEq (store_init_data_list ge m2 b 0 init); try congruence. + intros m3 STORE DROP NEUTRAL NEXT. + assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. eapply Mem.drop_inject_neutral; eauto. - eapply store_init_data_list_neutral with (b := b). + eapply store_init_data_list_neutral with (m := m2) (b := b); eauto. + eapply store_zeros_neutral with (m := m1); eauto. eapply Mem.alloc_inject_neutral; eauto. - rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. - eauto. - rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. Qed. Lemma alloc_variables_neutral: @@ -1099,11 +1216,12 @@ Proof. inv H. unfold alloc_variable; simpl. destruct (Mem.alloc m 0 (init_data_list_size init)). + destruct (store_zeros m0 b (init_data_list_size init)); auto. rewrite store_init_data_list_match. - destruct (store_init_data_list (globalenv p) m0 b 0 init); auto. + destruct (store_init_data_list (globalenv p) m1 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) + destruct (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar (mkglobvar info1 init ro vo))); auto. Qed. -- cgit