From 7999c9ee1f09f7d555e3efc39f030564f76a3354 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 10 May 2010 15:35:02 +0000 Subject: - Extended traces so that pointers within globals are supported as event values. - Revised handling of volatile reads: the execution environment dictates the value read, via the trace of events. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Globalenvs.v | 70 ++++++++++++++++++++++++++--------------------------- 1 file changed, 34 insertions(+), 36 deletions(-) (limited to 'common/Globalenvs.v') diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 9dbf9022..65ae06c1 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -71,7 +71,9 @@ Record t: Type := mkgenv { genv_nextvar_pos: genv_nextvar > 0; genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> b <> 0 /\ genv_nextfun < b /\ b < genv_nextvar; genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> genv_nextfun < b < 0; - genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_nextvar + genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_nextvar; + genv_vars_inj: forall id1 id2 b, + PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2 }. (** ** Lookup functions *) @@ -111,7 +113,7 @@ Program Definition add_function (ge: t) (idf: ident * F) : t := ge.(genv_vars) (ge.(genv_nextfun) - 1) ge.(genv_nextvar) - _ _ _ _ _. + _ _ _ _ _ _. Next Obligation. destruct ge; simpl; omega. Qed. @@ -131,6 +133,15 @@ Qed. Next Obligation. destruct ge; eauto. Qed. +Next Obligation. + destruct ge; simpl in *. + rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. + destruct (peq id1 i); destruct (peq id2 i). + congruence. + exploit genv_symb_range0; eauto. intros [A B]. inv H. omegaContradiction. + exploit genv_symb_range0; eauto. intros [A B]. inv H0. omegaContradiction. + eauto. +Qed. Program Definition add_variable (ge: t) (idv: ident * list init_data * V) : t := @mkgenv @@ -139,7 +150,7 @@ Program Definition add_variable (ge: t) (idv: ident * list init_data * V) : t := (ZMap.set ge.(genv_nextvar) (Some idv#2) ge.(genv_vars)) ge.(genv_nextfun) (ge.(genv_nextvar) + 1) - _ _ _ _ _. + _ _ _ _ _ _. Next Obligation. destruct ge; auto. Qed. @@ -159,9 +170,18 @@ Next Obligation. destruct (ZIndexed.eq b genv_nextvar0). subst; omega. exploit genv_vars_range0; eauto. omega. Qed. +Next Obligation. + destruct ge; simpl in *. + rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. + destruct (peq id1 i); destruct (peq id2 i). + congruence. + exploit genv_symb_range0; eauto. intros [A B]. inv H. omegaContradiction. + exploit genv_symb_range0; eauto. intros [A B]. inv H0. omegaContradiction. + eauto. +Qed. Program Definition empty_genv : t := - @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) (-1) 1 _ _ _ _ _. + @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) (-1) 1 _ _ _ _ _ _. Next Obligation. omega. Qed. @@ -177,6 +197,9 @@ Qed. Next Obligation. rewrite ZMap.gi in H. discriminate. Qed. +Next Obligation. + rewrite PTree.gempty in H. discriminate. +Qed. Definition add_functions (ge: t) (fl: list (ident * F)) : t := List.fold_left add_function fl ge. @@ -435,38 +458,13 @@ Proof. Qed. Theorem global_addresses_distinct: - forall p id1 id2 b1 b2, - id1<>id2 -> - find_symbol (globalenv p) id1 = Some b1 -> - find_symbol (globalenv p) id2 = Some b2 -> - b1<>b2. -Proof. - intros until b2; intro DIFF. - - set (P := fun ge => find_symbol ge id1 = Some b1 -> find_symbol ge id2 = Some b2 -> b1 <> b2). - - assert (forall fl ge, P ge -> P (add_functions ge fl)). - induction fl; intros; simpl. auto. - apply IHfl. red. unfold find_symbol; simpl. - repeat rewrite PTree.gsspec. - fold ident. destruct (peq id1 a#1); destruct (peq id2 a#1). - congruence. - intros. inversion H0. exploit genv_symb_range; eauto. unfold block; omega. - intros. inversion H1. exploit genv_symb_range; eauto. unfold block; omega. - auto. - - assert (forall vl ge, P ge -> P (add_variables ge vl)). - induction vl; intros; simpl. auto. - apply IHvl. red. unfold find_symbol; simpl. - repeat rewrite PTree.gsspec. - fold ident. destruct (peq id1 a#1#1); destruct (peq id2 a#1#1). - congruence. - intros. inversion H1. exploit genv_symb_range; eauto. unfold block; omega. - intros. inversion H2. exploit genv_symb_range; eauto. unfold block; omega. - auto. - - change (P (globalenv p)). unfold globalenv. apply H0. apply H. - red; unfold find_symbol; simpl; intros. rewrite PTree.gempty in H1. congruence. + forall ge id1 id2 b1 b2, + id1 <> id2 -> + find_symbol ge id1 = Some b1 -> + find_symbol ge id2 = Some b2 -> + b1 <> b2. +Proof. + intros. red; intros; subst. elim H. destruct ge. eauto. Qed. (** * Construction of the initial memory state *) -- cgit