summaryrefslogtreecommitdiff
path: root/common
diff options
context:
space:
mode:
Diffstat (limited to 'common')
-rw-r--r--common/AST.v422
-rw-r--r--common/Globalenvs.v1784
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: