From e4723d142aa7b1229cdf5989340342d7c5ce870c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:31:26 +0100 Subject: Update the back-end proofs to the new linking framework. --- backend/Unusedglobproof.v | 1120 +++++++++++++++++++++++++-------------------- 1 file changed, 611 insertions(+), 509 deletions(-) (limited to 'backend/Unusedglobproof.v') diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 7c1b60a9..bb40a2d3 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -12,28 +12,67 @@ (** Elimination of unreferenced static definitions *) -Require Import FSets. -Require Import Coqlib. -Require Import Ordered. -Require Import Maps. -Require Import Iteration. -Require Import AST. -Require Import Errors. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Op. -Require Import Registers. -Require Import RTL. +Require Import FSets Coqlib Maps Ordered Iteration Errors. +Require Import AST Linking. +Require Import Integers Values Memory Globalenvs Events Smallstep. +Require Import Op Registers RTL. Require Import Unusedglob. Module ISF := FSetFacts.Facts(IS). Module ISP := FSetProperties.Properties(IS). -(** * Properties of the analysis *) +(** * Relational specification of the transformation *) + +(** The transformed program is obtained from the original program + by keeping only the global definitions that belong to a given + set [u] of names. *) + +Record match_prog_1 (u: IS.t) (p tp: program) : Prop := { + match_prog_main: + tp.(prog_main) = p.(prog_main); + match_prog_public: + tp.(prog_public) = p.(prog_public); + match_prog_def: + forall id, + (prog_defmap tp)!id = if IS.mem id u then (prog_defmap p)!id else None; + match_prog_unique: + list_norepet (prog_defs_names tp) +}. + +(** This set [u] (as "used") must be closed under references, and + contain the entry point and the public identifiers of the program. *) + +Definition ref_function (f: function) (id: ident) : Prop := + exists pc i, f.(fn_code)!pc = Some i /\ In id (ref_instruction i). + +Definition ref_fundef (fd: fundef) (id: ident) : Prop := + match fd with Internal f => ref_function f id | External ef => False end. + +Definition ref_init (il: list init_data) (id: ident) : Prop := + exists ofs, In (Init_addrof id ofs) il. + +Definition ref_def (gd: globdef fundef unit) (id: ident) : Prop := + match gd with + | Gfun fd => ref_fundef fd id + | Gvar gv => ref_init gv.(gvar_init) id + end. + +Record valid_used_set (p: program) (u: IS.t) : Prop := { + used_closed: forall id gd id', + IS.In id u -> (prog_defmap p)!id = Some gd -> ref_def gd id' -> + IS.In id' u; + used_main: + IS.In p.(prog_main) u; + used_public: forall id, + In id p.(prog_public) -> IS.In id u; + used_defined: forall id, + IS.In id u -> In id (prog_defs_names p) \/ id = p.(prog_main) +}. + +Definition match_prog (p tp: program) : Prop := + exists u: IS.t, valid_used_set p u /\ match_prog_1 u p tp. + +(** * Properties of the static analysis *) (** Monotonic evolution of the workset. *) @@ -123,7 +162,7 @@ Proof. eapply workset_incl_trans. 2: apply add_workset_incl. generalize {| w_seen := IS.empty; w_todo := nil |}. induction (prog_public p); simpl; intros. apply workset_incl_refl. - eapply workset_incl_trans. eapply add_workset_incl. eapply IHl. + eapply workset_incl_trans. apply add_workset_incl. apply IHl. Qed. (** Soundness properties for functions that add identifiers to the workset *) @@ -148,9 +187,6 @@ Proof. apply IHl; auto. Qed. -Definition ref_function (f: function) (id: ident) : Prop := - exists pc i, f.(fn_code)!pc = Some i /\ In id (ref_instruction i). - Lemma seen_add_ref_function: forall id f w, ref_function f id -> IS.In id (add_ref_function f w). @@ -164,15 +200,6 @@ Proof. apply H1. exists pc, i; auto. Qed. -Definition ref_fundef (fd: fundef) (id: ident) : Prop := - match fd with Internal f => ref_function f id | External ef => False end. - -Definition ref_def (gd: globdef fundef unit) (id: ident) : Prop := - match gd with - | Gfun fd => ref_fundef fd id - | Gvar gv => exists ofs, List.In (Init_addrof id ofs) gv.(gvar_init) - end. - Lemma seen_add_ref_definition: forall pm id gd id' w, pm!id = Some gd -> ref_def gd id' -> IS.In id' (add_ref_definition pm id w). @@ -198,7 +225,7 @@ Qed. Lemma seen_main_initial_workset: forall p, IS.In p.(prog_main) (initial_workset p). Proof. - unfold initial_workset; intros. apply seen_add_workset. + intros. apply seen_add_workset. Qed. Lemma seen_public_initial_workset: @@ -217,19 +244,14 @@ Proof. apply H0. auto. Qed. -(** * Semantic preservation *) +(** * Correctness of the transformation with respect to the relational specification *) -Section SOUNDNESS. -Variable p: program. -Variable tp: program. -Hypothesis TRANSF: transform_program p = OK tp. -Let ge := Genv.globalenv p. -Let tge := Genv.globalenv tp. - -Let pm := program_map p. +(** Correctness of the dependency graph traversal. *) +Section ANALYSIS. -(** Correctness of the dependency graph traversal. *) +Variable p: program. +Let pm := prog_defmap p. Definition workset_invariant (w: workset) : Prop := forall id gd id', @@ -264,7 +286,7 @@ Proof. Qed. Theorem used_globals_sound: - forall u, used_globals p = Some u -> used_set_closed u. + forall u, used_globals p pm = Some u -> used_set_closed u. Proof. unfold used_globals; intros. eapply PrimIter.iterate_prop with (P := workset_invariant); eauto. - intros. apply iter_step_invariant; auto. @@ -275,7 +297,7 @@ Proof. Qed. Theorem used_globals_incl: - forall u, used_globals p = Some u -> IS.Subset (initial_workset p) u. + forall u, used_globals p pm = Some u -> IS.Subset (initial_workset p) u. Proof. unfold used_globals; intros. eapply PrimIter.iterate_prop with (P := fun (w: workset) => IS.Subset (initial_workset p) w); eauto. @@ -286,35 +308,34 @@ Proof. - red; auto. Qed. -Definition used: IS.t := - match used_globals p with Some u => u | None => IS.empty end. - -Remark USED_GLOBALS: used_globals p = Some used. +Corollary used_globals_valid: + forall u, + used_globals p pm = Some u -> + IS.for_all (global_defined p pm) u = true -> + valid_used_set p u. Proof. - unfold used. unfold transform_program in TRANSF. destruct (used_globals p). auto. discriminate. + intros. constructor. +- intros. eapply used_globals_sound; eauto. +- eapply used_globals_incl; eauto. apply seen_main_initial_workset. +- intros. eapply used_globals_incl; eauto. apply seen_public_initial_workset; auto. +- intros. apply ISF.for_all_iff in H0. ++ red in H0. apply H0 in H1. unfold global_defined in H1. + destruct pm!id as [g|] eqn:E. +* left. change id with (fst (id,g)). apply in_map. apply in_prog_defmap; auto. +* InvBooleans; auto. ++ hnf. simpl; intros; congruence. Qed. -Definition kept (id: ident) : Prop := IS.In id used. +End ANALYSIS. -Theorem kept_closed: - forall id gd id', - kept id -> pm!id = Some gd -> ref_def gd id' -> kept id'. -Proof. - intros. assert (UC: used_set_closed used) by (apply used_globals_sound; apply USED_GLOBALS). - eapply UC; eauto. -Qed. +(** Properties of the elimination of unused global definitions. *) -Theorem kept_main: - kept p.(prog_main). -Proof. - unfold kept. eapply used_globals_incl; eauto. apply USED_GLOBALS. apply seen_main_initial_workset. -Qed. +Section TRANSFORMATION. -Theorem kept_public: - forall id, In id p.(prog_public) -> kept id. -Proof. - intros. unfold kept. eapply used_globals_incl; eauto. apply USED_GLOBALS. apply seen_public_initial_workset; auto. -Qed. +Variable p: program. +Variable used: IS.t. + +Let add_def (m: prog_map) idg := PTree.set (fst idg) (snd idg) m. Remark filter_globdefs_accu: forall defs accu1 accu2 u, @@ -333,98 +354,154 @@ Proof. intros. rewrite <- filter_globdefs_accu. auto. Qed. -Theorem transform_program_charact: - forall id, (program_map tp)!id = if IS.mem id used then pm!id else None. +Lemma filter_globdefs_map_1: + forall id l u m1, + IS.mem id u = false -> + m1!id = None -> + (fold_left add_def (filter_globdefs u nil l) m1)!id = None. Proof. - intros. - assert (X: forall l u m1 m2, - IS.In id u -> - m1!id = m2!id -> - (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id = - (fold_left add_def_prog_map (List.rev l) m2)!id). - { - induction l; simpl; intros. - auto. - destruct a as [id1 gd1]. rewrite fold_left_app. simpl. - destruct (IS.mem id1 u) eqn:MEM. - rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. - unfold add_def_prog_map at 1 3. simpl. - rewrite ! PTree.gsspec. destruct (peq id id1). auto. - apply IHl; auto. apply IS.remove_2; auto. - unfold add_def_prog_map at 2. simpl. rewrite PTree.gso. apply IHl; auto. - red; intros; subst id1. - assert (IS.mem id u = true) by (apply IS.mem_1; auto). congruence. - } - assert (Y: forall l u m1, - IS.mem id u = false -> - m1!id = None -> - (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id = None). - { - induction l; simpl; intros. - auto. - destruct a as [id1 gd1]. - destruct (IS.mem id1 u) eqn:MEM. - rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. - unfold add_def_prog_map at 1. simpl. rewrite PTree.gso by congruence. eapply IHl; eauto. - rewrite ISF.remove_b. rewrite H; auto. - eapply IHl; eauto. - } - unfold pm, program_map. - unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF. inversion TRANSF. - simpl. destruct (IS.mem id used) eqn: MEM. - erewrite X. rewrite List.rev_involutive. eauto. apply IS.mem_2; auto. auto. - apply Y. auto. apply PTree.gempty. -Qed. - -(** Program map and Genv operations *) - -Definition genv_progmap_match (ge: genv) (pm: prog_map) : Prop := - forall id, - match Genv.find_symbol ge id with - | None => pm!id = None - | Some b => - match pm!id with - | None => False - | Some (Gfun fd) => Genv.find_funct_ptr ge b = Some fd - | Some (Gvar gv) => Genv.find_var_info ge b = Some gv - end - end. + induction l as [ | [id1 gd1] l]; simpl; intros. +- auto. +- destruct (IS.mem id1 u) eqn:MEM. ++ rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. + unfold add_def at 1. simpl. rewrite PTree.gso by congruence. eapply IHl; eauto. + rewrite ISF.remove_b. rewrite H; auto. ++ eapply IHl; eauto. +Qed. -Lemma genv_program_map: - forall p, genv_progmap_match (Genv.globalenv p) (program_map p). +Lemma filter_globdefs_map_2: + forall id l u m1 m2, + IS.mem id u = true -> + m1!id = m2!id -> + (fold_left add_def (filter_globdefs u nil l) m1)!id = (fold_left add_def (List.rev l) m2)!id. Proof. - intros. unfold Genv.globalenv, program_map. - assert (REC: forall defs g m, - genv_progmap_match g m -> - genv_progmap_match (Genv.add_globals g defs) (fold_left add_def_prog_map defs m)). - { - induction defs; simpl; intros. - auto. - apply IHdefs. red; intros. specialize (H id). - destruct a as [id1 [fd|gv]]; - unfold Genv.add_global, Genv.find_symbol, Genv.find_funct_ptr, Genv.find_var_info, add_def_prog_map in *; - simpl. - - rewrite PTree.gsspec. destruct (peq id id1); subst. - + rewrite ! PTree.gss. auto. - + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto. - * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. - * auto. - - rewrite PTree.gsspec. destruct (peq id id1); subst. - + rewrite ! PTree.gss. auto. - + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto. - * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. - * auto. - } - apply REC. red; intros. unfold Genv.find_symbol, Genv.empty_genv; simpl. rewrite ! PTree.gempty; auto. + induction l as [ | [id1 gd1] l]; simpl; intros. +- auto. +- rewrite fold_left_app. simpl. + destruct (IS.mem id1 u) eqn:MEM. ++ rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. + unfold add_def at 1 3. simpl. + rewrite ! PTree.gsspec. destruct (peq id id1). auto. + apply IHl; auto. + apply IS.mem_1. apply IS.remove_2; auto. apply IS.mem_2; auto. ++ unfold add_def at 2. simpl. rewrite PTree.gso by congruence. apply IHl; auto. Qed. -Lemma transform_program_kept: - forall id b, Genv.find_symbol tge id = Some b -> kept id. +Lemma filter_globdefs_map: + forall id u defs, + (PTree_Properties.of_list (filter_globdefs u nil (List.rev defs)))! id = + if IS.mem id u then (PTree_Properties.of_list defs)!id else None. Proof. - intros. generalize (genv_program_map tp id). fold tge; rewrite H. - rewrite transform_program_charact. intros. destruct (IS.mem id used) eqn:U. - unfold kept; apply IS.mem_2; auto. - contradiction. + intros. unfold PTree_Properties.of_list. fold prog_map. unfold PTree.elt. fold add_def. + destruct (IS.mem id u) eqn:MEM. +- erewrite filter_globdefs_map_2. rewrite List.rev_involutive. reflexivity. + auto. auto. +- apply filter_globdefs_map_1. auto. apply PTree.gempty. +Qed. + +Lemma filter_globdefs_domain: + forall id l u, + In id (map fst (filter_globdefs u nil l)) -> IS.In id u /\ In id (map fst l). +Proof. + induction l as [ | [id1 gd1] l]; simpl; intros. +- tauto. +- destruct (IS.mem id1 u) eqn:MEM. ++ rewrite filter_globdefs_nil, map_app, in_app_iff in H. destruct H. + apply IHl in H. rewrite ISF.remove_iff in H. tauto. + simpl in H. destruct H; try tauto. subst id1. split; auto. apply IS.mem_2; auto. ++ apply IHl in H. tauto. +Qed. + +Lemma filter_globdefs_unique_names: + forall l u, list_norepet (map fst (filter_globdefs u nil l)). +Proof. + induction l as [ | [id1 gd1] l]; simpl; intros. +- constructor. +- destruct (IS.mem id1 u) eqn:MEM; auto. + rewrite filter_globdefs_nil, map_app. simpl. + apply list_norepet_append; auto. + constructor. simpl; tauto. constructor. + red; simpl; intros. destruct H0; try tauto. subst y. + apply filter_globdefs_domain in H. rewrite ISF.remove_iff in H. intuition. +Qed. + +End TRANSFORMATION. + +Theorem transf_program_match: + forall p tp, transform_program p = OK tp -> match_prog p tp. +Proof. + unfold transform_program; intros p tp TR. set (pm := prog_defmap p) in *. + destruct (used_globals p pm) as [u|] eqn:U; try discriminate. + destruct (IS.for_all (global_defined p pm) u) eqn:DEF; inv TR. + exists u; split. + apply used_globals_valid; auto. + constructor; simpl; auto. + intros. unfold prog_defmap; simpl. apply filter_globdefs_map. + apply filter_globdefs_unique_names. +Qed. + +(** * Semantic preservation *) + +Section SOUNDNESS. + +Variable p: program. +Variable tp: program. +Variable used: IS.t. +Hypothesis USED_VALID: valid_used_set p used. +Hypothesis TRANSF: match_prog_1 used p tp. +Let ge := Genv.globalenv p. +Let tge := Genv.globalenv tp. +Let pm := prog_defmap p. + +Definition kept (id: ident) : Prop := IS.In id used. + +Lemma kept_closed: + forall id gd id', + kept id -> pm!id = Some gd -> ref_def gd id' -> kept id'. +Proof. + intros. eapply used_closed; eauto. +Qed. + +Lemma kept_main: + kept p.(prog_main). +Proof. + eapply used_main; eauto. +Qed. + +Lemma kept_public: + forall id, In id p.(prog_public) -> kept id. +Proof. + intros. eapply used_public; eauto. +Qed. + +(** Relating [Genv.find_symbol] operations in the original and transformed program *) + +Lemma transform_find_symbol_1: + forall id b, + Genv.find_symbol ge id = Some b -> kept id -> exists b', Genv.find_symbol tge id = Some b'. +Proof. + intros. + assert (A: exists g, (prog_defmap p)!id = Some g). + { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. } + destruct A as (g & P). + apply Genv.find_symbol_exists with g. + apply in_prog_defmap. + erewrite match_prog_def by eauto. rewrite IS.mem_1 by auto. auto. +Qed. + +Lemma transform_find_symbol_2: + forall id b, + Genv.find_symbol tge id = Some b -> kept id /\ exists b', Genv.find_symbol ge id = Some b'. +Proof. + intros. + assert (A: exists g, (prog_defmap tp)!id = Some g). + { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. } + destruct A as (g & P). + erewrite match_prog_def in P by eauto. + destruct (IS.mem id used) eqn:U; try discriminate. + split. apply IS.mem_2; auto. + apply Genv.find_symbol_exists with g. + apply in_prog_defmap. auto. Qed. (** Injections that preserve used globals. *) @@ -439,16 +516,13 @@ Record meminj_preserves_globals (f: meminj) : Prop := { symbols_inject_3: forall id b', Genv.find_symbol tge id = Some b' -> exists b, Genv.find_symbol ge id = Some b /\ f b = Some(b', 0); - funct_ptr_inject: forall b b' delta fd, - f b = Some(b', delta) -> Genv.find_funct_ptr ge b = Some fd -> - Genv.find_funct_ptr tge b' = Some fd /\ delta = 0 /\ - (forall id, ref_fundef fd id -> kept id); - var_info_inject: forall b b' delta gv, - f b = Some(b', delta) -> Genv.find_var_info ge b = Some gv -> - Genv.find_var_info tge b' = Some gv /\ delta = 0; - var_info_rev_inject: forall b b' delta gv, - f b = Some(b', delta) -> Genv.find_var_info tge b' = Some gv -> - Genv.find_var_info ge b = Some gv /\ delta = 0 + defs_inject: forall b b' delta gd, + f b = Some(b', delta) -> Genv.find_def ge b = Some gd -> + Genv.find_def tge b' = Some gd /\ delta = 0 /\ + (forall id, ref_def gd id -> kept id); + defs_rev_inject: forall b b' delta gd, + f b = Some(b', delta) -> Genv.find_def tge b' = Some gd -> + Genv.find_def ge b = Some gd /\ delta = 0 }. Definition init_meminj : meminj := @@ -462,6 +536,14 @@ Definition init_meminj : meminj := | None => None end. +Remark init_meminj_eq: + forall id b b', + Genv.find_symbol ge id = Some b -> Genv.find_symbol tge id = Some b' -> + init_meminj b = Some(b', 0). +Proof. + intros. unfold init_meminj. erewrite Genv.find_invert_symbol by eauto. rewrite H0. auto. +Qed. + Remark init_meminj_invert: forall b b' delta, init_meminj b = Some(b', delta) -> @@ -480,44 +562,26 @@ Proof. - exploit init_meminj_invert; eauto. intros (A & id1 & B & C). assert (id1 = id) by (eapply (Genv.genv_vars_inj ge); eauto). subst id1. auto. -- unfold init_meminj. erewrite Genv.find_invert_symbol by eauto. apply IS.mem_1 in H. - generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. - rewrite transform_program_charact. rewrite H, H0. - destruct (Genv.find_symbol tge id) as [b'|]; intros. - exists b'; auto. rewrite H2 in H1; contradiction. -- generalize (genv_program_map tp id). fold tge. rewrite H. intros. - destruct (program_map tp)!id as [gd|] eqn:PM; try contradiction. - generalize (transform_program_charact id). rewrite PM. - destruct (IS.mem id used) eqn:USED; intros; try discriminate. - generalize (genv_program_map p id). fold ge; fold pm. - destruct (Genv.find_symbol ge id) as [b|] eqn:FS; intros; try congruence. - exists b; split; auto. unfold init_meminj. - erewrite Genv.find_invert_symbol by eauto. rewrite H. auto. +- exploit transform_find_symbol_1; eauto. intros (b' & F). exists b'; split; auto. + eapply init_meminj_eq; eauto. +- exploit transform_find_symbol_2; eauto. intros (K & b & F). + exists b; split; auto. eapply init_meminj_eq; eauto. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). + assert (kept id) by (eapply transform_find_symbol_2; eauto). + assert (pm!id = Some gd). + { unfold pm; rewrite Genv.find_def_symbol. exists b; auto. } + assert ((prog_defmap tp)!id = Some gd). + { erewrite match_prog_def by eauto. rewrite IS.mem_1 by auto. auto. } + rewrite Genv.find_def_symbol in H3. destruct H3 as (b1 & P & Q). + fold tge in P. replace b' with b1 by congruence. split; auto. split; auto. + intros. eapply kept_closed; eauto. - exploit init_meminj_invert; eauto. intros (A & id & B & C). - generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. - rewrite transform_program_charact. rewrite B, C. intros. - destruct (IS.mem id used) eqn:KEPT; try contradiction. - destruct (pm!id) as [gd|] eqn:PM; try contradiction. - destruct gd as [fd'|gv']. - + assert (fd' = fd) by congruence. subst fd'. split. auto. split. auto. - intros. eapply kept_closed; eauto. red; apply IS.mem_2; auto. - + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence. -- exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto. - generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. - rewrite transform_program_charact. rewrite B, C. intros. - destruct (IS.mem id used); try contradiction. - destruct (pm!id) as [gd|]; try contradiction. - destruct gd as [fd'|gv']. - + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence. - + congruence. -- exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto. - generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. - rewrite transform_program_charact. rewrite B, C. intros. - destruct (IS.mem id used); try contradiction. - destruct (pm!id) as [gd|]; try contradiction. - destruct gd as [fd'|gv']. - + assert (b' <> b') by (eapply Genv.genv_funs_vars; eassumption). congruence. - + congruence. + assert ((prog_defmap tp)!id = Some gd). + { rewrite Genv.find_def_symbol. exists b'; auto. } + erewrite match_prog_def in H1 by eauto. + destruct (IS.mem id used); try discriminate. + rewrite Genv.find_def_symbol in H1. destruct H1 as (b1 & P & Q). + fold ge in P. replace b with b1 by congruence. auto. Qed. Lemma globals_symbols_inject: @@ -527,28 +591,33 @@ Proof. assert (E1: Genv.genv_public ge = p.(prog_public)). { apply Genv.globalenv_public. } assert (E2: Genv.genv_public tge = p.(prog_public)). - { unfold tge; rewrite Genv.globalenv_public. - unfold transform_program in TRANSF. rewrite USED_GLOBALS in TRANSF. inversion TRANSF. auto. } + { unfold tge; rewrite Genv.globalenv_public. eapply match_prog_public; eauto. } split; [|split;[|split]]; intros. + simpl; unfold Genv.public_symbol; rewrite E1, E2. destruct (Genv.find_symbol tge id) as [b'|] eqn:TFS. exploit symbols_inject_3; eauto. intros (b & FS & INJ). rewrite FS. auto. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. destruct (in_dec ident_eq id (prog_public p)); simpl; auto. - exploit symbols_inject_2; eauto. apply kept_public; auto. + exploit symbols_inject_2; eauto. + eapply kept_public; eauto. intros (b' & TFS' & INJ). congruence. + eapply symbols_inject_1; eauto. + simpl in *; unfold Genv.public_symbol in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. rewrite E1 in H0. destruct (in_dec ident_eq id (prog_public p)); try discriminate. inv H1. - exploit symbols_inject_2; eauto. apply kept_public; auto. + exploit symbols_inject_2; eauto. + eapply kept_public; eauto. intros (b' & A & B); exists b'; auto. + simpl. unfold Genv.block_is_volatile. destruct (Genv.find_var_info ge b1) as [gv|] eqn:V1. - exploit var_info_inject; eauto. intros [A B]. rewrite A. auto. + rewrite Genv.find_var_info_iff in V1. + exploit defs_inject; eauto. intros (A & B & C). + rewrite <- Genv.find_var_info_iff in A. rewrite A; auto. destruct (Genv.find_var_info tge b2) as [gv|] eqn:V2; auto. - exploit var_info_rev_inject; eauto. intros [A B]. congruence. + rewrite Genv.find_var_info_iff in V2. + exploit defs_rev_inject; eauto. intros (A & B). + rewrite <- Genv.find_var_info_iff in A. congruence. Qed. Lemma symbol_address_inject: @@ -661,12 +730,10 @@ Proof. exists b'; auto. + exploit symbols_inject_3; eauto. intros (b & A & B). exists b; auto. - + eapply funct_ptr_inject; eauto. apply SAME; auto. - eapply Genv.genv_funs_range; eauto. - + eapply var_info_inject; eauto. apply SAME; auto. - eapply Genv.genv_vars_range; eauto. - + eapply var_info_rev_inject; eauto. apply SAME'; auto. - eapply Genv.genv_vars_range; eauto. + + eapply defs_inject; eauto. apply SAME; auto. + eapply Genv.genv_defs_range; eauto. + + eapply defs_rev_inject; eauto. apply SAME'; auto. + eapply Genv.genv_defs_range; eauto. - econstructor; eauto. apply IHmatch_stacks. intros. exploit H1; eauto. intros [A B]. split; eapply Ple_trans; eauto. @@ -738,11 +805,15 @@ Proof. - exploit Genv.find_funct_inv; eauto. intros (b & R). rewrite R in H0. rewrite Genv.find_funct_find_funct_ptr in H0. specialize (H1 r). rewrite R in H1. inv H1. - exploit funct_ptr_inject; eauto. intros (A & B & C). + rewrite Genv.find_funct_ptr_iff in H0. + exploit defs_inject; eauto. intros (A & B & C). + rewrite <- Genv.find_funct_ptr_iff in A. rewrite B; auto. - destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. exploit symbols_inject_2; eauto. intros (tb & P & Q). rewrite P. - exploit funct_ptr_inject; eauto. intros (A & B & C). + rewrite Genv.find_funct_ptr_iff in H0. + exploit defs_inject; eauto. intros (A & B & C). + rewrite <- Genv.find_funct_ptr_iff in A. auto. Qed. @@ -973,285 +1044,159 @@ Qed. (** Relating initial memory states *) -Remark init_meminj_no_overlap: - forall m, Mem.meminj_no_overlap init_meminj m. +(* +Remark genv_find_def_exists: + forall (F V: Type) (p: AST.program F V) b, + Plt b (Genv.genv_next (Genv.globalenv p)) -> + exists gd, Genv.find_def (Genv.globalenv p) b = Some gd. Proof. - intros; red; intros. - exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1). - exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2). - left; red; intros; subst b2'. - assert (id1 = id2) by (eapply Genv.genv_vars_inj; eauto). - congruence. + intros until b. + set (P := fun (g: Genv.t F V) => + Plt b (Genv.genv_next g) -> exists gd, (Genv.genv_defs g)!b = Some gd). + assert (forall l g, P g -> P (Genv.add_globals g l)). + { induction l as [ | [id1 g1] l]; simpl; intros. + - auto. + - apply IHl. unfold Genv.add_global, P; simpl. intros LT. apply Plt_succ_inv in LT. destruct LT. + + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto. + + rewrite H0. rewrite PTree.gss. exists g1; auto. } + apply H. red; simpl; intros. exfalso; xomega. Qed. +*) -Lemma store_zeros_unmapped_inj: - forall m1 b1 i n m1', - store_zeros m1 b1 i n = Some m1' -> - forall m2, - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = None -> - Mem.mem_inj init_meminj m1' m2. -Proof. - intros until m1'. functional induction (store_zeros m1 b1 i n); intros. - inv H. auto. - eapply IHo; eauto. eapply Mem.store_unmapped_inj; eauto. - discriminate. -Qed. - -Lemma store_zeros_mapped_inj: - forall m1 b1 i n m1', - store_zeros m1 b1 i n = Some m1' -> - forall m2 b2, - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = Some(b2, 0) -> - exists m2', store_zeros m2 b2 i n = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. -Proof. - intros until m1'. functional induction (store_zeros m1 b1 i n); intros. - inv H. exists m2; split; auto. rewrite store_zeros_equation, e; auto. - exploit Mem.store_mapped_inj; eauto. apply init_meminj_no_overlap. instantiate (1 := Vzero); constructor. - intros (m2' & A & B). rewrite Zplus_0_r in A. - exploit IHo; eauto. intros (m3' & C & D). - exists m3'; split; auto. rewrite store_zeros_equation, e, A, C; auto. - discriminate. -Qed. - -Lemma store_init_data_unmapped_inj: - forall m1 b1 i id m1' m2, - Genv.store_init_data ge m1 b1 i id = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = None -> - Mem.mem_inj init_meminj m1' m2. -Proof. - intros. destruct id; simpl in H; try (eapply Mem.store_unmapped_inj; now eauto). - inv H; auto. - destruct (Genv.find_symbol ge i0); try discriminate. eapply Mem.store_unmapped_inj; now eauto. -Qed. - -Lemma store_init_data_mapped_inj: - forall m1 b1 i init m1' b2 m2, - Genv.store_init_data ge m1 b1 i init = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = Some(b2, 0) -> - (forall id ofs, init = Init_addrof id ofs -> kept id) -> - exists m2', Genv.store_init_data tge m2 b2 i init = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. -Proof. - intros. replace i with (i + 0) by omega. pose proof (init_meminj_no_overlap m1). - destruct init; simpl in *; try (eapply Mem.store_mapped_inj; now eauto). - inv H. exists m2; auto. - destruct (Genv.find_symbol ge i0) as [bi|] eqn:FS1; try discriminate. - exploit symbols_inject_2. eapply init_meminj_preserves_globals. eapply H2; eauto. eauto. - intros (bi' & A & B). rewrite A. eapply Mem.store_mapped_inj; eauto. - econstructor; eauto. rewrite Int.add_zero; auto. +Lemma init_meminj_invert_strong: + forall b b' delta, + init_meminj b = Some(b', delta) -> + delta = 0 /\ + exists id gd, + Genv.find_symbol ge id = Some b + /\ Genv.find_symbol tge id = Some b' + /\ Genv.find_def ge b = Some gd + /\ Genv.find_def tge b' = Some gd + /\ (forall i, ref_def gd i -> kept i). +Proof. + intros. exploit init_meminj_invert; eauto. intros (A & id & B & C). + assert (exists gd, (prog_defmap p)!id = Some gd). + { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. } + destruct H0 as [gd DM]. rewrite Genv.find_def_symbol in DM. + destruct DM as (b'' & P & Q). fold ge in P. rewrite P in B; inv B. + fold ge in Q. exploit defs_inject. apply init_meminj_preserves_globals. + eauto. eauto. intros (X & _ & Y). + split. auto. exists id, gd; auto. Qed. - Lemma store_init_data_list_unmapped_inj: - forall initlist m1 b1 i m1' m2, - Genv.store_init_data_list ge m1 b1 i initlist = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = None -> - Mem.mem_inj init_meminj m1' m2. -Proof. - induction initlist; simpl; intros. -- inv H; auto. -- destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate. - eapply IHinitlist; eauto. eapply store_init_data_unmapped_inj; eauto. -Qed. - -Lemma store_init_data_list_mapped_inj: - forall initlist m1 b1 i m1' b2 m2, - Genv.store_init_data_list ge m1 b1 i initlist = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = Some(b2, 0) -> - (forall id ofs, In (Init_addrof id ofs) initlist -> kept id) -> - exists m2', Genv.store_init_data_list tge m2 b2 i initlist = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. -Proof. - induction initlist; simpl; intros. -- inv H. exists m2; auto. -- destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate. - exploit store_init_data_mapped_inj; eauto. intros (m2'' & A & B). - exploit IHinitlist; eauto. intros (m2' & C & D). - exists m2'; split; auto. rewrite A; auto. -Qed. - -Lemma alloc_global_unmapped_inj: - forall m1 id g m1' m2, - Genv.alloc_global ge m1 (id, g) = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj (Mem.nextblock m1) = None -> - Mem.mem_inj init_meminj m1' m2. -Proof. - unfold Genv.alloc_global; intros. destruct g as [fd|gv]. -- destruct (Mem.alloc m1 0 1) as (m1a, b) eqn:ALLOC. - exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. - eapply Mem.drop_unmapped_inj with (m1 := m1a); eauto. - eapply Mem.alloc_left_unmapped_inj; eauto. -- set (sz := Genv.init_data_list_size (gvar_init gv)) in *. - destruct (Mem.alloc m1 0 sz) as (m1a, b) eqn:ALLOC. - destruct (store_zeros m1a b 0 sz) as [m1b|] eqn: STZ; try discriminate. - destruct (Genv.store_init_data_list ge m1b b 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate. - exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. - eapply Mem.drop_unmapped_inj with (m1 := m1c); eauto. - eapply store_init_data_list_unmapped_inj with (m1 := m1b); eauto. - eapply store_zeros_unmapped_inj with (m1 := m1a); eauto. - eapply Mem.alloc_left_unmapped_inj; eauto. -Qed. - -Lemma alloc_global_mapped_inj: - forall m1 id g m1' m2, - Genv.alloc_global ge m1 (id, g) = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj (Mem.nextblock m1) = Some(Mem.nextblock m2, 0) -> - (forall id, ref_def g id -> kept id) -> - exists m2', - Genv.alloc_global tge m2 (id, g) = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. -Proof. - unfold Genv.alloc_global; intros. destruct g as [fd|gv]. -- destruct (Mem.alloc m1 0 1) as (m1a, b1) eqn:ALLOC. - exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. - destruct (Mem.alloc m2 0 1) as (m2a, b2) eqn:ALLOC2. - exploit Mem.alloc_result; eauto. intros EQ2. rewrite <- EQ2 in H1. - assert (Mem.mem_inj init_meminj m1a m2a). - { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0). - eapply Mem.alloc_right_inj; eauto. - eauto. - eauto with mem. - red; intros; apply Z.divide_0_r. - intros. apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. omega. - auto. - } - exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap. -- set (sz := Genv.init_data_list_size (gvar_init gv)) in *. - destruct (Mem.alloc m1 0 sz) as (m1a, b1) eqn:ALLOC. - destruct (store_zeros m1a b1 0 sz) as [m1b|] eqn: STZ; try discriminate. - destruct (Genv.store_init_data_list ge m1b b1 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate. - exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. - destruct (Mem.alloc m2 0 sz) as (m2a, b2) eqn:ALLOC2. - exploit Mem.alloc_result; eauto. intros EQ2. rewrite <- EQ2 in H1. - assert (Mem.mem_inj init_meminj m1a m2a). - { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0). - eapply Mem.alloc_right_inj; eauto. - eauto. - eauto with mem. - red; intros; apply Z.divide_0_r. - intros. apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. omega. - auto. - } - exploit store_zeros_mapped_inj; eauto. intros (m2b & A & B). - exploit store_init_data_list_mapped_inj; eauto. - intros. apply H2. red. exists ofs; auto. intros (m2c & C & D). - exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap. intros (m2' & E & F). - exists m2'; split; auto. rewrite ! Zplus_0_r in E. rewrite A, C, E. auto. -Qed. - -Lemma alloc_globals_app: - forall F V (g: Genv.t F V) defs1 m defs2, - Genv.alloc_globals g m (defs1 ++ defs2) = - match Genv.alloc_globals g m defs1 with - | None => None - | Some m1 => Genv.alloc_globals g m1 defs2 - end. +Section INIT_MEM. + +Variables m tm: mem. +Hypothesis IM: Genv.init_mem p = Some m. +Hypothesis TIM: Genv.init_mem tp = Some tm. + +Lemma bytes_of_init_inject: + forall il, + (forall id, ref_init il id -> kept id) -> + list_forall2 (memval_inject init_meminj) (Genv.bytes_of_init_data_list ge il) (Genv.bytes_of_init_data_list tge il). Proof. - induction defs1; simpl; intros. auto. - destruct (Genv.alloc_global g m a); auto. + induction il as [ | i1 il]; simpl; intros. +- constructor. +- apply list_forall2_app. ++ destruct i1; simpl; try (apply inj_bytes_inject). + induction (Z.to_nat z); simpl; constructor. constructor. auto. + destruct (Genv.find_symbol ge i) as [b|] eqn:FS. + assert (kept i). { apply H. red. exists i0; auto with coqlib. } + exploit symbols_inject_2. apply init_meminj_preserves_globals. eauto. eauto. + intros (b' & A & B). rewrite A. apply inj_value_inject. + econstructor; eauto. symmetry; apply Int.add_zero. + destruct (Genv.find_symbol tge i) as [b'|] eqn:FS'. + exploit symbols_inject_3. apply init_meminj_preserves_globals. eauto. + intros (b & A & B). congruence. + apply repeat_Undef_inject_self with (n := 4%nat). ++ apply IHil. intros id [ofs IN]. apply H. exists ofs; auto with coqlib. Qed. -Lemma alloc_globals_snoc: - forall F V (g: Genv.t F V) m defs1 id_def, - Genv.alloc_globals g m (defs1 ++ id_def :: nil) = - match Genv.alloc_globals g m defs1 with - | None => None - | Some m1 => Genv.alloc_global g m1 id_def - end. +Lemma Mem_getN_forall2: + forall (P: memval -> memval -> Prop) c1 c2 i n p, + list_forall2 P (Mem.getN n p c1) (Mem.getN n p c2) -> + p <= i -> i < p + Z.of_nat n -> + P (ZMap.get i c1) (ZMap.get i c2). Proof. - intros. rewrite alloc_globals_app. - destruct (Genv.alloc_globals g m defs1); auto. unfold Genv.alloc_globals. - destruct (Genv.alloc_global g m0 id_def); auto. -Qed. - -Lemma alloc_globals_inj: - forall pubs defs m1 u g1 g2, - Genv.alloc_globals ge Mem.empty (List.rev defs) = Some m1 -> - g1 = Genv.add_globals (Genv.empty_genv _ _ pubs) (List.rev defs) -> - g2 = Genv.add_globals (Genv.empty_genv _ _ pubs) (filter_globdefs u nil defs) -> - Mem.nextblock m1 = Genv.genv_next g1 -> - (forall id, IS.In id u -> Genv.find_symbol g1 id = Genv.find_symbol ge id) -> - (forall id, IS.In id u -> Genv.find_symbol g2 id = Genv.find_symbol tge id) -> - (forall b id, Genv.find_symbol ge id = Some b -> Plt b (Mem.nextblock m1) -> kept id -> IS.In id u) -> - (forall id, IS.In id u -> (fold_left add_def_prog_map (List.rev defs) (PTree.empty _))!id = pm!id) -> - exists m2, - Genv.alloc_globals tge Mem.empty (filter_globdefs u nil defs) = Some m2 - /\ Mem.nextblock m2 = Genv.genv_next g2 - /\ Mem.mem_inj init_meminj m1 m2. -Proof. - induction defs; simpl; intros until g2; intros ALLOC GE1 GE2 NEXT1 SYMB1 SYMB2 SYMB3 PROGMAP. -- inv ALLOC. exists Mem.empty. intuition auto. constructor; intros. - eelim Mem.perm_empty; eauto. - exploit init_meminj_invert; eauto. intros [A B]. subst delta. apply Z.divide_0_r. - eelim Mem.perm_empty; eauto. -- rewrite Genv.add_globals_app in GE1. simpl in GE1. - set (g1' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (rev defs)) in *. - rewrite alloc_globals_snoc in ALLOC. - destruct (Genv.alloc_globals ge Mem.empty (rev defs)) as [m1'|] eqn:ALLOC1'; try discriminate. - exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK1. - assert (NEXTGE1: Genv.genv_next g1 = Pos.succ (Genv.genv_next g1')) by (rewrite GE1; reflexivity). - assert (NEXT1': Mem.nextblock m1' = Genv.genv_next g1') by (unfold block in *; xomega). - rewrite fold_left_app in PROGMAP. simpl in PROGMAP. - destruct a as [id gd]. unfold add_def_prog_map at 1 in PROGMAP. simpl in PROGMAP. - destruct (IS.mem id u) eqn:MEM. - + rewrite filter_globdefs_nil in *. rewrite alloc_globals_snoc. - rewrite Genv.add_globals_app in GE2. simpl in GE2. - set (g2' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (filter_globdefs (IS.remove id u) nil defs)) in *. - assert (NEXTGE2: Genv.genv_next g2 = Pos.succ (Genv.genv_next g2')) by (rewrite GE2; reflexivity). - assert (FS1: Genv.find_symbol ge id = Some (Mem.nextblock m1')). - { rewrite <- SYMB1 by (apply IS.mem_2; auto). - rewrite GE1. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. } - exploit (IHdefs m1' (IS.remove id u) g1' g2'); eauto. - intros. rewrite ISF.remove_iff in H; destruct H. - rewrite <- SYMB1 by auto. rewrite GE1. unfold Genv.find_symbol; simpl. - rewrite PTree.gso; auto. - intros. rewrite ISF.remove_iff in H; destruct H. - rewrite <- SYMB2 by auto. rewrite GE2. unfold Genv.find_symbol; simpl. - rewrite PTree.gso; auto. - intros. rewrite ISF.remove_iff. destruct (ident_eq id id0). - subst id0. rewrite FS1 in H. inv H. eelim Plt_strict; eauto. - exploit SYMB3. eexact H. unfold block in *; xomega. auto. tauto. - intros. rewrite ISF.remove_iff in H; destruct H. - rewrite <- PROGMAP by auto. rewrite PTree.gso by auto. auto. - intros (m2' & A & B & C). fold g2' in B. - assert (FS2: Genv.find_symbol tge id = Some (Mem.nextblock m2')). - { rewrite <- SYMB2 by (apply IS.mem_2; auto). - rewrite GE2. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. } - assert (INJ: init_meminj (Mem.nextblock m1') = Some (Mem.nextblock m2', 0)). - { apply Genv.find_invert_symbol in FS1. unfold init_meminj. rewrite FS1, FS2. auto. } - exploit alloc_global_mapped_inj. eexact ALLOC. eexact C. exact INJ. - intros. apply kept_closed with id gd. eapply transform_program_kept; eauto. - rewrite <- PROGMAP by (apply IS.mem_2; auto). apply PTree.gss. auto. - intros (m2 & D & E). - exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK2. - exists m2; split. rewrite A, D. auto. - split. unfold block in *; xomega. - auto. - + exploit (IHdefs m1' u g1' g2); auto. - intros. rewrite <- SYMB1 by auto. rewrite GE1. - unfold Genv.find_symbol; simpl. rewrite PTree.gso; auto. - red; intros; subst id0. apply IS.mem_1 in H. congruence. - intros. eapply SYMB3; eauto. unfold block in *; xomega. - intros. rewrite <- PROGMAP by auto. rewrite PTree.gso; auto. - apply IS.mem_1 in H. congruence. - intros (m2 & A & B & C). - assert (NOTINJ: init_meminj (Mem.nextblock m1') = None). - { destruct (init_meminj (Mem.nextblock m1')) as [[b' delta]|] eqn:J; auto. - exploit init_meminj_invert; eauto. intros (U & id1 & V & W). - exploit SYMB3; eauto. unfold block in *; xomega. - eapply transform_program_kept; eauto. - intros P. - revert V. rewrite <- SYMB1, GE1 by auto. unfold Genv.find_symbol; simpl. - rewrite PTree.gsspec. rewrite NEXT1'. destruct (peq id1 id); intros Q. - subst id1. apply IS.mem_1 in P. congruence. - eelim Plt_strict. eapply Genv.genv_symb_range; eauto. } - exists m2; intuition auto. eapply alloc_global_unmapped_inj; eauto. + induction n; simpl Mem.getN; intros. +- simpl in H1. omegaContradiction. +- inv H. rewrite inj_S in H1. destruct (zeq i p0). ++ congruence. ++ apply IHn with (p0 + 1); auto. omega. omega. +Qed. + +Lemma init_mem_inj_1: + Mem.mem_inj init_meminj m tm. +Proof. + intros; constructor; intros. +- exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). + exploit (Genv.init_mem_characterization_gen p); eauto. + exploit (Genv.init_mem_characterization_gen tp); eauto. + destruct gd as [f|v]. ++ intros (P2 & Q2) (P1 & Q1). + apply Q1 in H0. destruct H0. subst. + apply Mem.perm_cur. auto. ++ intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). + apply Q1 in H0. destruct H0. subst. + apply Mem.perm_cur. eapply Mem.perm_implies; eauto. + apply P2. omega. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). + subst delta. apply Zdivide_0. +- exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). + exploit (Genv.init_mem_characterization_gen p); eauto. + exploit (Genv.init_mem_characterization_gen tp); eauto. + destruct gd as [f|v]. ++ intros (P2 & Q2) (P1 & Q1). + apply Q1 in H0. destruct H0; discriminate. ++ intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). + apply Q1 in H0. destruct H0. + assert (NO: gvar_volatile v = false). + { unfold Genv.perm_globvar in H1. destruct (gvar_volatile v); auto. inv H1. } +Local Transparent Mem.loadbytes. + generalize (S1 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E1; inv E1. + generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2. + rewrite Zplus_0_r. + apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))). + rewrite H3, H4. apply bytes_of_init_inject. auto. + omega. + rewrite nat_of_Z_eq by (apply init_data_list_size_pos). omega. +Qed. + +Lemma init_mem_inj_2: + Mem.inject init_meminj m tm. +Proof. + constructor; intros. +- apply init_mem_inj_1. +- destruct (init_meminj b) as [[b' delta]|] eqn:INJ; auto. + elim H. exploit init_meminj_invert; eauto. intros (A & id & B & C). + eapply Genv.find_symbol_not_fresh; eauto. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). + eapply Genv.find_symbol_not_fresh; eauto. +- red; intros. + exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1). + exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2). + destruct (ident_eq id1 id2). congruence. left; eapply Genv.global_addresses_distinct; eauto. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. + split. omega. generalize (Int.unsigned_range_2 ofs). omega. +Qed. + +End INIT_MEM. + +Lemma init_mem_exists: + forall m, Genv.init_mem p = Some m -> + exists tm, Genv.init_mem tp = Some tm. +Proof. + intros. apply Genv.init_mem_exists. + intros. + assert (P: (prog_defmap tp)!id = Some (Gvar v)). + { eapply prog_defmap_norepet; eauto. eapply match_prog_unique; eauto. } + rewrite (match_prog_def _ _ _ TRANSF) in P. destruct (IS.mem id used) eqn:U; try discriminate. + exploit Genv.init_mem_inversion; eauto. apply in_prog_defmap; eauto. intros [AL FV]. + split. auto. + intros. exploit FV; eauto. intros (b & FS). + apply transform_find_symbol_1 with b; auto. + apply kept_closed with id (Gvar v). + apply IS.mem_2; auto. auto. red. red. exists o; auto. Qed. Theorem init_mem_inject: @@ -1260,40 +1205,25 @@ Theorem init_mem_inject: exists f tm, Genv.init_mem tp = Some tm /\ Mem.inject f m tm /\ meminj_preserves_globals f. Proof. intros. - unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; injection TRANSF. intros EQ. - destruct (alloc_globals_inj (prog_public p) (List.rev (prog_defs p)) m used ge tge) as (tm & A & B & C). - rewrite rev_involutive; auto. - rewrite rev_involutive; auto. - unfold tge; rewrite <- EQ; auto. - symmetry. apply Genv.init_mem_genv_next; auto. - auto. auto. auto. - intros. rewrite rev_involutive. auto. - assert (D: Genv.init_mem tp = Some tm). - { unfold Genv.init_mem. fold tge. rewrite <- EQ. exact A. } - pose proof (init_meminj_preserves_globals). - exists init_meminj, tm; intuition auto. - constructor; intros. - + auto. - + destruct (init_meminj b) as [[b1 delta1]|] eqn:INJ; auto. - exploit init_meminj_invert; eauto. intros (P & id & Q & R). - elim H1. eapply Genv.find_symbol_not_fresh; eauto. - + exploit init_meminj_invert; eauto. intros (P & id & Q & R). - eapply Genv.find_symbol_not_fresh; eauto. - + apply init_meminj_no_overlap. - + exploit init_meminj_invert; eauto. intros (P & id & Q & R). - split. omega. generalize (Int.unsigned_range_2 ofs). omega. + exploit init_mem_exists; eauto. intros [tm INIT]. + exists init_meminj, tm. + split. auto. + split. eapply init_mem_inj_2; eauto. + apply init_meminj_preserves_globals. Qed. Lemma transf_initial_states: forall S1, initial_state p S1 -> exists S2, initial_state tp S2 /\ match_states S1 S2. Proof. intros. inv H. exploit init_mem_inject; eauto. intros (j & tm & A & B & C). - exploit symbols_inject_2. eauto. apply kept_main. eexact H1. intros (tb & P & Q). - exploit funct_ptr_inject. eauto. eexact Q. exact H2. + exploit symbols_inject_2. eauto. eapply kept_main. eexact H1. intros (tb & P & Q). + rewrite Genv.find_funct_ptr_iff in H2. + exploit defs_inject. eauto. eexact Q. exact H2. intros (R & S & T). + rewrite <- Genv.find_funct_ptr_iff in R. exists (Callstate nil f nil tm); split. econstructor; eauto. - fold tge. unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; inversion TRANSF; auto. + fold tge. erewrite match_prog_main by eauto. auto. econstructor; eauto. constructor. auto. erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl. @@ -1307,7 +1237,7 @@ Proof. intros. inv H0. inv H. inv STACKS. inv RESINJ. constructor. Qed. -Theorem transf_program_correct: +Lemma transf_program_correct_1: forward_simulation (semantics p) (semantics tp). Proof. intros. @@ -1319,3 +1249,175 @@ Proof. Qed. End SOUNDNESS. + +Theorem transf_program_correct: + forall p tp, match_prog p tp -> forward_simulation (semantics p) (semantics tp). +Proof. + intros p tp (used & A & B). apply transf_program_correct_1 with used; auto. +Qed. + +(** * Commutation with linking *) + +Remark link_def_either: + forall (gd1 gd2 gd: globdef fundef unit), + link_def gd1 gd2 = Some gd -> gd = gd1 \/ gd = gd2. +Proof with (try discriminate). + intros until gd. +Local Transparent Linker_def Linker_fundef Linker_varinit Linker_vardef Linker_unit. + destruct gd1 as [f1|v1], gd2 as [f2|v2]... +(* Two fundefs *) + destruct f1 as [f1|ef1], f2 as [f2|ef2]; simpl... + destruct ef2; intuition congruence. + destruct ef1; intuition congruence. + destruct (external_function_eq ef1 ef2); intuition congruence. +(* Two vardefs *) + simpl. unfold link_vardef. destruct v1 as [info1 init1 ro1 vo1], v2 as [info2 init2 ro2 vo2]; simpl. + destruct (link_varinit init1 init2) as [init|] eqn:LI... + destruct (eqb ro1 ro2) eqn:RO... + destruct (eqb vo1 vo2) eqn:VO... + simpl. + destruct info1, info2. + assert (EITHER: init = init1 \/ init = init2). + { revert LI. unfold link_varinit. + destruct (classify_init init1), (classify_init init2); intro EQ; inv EQ; auto. + destruct (zeq sz (Z.max sz0 0 + 0)); inv H0; auto. + destruct (zeq sz (init_data_list_size il)); inv H0; auto. + destruct (zeq sz (init_data_list_size il)); inv H0; auto. } + apply eqb_prop in RO. apply eqb_prop in VO. + intro EQ; inv EQ. destruct EITHER; subst init; auto. +Qed. + +Remark used_not_defined: + forall p used id, + valid_used_set p used -> + (prog_defmap p)!id = None -> + IS.mem id used = false \/ id = prog_main p. +Proof. + intros. destruct (IS.mem id used) eqn:M; auto. + exploit used_defined; eauto using IS.mem_2. intros [A|A]; auto. + apply prog_defmap_dom in A. destruct A as [g E]; congruence. +Qed. + +Remark used_not_defined_2: + forall p used id, + valid_used_set p used -> + id <> prog_main p -> + (prog_defmap p)!id = None -> + ~IS.In id used. +Proof. + intros. exploit used_not_defined; eauto. intros [A|A]. + red; intros; apply IS.mem_1 in H2; congruence. + congruence. +Qed. + +Lemma link_valid_used_set: + forall p1 p2 p used1 used2, + link p1 p2 = Some p -> + valid_used_set p1 used1 -> + valid_used_set p2 used2 -> + valid_used_set p (IS.union used1 used2). +Proof. + intros until used2; intros L V1 V2. + destruct (link_prog_inv _ _ _ L) as (X & Y & Z). + rewrite Z; clear Z; constructor. +- intros. rewrite ISF.union_iff in H. rewrite ISF.union_iff. + rewrite prog_defmap_elements, PTree.gcombine in H0. + destruct (prog_defmap p1)!id as [gd1|] eqn:GD1; + destruct (prog_defmap p2)!id as [gd2|] eqn:GD2; + simpl in H0; try discriminate. ++ (* common definition *) + exploit Y; eauto. intros (PUB1 & PUB2 & _). + exploit link_def_either; eauto. intros [EQ|EQ]; subst gd. +* left. eapply used_closed. eexact V1. eapply used_public. eexact V1. eauto. eauto. auto. +* right. eapply used_closed. eexact V2. eapply used_public. eexact V2. eauto. eauto. auto. ++ (* left definition *) + inv H0. destruct (ISP.In_dec id used1). +* left; eapply used_closed; eauto. +* assert (IS.In id used2) by tauto. + exploit used_defined. eexact V2. eauto. intros [A|A]. + exploit prog_defmap_dom; eauto. intros [g E]; congruence. + elim n. rewrite A, <- X. eapply used_main; eauto. ++ (* right definition *) + inv H0. destruct (ISP.In_dec id used2). +* right; eapply used_closed; eauto. +* assert (IS.In id used1) by tauto. + exploit used_defined. eexact V1. eauto. intros [A|A]. + exploit prog_defmap_dom; eauto. intros [g E]; congruence. + elim n. rewrite A, X. eapply used_main; eauto. ++ (* no definition *) + auto. +- simpl. rewrite ISF.union_iff; left; eapply used_main; eauto. +- simpl. intros id. rewrite in_app_iff, ISF.union_iff. + intros [A|A]; [left|right]; eapply used_public; eauto. +- intros. rewrite ISF.union_iff in H. + destruct (ident_eq id (prog_main p1)). ++ right; assumption. ++ assert (E: exists g, link_prog_merge (prog_defmap p1)!id (prog_defmap p2)!id = Some g). + { destruct (prog_defmap p1)!id as [gd1|] eqn:GD1; + destruct (prog_defmap p2)!id as [gd2|] eqn:GD2; simpl. + * apply Y with id; auto. + * exists gd1; auto. + * exists gd2; auto. + * eapply used_not_defined_2 in GD1; eauto. eapply used_not_defined_2 in GD2; eauto. + tauto. + congruence. + } + destruct E as [g LD]. + left. unfold prog_defs_names; simpl. + change id with (fst (id, g)). apply in_map. apply PTree.elements_correct. + rewrite PTree.gcombine; auto. +Qed. + +Theorem link_match_program: + forall p1 p2 tp1 tp2 p, + link p1 p2 = Some p -> + match_prog p1 tp1 -> match_prog p2 tp2 -> + exists tp, link tp1 tp2 = Some tp /\ match_prog p tp. +Proof. + intros. destruct H0 as (used1 & A1 & B1). destruct H1 as (used2 & A2 & B2). + destruct (link_prog_inv _ _ _ H) as (U & V & W). + econstructor; split. +- apply link_prog_succeeds. ++ rewrite (match_prog_main _ _ _ B1), (match_prog_main _ _ _ B2). auto. ++ intros. + rewrite (match_prog_def _ _ _ B1) in H0. + rewrite (match_prog_def _ _ _ B2) in H1. + destruct (IS.mem id used1) eqn:U1; try discriminate. + destruct (IS.mem id used2) eqn:U2; try discriminate. + edestruct V as (X & Y & gd & Z); eauto. + split. rewrite (match_prog_public _ _ _ B1); auto. + split. rewrite (match_prog_public _ _ _ B2); auto. + congruence. +- exists (IS.union used1 used2); split. ++ eapply link_valid_used_set; eauto. ++ rewrite W. constructor; simpl; intros. +* eapply match_prog_main; eauto. +* rewrite (match_prog_public _ _ _ B1), (match_prog_public _ _ _ B2). auto. +* rewrite ! prog_defmap_elements, !PTree.gcombine by auto. + rewrite (match_prog_def _ _ _ B1 id), (match_prog_def _ _ _ B2 id). + rewrite ISF.union_b. +{ + destruct (prog_defmap p1)!id as [gd1|] eqn:GD1; + destruct (prog_defmap p2)!id as [gd2|] eqn:GD2. +- (* both defined *) + exploit V; eauto. intros (PUB1 & PUB2 & _). + assert (EQ1: IS.mem id used1 = true) by (apply IS.mem_1; eapply used_public; eauto). + assert (EQ2: IS.mem id used2 = true) by (apply IS.mem_1; eapply used_public; eauto). + rewrite EQ1, EQ2; auto. +- (* left defined *) + exploit used_not_defined; eauto. intros [A|A]. + rewrite A, orb_false_r. destruct (IS.mem id used1); auto. + replace (IS.mem id used1) with true. destruct (IS.mem id used2); auto. + symmetry. apply IS.mem_1. rewrite A, <- U. eapply used_main; eauto. +- (* right defined *) + exploit used_not_defined. eexact A1. eauto. intros [A|A]. + rewrite A, orb_false_l. destruct (IS.mem id used2); auto. + replace (IS.mem id used2) with true. destruct (IS.mem id used1); auto. + symmetry. apply IS.mem_1. rewrite A, U. eapply used_main; eauto. +- (* none defined *) + destruct (IS.mem id used1), (IS.mem id used2); auto. +} +* intros. apply PTree.elements_keys_norepet. +Qed. + +Instance TransfSelectionLink : TransfLink match_prog := link_match_program. -- cgit