From ad8c37d0ebb36cb2e54baeacf5a4c7ff145b1a99 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 3 Nov 2014 17:40:22 +0100 Subject: Add Genv.public_symbol operation. Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating. --- common/Globalenvs.v | 82 ++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 78 insertions(+), 4 deletions(-) (limited to 'common/Globalenvs.v') diff --git a/common/Globalenvs.v b/common/Globalenvs.v index e4772e25..eb98e876 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -82,6 +82,7 @@ Variable V: Type. (**r The type of information attached to variables *) (** The type of global environments. *) Record t: Type := mkgenv { + genv_public: list ident; (**r which symbol names are public *) genv_symb: PTree.t block; (**r mapping symbol -> block *) genv_funs: PTree.t F; (**r mapping function pointer -> definition *) genv_vars: PTree.t (globvar V); (**r mapping variable pointer -> info *) @@ -112,6 +113,14 @@ Definition symbol_address (ge: t) (id: ident) (ofs: int) : val := | None => Vundef end. +(** [public_symbol ge id] says whether the name [id] is public and defined. *) + +Definition public_symbol (ge: t) (id: ident) : bool := + match find_symbol ge id with + | None => false + | Some _ => In_dec ident_eq id ge.(genv_public) + end. + (** [find_funct_ptr ge b] returns the function description associated with the given address. *) @@ -144,6 +153,7 @@ Definition find_var_info (ge: t) (b: block) : option (globvar V) := Program Definition add_global (ge: t) (idg: ident * globdef F V) : t := @mkgenv + ge.(genv_public) (PTree.set idg#1 ge.(genv_next) ge.(genv_symb)) (match idg#2 with | Gfun f => PTree.set ge.(genv_next) f ge.(genv_funs) @@ -208,8 +218,8 @@ Proof. induction gl1; simpl; intros. auto. rewrite IHgl1; auto. Qed. -Program Definition empty_genv : t := - @mkgenv (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _. +Program Definition empty_genv (pub: list ident): t := + @mkgenv pub (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _. Next Obligation. rewrite PTree.gempty in H. discriminate. Qed. @@ -227,7 +237,7 @@ Next Obligation. Qed. Definition globalenv (p: program F V) := - add_globals empty_genv p.(prog_defs). + add_globals (empty_genv p.(prog_public)) p.(prog_defs). (** Proof principles *) @@ -277,6 +287,14 @@ End GLOBALENV_PRINCIPLES. (** ** Properties of the operations over global environments *) +Theorem public_symbol_exists: + forall ge id, public_symbol ge id = true -> exists b, find_symbol ge id = Some b. +Proof. + unfold public_symbol; intros. destruct (find_symbol ge id) as [b|]. + exists b; auto. + discriminate. +Qed. + Theorem shift_symbol_address: forall ge id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). @@ -486,6 +504,21 @@ Proof. rewrite IHgl. auto. Qed. +Remark genv_public_add_globals: + forall gl ge, + genv_public (add_globals ge gl) = genv_public ge. +Proof. + induction gl; simpl; intros. + auto. + rewrite IHgl; auto. +Qed. + +Theorem globalenv_public: + forall p, genv_public (globalenv p) = prog_public p. +Proof. + unfold globalenv; intros. rewrite genv_public_add_globals. auto. +Qed. + (** * Construction of the initial memory state *) Section INITMEM. @@ -1092,7 +1125,7 @@ Lemma init_mem_genv_next: forall p m, Proof. unfold init_mem; intros. exploit alloc_globals_nextblock; eauto. rewrite Mem.nextblock_empty. intro. - generalize (genv_next_add_globals (prog_defs p) empty_genv). + generalize (genv_next_add_globals (prog_defs p) (empty_genv (prog_public p))). fold (globalenv p). simpl genv_next. intros. congruence. Qed. @@ -1606,6 +1639,17 @@ Proof. intros. destruct globalenvs_match. unfold find_symbol. auto. Qed. +Theorem public_symbol_match: + forall (s : ident), + ~In s (map fst new_globs) -> + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + intros. unfold public_symbol. rewrite find_symbol_match by auto. + destruct (find_symbol (globalenv p) s); auto. + rewrite ! globalenv_public. + destruct progmatch as (P & Q & R). rewrite R. auto. +Qed. + Hypothesis new_ids_fresh : forall s', find_symbol (globalenv p) s' <> None -> ~In s' (map fst new_globs). @@ -1804,6 +1848,14 @@ Proof. intros. eapply find_symbol_match. eexact prog_match. auto. Qed. +Theorem public_symbol_transf_augment: + forall (s: ident), + ~ In s (map fst new_globs) -> + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + intros. eapply public_symbol_match. eexact prog_match. auto. +Qed. + Theorem init_mem_transf_augment: (forall s', find_symbol (globalenv p) s' <> None -> ~ In s' (map fst new_globs)) -> @@ -1910,6 +1962,14 @@ Proof. auto. Qed. +Theorem public_symbol_transf_partial2: + forall (s: ident), + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + pose proof (@public_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + auto. +Qed. + Theorem init_mem_transf_partial2: forall m, init_mem p = Some m -> init_mem p' = Some m. Proof. @@ -1968,6 +2028,13 @@ Proof. exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. +Theorem public_symbol_transf_partial: + forall (s: ident), + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + exact (@public_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). +Qed. + Theorem find_var_info_transf_partial: forall (b: block), find_var_info (globalenv p') b = find_var_info (globalenv p) b. @@ -2047,6 +2114,13 @@ Proof. exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). Qed. +Theorem public_symbol_transf: + forall (s: ident), + public_symbol (globalenv tp) s = public_symbol (globalenv p) s. +Proof. + exact (@public_symbol_transf_partial _ _ _ _ _ _ transf_OK). +Qed. + Theorem find_var_info_transf: forall (b: block), find_var_info (globalenv tp) b = find_var_info (globalenv p) b. -- cgit