diff options
Diffstat (limited to 'common')
| -rw-r--r-- | common/AST.v | 422 | ||||
| -rw-r--r-- | common/Globalenvs.v | 1784 |
2 files changed, 979 insertions, 1227 deletions
diff --git a/common/AST.v b/common/AST.v index 6425cb0..ccc9dbf 100644 --- a/common/AST.v +++ b/common/AST.v @@ -118,44 +118,29 @@ Record globvar (V: Type) : Type := mkglobvar { }. (** Whole programs consist of: -- a collection of function definitions (name and description); -- the name of the ``main'' function that serves as entry point in the program; -- a collection of global variable declarations (name and information). +- a collection of global definitions (name and description); +- the name of the ``main'' function that serves as entry point in the program. +A global definition is either a global function or a global variable. The type of function descriptions and that of additional information for variables vary among the various intermediate languages and are taken as parameters to the [program] type. The other parts of whole programs are common to all languages. *) -Record program (F V: Type) : Type := mkprogram { - prog_funct: list (ident * F); - prog_main: ident; - prog_vars: list (ident * globvar V) -}. +Inductive globdef (F V: Type) : Type := + | Gfun (f: F) + | Gvar (v: globvar V). -Definition funct_names (F: Type) (fl: list (ident * F)) : list ident := - map (@fst ident F) fl. +Implicit Arguments Gfun [F V]. +Implicit Arguments Gvar [F V]. -Lemma funct_names_app : forall (F: Type) (fl1 fl2 : list (ident * F)), - funct_names (fl1 ++ fl2) = funct_names fl1 ++ funct_names fl2. -Proof. - intros; unfold funct_names; apply list_append_map. -Qed. - -Definition var_names (V: Type) (vl: list (ident * globvar V)) : list ident := - map (@fst ident (globvar V)) vl. - -Lemma var_names_app : forall (V: Type) (vl1 vl2 : list (ident * globvar V)), - var_names (vl1 ++ vl2) = var_names vl1 ++ funct_names vl2. -Proof. - intros; unfold var_names; apply list_append_map. -Qed. - -Definition prog_funct_names (F V: Type) (p: program F V) : list ident := - funct_names p.(prog_funct). +Record program (F V: Type) : Type := mkprogram { + prog_defs: list (ident * globdef F V); + prog_main: ident +}. -Definition prog_var_names (F V: Type) (p: program F V) : list ident := - var_names p.(prog_vars). +Definition prog_defs_names (F V: Type) (p: program F V) : list ident := + List.map fst p.(prog_defs). (** * Generic transformations over programs *) @@ -168,253 +153,195 @@ Section TRANSF_PROGRAM. Variable A B V: Type. Variable transf: A -> B. -Definition transf_program (l: list (ident * A)) : list (ident * B) := - List.map (fun id_fn => (fst id_fn, transf (snd id_fn))) l. +Definition transform_program_globdef (idg: ident * globdef A V) : ident * globdef B V := + match idg with + | (id, Gfun f) => (id, Gfun (transf f)) + | (id, Gvar v) => (id, Gvar v) + end. Definition transform_program (p: program A V) : program B V := mkprogram - (transf_program p.(prog_funct)) - p.(prog_main) - p.(prog_vars). + (List.map transform_program_globdef p.(prog_defs)) + p.(prog_main). Lemma transform_program_function: forall p i tf, - In (i, tf) (transform_program p).(prog_funct) -> - exists f, In (i, f) p.(prog_funct) /\ transf f = tf. + In (i, Gfun tf) (transform_program p).(prog_defs) -> + exists f, In (i, Gfun f) p.(prog_defs) /\ transf f = tf. Proof. - simpl. unfold transf_program. intros. + simpl. unfold transform_program. intros. exploit list_in_map_inv; eauto. - intros [[i' f] [EQ IN]]. simpl in EQ. inversion EQ; subst. - exists f; split; auto. + intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. + exists f; auto. Qed. End TRANSF_PROGRAM. -(** The following is a variant of [transform_program] where the - code transformation function can fail and therefore returns an - option type. *) +(** The following is a more general presentation of [transform_program] where + global variable information can be transformed, in addition to function + definitions. Moreover, the transformation functions can fail and + return an error message. *) Open Local Scope error_monad_scope. Open Local Scope string_scope. -Section MAP_PARTIAL. +Section TRANSF_PROGRAM_GEN. -Variable A B C: Type. -Variable prefix_errmsg: A -> errmsg. -Variable f: B -> res C. +Variables A B V W: Type. +Variable transf_fun: A -> res B. +Variable transf_var: V -> res W. + +Definition transf_globvar (g: globvar V) : res (globvar W) := + do info' <- transf_var g.(gvar_info); + OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)). -Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) := +Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) := match l with | nil => OK nil - | (a, b) :: rem => - match f b with - | Error msg => Error (prefix_errmsg a ++ msg)%list - | OK c => - do rem' <- map_partial rem; - OK ((a, c) :: rem') + | (id, Gfun f) :: l' => + match transf_fun f with + | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg) + | OK tf => + do tl' <- transf_globdefs l'; OK ((id, Gfun tf) :: tl') + end + | (id, Gvar v) :: l' => + match transf_globvar v with + | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg) + | OK tv => + do tl' <- transf_globdefs l'; OK ((id, Gvar tv) :: tl') end end. -Remark In_map_partial: - forall l l' a c, - map_partial l = OK l' -> - In (a, c) l' -> - exists b, In (a, b) l /\ f b = OK c. -Proof. - induction l; simpl. - intros. inv H. elim H0. - intros until c. destruct a as [a1 b1]. - caseEq (f b1); try congruence. - intro c1; intros. monadInv H0. - elim H1; intro. inv H0. exists b1; auto. - exploit IHl; eauto. intros [b [P Q]]. exists b; auto. -Qed. +Definition transform_partial_program2 (p: program A V) : res (program B W) := + do gl' <- transf_globdefs p.(prog_defs); OK(mkprogram gl' p.(prog_main)). -Remark map_partial_forall2: - forall l l', - map_partial l = OK l' -> - list_forall2 - (fun (a_b: A * B) (a_c: A * C) => - fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c)) - l l'. +Lemma transform_partial_program2_function: + forall p tp i tf, + transform_partial_program2 p = OK tp -> + In (i, Gfun tf) tp.(prog_defs) -> + exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun f = OK tf. Proof. - induction l; simpl. - intros. inv H. constructor. - intro l'. destruct a as [a b]. - caseEq (f b). 2: congruence. intro c; intros. monadInv H0. - constructor. simpl. auto. auto. + intros. monadInv H. simpl in H0. + revert x EQ H0. induction (prog_defs p); simpl; intros. + inv EQ. contradiction. + destruct a as [id [f|v]]. + destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ. + simpl in H0; destruct H0. inv H. exists f; auto. + exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. + destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ. + simpl in H0; destruct H0. inv H. + exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. Qed. -End MAP_PARTIAL. - -Remark map_partial_total: - forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)), - map_partial prefix (fun b => OK (f b)) l = - OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l). +Lemma transform_partial_program2_variable: + forall p tp i tv, + transform_partial_program2 p = OK tp -> + In (i, Gvar tv) tp.(prog_defs) -> + exists v, + In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs) + /\ transf_var v = OK tv.(gvar_info). Proof. - induction l; simpl. - auto. - destruct a as [a1 b1]. rewrite IHl. reflexivity. + intros. monadInv H. simpl in H0. + revert x EQ H0. induction (prog_defs p); simpl; intros. + inv EQ. contradiction. + destruct a as [id [f|v]]. + destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ. + simpl in H0; destruct H0. inv H. + exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. + destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ. + simpl in H0; destruct H0. inv H. + monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto. + exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. Qed. -Remark map_partial_identity: - forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)), - map_partial prefix (fun b => OK b) l = OK l. +Lemma transform_partial_program2_main: + forall p tp, + transform_partial_program2 p = OK tp -> + tp.(prog_main) = p.(prog_main). Proof. - induction l; simpl. - auto. - destruct a as [a1 b1]. rewrite IHl. reflexivity. + intros. monadInv H. reflexivity. Qed. -Section TRANSF_PARTIAL_PROGRAM. +(** Additionally, we can also "augment" the program with new global definitions + and a different "main" function. *) -Variable A B V: Type. -Variable transf_partial: A -> res B. - -Definition prefix_name (id: ident) : errmsg := - MSG "In function " :: CTX id :: MSG ": " :: nil. +Section AUGMENT. -Definition transform_partial_program (p: program A V) : res (program B V) := - do fl <- map_partial prefix_name transf_partial p.(prog_funct); - OK (mkprogram fl p.(prog_main) p.(prog_vars)). +Variable new_globs: list(ident * globdef B W). +Variable new_main: ident. -Lemma transform_partial_program_function: - forall p tp i tf, - transform_partial_program p = OK tp -> - In (i, tf) tp.(prog_funct) -> - exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf. -Proof. - intros. monadInv H. simpl in H0. - eapply In_map_partial; eauto. -Qed. +Definition transform_partial_augment_program (p: program A V) : res (program B W) := + do gl' <- transf_globdefs p.(prog_defs); + OK(mkprogram (gl' ++ new_globs) new_main). -Lemma transform_partial_program_main: +Lemma transform_partial_augment_program_main: forall p tp, - transform_partial_program p = OK tp -> - tp.(prog_main) = p.(prog_main). + transform_partial_augment_program p = OK tp -> + tp.(prog_main) = new_main. Proof. intros. monadInv H. reflexivity. Qed. -Lemma transform_partial_program_vars: - forall p tp, - transform_partial_program p = OK tp -> - tp.(prog_vars) = p.(prog_vars). +End AUGMENT. + +Remark transform_partial_program2_augment: + forall p, + transform_partial_program2 p = + transform_partial_augment_program nil p.(prog_main) p. Proof. - intros. monadInv H. reflexivity. + unfold transform_partial_program2, transform_partial_augment_program; intros. + destruct (transf_globdefs (prog_defs p)); auto. + simpl. f_equal. f_equal. rewrite <- app_nil_end. auto. Qed. -End TRANSF_PARTIAL_PROGRAM. +End TRANSF_PROGRAM_GEN. -(** The following is a variant of [transform_program_partial] where - both the program functions and the additional variable information - are transformed by functions that can fail. *) +(** The following is a special case of [transform_partial_program2], + where only function definitions are transformed, but not variable definitions. *) -Section TRANSF_PARTIAL_PROGRAM2. - -Variable A B V W: Type. -Variable transf_partial_function: A -> res B. -Variable transf_partial_variable: V -> res W. - -Definition transf_globvar (g: globvar V) : res (globvar W) := - do info' <- transf_partial_variable g.(gvar_info); - OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)). - -Definition transform_partial_program2 (p: program A V) : res (program B W) := - do fl <- map_partial prefix_name transf_partial_function p.(prog_funct); - do vl <- map_partial prefix_name transf_globvar p.(prog_vars); - OK (mkprogram fl p.(prog_main) vl). +Section TRANSF_PARTIAL_PROGRAM. -Lemma transform_partial_program2_function: - forall p tp i tf, - transform_partial_program2 p = OK tp -> - In (i, tf) tp.(prog_funct) -> - exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf. -Proof. - intros. monadInv H. - eapply In_map_partial; eauto. -Qed. +Variable A B V: Type. +Variable transf_partial: A -> res B. -Lemma transform_partial_program2_variable: - forall p tp i tg, - transform_partial_program2 p = OK tp -> - In (i, tg) tp.(prog_vars) -> - exists v, - In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars) - /\ transf_partial_variable v = OK tg.(gvar_info). -Proof. - intros. monadInv H. exploit In_map_partial; eauto. intros [g [P Q]]. - monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto. - Qed. +Definition transform_partial_program (p: program A V) : res (program B V) := + transform_partial_program2 transf_partial (fun v => OK v) p. -Lemma transform_partial_program2_main: +Lemma transform_partial_program_main: forall p tp, - transform_partial_program2 p = OK tp -> + transform_partial_program p = OK tp -> tp.(prog_main) = p.(prog_main). Proof. - intros. monadInv H. reflexivity. + apply transform_partial_program2_main. Qed. -End TRANSF_PARTIAL_PROGRAM2. - -(** The following is a variant of [transform_partial_program2] where the - where the set of functions and global data is augmented, and - the main function is potentially changed. *) - -Section TRANSF_PARTIAL_AUGMENT_PROGRAM. - -Variable A B V W: Type. -Variable transf_partial_function: A -> res B. -Variable transf_partial_variable: V -> res W. - -Variable new_functs : list (ident * B). -Variable new_vars : list (ident * globvar W). -Variable new_main : ident. - -Definition transform_partial_augment_program (p: program A V) : res (program B W) := - do fl <- map_partial prefix_name transf_partial_function p.(prog_funct); - do vl <- map_partial prefix_name (transf_globvar transf_partial_variable) p.(prog_vars); - OK (mkprogram (fl ++ new_functs) new_main (vl ++ new_vars)). - -Lemma transform_partial_augment_program_function: +Lemma transform_partial_program_function: forall p tp i tf, - transform_partial_augment_program p = OK tp -> - In (i, tf) tp.(prog_funct) -> - (exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf) - \/ In (i,tf) new_functs. -Proof. - intros. monadInv H. simpl in H0. - rewrite in_app in H0. destruct H0. - left. eapply In_map_partial; eauto. - right. auto. -Qed. - -Lemma transform_partial_augment_program_main: - forall p tp, - transform_partial_augment_program p = OK tp -> - tp.(prog_main) = new_main. + transform_partial_program p = OK tp -> + In (i, Gfun tf) tp.(prog_defs) -> + exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial f = OK tf. Proof. - intros. monadInv H. reflexivity. + apply transform_partial_program2_function. Qed. +End TRANSF_PARTIAL_PROGRAM. -Lemma transform_partial_augment_program_variable: - forall p tp i tg, - transform_partial_augment_program p = OK tp -> - In (i, tg) tp.(prog_vars) -> - (exists v, In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars) /\ transf_partial_variable v = OK tg.(gvar_info)) - \/ In (i,tg) new_vars. +Lemma transform_program_partial_program: + forall (A B V: Type) (transf: A -> B) (p: program A V), + transform_partial_program (fun f => OK(transf f)) p = OK(transform_program transf p). Proof. - intros. monadInv H. - simpl in H0. rewrite in_app in H0. inversion H0. - left. exploit In_map_partial; eauto. intros [g [P Q]]. - monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto. - right. auto. + intros. + unfold transform_partial_program, transform_partial_program2, transform_program; intros. + replace (transf_globdefs (fun f => OK (transf f)) (fun v => OK v) p.(prog_defs)) + with (OK (map (transform_program_globdef transf) p.(prog_defs))). + auto. + induction (prog_defs p); simpl. + auto. + destruct a as [id [f|v]]; rewrite <- IHl. + auto. + destruct v; auto. Qed. -End TRANSF_PARTIAL_AUGMENT_PROGRAM. - - (** The following is a relational presentation of [transform_partial_augment_preogram]. Given relations between function definitions and between variable information, it defines a relation @@ -429,61 +356,50 @@ Variable A B V W: Type. Variable match_fundef: A -> B -> Prop. Variable match_varinfo: V -> W -> Prop. -Inductive match_funct_entry: ident * A -> ident * B -> Prop := - | match_funct_entry_intro: forall id fn1 fn2, - match_fundef fn1 fn2 -> - match_funct_entry (id, fn1) (id, fn2). - -Inductive match_var_entry: ident * globvar V -> ident * globvar W -> Prop := - | match_var_entry_intro: forall id info1 info2 init ro vo, +Inductive match_globdef: ident * globdef A V -> ident * globdef B W -> Prop := + | match_glob_fun: forall id f1 f2, + match_fundef f1 f2 -> + match_globdef (id, Gfun f1) (id, Gfun f2) + | match_glob_var: forall id init ro vo info1 info2, match_varinfo info1 info2 -> - match_var_entry (id, mkglobvar info1 init ro vo) - (id, mkglobvar info2 init ro vo). + match_globdef (id, Gvar (mkglobvar info1 init ro vo)) (id, Gvar (mkglobvar info2 init ro vo)). -Definition match_program (new_functs : list (ident * B)) - (new_vars : list (ident * globvar W)) +Definition match_program (new_globs : list (ident * globdef B W)) (new_main : ident) (p1: program A V) (p2: program B W) : Prop := - (exists tfuncts, list_forall2 match_funct_entry p1.(prog_funct) tfuncts /\ - (p2.(prog_funct) = tfuncts ++ new_functs)) /\ - (exists tvars, list_forall2 match_var_entry p1.(prog_vars) tvars /\ - (p2.(prog_vars) = tvars ++ new_vars)) /\ + (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\ + p2.(prog_defs) = tglob ++ new_globs) /\ p2.(prog_main) = new_main. End MATCH_PROGRAM. -Remark transform_partial_augment_program_match: +Lemma transform_partial_augment_program_match: forall (A B V W: Type) - (transf_partial_function: A -> res B) - (transf_partial_variable : V -> res W) + (transf_fun: A -> res B) + (transf_var: V -> res W) (p: program A V) - (new_functs : list (ident * B)) - (new_vars : list (ident * globvar W)) + (new_globs : list (ident * globdef B W)) (new_main : ident) (tp: program B W), - transform_partial_augment_program transf_partial_function transf_partial_variable new_functs new_vars new_main p = OK tp -> + transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK tp -> match_program - (fun fd tfd => transf_partial_function fd = OK tfd) - (fun info tinfo => transf_partial_variable info = OK tinfo) - new_functs new_vars new_main + (fun fd tfd => transf_fun fd = OK tfd) + (fun info tinfo => transf_var info = OK tinfo) + new_globs new_main p tp. Proof. - intros. unfold transform_partial_augment_program in H. monadInv H. split. - exists x. split. - apply list_forall2_imply with - (fun (ab: ident * A) (ac: ident * B) => - fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)). - eapply map_partial_forall2. eauto. - intros. destruct v1; destruct v2; simpl in *. - destruct H1; subst. constructor. auto. - auto. - split. exists x0. split. - apply list_forall2_imply with - (fun (ab: ident * globvar V) (ac: ident * globvar W) => - fst ab = fst ac /\ transf_globvar transf_partial_variable (snd ab) = OK (snd ac)). - eapply map_partial_forall2. eauto. - intros. destruct v1; destruct v2; simpl in *. destruct H1; subst. - monadInv H2. destruct g; simpl in *. constructor. auto. auto. auto. + unfold transform_partial_augment_program; intros. monadInv H. + red; simpl. split; auto. exists x; split; auto. + revert x EQ. generalize (prog_defs p). induction l; simpl; intros. + monadInv EQ. constructor. + destruct a as [id [f|v]]. + (* function *) + destruct (transf_fun f) as [tf|?]_eqn; monadInv EQ. + constructor; auto. constructor; auto. + (* variable *) + unfold transf_globvar in EQ. + destruct (transf_var (gvar_info v)) as [tinfo|?]_eqn; simpl in EQ; monadInv EQ. + constructor; auto. destruct v; simpl in *. constructor; auto. Qed. (** * External functions *) diff --git a/common/Globalenvs.v b/common/Globalenvs.v index ba038f8..8565ae6 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -69,13 +69,13 @@ Record t: Type := mkgenv { genv_symb: PTree.t block; (**r mapping symbol -> block *) genv_funs: ZMap.t (option F); (**r mapping function pointer -> definition *) genv_vars: ZMap.t (option (globvar V)); (**r mapping variable pointer -> info *) - genv_nextfun: block; (**r next function pointer *) - genv_nextvar: block; (**r next variable pointer *) - genv_nextfun_neg: genv_nextfun < 0; - 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_next: block; (**r next symbol pointer *) + genv_next_pos: genv_next > 0; + genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> 0 < b < genv_next; + genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> 0 < b < genv_next; + genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_next; + genv_funs_vars: forall b1 b2 f v, + ZMap.get b1 genv_funs = Some f -> ZMap.get b2 genv_vars = Some v -> b1 <> b2; genv_vars_inj: forall id1 id2 b, PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2 }. @@ -117,69 +117,53 @@ Definition find_var_info (ge: t) (b: block) : option (globvar V) := (** ** Constructing the global environment *) -Program Definition add_function (ge: t) (idf: ident * F) : t := +Program Definition add_global (ge: t) (idg: ident * globdef F V) : t := @mkgenv - (PTree.set idf#1 ge.(genv_nextfun) ge.(genv_symb)) - (ZMap.set ge.(genv_nextfun) (Some idf#2) ge.(genv_funs)) - ge.(genv_vars) - (ge.(genv_nextfun) - 1) - ge.(genv_nextvar) + (PTree.set idg#1 ge.(genv_next) ge.(genv_symb)) + (match idg#2 with + | Gfun f => ZMap.set ge.(genv_next) (Some f) ge.(genv_funs) + | Gvar v => ge.(genv_funs) + end) + (match idg#2 with + | Gfun f => ge.(genv_vars) + | Gvar v => ZMap.set ge.(genv_next) (Some v) ge.(genv_vars) + end) + (ge.(genv_next) + 1) _ _ _ _ _ _. Next Obligation. destruct ge; simpl; omega. Qed. Next Obligation. - destruct ge; auto. -Qed. -Next Obligation. destruct ge; simpl in *. rewrite PTree.gsspec in H. destruct (peq id i). inv H. unfold block; omega. exploit genv_symb_range0; eauto. unfold block; omega. Qed. Next Obligation. - destruct ge; simpl in *. rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b genv_nextfun0). subst; omega. + destruct ge; simpl in *. + destruct g. + rewrite ZMap.gsspec in H. + destruct (ZIndexed.eq b genv_next0). subst; omega. + exploit genv_funs_range0; eauto. omega. exploit genv_funs_range0; eauto. omega. -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 * globvar V) : t := - @mkgenv - (PTree.set idv#1 ge.(genv_nextvar) ge.(genv_symb)) - ge.(genv_funs) - (ZMap.set ge.(genv_nextvar) (Some idv#2) ge.(genv_vars)) - ge.(genv_nextfun) - (ge.(genv_nextvar) + 1) - _ _ _ _ _ _. -Next Obligation. - destruct ge; auto. -Qed. -Next Obligation. - destruct ge; simpl; omega. -Qed. -Next Obligation. - destruct ge; simpl in *. - rewrite PTree.gsspec in H. destruct (peq id i). inv H. unfold block; omega. - exploit genv_symb_range0; eauto. unfold block; omega. -Qed. -Next Obligation. - destruct ge; eauto. + destruct g. + exploit genv_vars_range0; eauto. omega. + rewrite ZMap.gsspec in H. + destruct (ZIndexed.eq b genv_next0). subst; omega. + exploit genv_vars_range0; eauto. omega. Qed. Next Obligation. - destruct ge; simpl in *. rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b genv_nextvar0). subst; omega. - exploit genv_vars_range0; eauto. omega. + destruct ge; simpl in *. destruct g. + rewrite ZMap.gsspec in H. + destruct (ZIndexed.eq b1 genv_next0). inv H. + exploit genv_vars_range0; eauto. unfold ZIndexed.t; omega. + eauto. + rewrite ZMap.gsspec in H0. + destruct (ZIndexed.eq b2 genv_next0). inv H. + exploit genv_funs_range0; eauto. unfold ZIndexed.t; omega. + eauto. Qed. Next Obligation. destruct ge; simpl in *. @@ -191,16 +175,26 @@ Next Obligation. eauto. Qed. +Definition add_globals (ge: t) (gl: list (ident * globdef F V)) : t := + List.fold_left add_global gl ge. + +Lemma add_globals_app: + forall gl2 gl1 ge, + add_globals ge (gl1 ++ gl2) = add_globals (add_globals ge gl1) gl2. +Proof. + induction gl1; simpl; intros. auto. rewrite IHgl1; auto. +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 _ _ _ _ _ _. Next Obligation. omega. Qed. Next Obligation. - omega. + rewrite PTree.gempty in H. discriminate. Qed. Next Obligation. - rewrite PTree.gempty in H. discriminate. + rewrite ZMap.gi in H. discriminate. Qed. Next Obligation. rewrite ZMap.gi in H. discriminate. @@ -212,27 +206,54 @@ 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. +Definition globalenv (p: program F V) := + add_globals empty_genv p.(prog_defs). -Lemma add_functions_app : forall ge fl1 fl2, - add_functions ge (fl1 ++ fl2) = add_functions (add_functions ge fl1) fl2. -Proof. - intros. unfold add_functions. rewrite fold_left_app. auto. -Qed. +(** Proof principles *) +Section GLOBALENV_PRINCIPLES. -Definition add_variables (ge: t) (vl: list (ident * globvar V)) : t := - List.fold_left add_variable vl ge. +Variable P: t -> Prop. -Lemma add_variables_app : forall ge vl1 vl2 , - add_variables ge (vl1 ++ vl2) = add_variables (add_variables ge vl1) vl2. -Proof. - intros. unfold add_variables. rewrite fold_left_app. auto. +Lemma add_globals_preserves: + forall gl ge, + (forall ge id g, P ge -> In (id, g) gl -> P (add_global ge (id, g))) -> + P ge -> P (add_globals ge gl). +Proof. + induction gl; simpl; intros. + auto. + destruct a. apply IHgl; auto. Qed. -Definition globalenv (p: program F V) := - add_variables (add_functions empty_genv p.(prog_funct)) p.(prog_vars). +Lemma add_globals_ensures: + forall id g gl ge, + (forall ge id g, P ge -> In (id, g) gl -> P (add_global ge (id, g))) -> + (forall ge, P (add_global ge (id, g))) -> + In (id, g) gl -> P (add_globals ge gl). +Proof. + induction gl; simpl; intros. + contradiction. + destruct H1. subst a. apply add_globals_preserves; auto. + apply IHgl; auto. +Qed. + +Lemma add_globals_norepet_ensures: + forall id g gl ge, + (forall ge id1 g1, P ge -> In (id1, g1) gl -> id1 <> id -> P (add_global ge (id1, g1))) -> + (forall ge, P (add_global ge (id, g))) -> + In (id, g) gl -> list_norepet (map fst gl) -> P (add_globals ge gl). +Proof. + induction gl; simpl; intros. + contradiction. + inv H2. + destruct H1. subst a. simpl in H5. + apply add_globals_preserves; auto. + intros. apply H. auto. auto. red; intros; subst id0. elim H5. + change id with (fst (id, g0)). apply List.in_map; auto. + apply IHgl; auto. +Qed. + +End GLOBALENV_PRINCIPLES. (** ** Properties of the operations over global environments *) @@ -254,298 +275,132 @@ Proof. Qed. Theorem find_symbol_exists: - forall p id gv, - In (id, gv) (prog_vars p) -> + forall p id g, + In (id, g) (prog_defs p) -> exists b, find_symbol (globalenv p) id = Some b. Proof. - intros until gv. - assert (forall vl ge, - (exists b, find_symbol ge id = Some b) -> - exists b, find_symbol (add_variables ge vl) id = Some b). - unfold find_symbol; induction vl; simpl; intros. auto. apply IHvl. - simpl. rewrite PTree.gsspec. fold ident. destruct (peq id a#1). - exists (genv_nextvar ge); auto. auto. - - assert (forall vl ge, In (id, gv) vl -> - exists b, find_symbol (add_variables ge vl) id = Some b). - unfold find_symbol; induction vl; simpl; intros. contradiction. - destruct H0. apply H. subst; unfold find_symbol; simpl. - rewrite PTree.gss. exists (genv_nextvar ge); auto. - eauto. + intros. unfold globalenv. eapply add_globals_ensures; eauto. +(* preserves *) + intros. unfold find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id0). + econstructor; eauto. + auto. +(* ensures *) + intros. unfold find_symbol; simpl. rewrite PTree.gss. econstructor; eauto. +Qed. - intros. unfold globalenv; eauto. +Theorem find_funct_ptr_exists: + forall p id f, + list_norepet (prog_defs_names p) -> + In (id, Gfun f) (prog_defs p) -> + exists b, + find_symbol (globalenv p) id = Some b + /\ find_funct_ptr (globalenv p) b = Some f. +Proof. + intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto. +(* preserves *) + intros. unfold find_symbol, find_funct_ptr in *; simpl. + destruct H1 as [b [A B]]. exists b; split. + rewrite PTree.gso; auto. + destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto. + exploit genv_funs_range; eauto. unfold ZIndexed.t; omega. + auto. +(* ensures *) + intros. unfold find_symbol, find_funct_ptr in *; simpl. + exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. Qed. Theorem find_var_exists: - forall p id gv, - list_norepet (prog_var_names p) -> - In (id, gv) (prog_vars p) -> + forall p id v, + list_norepet (prog_defs_names p) -> + In (id, Gvar v) (prog_defs p) -> exists b, find_symbol (globalenv p) id = Some b - /\ find_var_info (globalenv p) b = Some gv. -Proof. - intros until gv. - assert (forall vl ge, - ~In id (var_names vl) -> - (exists b, find_symbol ge id = Some b /\ find_var_info ge b = Some gv) -> - (exists b, find_symbol (add_variables ge vl) id = Some b - /\ find_var_info (add_variables ge vl) b = Some gv)). - induction vl; simpl; intros. - auto. - apply IHvl. tauto. destruct a as [id1 gv1]. destruct H0 as [b [P Q]]. - unfold add_variable, find_symbol, find_var_info; simpl. - exists b; split. rewrite PTree.gso. auto. intuition. - rewrite ZMap.gso. auto. exploit genv_vars_range; eauto. - unfold ZIndexed.t; omega. - - unfold globalenv, prog_var_names. - generalize (prog_vars p) (add_functions empty_genv (prog_funct p)). - induction l; simpl; intros. - contradiction. - destruct a as [id1 gv1]; simpl in *. inv H0. - destruct H1. inv H0. - apply H; auto. - exists (genv_nextvar t0); split. - unfold find_symbol, add_variable; simpl. apply PTree.gss. - unfold find_var_info, add_variable; simpl. apply ZMap.gss. - apply IHl; auto. -Qed. - -Remark add_variables_inversion : forall vs e x b, - find_symbol (add_variables e vs) x = Some b -> - In x (var_names vs) \/ find_symbol e x = Some b. -Proof. - induction vs; intros. - simpl in H. intuition. - simpl in H. destruct (IHvs _ _ _ H). - left. simpl. intuition. - destruct a as [y ?]. - unfold add_variable, find_symbol in H0. simpl in H0. - rewrite PTree.gsspec in H0. destruct (peq x y); subst; simpl; intuition. -Qed. - -Remark add_functions_inversion : forall fs e x b, - find_symbol (add_functions e fs) x = Some b -> - In x (funct_names fs) \/ find_symbol e x = Some b. -Proof. - induction fs; intros. - simpl in H. intuition. - simpl in H. destruct (IHfs _ _ _ H). - left. simpl. intuition. - destruct a as [y ?]. - unfold add_variable, find_symbol in H0. simpl in H0. - rewrite PTree.gsspec in H0. destruct (peq x y); subst; simpl; intuition. + /\ find_var_info (globalenv p) b = Some v. +Proof. + intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto. +(* preserves *) + intros. unfold find_symbol, find_var_info in *; simpl. + destruct H1 as [b [A B]]. exists b; split. + rewrite PTree.gso; auto. + destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto. + exploit genv_vars_range; eauto. unfold ZIndexed.t; omega. +(* ensures *) + intros. unfold find_symbol, find_var_info in *; simpl. + exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. Qed. Lemma find_symbol_inversion : forall p x b, find_symbol (globalenv p) x = Some b -> - In x (prog_var_names p ++ prog_funct_names p). -Proof. - unfold prog_var_names, prog_funct_names, globalenv. - intros. - apply in_app. - apply add_variables_inversion in H. intuition. - apply add_functions_inversion in H0. inversion H0. intuition. - unfold find_symbol in H. - rewrite PTree.gempty in H. inversion H. -Qed. - - -Remark add_functions_same_symb: - forall id fl ge, - ~In id (funct_names fl) -> - find_symbol (add_functions ge fl) id = find_symbol ge id. -Proof. - induction fl; simpl; intros. auto. - rewrite IHfl. unfold find_symbol; simpl. apply PTree.gso. intuition. intuition. -Qed. - -Remark add_functions_same_address: - forall b fl ge, - b > ge.(genv_nextfun) -> - find_funct_ptr (add_functions ge fl) b = find_funct_ptr ge b. -Proof. - induction fl; simpl; intros. auto. - rewrite IHfl. unfold find_funct_ptr; simpl. apply ZMap.gso. - red; intros; subst b; omegaContradiction. - simpl. omega. -Qed. - -Remark add_variables_same_symb: - forall id vl ge, - ~In id (var_names vl) -> - find_symbol (add_variables ge vl) id = find_symbol ge id. + In x (prog_defs_names p). Proof. - induction vl; simpl; intros. auto. - rewrite IHvl. unfold find_symbol; simpl. apply PTree.gso. intuition. intuition. -Qed. - -Remark add_variables_same_address: - forall b vl ge, - b < ge.(genv_nextvar) -> - find_var_info (add_variables ge vl) b = find_var_info ge b. -Proof. - induction vl; simpl; intros. auto. - rewrite IHvl. unfold find_var_info; simpl. apply ZMap.gso. - red; intros; subst b; omegaContradiction. - simpl. omega. -Qed. - -Remark add_variables_same_funs: - forall b vl ge, find_funct_ptr (add_variables ge vl) b = find_funct_ptr ge b. -Proof. - induction vl; simpl; intros. auto. rewrite IHvl. auto. + intros until b; unfold globalenv. eapply add_globals_preserves. +(* preserves *) + unfold find_symbol; simpl; intros. rewrite PTree.gsspec in H1. + destruct (peq x id). subst x. change id with (fst (id, g)). apply List.in_map; auto. + auto. +(* base *) + unfold find_symbol; simpl; intros. rewrite PTree.gempty in H. discriminate. Qed. -Remark add_functions_nextvar: - forall fl ge, genv_nextvar (add_functions ge fl) = genv_nextvar ge. +Theorem find_funct_ptr_inversion: + forall p b f, + find_funct_ptr (globalenv p) b = Some f -> + exists id, In (id, Gfun f) (prog_defs p). Proof. - induction fl; simpl; intros. auto. rewrite IHfl. auto. + intros until f. unfold globalenv. apply add_globals_preserves. +(* preserves *) + unfold find_funct_ptr; simpl; intros. destruct g; auto. + rewrite ZMap.gsspec in H1. destruct (ZIndexed.eq b (genv_next ge)). + inv H1. exists id; auto. + auto. +(* base *) + unfold find_funct_ptr; simpl; intros. rewrite ZMap.gi in H. discriminate. Qed. -Remark add_variables_nextvar: - forall vl ge, genv_nextvar (add_variables ge vl) = genv_nextvar ge + Z_of_nat(List.length vl). +Theorem find_funct_inversion: + forall p v f, + find_funct (globalenv p) v = Some f -> + exists id, In (id, Gfun f) (prog_defs p). Proof. - induction vl; intros. - simpl. unfold block; omega. - simpl length; rewrite inj_S; simpl. rewrite IHvl. simpl. unfold block; omega. -Qed. - -Theorem find_funct_ptr_exists: - forall p id f, - list_norepet (prog_funct_names p) -> - list_disjoint (prog_funct_names p) (prog_var_names p) -> - In (id, f) (prog_funct p) -> - exists b, find_symbol (globalenv p) id = Some b - /\ find_funct_ptr (globalenv p) b = Some f. -Proof. - intros until f. - - assert (forall fl ge, In (id, f) fl -> list_norepet (funct_names fl) -> - exists b, find_symbol (add_functions ge fl) id = Some b - /\ find_funct_ptr (add_functions ge fl) b = Some f). - induction fl; simpl; intros. contradiction. inv H0. - destruct H. subst a. exists (genv_nextfun ge); split. - rewrite add_functions_same_symb; auto. unfold find_symbol; simpl. apply PTree.gss. - rewrite add_functions_same_address. unfold find_funct_ptr; simpl. apply ZMap.gss. - simpl; omega. - apply IHfl; auto. - - intros. exploit (H p.(prog_funct) empty_genv); eauto. intros [b [A B]]. - unfold globalenv; exists b; split. - rewrite add_variables_same_symb. auto. eapply list_disjoint_notin; eauto. - unfold prog_funct_names. change id with (fst (id, f)). apply in_map; auto. - rewrite add_variables_same_funs. auto. + intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. + rewrite find_funct_find_funct_ptr in H. + eapply find_funct_ptr_inversion; eauto. Qed. Theorem find_funct_ptr_prop: forall (P: F -> Prop) p b f, - (forall id f, In (id, f) (prog_funct p) -> P f) -> + (forall id f, In (id, Gfun f) (prog_defs p) -> P f) -> find_funct_ptr (globalenv p) b = Some f -> P f. Proof. - intros until f. intros PROP. - assert (forall fl ge, - List.incl fl (prog_funct p) -> - match find_funct_ptr ge b with None => True | Some f => P f end -> - match find_funct_ptr (add_functions ge fl) b with None => True | Some f => P f end). - induction fl; simpl; intros. auto. - apply IHfl. eauto with coqlib. unfold find_funct_ptr; simpl. - destruct a as [id' f']; simpl. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b (genv_nextfun ge)). - apply PROP with id'. apply H. auto with coqlib. - assumption. - - unfold globalenv. rewrite add_variables_same_funs. intro. - exploit (H p.(prog_funct) empty_genv). auto with coqlib. - unfold find_funct_ptr; simpl. rewrite ZMap.gi. auto. - rewrite H0. auto. + intros. exploit find_funct_ptr_inversion; eauto. intros [id IN]. eauto. Qed. Theorem find_funct_prop: forall (P: F -> Prop) p v f, - (forall id f, In (id, f) (prog_funct p) -> P f) -> + (forall id f, In (id, Gfun f) (prog_defs p) -> P f) -> find_funct (globalenv p) v = Some f -> P f. Proof. - intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. - rewrite find_funct_find_funct_ptr in H0. - eapply find_funct_ptr_prop; eauto. -Qed. - -Theorem find_funct_ptr_inversion: - forall p b f, - find_funct_ptr (globalenv p) b = Some f -> - exists id, In (id, f) (prog_funct p). -Proof. - intros. pattern f. apply find_funct_ptr_prop with p b; auto. - intros. exists id; auto. -Qed. - -Theorem find_funct_inversion: - forall p v f, - find_funct (globalenv p) v = Some f -> - exists id, In (id, f) (prog_funct p). -Proof. - intros. pattern f. apply find_funct_prop with p v; auto. - intros. exists id; auto. -Qed. - -Theorem find_funct_ptr_negative: - forall p b f, - find_funct_ptr (globalenv p) b = Some f -> b < 0. -Proof. - unfold find_funct_ptr. intros. destruct (globalenv p). simpl in H. - exploit genv_funs_range0; eauto. omega. -Qed. - -Theorem find_var_info_positive: - forall p b v, - find_var_info (globalenv p) b = Some v -> b > 0. -Proof. - unfold find_var_info. intros. destruct (globalenv p). simpl in H. - exploit genv_vars_range0; eauto. omega. -Qed. - -Remark add_variables_symb_neg: - forall id b vl ge, - find_symbol (add_variables ge vl) id = Some b -> b < 0 -> - find_symbol ge id = Some b. -Proof. - induction vl; simpl; intros. auto. - exploit IHvl; eauto. unfold find_symbol; simpl. rewrite PTree.gsspec. - fold ident. destruct (peq id (a#1)); auto. intros. inv H1. - generalize (genv_nextvar_pos ge). intros. omegaContradiction. + intros. exploit find_funct_inversion; eauto. intros [id IN]. eauto. Qed. Theorem find_funct_ptr_symbol_inversion: forall p id b f, find_symbol (globalenv p) id = Some b -> find_funct_ptr (globalenv p) b = Some f -> - In (id, f) p.(prog_funct). -Proof. - intros until f. - - assert (forall fl ge, - find_symbol (add_functions ge fl) id = Some b -> - find_funct_ptr (add_functions ge fl) b = Some f -> - In (id, f) fl \/ (find_symbol ge id = Some b /\ find_funct_ptr ge b = Some f)). - induction fl; simpl; intros. + In (id, Gfun f) p.(prog_defs). +Proof. + intros until f. unfold globalenv, find_symbol, find_funct_ptr. apply add_globals_preserves. +(* preserves *) + intros. simpl in *. rewrite PTree.gsspec in H1. destruct (peq id id0). + inv H1. destruct g as [f1|v1]. rewrite ZMap.gss in H2. inv H2. auto. + exploit genv_funs_range; eauto. intros. omegaContradiction. + destruct g as [f1|v1]. rewrite ZMap.gso in H2. auto. + exploit genv_symb_range; eauto. unfold ZIndexed.t; omega. auto. - exploit IHfl; eauto. intros [A | [A B]]. auto. - destruct a as [id' f']. - unfold find_symbol in A; simpl in A. - unfold find_funct_ptr in B; simpl in B. - rewrite PTree.gsspec in A. destruct (peq id id'). inv A. - rewrite ZMap.gss in B. inv B. auto. - rewrite ZMap.gso in B. right; auto. - exploit genv_symb_range; eauto. unfold block, ZIndexed.t; omega. - - intros. assert (b < 0) by (eapply find_funct_ptr_negative; eauto). - unfold globalenv in *. rewrite add_variables_same_funs in H1. - exploit (H (prog_funct p) empty_genv). - eapply add_variables_symb_neg; eauto. auto. - intuition. unfold find_symbol in H3; simpl in H3. rewrite PTree.gempty in H3. discriminate. +(* initial *) + intros. simpl in *. rewrite PTree.gempty in H. discriminate. Qed. Theorem find_symbol_not_nullptr: @@ -553,7 +408,7 @@ Theorem find_symbol_not_nullptr: find_symbol (globalenv p) id = Some b -> b <> Mem.nullptr. Proof. intros until b. unfold find_symbol. destruct (globalenv p); simpl. - intros. exploit genv_symb_range0; eauto. intuition. + intros. exploit genv_symb_range0; eauto. unfold Mem.nullptr, block. omega. Qed. Theorem global_addresses_distinct: @@ -599,6 +454,16 @@ Proof. congruence. Qed. +Remark genv_next_add_globals: + forall gl ge, + genv_next (add_globals ge gl) = genv_next ge + Z_of_nat (length gl). +Proof. + induction gl; intros. + simpl. unfold block; omega. + simpl add_globals; simpl length; rewrite inj_S. + rewrite IHgl. simpl. unfold block; omega. +Qed. + (** * Construction of the initial memory state *) Section INITMEM. @@ -622,6 +487,18 @@ Proof. destruct i; simpl; try omega. generalize (Zle_max_r z 0). omega. Qed. +Function store_zeros (m: mem) (b: block) (p: Z) (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 p Vzero with + | Some m' => store_zeros m' b (p + 1) n' + | None => None + end. +Proof. + intros. red. omega. + apply Zwf_well_founded. +Qed. + Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option mem := match id with | Init_int8 n => Mem.store Mint8unsigned m b p (Vint n) @@ -648,18 +525,6 @@ 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 @@ -671,37 +536,54 @@ Definition perm_globvar (gv: globvar V) : permission := 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 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 m2 => - match store_init_data_list m2 b 0 init with +Definition alloc_global (m: mem) (idg: ident * globdef F V): option mem := + match idg with + | (id, Gfun f) => + let (m1, b) := Mem.alloc m 0 1 in + Mem.drop_perm m1 b 0 1 Nonempty + | (id, Gvar v) => + let init := v.(gvar_init) in + let sz := init_data_list_size init in + let (m1, b) := Mem.alloc m 0 sz in + match store_zeros m1 b 0 sz with | None => None - | Some m3 => Mem.drop_perm m3 b 0 sz (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 v) + end end end. -Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V)) - {struct vl} : option mem := - match vl with +Fixpoint alloc_globals (m: mem) (gl: list (ident * globdef F V)) + {struct gl} : option mem := + match gl with | nil => Some m - | v :: vl' => - match alloc_variable m v with + | g :: gl' => + match alloc_global m g with | None => None - | Some m' => alloc_variables m' vl' + | Some m' => alloc_globals m' gl' end end. -Lemma alloc_variables_app : forall vl1 vl2 m m1, - alloc_variables m vl1 = Some m1 -> - alloc_variables m1 vl2 = alloc_variables m (vl1 ++ vl2). +Lemma alloc_globals_app : forall gl1 gl2 m m1, + alloc_globals m gl1 = Some m1 -> + alloc_globals m1 gl2 = alloc_globals m (gl1 ++ gl2). +Proof. + induction gl1. + simpl. intros. inversion H; subst. auto. + simpl. intros. destruct (alloc_global m a); eauto. inversion H. +Qed. + +(** Next-block properties *) + +Remark store_zeros_nextblock: + forall m b p n m', store_zeros m b p n = Some m' -> Mem.nextblock m' = Mem.nextblock m. Proof. - induction vl1. - simpl. intros. inversion H; subst. auto. - simpl. intros. destruct (alloc_variable m a); eauto. inversion H. + intros until n. functional induction (store_zeros m b p n); intros. + inv H; auto. + rewrite IHo; eauto with mem. + congruence. Qed. Remark store_init_data_list_nextblock: @@ -714,71 +596,52 @@ Proof. caseEq (store_init_data m b p a); try congruence. intros. transitivity (Mem.nextblock m0). eauto. destruct a; simpl in H; try (eapply Mem.nextblock_store; eauto; fail). - congruence. - 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. + destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto. Qed. -Remark alloc_variable_nextblock: - forall v m m', - alloc_variable m v = Some m' -> +Remark alloc_global_nextblock: + forall g m m', + alloc_global m g = Some m' -> Mem.nextblock m' = Zsucc(Mem.nextblock m). Proof. - unfold alloc_variable. - intros until m'. - set (init := gvar_init v#2). - 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 v#2)); try congruence. intros m4 DROP REC. - inv REC; subst. - rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ STORE). - rewrite (store_zeros_nextblock _ _ _ STZ). - rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). - auto. -Qed. - - -Remark alloc_variables_nextblock: - forall vl m m', - alloc_variables m vl = Some m' -> - Mem.nextblock m' = Mem.nextblock m + Z_of_nat(List.length vl). -Proof. - induction vl. + unfold alloc_global. intros. + destruct g as [id [f|v]]. + (* function *) + destruct (Mem.alloc m 0 1) as [m1 b]_eqn. + erewrite Mem.nextblock_drop; eauto. erewrite Mem.nextblock_alloc; eauto. + (* variable *) + set (init := gvar_init v) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m1 b]_eqn. + destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate. + destruct (store_init_data_list m2 b 0 init) as [m3|]_eqn; try discriminate. + erewrite Mem.nextblock_drop; eauto. + erewrite store_init_data_list_nextblock; eauto. + erewrite store_zeros_nextblock; eauto. + erewrite Mem.nextblock_alloc; eauto. +Qed. + +Remark alloc_globals_nextblock: + forall gl m m', + alloc_globals m gl = Some m' -> + Mem.nextblock m' = Mem.nextblock m + Z_of_nat(List.length gl). +Proof. + induction gl. simpl; intros. inv H; unfold block; omega. - simpl length; rewrite inj_S; simpl. intros m m'. - unfold alloc_variable. - set (init := gvar_init a#2). - 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. + simpl length; rewrite inj_S; simpl; intros. + destruct (alloc_global m a) as [m1|]_eqn; try discriminate. + erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto. unfold block; omega. Qed. +(** Permissions *) Remark store_zeros_perm: - forall k prm b' q m b n m', - store_zeros m b n = Some m' -> + forall k prm b' q m b p n m', + store_zeros m b p n = Some m' -> (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. - intros until n. functional induction (store_zeros m b n); intros. + intros until n. functional induction (store_zeros m b p n); intros. inv H; tauto. destruct (IHo _ H); intros. split; eauto with mem. congruence. @@ -793,56 +656,74 @@ Proof. intros. inv H. tauto. caseEq (store_init_data m b p a); try congruence. intros. rewrite <- (IHidl _ _ _ _ H0). - destruct a; simpl in H; split; eauto with mem. - inv H; auto. inv H; auto. - destruct (find_symbol ge i); try congruence. eauto with mem. - destruct (find_symbol ge i); try congruence. eauto with mem. + assert (forall chunk v, + Mem.store chunk m b p v = Some m0 -> + (Mem.perm m b' q k prm <-> Mem.perm m0 b' q k prm)). + intros; split; eauto with mem. + destruct a; simpl in H; eauto. + inv H; tauto. + destruct (find_symbol ge i). eauto. discriminate. Qed. -Remark alloc_variables_perm: - forall k prm b' q vl m m', - alloc_variables m vl = Some m' -> +Remark alloc_global_perm: + forall k prm b' q idg m m', + alloc_global m idg = Some m' -> Mem.valid_block m b' -> (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. - induction vl. - simpl; intros. inv H. tauto. - intros until m'. simpl. unfold alloc_variable. - set (init := gvar_init a#2). - 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 VALID. + intros. destruct idg as [id [f|v]]; simpl in H. + (* function *) + destruct (Mem.alloc m 0 1) as [m1 b]_eqn. + assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem. + split; intros. + eapply Mem.perm_drop_3; eauto. eapply Mem.perm_alloc_1; eauto. + eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_drop_4; eauto. + (* variable *) + set (init := gvar_init v) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m1 b]_eqn. + destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate. + destruct (store_init_data_list m2 b 0 init) as [m3|]_eqn; try discriminate. assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem. - assert (VALID': Mem.valid_block m4 b'). - unfold Mem.valid_block. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ STORE). - rewrite (store_zeros_nextblock _ _ _ STZ). - change (Mem.valid_block m1 b'). eauto with mem. - rewrite <- (IHvl _ _ REC VALID'). split; intros. eapply Mem.perm_drop_3; eauto. - rewrite <- store_init_data_list_perm; [idtac|eauto]. - rewrite <- store_zeros_perm; [idtac|eauto]. - eauto with mem. - assert (Mem.perm m1 b' q k prm). - rewrite store_zeros_perm; [idtac|eauto]. - rewrite store_init_data_list_perm; [idtac|eauto]. - eapply Mem.perm_drop_4; eauto. - exploit Mem.perm_alloc_inv; eauto. rewrite zeq_false; auto. + erewrite <- store_init_data_list_perm; [idtac|eauto]. + erewrite <- store_zeros_perm; [idtac|eauto]. + eapply Mem.perm_alloc_1; eauto. + eapply Mem.perm_alloc_4; eauto. + erewrite store_zeros_perm; [idtac|eauto]. + erewrite store_init_data_list_perm; [idtac|eauto]. + eapply Mem.perm_drop_4; eauto. +Qed. + +Remark alloc_globals_perm: + forall k prm b' q gl m m', + alloc_globals m gl = Some m' -> + Mem.valid_block m b' -> + (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). +Proof. + induction gl. + simpl; intros. inv H. tauto. + simpl; intros. destruct (alloc_global m a) as [m1|]_eqn; try discriminate. + erewrite alloc_global_perm; eauto. eapply IHgl; eauto. + unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. omega. Qed. +(** Data preservation properties *) + 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. + forall m b p n m', + store_zeros m b p n = Some m' -> + forall chunk b' p', + b' <> b \/ p' + size_chunk chunk <= p \/ p + n <= p' -> + Mem.load chunk m' b' p' = Mem.load chunk m b' p'. Proof. - intros until n. functional induction (store_zeros m b n); intros. + intros until n. functional induction (store_zeros m b p n); intros. inv H; auto. - rewrite IHo; auto. eapply Mem.load_store_other; eauto. - inv H. + transitivity (Mem.load chunk m' b' p'). + apply IHo. auto. unfold block in *; omega. + eapply Mem.load_store_other; eauto. simpl. unfold block in *; omega. + discriminate. Qed. Remark store_init_data_list_outside: @@ -854,12 +735,12 @@ Remark store_init_data_list_outside: Proof. induction il; simpl. intros; congruence. - intros until m'. caseEq (store_init_data m b p a); try congruence. - intros m1 A B chunk b' q C. transitivity (Mem.load chunk m1 b' q). + intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence. + transitivity (Mem.load chunk m1 b' q). eapply IHil; eauto. generalize (init_data_size_pos a). intuition omega. - destruct a; simpl in A; + destruct a; simpl in Heqo; try (eapply Mem.load_store_other; eauto; intuition; fail). - congruence. + inv Heqo. auto. destruct (find_symbol ge i); try congruence. eapply Mem.load_store_other; eauto; intuition. Qed. @@ -904,10 +785,9 @@ Proof. induction il; simpl. auto. - intros until m'. caseEq (store_init_data m b p a); try congruence. - intros m1 B C. + intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence. exploit IHil; eauto. intro D. - destruct a; simpl in B; intuition. + destruct a; simpl in Heqo; intuition. eapply (A Mint8unsigned (Vint i)); eauto. eapply (A Mint16unsigned (Vint i)); eauto. eapply (A Mint32 (Vint i)); eauto. @@ -917,36 +797,49 @@ Proof. eapply (A Mint32 (Vptr b0 i0)); eauto. Qed. -Remark load_alloc_variables: - forall chunk b p vl m m', - alloc_variables m vl = Some m' -> +Remark load_alloc_global: + forall chunk b p id g m m', + alloc_global m (id, g) = Some m' -> Mem.valid_block m b -> Mem.load chunk m' b p = Mem.load chunk m b p. Proof. - induction vl; simpl; intros until m'. - congruence. - unfold alloc_variable. - set (init := gvar_init a#2). - 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 m4 b p). - apply IHvl; auto. red. - rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - 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 m3 b p). + intros. destruct g as [f|v]; simpl in H. + (* function *) + destruct (Mem.alloc m 0 1) as [m1 b']_eqn. + assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem. + transitivity (Mem.load chunk m1 b p). eapply Mem.load_drop; eauto. + eapply Mem.load_alloc_unchanged; eauto. + (* variable *) + set (init := gvar_init v) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m1 b']_eqn. + destruct (store_zeros m1 b' 0 sz) as [m2|]_eqn; try discriminate. + destruct (store_init_data_list m2 b' 0 init) as [m3|]_eqn; try discriminate. + assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem. + 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. + eapply store_init_data_list_outside; eauto. transitivity (Mem.load chunk m1 b p). eapply store_zeros_outside; eauto. eapply Mem.load_alloc_unchanged; eauto. -Qed. +Qed. + +Remark load_alloc_globals: + forall chunk b p gl m m', + alloc_globals m gl = Some m' -> + Mem.valid_block m b -> + Mem.load chunk m' b p = Mem.load chunk m b p. +Proof. + induction gl; simpl; intros. + congruence. + destruct (alloc_global m a) as [m''|]_eqn; try discriminate. + transitivity (Mem.load chunk m'' b p). + apply IHgl; auto. unfold Mem.valid_block in *. + erewrite alloc_global_nextblock; eauto. omega. + destruct a as [id g]. eapply load_alloc_global; eauto. +Qed. Remark load_store_init_data_invariant: forall m m' b, @@ -967,114 +860,147 @@ Definition variables_initialized (g: t) (m: mem) := 0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p) /\ (gv.(gvar_volatile) = false -> load_store_init_data m b 0 gv.(gvar_init)). -Lemma alloc_variable_initialized: - forall g m id v m', - genv_nextvar g = Mem.nextblock m -> - alloc_variable m (id, v) = Some m' -> - variables_initialized g m -> - variables_initialized (add_variable g (id, v)) m' - /\ genv_nextvar (add_variable g (id,v)) = Mem.nextblock m'. -Proof. - intros. revert H0. unfold alloc_variable. simpl. - set (il := gvar_init v). - set (sz := init_data_list_size il). - caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC. - caseEq (store_zeros m1 b1 sz); try congruence. intros m2 ZEROS. - caseEq (store_init_data_list m2 b1 0 il); try congruence. intros m3 INIT DROP. - exploit Mem.nextblock_alloc; eauto. intros NB1. - assert (Mem.nextblock m' = Mem.nextblock m1). - rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ INIT). - eapply store_zeros_nextblock; eauto. - exploit Mem.alloc_result; eauto. intro RES. - split. - (* var-init *) - red; intros. revert H2. - unfold add_variable, find_var_info; simpl. - rewrite H; rewrite <- RES. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b b1); intros VI. - (* new var *) - injection VI; intro EQ. subst b gv. clear VI. - fold il. fold sz. - split. red; intros. eapply Mem.perm_drop_1; eauto. - split. intros. - assert (0 <= ofs < sz). - eapply Mem.perm_alloc_3; eauto. - rewrite store_zeros_perm; [idtac|eauto]. - rewrite store_init_data_list_perm; [idtac|eauto]. - eapply Mem.perm_drop_4; eauto. - split; auto. eapply Mem.perm_drop_2; eauto. +Definition functions_initialized (g: t) (m: mem) := + forall b fd, + find_funct_ptr g b = Some fd -> + Mem.perm m b 0 Cur Nonempty + /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p). + +Lemma alloc_global_initialized: + forall ge m id g m', + genv_next ge = Mem.nextblock m -> + alloc_global m (id, g) = Some m' -> + variables_initialized ge m -> + functions_initialized ge m -> + variables_initialized (add_global ge (id, g)) m' + /\ functions_initialized (add_global ge (id, g)) m' + /\ genv_next (add_global ge (id, g)) = Mem.nextblock m'. +Proof. intros. - apply load_store_init_data_invariant with m3. - intros. eapply Mem.load_drop; eauto. right; right; right. - unfold perm_globvar. destruct (gvar_volatile v); try discriminate. - destruct (gvar_readonly v); auto with mem. + exploit alloc_global_nextblock; eauto. intros NB. split. +(* variables-initialized *) + destruct g as [f|v]. +(* function *) + red; intros. unfold find_var_info in H3. simpl in H3. + exploit H1; eauto. intros [A [B C]]. + assert (D: Mem.valid_block m b). + red. exploit genv_vars_range; eauto. rewrite H; omega. + split. red; intros. erewrite <- alloc_global_perm; eauto. + split. intros. eapply B. erewrite alloc_global_perm; eauto. + intros. apply load_store_init_data_invariant with m; auto. + intros. eapply load_alloc_global; eauto. +(* variable *) + red; intros. unfold find_var_info in H3. simpl in H3. rewrite ZMap.gsspec in H3. + destruct (ZIndexed.eq b (genv_next ge0)). + (* same *) + inv H3. simpl in H0. + set (init := gvar_init gv) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m1 b']_eqn. + destruct (store_zeros m1 b' 0 sz) as [m2|]_eqn; try discriminate. + destruct (store_init_data_list m2 b' 0 init) as [m3|]_eqn; try discriminate. + exploit Mem.alloc_result; eauto. intro RES. + replace (genv_next ge0) with b' by congruence. + split. red; intros. eapply Mem.perm_drop_1; eauto. + split. intros. + assert (0 <= ofs < sz). + eapply Mem.perm_alloc_3; eauto. + erewrite store_zeros_perm; [idtac|eauto]. + erewrite store_init_data_list_perm; [idtac|eauto]. + eapply Mem.perm_drop_4; eauto. + split. auto. eapply Mem.perm_drop_2; eauto. + intros. apply load_store_init_data_invariant with m3. + intros. eapply Mem.load_drop; eauto. + right; right; right. unfold perm_globvar. rewrite H3. + destruct (gvar_readonly gv); auto with mem. eapply store_init_data_list_charact; eauto. - (* older vars *) + (* older var *) exploit H1; eauto. intros [A [B C]]. - split. red; intros. eapply Mem.perm_drop_3; eauto. - rewrite <- store_init_data_list_perm; [idtac|eauto]. - rewrite <- store_zeros_perm; [idtac|eauto]. - eapply Mem.perm_alloc_1; eauto. - split. intros. eapply B. - eapply Mem.perm_alloc_4; eauto. - rewrite store_zeros_perm; [idtac|eauto]. - rewrite store_init_data_list_perm; [idtac|eauto]. - eapply Mem.perm_drop_4; eauto. - intros. apply load_store_init_data_invariant with m; auto. - intros. transitivity (Mem.load chunk m3 b ofs). - eapply Mem.load_drop; eauto. - transitivity (Mem.load chunk m2 b ofs). - eapply store_init_data_list_outside; eauto. - transitivity (Mem.load chunk m1 b ofs). - eapply store_zeros_outside; eauto. - eapply Mem.load_alloc_unchanged; eauto. - red. exploit genv_vars_range; eauto. rewrite <- H. omega. - rewrite H0; rewrite NB1; rewrite H; auto. -Qed. - -Lemma alloc_variables_initialized: - forall vl g m m', - genv_nextvar g = Mem.nextblock m -> - alloc_variables m vl = Some m' -> - variables_initialized g m -> - variables_initialized (add_variables g vl) m'. -Proof. - induction vl; simpl; intros. + assert (D: Mem.valid_block m b). + red. exploit genv_vars_range; eauto. rewrite H; omega. + split. red; intros. erewrite <- alloc_global_perm; eauto. + split. intros. eapply B. erewrite alloc_global_perm; eauto. + intros. apply load_store_init_data_invariant with m; auto. + intros. eapply load_alloc_global; eauto. +(* functions-initialized *) + split. destruct g as [f|v]. +(* function *) + red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite ZMap.gsspec in H3. + destruct (ZIndexed.eq b (genv_next ge0)). + (* same *) + inv H3. simpl in H0. + destruct (Mem.alloc m 0 1) as [m1 b']_eqn. + exploit Mem.alloc_result; eauto. intro RES. + replace (genv_next ge0) with b' by congruence. + split. eapply Mem.perm_drop_1; eauto. omega. + intros. + assert (0 <= ofs < 1). + eapply Mem.perm_alloc_3; eauto. + eapply Mem.perm_drop_4; eauto. + split. omega. eapply Mem.perm_drop_2; eauto. + (* older function *) + exploit H2; eauto. intros [A B]. + assert (D: Mem.valid_block m b). + red. exploit genv_funs_range; eauto. rewrite H; omega. + split. erewrite <- alloc_global_perm; eauto. + intros. eapply B. erewrite alloc_global_perm; eauto. +(* variables *) + red; intros. unfold find_funct_ptr in H3. simpl in H3. + exploit H2; eauto. intros [A B]. + assert (D: Mem.valid_block m b). + red. exploit genv_funs_range; eauto. rewrite H; omega. + split. erewrite <- alloc_global_perm; eauto. + intros. eapply B. erewrite alloc_global_perm; eauto. +(* nextblock *) + rewrite NB. simpl. rewrite H. unfold block; omega. +Qed. + +Lemma alloc_globals_initialized: + forall gl ge m m', + genv_next ge = Mem.nextblock m -> + alloc_globals m gl = Some m' -> + variables_initialized ge m -> + functions_initialized ge m -> + variables_initialized (add_globals ge gl) m' /\ functions_initialized (add_globals ge gl) m'. +Proof. + induction gl; simpl; intros. inv H0; auto. - destruct (alloc_variable m a) as [m1|]_eqn; try discriminate. - destruct a as [id gv]. - exploit alloc_variable_initialized; eauto. intros [P Q]. - eapply IHvl; eauto. + destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|]_eqn; try discriminate. + exploit alloc_global_initialized; eauto. intros [P [Q R]]. + eapply IHgl; eauto. Qed. End INITMEM. Definition init_mem (p: program F V) := - alloc_variables (globalenv p) Mem.empty p.(prog_vars). + alloc_globals (globalenv p) Mem.empty p.(prog_defs). + +Lemma init_mem_genv_next: forall p m, + init_mem p = Some m -> + genv_next (globalenv p) = Mem.nextblock 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). + fold (globalenv p). simpl genv_next. intros. congruence. +Qed. Theorem find_symbol_not_fresh: forall p id b m, init_mem p = Some m -> find_symbol (globalenv p) id = Some b -> Mem.valid_block m b. Proof. - unfold init_mem; intros. - exploit alloc_variables_nextblock; eauto. rewrite Mem.nextblock_empty. intro. - exploit genv_symb_range; eauto. intros. - generalize (add_variables_nextvar (prog_vars p) (add_functions empty_genv (prog_funct p))). - rewrite add_functions_nextvar. simpl genv_nextvar. intro. - red. rewrite H1. rewrite <- H3. intuition. + intros. red. erewrite <- init_mem_genv_next; eauto. + exploit genv_symb_range; eauto. omega. Qed. -Lemma init_mem_genv_vars : forall p m, - init_mem p = Some m -> - genv_nextvar (globalenv p) = Mem.nextblock m. +Theorem find_funct_ptr_not_fresh: + forall p b f m, + init_mem p = Some m -> + find_funct_ptr (globalenv p) b = Some f -> Mem.valid_block m b. Proof. - clear. unfold globalenv, init_mem. intros. - exploit alloc_variables_nextblock; eauto. - simpl (Mem.nextblock Mem.empty). - rewrite add_variables_nextvar. rewrite add_functions_nextvar. - simpl (genv_nextvar empty_genv). auto. + intros. red. erewrite <- init_mem_genv_next; eauto. + exploit genv_funs_range; eauto. omega. Qed. Theorem find_var_info_not_fresh: @@ -1082,12 +1008,8 @@ Theorem find_var_info_not_fresh: init_mem p = Some m -> find_var_info (globalenv p) b = Some gv -> Mem.valid_block m b. Proof. - unfold init_mem; intros. - exploit alloc_variables_nextblock; eauto. rewrite Mem.nextblock_empty. intro. - exploit genv_vars_range; eauto. intros. - generalize (add_variables_nextvar (prog_vars p) (add_functions empty_genv (prog_funct p))). - rewrite add_functions_nextvar. simpl genv_nextvar. intro. - red. rewrite H1. rewrite <- H3. intuition. + intros. red. erewrite <- init_mem_genv_next; eauto. + exploit genv_vars_range; eauto. omega. Qed. Theorem init_mem_characterization: @@ -1099,10 +1021,23 @@ Theorem init_mem_characterization: 0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p) /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)). Proof. - intros. eapply alloc_variables_initialized; eauto. - rewrite add_functions_nextvar; auto. - red; intros. exploit genv_vars_range; eauto. rewrite add_functions_nextvar. - simpl. intros. omegaContradiction. + intros. eapply alloc_globals_initialized; eauto. + rewrite Mem.nextblock_empty. auto. + red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction. + red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction. +Qed. + +Theorem init_mem_characterization_2: + forall p b fd m, + find_funct_ptr (globalenv p) b = Some fd -> + init_mem p = Some m -> + Mem.perm m b 0 Cur Nonempty + /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p). +Proof. + intros. unfold init_mem in H0. eapply alloc_globals_initialized; eauto. + rewrite Mem.nextblock_empty. auto. + red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction. + red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction. Qed. (** ** Compatibility with memory injections *) @@ -1113,6 +1048,19 @@ Variable ge: t. Variable thr: block. Hypothesis symb_inject: forall id b, find_symbol ge id = Some b -> b < thr. +Lemma store_zeros_neutral: + forall m b p n m', + Mem.inject_neutral thr m -> + b < thr -> + store_zeros m b p n = Some m' -> + Mem.inject_neutral thr m'. +Proof. + intros until n. functional induction (store_zeros m b p n); intros. + inv H1; auto. + apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor. + inv H1. +Qed. + Lemma store_init_data_neutral: forall m b p id m', Mem.inject_neutral thr m -> @@ -1122,7 +1070,7 @@ Lemma store_init_data_neutral: Proof. intros. destruct id; simpl in H1; try (eapply Mem.store_inject_neutral; eauto; fail). - inv H1; auto. + congruence. revert H1. caseEq (find_symbol ge i); try congruence. intros b' FS ST. eapply Mem.store_inject_neutral; eauto. econstructor. unfold Mem.flat_inj. apply zlt_true; eauto. @@ -1143,54 +1091,46 @@ 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' -> +Lemma alloc_global_neutral: + forall idg m m', + alloc_global ge m idg = Some m' -> Mem.inject_neutral thr m -> Mem.nextblock m < thr -> Mem.inject_neutral thr m'. Proof. - 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. + intros. destruct idg as [id [f|v]]; simpl in H. + (* function *) + destruct (Mem.alloc m 0 1) as [m1 b]_eqn. + assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. + eapply Mem.drop_inject_neutral; eauto. + eapply Mem.alloc_inject_neutral; eauto. + (* variable *) + set (init := gvar_init v) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m1 b]_eqn. + destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate. + destruct (store_init_data_list ge m2 b 0 init) as [m3|]_eqn; try discriminate. + assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. eapply Mem.drop_inject_neutral; eauto. 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. Qed. -Lemma alloc_variables_neutral: - forall idl m m', - alloc_variables ge m idl = Some m' -> +Lemma alloc_globals_neutral: + forall gl m m', + alloc_globals ge m gl = Some m' -> Mem.inject_neutral thr m -> Mem.nextblock m' <= thr -> Mem.inject_neutral thr m'. Proof. - induction idl; simpl. + induction gl; simpl. intros. congruence. - intros until m'. caseEq (alloc_variable ge m a); try congruence. intros. - assert (Mem.nextblock m' = Mem.nextblock m + Z_of_nat(length (a :: idl))). - eapply alloc_variables_nextblock with ge. simpl. rewrite H. auto. + intros until m'. caseEq (alloc_global ge m a); try congruence. intros. + assert (Mem.nextblock m' = Mem.nextblock m + Z_of_nat(length (a :: gl))). + eapply alloc_globals_nextblock with ge. simpl. rewrite H. auto. simpl length in H3. rewrite inj_S in H3. - exploit alloc_variable_neutral; eauto. unfold block in *; omega. + exploit alloc_global_neutral; eauto. unfold block in *; omega. Qed. End INITMEM_INJ. @@ -1202,7 +1142,7 @@ Theorem initmem_inject: Proof. unfold init_mem; intros. apply Mem.neutral_inject. - eapply alloc_variables_neutral; eauto. + eapply alloc_globals_neutral; eauto. intros. exploit find_symbol_not_fresh; eauto. apply Mem.empty_inject_neutral. omega. @@ -1213,6 +1153,22 @@ Section INITMEM_AUGMENT_INJ. Variable ge: t. Variable thr: block. +Lemma store_zeros_augment: + forall m1 m2 b p n m2', + Mem.inject (Mem.flat_inj thr) m1 m2 -> + b >= thr -> + store_zeros m2 b p n = Some m2' -> + Mem.inject (Mem.flat_inj thr) m1 m2'. +Proof. + intros until n. functional induction (store_zeros m2 b p n); intros. + inv H1; auto. + apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. + intros. exfalso. unfold Mem.flat_inj in H2. destruct (zlt b' thr). + inversion H2; subst; omega. + discriminate. + inv H1. +Qed. + Lemma store_init_data_augment: forall m1 m2 b p id m2', Mem.inject (Mem.flat_inj thr) m1 m2 -> @@ -1228,7 +1184,7 @@ Proof. intros. unfold Mem.flat_inj in H0. destruct (zlt b' thr); inversion H0; subst. omega. destruct id; simpl in ST; try (eapply P; eauto; fail). - inv ST; auto. + congruence. revert ST. caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. Qed. @@ -1246,59 +1202,49 @@ Proof. eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto. Qed. -Lemma store_zeros_augment: - forall m1 m2 b n m2', - Mem.inject (Mem.flat_inj thr) m1 m2 -> - b >= thr -> - store_zeros m2 b n = Some m2' -> - Mem.inject (Mem.flat_inj thr) m1 m2'. -Proof. - intros until n. functional induction (store_zeros m2 b n); intros. - inv H1; auto. - apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. - intros. exfalso. unfold Mem.flat_inj in H2. destruct (zlt b' thr). - inversion H2; subst; omega. - discriminate. - inv H1. -Qed. - -Lemma alloc_variable_augment: - forall id m1 m2 m2', - alloc_variable ge m2 id = Some m2' -> +Lemma alloc_global_augment: + forall idg m1 m2 m2', + alloc_global ge m2 idg = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2 -> Mem.nextblock m2 >= thr -> Mem.inject (Mem.flat_inj thr) m1 m2'. Proof. - intros until m2'. unfold alloc_variable. - set (sz := init_data_list_size (gvar_init id#2)). - caseEq (Mem.alloc m2 0 sz); try congruence. intros m3 b ALLOC. - caseEq (store_zeros m3 b sz); try congruence. intros m4 STZ. - caseEq (store_init_data_list ge m4 b 0 (gvar_init id#2)); try congruence. - intros m5 STORE DROP INJ NEXT. - assert (b >= thr). - pose proof (Mem.fresh_block_alloc _ _ _ _ _ ALLOC). - unfold Mem.valid_block in H. unfold block in *; omega. - eapply Mem.drop_outside_inject. 2: eauto. - eapply store_init_data_list_augment. 2: eauto. 2: eauto. - eapply store_zeros_augment. 2: eauto. 2: eauto. - eapply Mem.alloc_right_inject; eauto. - intros. unfold Mem.flat_inj in H0. destruct (zlt b' thr); inversion H0. + intros. destruct idg as [id [f|v]]; simpl in H. + (* function *) + destruct (Mem.alloc m2 0 1) as [m3 b]_eqn. + assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. + eapply Mem.drop_outside_inject. 2: eauto. + eapply Mem.alloc_right_inject; eauto. + intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3. + subst; exfalso; omega. + (* variable *) + set (init := gvar_init v) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m2 0 sz) as [m3 b]_eqn. + destruct (store_zeros m3 b 0 sz) as [m4|]_eqn; try discriminate. + destruct (store_init_data_list ge m4 b 0 init) as [m5|]_eqn; try discriminate. + assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. + eapply Mem.drop_outside_inject. 2: eauto. + eapply store_init_data_list_augment. 3: eauto. 2: eauto. + eapply store_zeros_augment. 3: eauto. 2: eauto. + eapply Mem.alloc_right_inject; eauto. + intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3. subst; exfalso; omega. Qed. -Lemma alloc_variables_augment: - forall idl m1 m2 m2', - alloc_variables ge m2 idl = Some m2' -> +Lemma alloc_globals_augment: + forall gl m1 m2 m2', + alloc_globals ge m2 gl = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2 -> Mem.nextblock m2 >= thr -> Mem.inject (Mem.flat_inj thr) m1 m2'. Proof. - induction idl; simpl. + induction gl; simpl. intros. congruence. - intros until m2'. caseEq (alloc_variable ge m2 a); try congruence. intros. - eapply IHidl with (m2 := m); eauto. - eapply alloc_variable_augment; eauto. - rewrite (alloc_variable_nextblock _ _ _ H). + intros until m2'. caseEq (alloc_global ge m2 a); try congruence. intros. + eapply IHgl with (m2 := m); eauto. + eapply alloc_global_augment; eauto. + rewrite (alloc_global_nextblock _ _ _ H). unfold block in *; omega. Qed. @@ -1321,216 +1267,156 @@ Inductive match_globvar: globvar V -> globvar W -> Prop := match_varinfo info1 info2 -> match_globvar (mkglobvar info1 init ro vo) (mkglobvar info2 init ro vo). -Record match_genvs (new_functs : list (ident * B)) (new_vars : list (ident * globvar W)) +Record match_genvs (new_globs : list (ident * globdef B W)) (ge1: t A V) (ge2: t B W): Prop := { - mge_nextfun: genv_nextfun ge2 = genv_nextfun ge1 - Z_of_nat(length new_functs); - mge_nextvar: genv_nextvar ge2 = genv_nextvar ge1 + Z_of_nat(length new_vars); - mge_symb: forall id, ~ In id ((funct_names new_functs) ++ (var_names new_vars)) -> + mge_next: + genv_next ge2 = genv_next ge1 + Z_of_nat(length new_globs); + mge_symb: + forall id, ~ In id (map fst new_globs) -> PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1); mge_funs: forall b f, ZMap.get b (genv_funs ge1) = Some f -> exists tf, ZMap.get b (genv_funs ge2) = Some tf /\ match_fun f tf; mge_rev_funs: forall b tf, ZMap.get b (genv_funs ge2) = Some tf -> - if zlt (genv_nextfun ge1) b then + if zlt b (genv_next ge1) then exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf else - In tf (map (@snd ident B) new_functs); + In (Gfun tf) (map snd new_globs); mge_vars: forall b v, ZMap.get b (genv_vars ge1) = Some v -> exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_globvar v tv; mge_rev_vars: forall b tv, ZMap.get b (genv_vars ge2) = Some tv -> - if zlt b (genv_nextvar ge1) then + if zlt b (genv_next ge1) then exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv else - In tv (map (@snd ident (globvar W)) new_vars) + In (Gvar tv) (map snd new_globs) }. -Lemma add_function_match: - forall ge1 ge2 id f1 f2, - match_genvs nil nil ge1 ge2 -> - match_fun f1 f2 -> - match_genvs nil nil (add_function ge1 (id, f1)) (add_function ge2 (id, f2)). +Lemma add_global_match: + forall ge1 ge2 idg1 idg2, + match_genvs nil ge1 ge2 -> + match_globdef match_fun match_varinfo idg1 idg2 -> + match_genvs nil (add_global ge1 idg1) (add_global ge2 idg2). Proof. intros. destruct H. - simpl in mge_nextfun0. rewrite Zminus_0_r in mge_nextfun0. - simpl in mge_nextvar0. rewrite Zplus_0_r in mge_nextvar0. - constructor; simpl. - rewrite Zminus_0_r. congruence. + simpl in mge_next0. rewrite Zplus_0_r in mge_next0. + inv H0. +(* two functions *) + constructor; simpl. rewrite Zplus_0_r. congruence. - intros. rewrite mge_nextfun0. - repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. - rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_nextfun ge1)). + intros. rewrite mge_next0. + repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. + rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. + destruct (ZIndexed.eq b (genv_next ge1)). exists f2; split; congruence. eauto. - rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_nextfun ge1)). - subst b. destruct (zlt (genv_nextfun ge1 - 1) (genv_nextfun ge1)). - exists f1; split; congruence. omega. - pose proof (mge_rev_funs0 b tf H). - destruct (zlt (genv_nextfun ge1) b); - destruct (zlt (genv_nextfun ge1 - 1) b). auto. omega. exfalso; omega. intuition. - auto. - auto. -Qed. - -Lemma add_functions_match: - forall fl1 fl2, list_forall2 (match_funct_entry match_fun) fl1 fl2 -> - forall ge1 ge2, match_genvs nil nil ge1 ge2 -> - match_genvs nil nil (add_functions ge1 fl1) (add_functions ge2 fl2). -Proof. - induction 1; intros; simpl. - auto. - destruct a1 as [id1 f1]; destruct b1 as [id2 f2]. - destruct H. subst. apply IHlist_forall2. apply add_function_match; auto. -Qed. - -Lemma add_function_augment_match: - forall new_functs new_vars ge1 ge2 id f2, - match_genvs new_functs new_vars ge1 ge2 -> - match_genvs (new_functs++((id,f2)::nil)) new_vars ge1 (add_function ge2 (id, f2)). -Proof. - intros. destruct H. constructor; simpl. - rewrite mge_nextfun0. rewrite app_length. - simpl. rewrite inj_plus. rewrite inj_S. rewrite inj_0. unfold block; omega. (* painful! *) - auto. - intros. unfold funct_names in H. rewrite map_app in H. rewrite in_app in H. rewrite in_app in H. simpl in H. - destruct (peq id id0). subst. intuition. rewrite PTree.gso. - apply mge_symb0. intro. apply H. rewrite in_app in H0. inversion H0; intuition. intuition. - intros. rewrite ZMap.gso. auto. - rewrite mge_nextfun0. pose proof (genv_funs_range ge1 b H). intro; subst; omega. - intros. rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b (genv_nextfun ge2)). - destruct (zlt (genv_nextfun ge1) b). - exfalso. rewrite mge_nextfun0 in e. unfold block; omega. - rewrite map_app. rewrite in_app. simpl. inversion H; intuition. - pose proof (mge_rev_funs0 b tf H). - destruct (zlt (genv_nextfun ge1) b). - auto. - rewrite map_app. rewrite in_app. intuition. - auto. - auto. -Qed. - - -Lemma add_functions_augment_match: - forall fl new_functs new_vars ge1 ge2, - match_genvs new_functs new_vars ge1 ge2 -> - match_genvs (new_functs++fl) new_vars ge1 (add_functions ge2 fl). -Proof. - induction fl; simpl. - intros. rewrite app_nil_r. auto. - intros. replace (new_functs ++ a :: fl) with ((new_functs ++ (a::nil)) ++ fl) - by (rewrite app_ass; auto). - apply IHfl. destruct a. apply add_function_augment_match. auto. -Qed. - - -Lemma add_variable_match: - forall new_functs ge1 ge2 id v1 v2, - match_genvs new_functs nil ge1 ge2 -> - match_globvar v1 v2 -> - match_genvs new_functs nil (add_variable ge1 (id, v1)) (add_variable ge2 (id, v2)). -Proof. - intros. destruct H. - simpl in mge_nextvar0. rewrite Zplus_0_r in mge_nextvar0. - constructor; simpl. - auto. - rewrite Zplus_0_r. rewrite mge_nextvar0. auto. - intros. rewrite mge_nextvar0. - repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. - auto. - auto. - rewrite mge_nextvar0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_nextvar ge1)). - exists v2; split; congruence. - eauto. - rewrite mge_nextvar0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_nextvar ge1)). - subst b. inversion H; subst. - destruct (zlt (genv_nextvar ge1) (genv_nextvar ge1 + 1)). - exists v1; split; congruence. omega. - pose proof (mge_rev_vars0 _ _ H). - destruct (zlt b (genv_nextvar ge1)); - destruct (zlt b (genv_nextvar ge1 + 1)). auto. omega. exfalso; omega. intuition. + rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. + destruct (ZIndexed.eq b (genv_next ge1)). + subst b. rewrite zlt_true. exists f1; split; congruence. omega. + pose proof (mge_rev_funs0 b tf H0). + destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + contradiction. + eauto. + intros. + pose proof (mge_rev_vars0 b tv H0). + destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + contradiction. +(* two variables *) + constructor; simpl. + rewrite Zplus_0_r. congruence. + intros. rewrite mge_next0. + repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. + eauto. + intros. + pose proof (mge_rev_funs0 b tf H0). + destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + contradiction. + rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. + destruct (ZIndexed.eq b (genv_next ge1)). + econstructor; split. eauto. inv H0. constructor; auto. + eauto. + rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. + destruct (ZIndexed.eq b (genv_next ge1)). + subst b. rewrite zlt_true. + econstructor; split. eauto. inv H0. constructor; auto. + omega. + pose proof (mge_rev_vars0 b tv H0). + destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + contradiction. Qed. -Lemma add_variables_match: - forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 -> - forall new_functs ge1 ge2, match_genvs new_functs nil ge1 ge2 -> - match_genvs new_functs nil (add_variables ge1 vl1) (add_variables ge2 vl2). +Lemma add_globals_match: + forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 -> + forall ge1 ge2, match_genvs nil ge1 ge2 -> + match_genvs nil (add_globals ge1 gl1) (add_globals ge2 gl2). Proof. induction 1; intros; simpl. auto. - inv H. apply IHlist_forall2. apply add_variable_match; auto. constructor; auto. + apply IHlist_forall2. apply add_global_match; auto. Qed. - -Lemma add_variable_augment_match: - forall ge1 new_functs new_vars ge2 id v2, - match_genvs new_functs new_vars ge1 ge2 -> - match_genvs new_functs (new_vars++((id,v2)::nil)) ge1 (add_variable ge2 (id, v2)). +Lemma add_global_augment_match: + forall new_globs ge1 ge2 idg, + match_genvs new_globs ge1 ge2 -> + match_genvs (new_globs ++ (idg :: nil)) ge1 (add_global ge2 idg). Proof. intros. destruct H. constructor; simpl. - auto. - rewrite mge_nextvar0. rewrite app_length. - simpl. rewrite inj_plus. rewrite inj_S. rewrite inj_0. unfold block; omega. (* painful! *) - intros. unfold funct_names, var_names in H. rewrite map_app in H. rewrite in_app in H. rewrite in_app in H. simpl in H. - destruct (peq id id0). subst. intuition. rewrite PTree.gso. - apply mge_symb0. intro. apply H. rewrite in_app in H0. inversion H0; intuition. intuition. - auto. - auto. - intros. rewrite ZMap.gso. auto. - rewrite mge_nextvar0. pose proof (genv_vars_range ge1 b H). intro; subst; omega. - intros. rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b (genv_nextvar ge2)). - destruct (zlt b (genv_nextvar ge1)). - exfalso. rewrite mge_nextvar0 in e. unfold block; omega. - rewrite map_app. rewrite in_app. simpl. inversion H; intuition. - pose proof (mge_rev_vars0 b tv H). - destruct (zlt b (genv_nextvar ge1)). - auto. - rewrite map_app. rewrite in_app. intuition. - -Qed. - -Lemma add_variables_augment_match: - forall vl ge1 new_functs new_vars ge2, - match_genvs new_functs new_vars ge1 ge2 -> - match_genvs new_functs (new_vars++vl) ge1 (add_variables ge2 vl). -Proof. - induction vl; simpl. + rewrite mge_next0. rewrite app_length. + simpl. rewrite inj_plus. change (Z_of_nat 1) with 1. unfold block; omega. + intros. rewrite map_app in H. rewrite in_app in H. simpl in H. + destruct (peq id idg#1). subst. intuition. rewrite PTree.gso. + apply mge_symb0. intuition. auto. + intros. destruct idg as [id1 [f1|v1]]; simpl; eauto. + rewrite ZMap.gso. eauto. exploit genv_funs_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega. + intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H. + rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)). + rewrite zlt_false. rewrite in_app. simpl; right; left. congruence. + subst b. rewrite mge_next0. omega. + exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto. + rewrite in_app. tauto. + exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto. + rewrite in_app. tauto. + intros. destruct idg as [id1 [f1|v1]]; simpl; eauto. + rewrite ZMap.gso. eauto. exploit genv_vars_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega. + intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H. + exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto. + rewrite in_app. tauto. + rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)). + rewrite zlt_false. rewrite in_app. simpl; right; left. congruence. + subst b. rewrite mge_next0. omega. + exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto. + rewrite in_app. tauto. +Qed. + +Lemma add_globals_augment_match: + forall gl new_globs ge1 ge2, + match_genvs new_globs ge1 ge2 -> + match_genvs (new_globs ++ gl) ge1 (add_globals ge2 gl). +Proof. + induction gl; simpl. intros. rewrite app_nil_r. auto. - intros. replace (new_vars ++ a :: vl) with ((new_vars ++ (a::nil)) ++ vl) - by (rewrite app_ass; auto). - apply IHvl. destruct a. apply add_variable_augment_match. auto. + intros. change (a :: gl) with ((a :: nil) ++ gl). rewrite <- app_ass. + apply IHgl. apply add_global_augment_match. auto. Qed. -Variable new_functs : list (ident * B). -Variable new_vars : list (ident * globvar W). +Variable new_globs : list (ident * globdef B W). Variable new_main : ident. Variable p: program A V. Variable p': program B W. Hypothesis progmatch: - match_program match_fun match_varinfo new_functs new_vars new_main p p'. + match_program match_fun match_varinfo new_globs new_main p p'. Lemma globalenvs_match: - match_genvs new_functs new_vars (globalenv p) (globalenv p'). -Proof. - unfold globalenv. destruct progmatch. clear progmatch. - destruct H as [tfuncts [P1 P2]]. destruct H0. clear H0. destruct H as [tvars [Q1 Q2]]. - rewrite P2. rewrite Q2. clear P2 Q2. - rewrite add_variables_app. - rewrite add_functions_app. - pattern new_vars at 1. replace new_vars with (nil++new_vars) by auto. - apply add_variables_augment_match. - apply add_variables_match; auto. - pattern new_functs at 1. replace new_functs with (nil++new_functs) by auto. - apply add_functions_augment_match. - apply add_functions_match; auto. + match_genvs new_globs (globalenv p) (globalenv p'). +Proof. + unfold globalenv. destruct progmatch as [[tglob [P Q]] R]. + rewrite Q. rewrite add_globals_app. + change new_globs with (nil ++ new_globs) at 1. + apply add_globals_augment_match. + apply add_globals_match; auto. constructor; simpl; auto; intros; rewrite ZMap.gi in H; congruence. Qed. @@ -1544,10 +1430,10 @@ Proof (mge_funs globalenvs_match). Theorem find_funct_ptr_rev_match: forall (b : block) (tf : B), find_funct_ptr (globalenv p') b = Some tf -> - if zlt (genv_nextfun (globalenv p)) b then + if zlt b (genv_next (globalenv p)) then exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf else - In tf (map (@snd ident B) new_functs). + In (Gfun tf) (map snd new_globs). Proof (mge_rev_funs globalenvs_match). Theorem find_funct_match: @@ -1565,13 +1451,13 @@ Theorem find_funct_rev_match: forall (v : val) (tf : B), find_funct (globalenv p') v = Some tf -> (exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf) - \/ (In tf (map (@snd ident B) new_functs)). + \/ (In (Gfun tf) (map snd new_globs)). Proof. intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. rewrite find_funct_find_funct_ptr in H. rewrite find_funct_find_funct_ptr. apply find_funct_ptr_rev_match in H. - destruct (zlt (genv_nextfun (globalenv p)) b); intuition. + destruct (zlt b (genv_next (globalenv p))); auto. Qed. Theorem find_var_info_match: @@ -1584,23 +1470,23 @@ Proof (mge_vars globalenvs_match). Theorem find_var_info_rev_match: forall (b : block) (tv : globvar W), find_var_info (globalenv p') b = Some tv -> - if zlt b (genv_nextvar (globalenv p)) then + if zlt b (genv_next (globalenv p)) then exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv else - In tv (map (@snd ident (globvar W)) new_vars). + In (Gvar tv) (map snd new_globs). Proof (mge_rev_vars globalenvs_match). Theorem find_symbol_match: forall (s : ident), - ~In s (funct_names new_functs ++ var_names new_vars) -> + ~In s (map fst new_globs) -> find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. intros. destruct globalenvs_match. unfold find_symbol. auto. Qed. Hypothesis new_ids_fresh : - (forall s', find_symbol (globalenv p) s' <> None -> - ~In s' (funct_names new_functs ++ var_names new_vars)). + forall s', find_symbol (globalenv p) s' <> None -> + ~In s' (map fst new_globs). Lemma store_init_data_list_match: forall idl m b ofs m', @@ -1611,46 +1497,43 @@ Proof. auto. assert (forall m', store_init_data (globalenv p) m b ofs a = Some m' -> store_init_data (globalenv p') m b ofs a = Some m'). - destruct a; simpl; auto. rewrite find_symbol_match. auto. - inversion H. case_eq (find_symbol (globalenv p) i). - intros. apply new_ids_fresh. intro. rewrite H0 in H2; inversion H2. - intro. rewrite H0 in H1. inversion H1. + destruct a; simpl; auto. rewrite find_symbol_match. auto. + simpl in H. destruct (find_symbol (globalenv p) i) as [b'|]_eqn; try discriminate. + apply new_ids_fresh. congruence. case_eq (store_init_data (globalenv p) m b ofs a); intros. rewrite H1 in H. pose proof (H0 _ H1). rewrite H2. auto. rewrite H1 in H. inversion H. Qed. -Lemma alloc_variables_match: - forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 -> +Lemma alloc_globals_match: + forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 -> forall m m', - alloc_variables (globalenv p) m vl1 = Some m' -> - alloc_variables (globalenv p') m vl2 = Some m'. + alloc_globals (globalenv p) m gl1 = Some m' -> + alloc_globals (globalenv p') m gl2 = Some m'. Proof. - induction 1; intros until m'; simpl. + induction 1; simpl; intros. auto. - 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. - case_eq (store_init_data_list (globalenv p) m1 b 0 init); intros m2 P. - rewrite (store_init_data_list_match _ _ _ _ P). - change (perm_globvar (mkglobvar info2 init ro vo)) - with (perm_globvar (mkglobvar info1 init ro vo)). - destruct (Mem.drop_perm m2 b 0 (init_data_list_size init) - (perm_globvar (mkglobvar info1 init ro vo))); auto. - inversion P. + destruct (alloc_global (globalenv p) m a1) as [m1|]_eqn; try discriminate. + assert (alloc_global (globalenv p') m b1 = Some m1). + inv H; simpl in *. + auto. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m2 b]_eqn. + destruct (store_zeros m2 b 0 sz) as [m3|]_eqn; try discriminate. + destruct (store_init_data_list (globalenv p) m3 b 0 init) as [m4|]_eqn; try discriminate. + erewrite store_init_data_list_match; eauto. + rewrite H2. eauto. Qed. Theorem init_mem_match: forall m, init_mem p = Some m -> - init_mem p' = alloc_variables (globalenv p') m new_vars. + init_mem p' = alloc_globals (globalenv p') m new_globs. Proof. - unfold init_mem. destruct progmatch. destruct H0. destruct H0 as [tvars [P1 P2]]. - rewrite P2. - intros. - erewrite <- alloc_variables_app; eauto. - eapply alloc_variables_match; eauto. + unfold init_mem; intros. + destruct progmatch as [[tglob [P Q]] R]. + rewrite Q. erewrite <- alloc_globals_app; eauto. + eapply alloc_globals_match; eauto. Qed. End MATCH_PROGRAMS. @@ -1661,21 +1544,20 @@ Variable A B V W: Type. Variable transf_fun: A -> res B. Variable transf_var: V -> res W. -Variable new_functs : list (ident * B). -Variable new_vars : list (ident * globvar W). +Variable new_globs : list (ident * globdef B W). Variable new_main : ident. Variable p: program A V. Variable p': program B W. Hypothesis transf_OK: - transform_partial_augment_program transf_fun transf_var new_functs new_vars new_main p = OK p'. + transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK p'. Remark prog_match: match_program (fun fd tfd => transf_fun fd = OK tfd) (fun info tinfo => transf_var info = OK tinfo) - new_functs new_vars new_main + new_globs new_main p p'. Proof. apply transform_partial_augment_program_match; auto. @@ -1692,51 +1574,39 @@ Proof. intros [tf [X Y]]. exists tf; auto. Qed. - - -(* This may not yet be in the ideal form for easy use .*) Theorem find_new_funct_ptr_exists: - list_norepet (prog_funct_names p ++ funct_names new_functs) -> - list_disjoint (prog_funct_names p ++ funct_names new_functs) (prog_var_names p ++ var_names new_vars) -> - forall id f, In (id, f) new_functs -> + list_norepet (List.map fst new_globs) -> + forall id f, In (id, Gfun f) new_globs -> exists b, find_symbol (globalenv p') id = Some b /\ find_funct_ptr (globalenv p') b = Some f. Proof. - intros. - destruct p. - unfold transform_partial_augment_program in transf_OK. - monadInv transf_OK. rename x into prog_funct'. rename x0 into prog_vars'. simpl in *. - assert (funct_names prog_funct = funct_names prog_funct'). - clear - EQ. generalize dependent prog_funct'. induction prog_funct; intros. - simpl in EQ. inversion EQ; subst; auto. - simpl in EQ. destruct a. destruct (transf_fun a); try discriminate. monadInv EQ. - simpl; f_equal; auto. - assert (var_names prog_vars = var_names prog_vars'). - clear - EQ1. generalize dependent prog_vars'. induction prog_vars; intros. - simpl in EQ1. inversion EQ1; subst; auto. - simpl in EQ1. destruct a. destruct (transf_globvar transf_var g); try discriminate. monadInv EQ1. - simpl; f_equal; auto. - apply find_funct_ptr_exists. - unfold prog_funct_names in *; simpl in *. - rewrite funct_names_app. rewrite <- H2. auto. - unfold prog_funct_names, prog_var_names in *; simpl in *. - rewrite funct_names_app. rewrite var_names_app. rewrite <- H2. rewrite <- H3. auto. - simpl. intuition. + intros. destruct prog_match as [[tglob [P Q]] R]. + unfold globalenv. rewrite Q. rewrite add_globals_app. + eapply add_globals_norepet_ensures; eauto. +(* preserves *) + intros. unfold find_symbol, find_funct_ptr in *; simpl. + destruct H1 as [b [X Y]]. exists b; split. + rewrite PTree.gso; auto. + destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto. + exploit genv_funs_range; eauto. unfold ZIndexed.t; omega. + auto. +(* ensures *) + intros. unfold find_symbol, find_funct_ptr in *; simpl. + exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. Qed. Theorem find_funct_ptr_rev_transf_augment: forall (b: block) (tf: B), find_funct_ptr (globalenv p') b = Some tf -> - if (zlt (genv_nextfun (globalenv p)) b) then + if zlt b (genv_next (globalenv p)) then (exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf) else - In tf (map (@snd ident B) new_functs). + In (Gfun tf) (map snd new_globs). Proof. intros. - exploit find_funct_ptr_rev_match;eauto. eexact prog_match; eauto. auto. + exploit find_funct_ptr_rev_match; eauto. eexact prog_match; eauto. auto. Qed. - Theorem find_funct_transf_augment: forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> @@ -1744,15 +1614,14 @@ Theorem find_funct_transf_augment: find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. Proof. intros. - exploit find_funct_match. eexact prog_match. eauto. - intros [tf [X Y]]. exists tf; auto. + exploit find_funct_match. eexact prog_match. eauto. auto. Qed. Theorem find_funct_rev_transf_augment: forall (v: val) (tf: B), find_funct (globalenv p') v = Some tf -> (exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf) \/ - In tf (map (@snd ident B) new_functs). + In (Gfun tf) (map snd new_globs). Proof. intros. exploit find_funct_rev_match. eexact prog_match. eauto. auto. @@ -1765,65 +1634,49 @@ Theorem find_var_info_transf_augment: find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'. Proof. intros. - exploit find_var_info_match. eexact prog_match. eauto. - intros [tv [X Y]]. exists tv; split; auto. inv Y. unfold transf_globvar; simpl. + exploit find_var_info_match. eexact prog_match. eauto. intros [tv [X Y]]. + exists tv; split; auto. inv Y. unfold transf_globvar; simpl. rewrite H0; simpl. auto. Qed. Theorem find_new_var_exists: - forall id gv, - list_norepet (var_names new_vars) -> - In (id, gv) new_vars -> - exists b, find_symbol (globalenv p') id = Some b /\ find_var_info (globalenv p') b = Some gv. -Proof. - intros. - assert (P: forall b vars (ge: t B W), - ~In id (var_names vars) -> - find_symbol ge id = Some b - /\ find_var_info ge b = Some gv -> - find_symbol (add_variables ge vars) id = Some b - /\ find_var_info (add_variables ge vars) b = Some gv). - induction vars; simpl; intros. auto. apply IHvars. tauto. - destruct a as [id1 gv1]; unfold add_variable, find_symbol, find_var_info; simpl in *. - destruct H2; split. rewrite PTree.gso. auto. intuition. - rewrite ZMap.gso. auto. exploit genv_vars_range; eauto. unfold ZIndexed.t; omega. - - assert (Q: forall vars (ge: t B W), - list_norepet (var_names vars) -> - In (id, gv) vars -> - exists b, find_symbol (add_variables ge vars) id = Some b - /\ find_var_info (add_variables ge vars) b = Some gv). - induction vars; simpl; intros. - contradiction. - destruct a as [id1 gv1]; simpl in *. inv H1. destruct H2. inv H1. - exists (genv_nextvar ge). apply P; auto. - unfold add_variable, find_symbol, find_var_info; simpl in *. - split. apply PTree.gss. apply ZMap.gss. - apply IHvars; auto. - - unfold transform_partial_augment_program in transf_OK. - monadInv transf_OK. rename x into prog_funct'. rename x0 into prog_vars'. simpl in *. - unfold globalenv; simpl. repeat rewrite add_variables_app. apply Q; auto. + list_norepet (List.map fst new_globs) -> + forall id gv, In (id, Gvar gv) new_globs -> + exists b, find_symbol (globalenv p') id = Some b + /\ find_var_info (globalenv p') b = Some gv. +Proof. + intros. destruct prog_match as [[tglob [P Q]] R]. + unfold globalenv. rewrite Q. rewrite add_globals_app. + eapply add_globals_norepet_ensures; eauto. +(* preserves *) + intros. unfold find_symbol, find_var_info in *; simpl. + destruct H1 as [b [X Y]]. exists b; split. + rewrite PTree.gso; auto. + destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto. + exploit genv_vars_range; eauto. unfold ZIndexed.t; omega. +(* ensures *) + intros. unfold find_symbol, find_var_info in *; simpl. + exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. Qed. Theorem find_var_info_rev_transf_augment: forall (b: block) (v': globvar W), find_var_info (globalenv p') b = Some v' -> - if zlt b (genv_nextvar (globalenv p)) then + if zlt b (genv_next (globalenv p)) then (exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v') else - (In v' (map (@snd ident (globvar W)) new_vars)). + (In (Gvar v') (map snd new_globs)). Proof. intros. exploit find_var_info_rev_match. eexact prog_match. eauto. - destruct (zlt b (genv_nextvar (globalenv p))); auto. + destruct (zlt b (genv_next (globalenv p))); auto. intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl. rewrite H0; simpl. auto. Qed. Theorem find_symbol_transf_augment: forall (s: ident), - ~ In s (funct_names new_functs ++ var_names new_vars) -> + ~ In s (map fst new_globs) -> find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. intros. eapply find_symbol_match. eexact prog_match. auto. @@ -1831,16 +1684,16 @@ Qed. Theorem init_mem_transf_augment: (forall s', find_symbol (globalenv p) s' <> None -> - ~ In s' (funct_names new_functs ++ var_names new_vars)) -> + ~ In s' (map fst new_globs)) -> forall m, init_mem p = Some m -> - init_mem p' = alloc_variables (globalenv p') m new_vars. + init_mem p' = alloc_globals (globalenv p') m new_globs. Proof. intros. eapply init_mem_match. eexact prog_match. auto. auto. Qed. Theorem init_mem_inject_transf_augment: (forall s', find_symbol (globalenv p) s' <> None -> - ~ In s' (funct_names new_functs ++ var_names new_vars)) -> + ~ In s' (map fst new_globs)) -> forall m, init_mem p = Some m -> forall m', init_mem p' = Some m' -> Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m'. @@ -1848,10 +1701,9 @@ Proof. intros. pose proof (initmem_inject p H0). erewrite init_mem_transf_augment in H1; eauto. - eapply alloc_variables_augment; eauto. omega. + eapply alloc_globals_augment; eauto. omega. Qed. - End TRANSF_PROGRAM_AUGMENT. Section TRANSF_PROGRAM_PARTIAL2. @@ -1865,13 +1717,9 @@ Hypothesis transf_OK: transform_partial_program2 transf_fun transf_var p = OK p'. Remark transf_augment_OK: - transform_partial_augment_program transf_fun transf_var nil nil p.(prog_main) p = OK p'. + transform_partial_augment_program transf_fun transf_var nil p.(prog_main) p = OK p'. Proof. - rewrite <- transf_OK. - unfold transform_partial_augment_program, transform_partial_program2. - destruct (map_partial prefix_name transf_fun (prog_funct p)); auto. simpl. - destruct (map_partial prefix_name (transf_globvar transf_var) (prog_vars p)); simpl. - repeat rewrite app_nil_r. auto. auto. + rewrite <- transf_OK. apply symmetry. apply transform_partial_program2_augment. Qed. Theorem find_funct_ptr_transf_partial2: @@ -1880,7 +1728,7 @@ Theorem find_funct_ptr_transf_partial2: exists f', find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'. Proof. - exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). Qed. Theorem find_funct_ptr_rev_transf_partial2: @@ -1888,9 +1736,9 @@ Theorem find_funct_ptr_rev_transf_partial2: find_funct_ptr (globalenv p') b = Some tf -> exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf. Proof. - pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). intros. pose proof (H b tf H0). - destruct (zlt (genv_nextfun (globalenv p)) b). auto. inversion H1. + destruct (zlt b (genv_next (globalenv p))). auto. contradiction. Qed. Theorem find_funct_transf_partial2: @@ -1899,7 +1747,7 @@ Theorem find_funct_transf_partial2: exists f', find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. Proof. - exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). Qed. Theorem find_funct_rev_transf_partial2: @@ -1907,9 +1755,9 @@ Theorem find_funct_rev_transf_partial2: find_funct (globalenv p') v = Some tf -> exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf. Proof. - pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). intros. pose proof (H v tf H0). - destruct H1. auto. inversion H1. + destruct H1. auto. contradiction. Qed. Theorem find_var_info_transf_partial2: @@ -1918,7 +1766,7 @@ Theorem find_var_info_transf_partial2: exists v', find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'. Proof. - exact (@find_var_info_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + exact (@find_var_info_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). Qed. Theorem find_var_info_rev_transf_partial2: @@ -1927,23 +1775,23 @@ Theorem find_var_info_rev_transf_partial2: exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v'. Proof. - pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). intros. pose proof (H b v' H0). - destruct (zlt b (genv_nextvar (globalenv p))). auto. inversion H1. + destruct (zlt b (genv_next (globalenv p))). auto. contradiction. Qed. Theorem find_symbol_transf_partial2: forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. - pose proof (@find_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + pose proof (@find_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. - pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). intros. simpl in H. apply H; auto. Qed. @@ -1957,24 +1805,13 @@ Variable p: program A V. Variable p': program B V. Hypothesis transf_OK: transform_partial_program transf p = OK p'. -Remark transf2_OK: - transform_partial_program2 transf (fun x => OK x) p = OK p'. -Proof. - rewrite <- transf_OK. - unfold transform_partial_program2, transform_partial_program. - destruct (map_partial prefix_name transf (prog_funct p)); auto. - simpl. replace (transf_globvar (fun (x : V) => OK x)) with (fun (v: globvar V) => OK v). - rewrite map_partial_identity; auto. - apply extensionality; intros. destruct x; auto. -Qed. - Theorem find_funct_ptr_transf_partial: forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> exists f', find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'. Proof. - exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. Theorem find_funct_ptr_rev_transf_partial: @@ -1982,7 +1819,7 @@ Theorem find_funct_ptr_rev_transf_partial: find_funct_ptr (globalenv p') b = Some tf -> exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf. Proof. - exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. Theorem find_funct_transf_partial: @@ -1991,7 +1828,7 @@ Theorem find_funct_transf_partial: exists f', find_funct (globalenv p') v = Some f' /\ transf f = OK f'. Proof. - exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. Theorem find_funct_rev_transf_partial: @@ -1999,14 +1836,14 @@ Theorem find_funct_rev_transf_partial: find_funct (globalenv p') v = Some tf -> exists f, find_funct (globalenv p) v = Some f /\ transf f = OK tf. Proof. - exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. Theorem find_symbol_transf_partial: forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. - exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. Theorem find_var_info_transf_partial: @@ -2014,10 +1851,10 @@ Theorem find_var_info_transf_partial: find_var_info (globalenv p') b = find_var_info (globalenv p) b. Proof. intros. case_eq (find_var_info (globalenv p) b); intros. - exploit find_var_info_transf_partial2. eexact transf2_OK. eauto. + exploit find_var_info_transf_partial2. eexact transf_OK. eauto. intros [v' [P Q]]. monadInv Q. rewrite P. inv EQ. destruct g; auto. case_eq (find_var_info (globalenv p') b); intros. - exploit find_var_info_rev_transf_partial2. eexact transf2_OK. eauto. + exploit find_var_info_rev_transf_partial2. eexact transf_OK. eauto. intros [v' [P Q]]. monadInv Q. inv EQ. congruence. auto. Qed. @@ -2025,7 +1862,7 @@ Qed. Theorem init_mem_transf_partial: forall m, init_mem p = Some m -> init_mem p' = Some m. Proof. - exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. End TRANSF_PROGRAM_PARTIAL. @@ -2040,8 +1877,7 @@ Let tp := transform_program transf p. Remark transf_OK: transform_partial_program (fun x => OK (transf x)) p = OK tp. Proof. - unfold tp, transform_program, transform_partial_program. - rewrite map_partial_total. reflexivity. + unfold tp. apply transform_program_partial_program. Qed. Theorem find_funct_ptr_transf: |