diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-21 08:48:20 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-21 08:48:20 +0100 |
commit | 01e32a075023ce7b037d42d048b1904ba3d9a82b (patch) | |
tree | 2d01f3855234e6eb945b929e489232001c406592 /common | |
parent | 093e0ea167fde39429bf4bd3fc693a232af0d093 (diff) | |
parent | 1fdca8371317e656cb08eaec3adb4596d6447e9b (diff) | |
download | compcert-01e32a075023ce7b037d42d048b1904ba3d9a82b.tar.gz compcert-01e32a075023ce7b037d42d048b1904ba3d9a82b.zip |
Merge branch 'master' into cleanup
Diffstat (limited to 'common')
-rw-r--r-- | common/AST.v | 576 | ||||
-rw-r--r-- | common/Behaviors.v | 96 | ||||
-rw-r--r-- | common/Events.v | 84 | ||||
-rw-r--r-- | common/Globalenvs.v | 1875 | ||||
-rw-r--r-- | common/Linking.v | 905 | ||||
-rw-r--r-- | common/Memory.v | 61 | ||||
-rw-r--r-- | common/PrintAST.ml | 5 | ||||
-rw-r--r-- | common/Smallstep.v | 530 |
8 files changed, 2166 insertions, 1966 deletions
diff --git a/common/AST.v b/common/AST.v index 16673c47..415e90e2 100644 --- a/common/AST.v +++ b/common/AST.v @@ -17,10 +17,7 @@ the abstract syntax trees of many of the intermediate languages. *) Require Import String. -Require Import Coqlib. -Require Import Errors. -Require Import Integers. -Require Import Floats. +Require Import Coqlib Maps Errors Integers Floats. Set Implicit Arguments. @@ -106,6 +103,12 @@ Record calling_convention : Type := mkcallconv { Definition cc_default := {| cc_vararg := false; cc_unproto := false; cc_structret := false |}. +Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}. +Proof. + decide equality; apply bool_dec. +Defined. +Global Opaque calling_convention_eq. + Record signature : Type := mksignature { sig_args: list typ; sig_res: option typ; @@ -120,8 +123,7 @@ Definition proj_sig_res (s: signature) : typ := Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}. Proof. - generalize opt_typ_eq, list_typ_eq; intros; decide equality. - generalize bool_dec; intros. decide equality. + generalize opt_typ_eq, list_typ_eq, calling_convention_eq; decide equality. Defined. Global Opaque signature_eq. @@ -189,6 +191,36 @@ Inductive init_data: Type := | Init_space: Z -> init_data | Init_addrof: ident -> int -> init_data. (**r address of symbol + offset *) +Definition init_data_size (i: init_data) : Z := + match i with + | Init_int8 _ => 1 + | Init_int16 _ => 2 + | Init_int32 _ => 4 + | Init_int64 _ => 8 + | Init_float32 _ => 4 + | Init_float64 _ => 8 + | Init_addrof _ _ => 4 + | Init_space n => Zmax n 0 + end. + +Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := + match il with + | nil => 0 + | i :: il' => init_data_size i + init_data_list_size il' + end. + +Lemma init_data_size_pos: + forall i, init_data_size i >= 0. +Proof. + destruct i; simpl; xomega. +Qed. + +Lemma init_data_list_size_pos: + forall il, init_data_list_size il >= 0. +Proof. + induction il; simpl. omega. generalize (init_data_size_pos a); omega. +Qed. + (** Information attached to global variables. *) Record globvar (V: Type) : Type := mkglobvar { @@ -226,6 +258,49 @@ Record program (F V: Type) : Type := mkprogram { Definition prog_defs_names (F V: Type) (p: program F V) : list ident := List.map fst p.(prog_defs). +(** The "definition map" of a program maps names of globals to their definitions. + If several definitions have the same name, the one appearing last in [p.(prog_defs)] wins. *) + +Definition prog_defmap (F V: Type) (p: program F V) : PTree.t (globdef F V) := + PTree_Properties.of_list p.(prog_defs). + +Section DEFMAP. + +Variables F V: Type. +Variable p: program F V. + +Lemma in_prog_defmap: + forall id g, (prog_defmap p)!id = Some g -> In (id, g) (prog_defs p). +Proof. + apply PTree_Properties.in_of_list. +Qed. + +Lemma prog_defmap_dom: + forall id, In id (prog_defs_names p) -> exists g, (prog_defmap p)!id = Some g. +Proof. + apply PTree_Properties.of_list_dom. +Qed. + +Lemma prog_defmap_unique: + forall defs1 id g defs2, + prog_defs p = defs1 ++ (id, g) :: defs2 -> + ~In id (map fst defs2) -> + (prog_defmap p)!id = Some g. +Proof. + unfold prog_defmap; intros. rewrite H. apply PTree_Properties.of_list_unique; auto. +Qed. + +Lemma prog_defmap_norepet: + forall id g, + list_norepet (prog_defs_names p) -> + In (id, g) (prog_defs p) -> + (prog_defmap p)!id = Some g. +Proof. + apply PTree_Properties.of_list_norepet. +Qed. + +End DEFMAP. + (** * Generic transformations over programs *) (** We now define a general iterator over programs that applies a given @@ -249,109 +324,44 @@ Definition transform_program (p: program A V) : program B V := p.(prog_public) p.(prog_main). -Lemma transform_program_function: - forall p i 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 transform_program. intros. - exploit list_in_map_inv; eauto. - intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. - exists f; auto. -Qed. - End TRANSF_PROGRAM. -(** General iterator over program that applies a given code transfomration - function to all function descriptions with their identifers and leaves - teh other parts of the program unchanged. *) - -Section TRANSF_PROGRAM_IDENT. - -Variable A B V: Type. -Variable transf: ident -> A -> B. - -Definition transform_program_globdef_ident (idg: ident * globdef A V) : ident * globdef B V := - match idg with - | (id, Gfun f) => (id, Gfun (transf id f)) - | (id, Gvar v) => (id, Gvar v) - end. - -Definition transform_program_ident (p: program A V): program B V := - mkprogram - (List.map transform_program_globdef_ident p.(prog_defs)) - p.(prog_public) - p.(prog_main). - -Lemma tranforma_program_function_ident: - forall p i tf, - In (i, Gfun tf) (transform_program_ident p).(prog_defs) -> - exists f, In (i, Gfun f) p.(prog_defs) /\ transf i f = tf. -Proof. - simpl. unfold transform_program_ident. intros. - exploit list_in_map_inv; eauto. - intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. - exists f; auto. -Qed. - -End TRANSF_PROGRAM_IDENT. - -(** 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. Also the transformation functions are defined - for the case the identifier of the function is passed as additional - argument *) +(** The following is a more general presentation of [transform_program]: +- Global variable information can be transformed, in addition to function + definitions. +- The transformation functions can fail and return an error message. +- The transformation for function definitions receives a global context + (derived from the compilation unit being transformed) as additiona + argument. +- The transformation functions receive the name of the global as + additional argument. *) Local Open Scope error_monad_scope. Section TRANSF_PROGRAM_GEN. Variables A B V W: Type. -Variable transf_fun: A -> res B. -Variable transf_fun_ident: ident -> A -> res B. -Variable transf_var: V -> res W. -Variable transf_var_ident: ident -> V -> res W. +Variable transf_fun: ident -> A -> res B. +Variable transf_var: ident -> 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)). - -Definition transf_globvar_ident (i: ident) (g: globvar V) : res (globvar W) := - do info' <- transf_var_ident i g.(gvar_info); +Definition transf_globvar (i: ident) (g: globvar V) : res (globvar W) := + do info' <- transf_var i g.(gvar_info); OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)). Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) := match l with | nil => OK nil | (id, Gfun f) :: l' => - match transf_fun f with + match transf_fun id 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. - -Fixpoint transf_globdefs_ident (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) := - match l with - | nil => OK nil - | (id, Gfun f) :: l' => - match transf_fun_ident id f with - | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg) - | OK tf => - do tl' <- transf_globdefs_ident l'; OK ((id, Gfun tf) :: tl') + do tl' <- transf_globdefs l'; OK ((id, Gfun tf) :: tl') end | (id, Gvar v) :: l' => - match transf_globvar_ident id v with + match transf_globvar id v with | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg) | OK tv => - do tl' <- transf_globdefs_ident l'; OK ((id, Gvar tv) :: tl') + do tl' <- transf_globdefs l'; OK ((id, Gvar tv) :: tl') end end. @@ -359,213 +369,6 @@ Definition transform_partial_program2 (p: program A V) : res (program B W) := do gl' <- transf_globdefs p.(prog_defs); OK (mkprogram gl' p.(prog_public) p.(prog_main)). -Definition transform_partial_ident_program2 (p: program A V) : res (program B W) := - do gl' <- transf_globdefs_ident p.(prog_defs); - OK (mkprogram gl' p.(prog_public) p.(prog_main)). - -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. - 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. - -Lemma transform_partial_ident_program2_function: - forall p tp i tf, - transform_partial_ident_program2 p = OK tp -> - In (i, Gfun tf) tp.(prog_defs) -> - exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun_ident i f = OK tf. -Proof. - 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_ident id 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_ident id 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. - -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. - 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. - - -Lemma transform_partial_ident_program2_variable: - forall p tp i tv, - transform_partial_ident_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_ident i v = OK tv.(gvar_info). -Proof. - 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_ident id 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_ident id 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. - -Lemma transform_partial_program2_succeeds: - forall p tp i g, - transform_partial_program2 p = OK tp -> - In (i, g) p.(prog_defs) -> - match g with - | Gfun fd => exists tfd, transf_fun fd = OK tfd - | Gvar gv => exists tv, transf_var gv.(gvar_info) = OK tv - end. -Proof. - intros. monadInv H. - revert x EQ H0. induction (prog_defs p); simpl; intros. - contradiction. - destruct a as [id1 g1]. destruct g1. - destruct (transf_fun f) eqn:TF; try discriminate. monadInv EQ. - destruct H0. inv H. econstructor; eauto. eapply IHl; eauto. - destruct (transf_globvar v) eqn:TV; try discriminate. monadInv EQ. - destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto. -Qed. - -Lemma transform_partial_ident_program2_succeeds: - forall p tp i g, - transform_partial_ident_program2 p = OK tp -> - In (i, g) p.(prog_defs) -> - match g with - | Gfun fd => exists tfd, transf_fun_ident i fd = OK tfd - | Gvar gv => exists tv, transf_var_ident i gv.(gvar_info) = OK tv - end. -Proof. - intros. monadInv H. - revert x EQ H0. induction (prog_defs p); simpl; intros. - contradiction. - destruct a as [id1 g1]. destruct g1. - destruct (transf_fun_ident id1 f) eqn:TF; try discriminate. monadInv EQ. - destruct H0. inv H. econstructor; eauto. eapply IHl; eauto. - destruct (transf_globvar_ident id1 v) eqn:TV; try discriminate. monadInv EQ. - destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto. -Qed. - -Lemma transform_partial_program2_main: - forall p tp, - transform_partial_program2 p = OK tp -> - tp.(prog_main) = p.(prog_main). -Proof. - intros. monadInv H. reflexivity. -Qed. - -Lemma transform_partial_ident_program2_main: - forall p tp, - transform_partial_ident_program2 p = OK tp -> - tp.(prog_main) = p.(prog_main). -Proof. - intros. monadInv H. reflexivity. -Qed. - -Lemma transform_partial_program2_public: - forall p tp, - transform_partial_program2 p = OK tp -> - tp.(prog_public) = p.(prog_public). -Proof. - intros. monadInv H. reflexivity. -Qed. - -Lemma transform_partial_ident_program2_public: - forall p tp, - transform_partial_ident_program2 p = OK tp -> - tp.(prog_public) = p.(prog_public). -Proof. - intros. monadInv H. reflexivity. -Qed. - -(** Additionally, we can also "augment" the program with new global definitions - and a different "main" function. *) - -Section AUGMENT. - -Variable new_globs: list(ident * globdef B W). -Variable new_main: ident. - -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) p.(prog_public) new_main). - -Lemma transform_partial_augment_program_main: - forall p tp, - transform_partial_augment_program p = OK tp -> - tp.(prog_main) = new_main. -Proof. - intros. monadInv H. reflexivity. -Qed. - -Definition transform_partial_augment_ident_program (p: program A V) : res (program B W) := - do gl' <- transf_globdefs_ident p.(prog_defs); - OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main). - -Lemma transform_partial_augment_ident_program_main: - forall p tp, - transform_partial_augment_ident_program p = OK tp -> - tp.(prog_main) = new_main. -Proof. - intros. monadInv H. reflexivity. -Qed. - -End AUGMENT. - -Remark transform_partial_program2_augment: - forall p, - transform_partial_program2 p = - transform_partial_augment_program nil p.(prog_main) p. -Proof. - 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. - -Remark transform_partial_ident_program2_augment: - forall p, - transform_partial_ident_program2 p = - transform_partial_augment_ident_program nil p.(prog_main) p. -Proof. - unfold transform_partial_ident_program2, transform_partial_augment_ident_program; intros. - destruct (transf_globdefs_ident (prog_defs p)); auto. - simpl. f_equal. f_equal. rewrite <- app_nil_end. auto. -Qed. - End TRANSF_PROGRAM_GEN. (** The following is a special case of [transform_partial_program2], @@ -574,178 +377,26 @@ End TRANSF_PROGRAM_GEN. Section TRANSF_PARTIAL_PROGRAM. Variable A B V: Type. -Variable transf_partial: A -> res B. -Variable transf_partial_ident: ident -> A -> res B. +Variable transf_fun: A -> res B. Definition transform_partial_program (p: program A V) : res (program B V) := - transform_partial_program2 transf_partial (fun v => OK v) p. - -Definition transform_partial_ident_program (p: program A V) : res (program B V) := - transform_partial_ident_program2 transf_partial_ident (fun _ v => OK v) p. - -Lemma transform_partial_program_main: - forall p tp, - transform_partial_program p = OK tp -> - tp.(prog_main) = p.(prog_main). -Proof. - apply transform_partial_program2_main. -Qed. - -Lemma transform_partial_ident_program_main: - forall p tp, - transform_partial_ident_program p = OK tp -> - tp.(prog_main) = p.(prog_main). -Proof. - apply transform_partial_ident_program2_main. -Qed. - -Lemma transform_partial_program_public: - forall p tp, - transform_partial_program p = OK tp -> - tp.(prog_public) = p.(prog_public). -Proof. - apply transform_partial_program2_public. -Qed. - -Lemma transform_partial_ident_program_public: - forall p tp, - transform_partial_ident_program p = OK tp -> - tp.(prog_public) = p.(prog_public). -Proof. - apply transform_partial_ident_program2_public. -Qed. - -Lemma transform_partial_program_function: - forall p tp i tf, - 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. - apply transform_partial_program2_function. -Qed. - -Lemma transform_partial_ident_program_function: - forall p tp i tf, - transform_partial_ident_program p = OK tp -> - In (i, Gfun tf) tp.(prog_defs) -> - exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial_ident i f = OK tf. -Proof. - apply transform_partial_ident_program2_function. -Qed. - -Lemma transform_partial_program_succeeds: - forall p tp i fd, - transform_partial_program p = OK tp -> - In (i, Gfun fd) p.(prog_defs) -> - exists tfd, transf_partial fd = OK tfd. -Proof. - unfold transform_partial_program; intros. - exploit transform_partial_program2_succeeds; eauto. -Qed. - -Lemma transform_partial_ident_program_succeeds: - forall p tp i fd, - transform_partial_ident_program p = OK tp -> - In (i, Gfun fd) p.(prog_defs) -> - exists tfd, transf_partial_ident i fd = OK tfd. -Proof. - unfold transform_partial_ident_program; intros. - exploit transform_partial_ident_program2_succeeds; eauto. -Qed. + transform_partial_program2 (fun i f => transf_fun f) (fun i v => OK v) p. End TRANSF_PARTIAL_PROGRAM. 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. - 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. - -Lemma transform_program_partial_ident_program: - forall (A B V: Type) (transf: ident -> A -> B) (p: program A V), - transform_partial_ident_program (fun id f => OK(transf id f)) p = OK(transform_program_ident transf p). -Proof. - intros. - unfold transform_partial_ident_program, transform_partial_ident_program2, transform_program; intros. - replace (transf_globdefs_ident (fun id f => OK (transf id f)) (fun _ v => OK v) p.(prog_defs)) - with (OK (map (transform_program_globdef_ident transf) p.(prog_defs))). - auto. - induction (prog_defs p); simpl. - auto. - destruct a as [id [f|v]]; rewrite <- IHl. - auto. - destruct v; auto. -Qed. - -(** The following is a relational presentation of - [transform_partial_augment_preogram]. Given relations between function - definitions and between variable information, it defines a relation - between programs stating that the two programs have appropriately related - shapes (global names are preserved and possibly augmented, etc) - and that identically-named function definitions - and variable information are related. *) - -Section MATCH_PROGRAM. - -Variable A B V W: Type. -Variable match_fundef: A -> B -> Prop. -Variable match_varinfo: V -> W -> Prop. - -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_globdef (id, Gvar (mkglobvar info1 init ro vo)) (id, Gvar (mkglobvar info2 init ro vo)). - -Definition match_program (new_globs : list (ident * globdef B W)) - (new_main : ident) - (p1: program A V) (p2: program B W) : Prop := - (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\ - p2.(prog_defs) = tglob ++ new_globs) /\ - p2.(prog_main) = new_main /\ - p2.(prog_public) = p1.(prog_public). - -End MATCH_PROGRAM. - -Lemma transform_partial_augment_program_match: - forall (A B V W: Type) - (transf_fun: A -> res B) - (transf_var: V -> res W) - (p: program A V) - (new_globs : list (ident * globdef B W)) - (new_main : ident) - (tp: program B W), - transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK tp -> - match_program - (fun fd tfd => transf_fun fd = OK tfd) - (fun info tinfo => transf_var info = OK tinfo) - new_globs new_main - p tp. + forall (A B V: Type) (transf_fun: A -> B) (p: program A V), + transform_partial_program (fun f => OK (transf_fun f)) p = OK (transform_program transf_fun p). Proof. - 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. + intros. unfold transform_partial_program, transform_partial_program2. + assert (EQ: forall l, + transf_globdefs (fun i f => OK (transf_fun f)) (fun i (v: V) => OK v) l = + OK (List.map (transform_program_globdef transf_fun) l)). + { induction l as [ | [id g] l]; simpl. + - auto. + - destruct g; simpl; rewrite IHl; simpl. auto. destruct v; auto. + } + rewrite EQ; simpl. auto. Qed. (** * External functions *) @@ -763,6 +414,9 @@ Inductive external_function : Type := | EF_builtin (name: string) (sg: signature) (** A compiler built-in function. Behaves like an external, but can be inlined by the compiler. *) + | EF_runtime (name: string) (sg: signature) + (** A function from the run-time library. Behaves like an + external, but must not be redefined. *) | EF_vload (chunk: memory_chunk) (** A volatile read operation. If the adress given as first argument points within a volatile global variable, generate an @@ -808,6 +462,7 @@ Definition ef_sig (ef: external_function): signature := match ef with | EF_external name sg => sg | EF_builtin name sg => sg + | EF_runtime name sg => sg | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default @@ -825,6 +480,7 @@ Definition ef_inline (ef: external_function) : bool := match ef with | EF_external name sg => false | EF_builtin name sg => true + | EF_runtime name sg => false | EF_vload chunk => true | EF_vstore chunk => true | EF_malloc => false diff --git a/common/Behaviors.v b/common/Behaviors.v index 1a6b8bd6..ef99b205 100644 --- a/common/Behaviors.v +++ b/common/Behaviors.v @@ -281,31 +281,29 @@ End PROGRAM_BEHAVIORS. Section FORWARD_SIMULATIONS. -Variable L1: semantics. -Variable L2: semantics. -Variable S: forward_simulation L1 L2. +Context L1 L2 index order match_states (S: fsim_properties L1 L2 index order match_states). Lemma forward_simulation_state_behaves: forall i s1 s2 beh1, - S i s1 s2 -> state_behaves L1 s1 beh1 -> + match_states i s1 s2 -> state_behaves L1 s1 beh1 -> exists beh2, state_behaves L2 s2 beh2 /\ behavior_improves beh1 beh2. Proof. intros. inv H0. -(* termination *) +- (* termination *) exploit simulation_star; eauto. intros [i' [s2' [A B]]]. exists (Terminates t r); split. econstructor; eauto. eapply fsim_match_final_states; eauto. apply behavior_improves_refl. -(* silent divergence *) +- (* silent divergence *) exploit simulation_star; eauto. intros [i' [s2' [A B]]]. exists (Diverges t); split. econstructor; eauto. eapply simulation_forever_silent; eauto. apply behavior_improves_refl. -(* reactive divergence *) +- (* reactive divergence *) exists (Reacts T); split. econstructor. eapply simulation_forever_reactive; eauto. apply behavior_improves_refl. -(* going wrong *) +- (* going wrong *) exploit simulation_star; eauto. intros [i' [s2' [A B]]]. destruct (state_behaves_exists L2 s2') as [beh' SB]. exists (behavior_app t beh'); split. @@ -315,16 +313,19 @@ Proof. simpl. decEq. traceEq. Qed. +End FORWARD_SIMULATIONS. + Theorem forward_simulation_behavior_improves: + forall L1 L2, forward_simulation L1 L2 -> forall beh1, program_behaves L1 beh1 -> exists beh2, program_behaves L2 beh2 /\ behavior_improves beh1 beh2. Proof. - intros. inv H. -(* initial state defined *) + intros L1 L2 FS. destruct FS as [init order match_states S]. intros. inv H. +- (* initial state defined *) exploit (fsim_match_initial_states S); eauto. intros [i [s' [INIT MATCH]]]. exploit forward_simulation_state_behaves; eauto. intros [beh2 [A B]]. exists beh2; split; auto. econstructor; eauto. -(* initial state undefined *) +- (* initial state undefined *) destruct (classic (exists s', initial_state L2 s')). destruct H as [s' INIT]. destruct (state_behaves_exists L2 s') as [beh' SB]. @@ -336,6 +337,7 @@ Proof. Qed. Corollary forward_simulation_same_safe_behavior: + forall L1 L2, forward_simulation L1 L2 -> forall beh, program_behaves L1 beh -> not_wrong beh -> program_behaves L2 beh. @@ -343,18 +345,14 @@ Proof. intros. exploit forward_simulation_behavior_improves; eauto. intros [beh' [A B]]. destruct B. congruence. - destruct H1 as [t [C D]]. subst. contradiction. + destruct H2 as [t [C D]]. subst. contradiction. Qed. -End FORWARD_SIMULATIONS. - (** * Backward simulations and program behaviors *) Section BACKWARD_SIMULATIONS. -Variable L1: semantics. -Variable L2: semantics. -Variable S: backward_simulation L1 L2. +Context L1 L2 index order match_states (S: bsim_properties L1 L2 index order match_states). Definition safe_along_behavior (s: state L1) (b: program_behavior) : Prop := forall t1 s' b2, Star L1 s t1 s' -> b = behavior_app t1 b2 -> @@ -402,8 +400,8 @@ Qed. Lemma backward_simulation_star: forall s2 t s2', Star L2 s2 t s2' -> - forall i s1 b, S i s1 s2 -> safe_along_behavior s1 (behavior_app t b) -> - exists i', exists s1', Star L1 s1 t s1' /\ S i' s1' s2'. + forall i s1 b, match_states i s1 s2 -> safe_along_behavior s1 (behavior_app t b) -> + exists i', exists s1', Star L1 s1 t s1' /\ match_states i' s1' s2'. Proof. induction 1; intros. exists i; exists s1; split; auto. apply star_refl. @@ -418,12 +416,12 @@ Qed. Lemma backward_simulation_forever_silent: forall i s1 s2, - Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 -> + Forever_silent L2 s2 -> match_states i s1 s2 -> safe L1 s1 -> Forever_silent L1 s1. Proof. assert (forall i s1 s2, - Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 -> - forever_silent_N (step L1) (bsim_order S) (globalenv L1) i s1). + Forever_silent L2 s2 -> match_states i s1 s2 -> safe L1 s1 -> + forever_silent_N (step L1) order (globalenv L1) i s1). cofix COINDHYP; intros. inv H. destruct (bsim_simulation S _ _ _ H2 _ H0 H1) as [i' [s2' [A B]]]. destruct A as [C | [C D]]. @@ -431,29 +429,29 @@ Proof. eapply star_safe; eauto. apply plus_star; auto. eapply forever_silent_N_star; eauto. eapply COINDHYP; eauto. eapply star_safe; eauto. - intros. eapply forever_silent_N_forever; eauto. apply bsim_order_wf. + intros. eapply forever_silent_N_forever; eauto. eapply bsim_order_wf; eauto. Qed. Lemma backward_simulation_forever_reactive: forall i s1 s2 T, - Forever_reactive L2 s2 T -> S i s1 s2 -> safe_along_behavior s1 (Reacts T) -> + Forever_reactive L2 s2 T -> match_states i s1 s2 -> safe_along_behavior s1 (Reacts T) -> Forever_reactive L1 s1 T. Proof. cofix COINDHYP; intros. inv H. - destruct (backward_simulation_star H2 _ (Reacts T0) H0) as [i' [s1' [A B]]]; eauto. + destruct (backward_simulation_star H2 (Reacts T0) H0) as [i' [s1' [A B]]]; eauto. econstructor; eauto. eapply COINDHYP; eauto. eapply star_safe_along; eauto. Qed. Lemma backward_simulation_state_behaves: forall i s1 s2 beh2, - S i s1 s2 -> state_behaves L2 s2 beh2 -> + match_states i s1 s2 -> state_behaves L2 s2 beh2 -> exists beh1, state_behaves L1 s1 beh1 /\ behavior_improves beh1 beh2. Proof. intros. destruct (classic (safe_along_behavior s1 beh2)). -(* 1. Safe along *) +- (* 1. Safe along *) exists beh2; split; [idtac|apply behavior_improves_refl]. inv H0. -(* termination *) ++ (* termination *) assert (Terminates t r = behavior_app t (Terminates E0 r)). simpl. rewrite E0_right; auto. rewrite H0 in H1. @@ -463,7 +461,7 @@ Proof. eapply safe_along_safe. eapply star_safe_along; eauto. intros [s1'' [C D]]. econstructor. eapply star_trans; eauto. traceEq. auto. -(* silent divergence *) ++ (* silent divergence *) assert (Diverges t = behavior_app t (Diverges E0)). simpl. rewrite E0_right; auto. rewrite H0 in H1. @@ -471,9 +469,9 @@ Proof. intros [i' [s1' [A B]]]. econstructor. eauto. eapply backward_simulation_forever_silent; eauto. eapply safe_along_safe. eapply star_safe_along; eauto. -(* reactive divergence *) ++ (* reactive divergence *) econstructor. eapply backward_simulation_forever_reactive; eauto. -(* goes wrong *) ++ (* goes wrong *) assert (Goes_wrong t = behavior_app t (Goes_wrong E0)). simpl. rewrite E0_right; auto. rewrite H0 in H1. @@ -484,7 +482,7 @@ Proof. elim (H4 _ FIN). elim (H3 _ _ STEP2). -(* 2. Not safe along *) +- (* 2. Not safe along *) exploit not_safe_along_behavior; eauto. intros [t [s1' [PREF [STEPS [NOSTEP NOFIN]]]]]. exists (Goes_wrong t); split. @@ -492,23 +490,26 @@ Proof. right. exists t; auto. Qed. +End BACKWARD_SIMULATIONS. + Theorem backward_simulation_behavior_improves: + forall L1 L2, backward_simulation L1 L2 -> forall beh2, program_behaves L2 beh2 -> exists beh1, program_behaves L1 beh1 /\ behavior_improves beh1 beh2. Proof. - intros. inv H. -(* L2's initial state is defined. *) + intros L1 L2 S beh2 H. destruct S as [index order match_states S]. inv H. +- (* L2's initial state is defined. *) destruct (classic (exists s1, initial_state L1 s1)) as [[s1 INIT] | NOINIT]. -(* L1's initial state is defined too. *) ++ (* L1's initial state is defined too. *) exploit (bsim_match_initial_states S); eauto. intros [i [s1' [INIT1' MATCH]]]. exploit backward_simulation_state_behaves; eauto. intros [beh1 [A B]]. exists beh1; split; auto. econstructor; eauto. -(* L1 has no initial state *) ++ (* L1 has no initial state *) exists (Goes_wrong E0); split. apply program_goes_initially_wrong. intros; red; intros. elim NOINIT; exists s0; auto. apply behavior_improves_bot. -(* L2 has no initial state *) +- (* L2 has no initial state *) exists (Goes_wrong E0); split. apply program_goes_initially_wrong. intros; red; intros. @@ -518,17 +519,16 @@ Proof. Qed. Corollary backward_simulation_same_safe_behavior: + forall L1 L2, backward_simulation L1 L2 -> (forall beh, program_behaves L1 beh -> not_wrong beh) -> (forall beh, program_behaves L2 beh -> program_behaves L1 beh). Proof. intros. exploit backward_simulation_behavior_improves; eauto. intros [beh' [A B]]. destruct B. congruence. - destruct H1 as [t [C D]]. subst. elim (H (Goes_wrong t)). auto. + destruct H2 as [t [C D]]. subst. elim (H0 (Goes_wrong t)). auto. Qed. -End BACKWARD_SIMULATIONS. - (** * Program behaviors for the "atomic" construction *) Section ATOMIC. @@ -635,7 +635,7 @@ Theorem atomic_behaviors: forall beh, program_behaves L beh <-> program_behaves (atomic L) beh. Proof. intros; split; intros. - (* L -> atomic L *) +- (* L -> atomic L *) exploit forward_simulation_behavior_improves. eapply atomic_forward_simulation. eauto. intros [beh2 [A B]]. red in B. destruct B as [EQ | [t [C D]]]. congruence. @@ -646,23 +646,23 @@ Proof. intros; red; intros. simpl in H. destruct H. eelim H4; eauto. apply program_goes_initially_wrong. intros; red; intros. simpl in H; destruct H. eelim H1; eauto. - (* atomic L -> L *) +- (* atomic L -> L *) inv H. - (* initial state defined *) ++ (* initial state defined *) destruct s as [t s]. simpl in H0. destruct H0; subst t. apply program_runs with s; auto. inv H1. - (* termination *) +* (* termination *) destruct s' as [t' s']. simpl in H2; destruct H2; subst t'. econstructor. eapply atomic_star_star; eauto. auto. - (* silent divergence *) +* (* silent divergence *) destruct s' as [t' s']. assert (t' = E0). inv H2. inv H1; auto. subst t'. econstructor. eapply atomic_star_star; eauto. change s' with (snd (E0,s')). apply atomic_forever_silent_forever_silent. auto. - (* reactive divergence *) +* (* reactive divergence *) econstructor. apply atomic_forever_reactive_forever_reactive. auto. - (* going wrong *) +* (* going wrong *) destruct s' as [t' s']. assert (t' = E0). destruct t'; auto. eelim H2. simpl. apply atomic_step_continue. @@ -672,7 +672,7 @@ Proof. elim (H2 E0 (E0,s'0)). constructor; auto. elim (H2 (e::nil) (t0,s'0)). constructor; auto. intros; red; intros. elim (H3 r). simpl; auto. - (* initial state undefined *) ++ (* initial state undefined *) apply program_goes_initially_wrong. intros; red; intros. elim (H0 (E0,s)); simpl; auto. Qed. diff --git a/common/Events.v b/common/Events.v index 7029a984..040029fb 100644 --- a/common/Events.v +++ b/common/Events.v @@ -619,9 +619,7 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := (** The semantics is invariant under change of global environment that preserves symbols. *) ec_symbols_preserved: forall ge1 ge2 vargs m1 t vres m2, - (forall id, Senv.find_symbol ge2 id = Senv.find_symbol ge1 id) -> - (forall id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id) -> - (forall b, Senv.block_is_volatile ge2 b = Senv.block_is_volatile ge1 b) -> + Senv.equiv ge1 ge2 -> sem ge1 vargs m1 t vres m2 -> sem ge2 vargs m1 t vres m2; @@ -704,17 +702,15 @@ Inductive volatile_load_sem (chunk: memory_chunk) (ge: Senv.t): Lemma volatile_load_preserved: forall ge1 ge2 chunk m b ofs t v, - (forall id, Senv.find_symbol ge2 id = Senv.find_symbol ge1 id) -> - (forall id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id) -> - (forall b, Senv.block_is_volatile ge2 b = Senv.block_is_volatile ge1 b) -> + Senv.equiv ge1 ge2 -> volatile_load ge1 chunk m b ofs t v -> volatile_load ge2 chunk m b ofs t v. Proof. - intros. inv H2; constructor; auto. - rewrite H1; auto. - rewrite H; auto. + intros. destruct H as (A & B & C). inv H0; constructor; auto. + rewrite C; auto. + rewrite A; auto. eapply eventval_match_preserved; eauto. - rewrite H1; auto. + rewrite C; auto. Qed. Lemma volatile_load_extends: @@ -773,7 +769,7 @@ Proof. - unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. eapply Mem.load_type; eauto. (* symbols *) -- inv H2. constructor. eapply volatile_load_preserved; eauto. +- inv H0. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) - inv H; auto. (* max perms *) @@ -817,17 +813,15 @@ Inductive volatile_store_sem (chunk: memory_chunk) (ge: Senv.t): Lemma volatile_store_preserved: forall ge1 ge2 chunk m1 b ofs v t m2, - (forall id, Senv.find_symbol ge2 id = Senv.find_symbol ge1 id) -> - (forall id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id) -> - (forall b, Senv.block_is_volatile ge2 b = Senv.block_is_volatile ge1 b) -> + Senv.equiv ge1 ge2 -> volatile_store ge1 chunk m1 b ofs v t m2 -> volatile_store ge2 chunk m1 b ofs v t m2. Proof. - intros. inv H2; constructor; auto. - rewrite H1; auto. - rewrite H; auto. + intros. destruct H as (A & B & C). inv H0; constructor; auto. + rewrite C; auto. + rewrite A; auto. eapply eventval_match_preserved; eauto. - rewrite H1; auto. + rewrite C; auto. Qed. Lemma volatile_store_readonly: @@ -925,7 +919,7 @@ Proof. (* well typed *) - unfold proj_sig_res; simpl. inv H; constructor. (* symbols preserved *) -- inv H2. constructor. eapply volatile_store_preserved; eauto. +- inv H0. constructor. eapply volatile_store_preserved; eauto. (* valid block *) - inv H. inv H1. auto. eauto with mem. (* perms *) @@ -972,19 +966,18 @@ Proof. Mem.store Mint32 m' b (-4) (Vint n) = Some m'' -> Mem.unchanged_on P m m''). { - intros; constructor; intros. - - split; intros; eauto with mem. - - assert (b0 <> b) by (eapply Mem.valid_not_valid_diff; eauto with mem). - erewrite Mem.store_mem_contents; eauto. rewrite Maps.PMap.gso by auto. - Local Transparent Mem.alloc. unfold Mem.alloc in H. injection H; intros A B. - rewrite <- B; simpl. rewrite A. rewrite Maps.PMap.gso by auto. auto. + intros. + apply Mem.unchanged_on_implies with (fun b1 ofs1 => b1 <> b). + apply Mem.unchanged_on_trans with m'. + eapply Mem.alloc_unchanged_on; eauto. + eapply Mem.store_unchanged_on; eauto. + intros. eapply Mem.valid_not_valid_diff; eauto with mem. } - constructor; intros. (* well typed *) - inv H. unfold proj_sig_res; simpl. auto. (* symbols preserved *) -- inv H2; econstructor; eauto. +- inv H0; econstructor; eauto. (* valid block *) - inv H. eauto with mem. (* perms *) @@ -1045,7 +1038,7 @@ Proof. (* well typed *) - inv H. unfold proj_sig_res. simpl. auto. (* symbols preserved *) -- inv H2; econstructor; eauto. +- inv H0; econstructor; eauto. (* valid block *) - inv H. eauto with mem. (* perms *) @@ -1124,7 +1117,7 @@ Proof. - (* return type *) intros. inv H. constructor. - (* change of globalenv *) - intros. inv H2. econstructor; eauto. + intros. inv H0. econstructor; eauto. - (* valid blocks *) intros. inv H. eauto with mem. - (* perms *) @@ -1235,7 +1228,7 @@ Proof. (* well typed *) - inv H. simpl. auto. (* symbols *) -- inv H2. econstructor; eauto. +- destruct H as (A & B & C). inv H0. econstructor; eauto. eapply eventval_list_match_preserved; eauto. (* valid blocks *) - inv H; auto. @@ -1280,7 +1273,7 @@ Proof. (* well typed *) - inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. (* symbols *) -- inv H2. econstructor; eauto. +- destruct H as (A & B & C). inv H0. econstructor; eauto. eapply eventval_match_preserved; eauto. (* valid blocks *) - inv H; auto. @@ -1324,7 +1317,7 @@ Proof. (* well typed *) - inv H. simpl. auto. (* symbols *) -- inv H2. econstructor; eauto. +- inv H0. econstructor; eauto. (* valid blocks *) - inv H; auto. (* perms *) @@ -1351,8 +1344,9 @@ Qed. (** ** Semantics of external functions. *) -(** For functions defined outside the program ([EF_external] and [EF_builtin]), - we do not define their semantics, but only assume that it satisfies +(** For functions defined outside the program ([EF_external], + [EF_builtin] and [EF_runtime]), we do not define their + semantics, but only assume that it satisfies [extcall_properties]. *) Parameter external_functions_sem: String.string -> signature -> extcall_sem. @@ -1384,6 +1378,7 @@ Definition external_call (ef: external_function): extcall_sem := match ef with | EF_external name sg => external_functions_sem name sg | EF_builtin name sg => external_functions_sem name sg + | EF_runtime name sg => external_functions_sem name sg | EF_vload chunk => volatile_load_sem chunk | EF_vstore chunk => volatile_store_sem chunk | EF_malloc => extcall_malloc_sem @@ -1402,6 +1397,7 @@ Proof. intros. unfold external_call, ef_sig; destruct ef. apply external_functions_properties. apply external_functions_properties. + apply external_functions_properties. apply volatile_load_ok. apply volatile_store_ok. apply extcall_malloc_ok. @@ -1414,7 +1410,7 @@ Proof. Qed. Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). -Definition external_call_symbols_preserved_gen ef := ec_symbols_preserved (external_call_spec ef). +Definition external_call_symbols_preserved ef := ec_symbols_preserved (external_call_spec ef). Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef). Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef). Definition external_call_readonly ef := ec_readonly (external_call_spec ef). @@ -1424,20 +1420,6 @@ Definition external_call_trace_length ef := ec_trace_length (external_call_spec Definition external_call_receptive ef := ec_receptive (external_call_spec ef). Definition external_call_determ ef := ec_determ (external_call_spec ef). -(** Special cases of [external_call_symbols_preserved_gen]. *) - -Lemma external_call_symbols_preserved: - forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2, - external_call ef ge1 vargs m1 t vres m2 -> - (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> - (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> - (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) -> - external_call ef ge2 vargs m1 t vres m2. -Proof. - intros. apply external_call_symbols_preserved_gen with (ge1 := ge1); auto. - intros. simpl. unfold Genv.block_is_volatile. rewrite H2. auto. -Qed. - (** Corollary of [external_call_valid_block]. *) Lemma external_call_nextblock: @@ -1596,9 +1578,7 @@ Qed. Lemma external_call_symbols_preserved': forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2, external_call' ef ge1 vargs m1 t vres m2 -> - (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> - (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> - (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) -> + Senv.equiv ge1 ge2 -> external_call' ef ge2 vargs m1 t vres m2. Proof. intros. inv H. exists v; auto. eapply external_call_symbols_preserved; eauto. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 5f78ea6b..a8d0512c 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -3,7 +3,6 @@ (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* with contributions from Andrew Tolmach (Portland State University) *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -36,14 +35,8 @@ Require Recdef. Require Import Zwf. -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. +Require Import Axioms Coqlib Errors Maps AST Linking. +Require Import Integers Floats Values Memory. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. @@ -113,6 +106,11 @@ Proof. intros. unfold symbol_address. destruct (find_symbol ge id); auto. Qed. +Definition equiv (se1 se2: t) : Prop := + (forall id, find_symbol se2 id = find_symbol se1 id) + /\ (forall id, public_symbol se2 id = public_symbol se1 id) + /\ (forall b, block_is_volatile se2 b = block_is_volatile se1 b). + End Senv. Module Genv. @@ -129,14 +127,10 @@ Variable V: Type. (**r The type of information attached to variables *) Record t: Type := mkgenv { genv_public: list ident; (**r which symbol names are public *) genv_symb: PTree.t block; (**r mapping symbol -> block *) - genv_funs: PTree.t F; (**r mapping function pointer -> definition *) - genv_vars: PTree.t (globvar V); (**r mapping variable pointer -> info *) + genv_defs: PTree.t (globdef F V); (**r mapping block -> definition *) genv_next: block; (**r next symbol pointer *) genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> Plt b genv_next; - genv_funs_range: forall b f, PTree.get b genv_funs = Some f -> Plt b genv_next; - genv_vars_range: forall b v, PTree.get b genv_vars = Some v -> Plt b genv_next; - genv_funs_vars: forall b1 b2 f v, - PTree.get b1 genv_funs = Some f -> PTree.get b2 genv_vars = Some v -> b1 <> b2; + genv_defs_range: forall b g, PTree.get b genv_defs = Some g -> Plt b genv_next; genv_vars_inj: forall id1 id2 b, PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2 }. @@ -166,11 +160,16 @@ Definition public_symbol (ge: t) (id: ident) : bool := | Some _ => In_dec ident_eq id ge.(genv_public) end. +(** [find_def ge b] returns the global definition associated with the given address. *) + +Definition find_def (ge: t) (b: block) : option (globdef F V) := + PTree.get b ge.(genv_defs). + (** [find_funct_ptr ge b] returns the function description associated with the given address. *) Definition find_funct_ptr (ge: t) (b: block) : option F := - PTree.get b ge.(genv_funs). + match find_def ge b with Some (Gfun f) => Some f | _ => None end. (** [find_funct] is similar to [find_funct_ptr], but the function address is given as a value, which must be a pointer with offset 0. *) @@ -192,7 +191,7 @@ Definition invert_symbol (ge: t) (b: block) : option ident := at address [b]. *) Definition find_var_info (ge: t) (b: block) : option (globvar V) := - PTree.get b ge.(genv_vars). + match find_def ge b with Some (Gvar v) => Some v | _ => None end. (** [block_is_volatile ge b] returns [true] if [b] points to a global variable of volatile type, [false] otherwise. *) @@ -209,16 +208,9 @@ Program Definition add_global (ge: t) (idg: ident * globdef F V) : t := @mkgenv ge.(genv_public) (PTree.set idg#1 ge.(genv_next) ge.(genv_symb)) - (match idg#2 with - | Gfun f => PTree.set ge.(genv_next) f ge.(genv_funs) - | Gvar v => ge.(genv_funs) - end) - (match idg#2 with - | Gfun f => ge.(genv_vars) - | Gvar v => PTree.set ge.(genv_next) v ge.(genv_vars) - end) + (PTree.set ge.(genv_next) idg#2 ge.(genv_defs)) (Psucc ge.(genv_next)) - _ _ _ _ _. + _ _ _. Next Obligation. destruct ge; simpl in *. rewrite PTree.gsspec in H. destruct (peq id i). inv H. apply Plt_succ. @@ -226,34 +218,12 @@ Next Obligation. Qed. Next Obligation. destruct ge; simpl in *. - destruct g. - rewrite PTree.gsspec in H. - destruct (peq b genv_next0). inv H. apply Plt_succ. - apply Plt_trans_succ; eauto. + rewrite PTree.gsspec in H. destruct (peq b genv_next0). + inv H. apply Plt_succ. apply Plt_trans_succ; eauto. Qed. Next Obligation. destruct ge; simpl in *. - destruct g. - apply Plt_trans_succ; eauto. - rewrite PTree.gsspec in H. - destruct (peq b genv_next0). inv H. apply Plt_succ. - apply Plt_trans_succ; eauto. -Qed. -Next Obligation. - destruct ge; simpl in *. - destruct g. - rewrite PTree.gsspec in H. - destruct (peq b1 genv_next0). inv H. - apply sym_not_equal; apply Plt_ne; eauto. - eauto. - rewrite PTree.gsspec in H0. - destruct (peq b2 genv_next0). inv H0. - apply Plt_ne; eauto. - 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. @@ -269,17 +239,11 @@ 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. + intros. apply fold_left_app. Qed. Program Definition empty_genv (pub: list ident): t := - @mkgenv pub (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _. -Next Obligation. - rewrite PTree.gempty in H. discriminate. -Qed. -Next Obligation. - rewrite PTree.gempty in H. discriminate. -Qed. + @mkgenv pub (PTree.empty _) (PTree.empty _) 1%positive _ _ _. Next Obligation. rewrite PTree.gempty in H. discriminate. Qed. @@ -400,84 +364,62 @@ Proof. intros; simpl. apply dec_eq_true. Qed. -Theorem find_symbol_exists: - forall p id g, - In (id, g) (prog_defs p) -> - exists b, find_symbol (globalenv p) id = Some b. +Theorem find_funct_ptr_iff: + forall ge b f, find_funct_ptr ge b = Some f <-> find_def ge b = Some (Gfun f). Proof. - 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. + intros. unfold find_funct_ptr. destruct (find_def ge b) as [[f1|v1]|]; intuition congruence. Qed. -Theorem find_funct_ptr_exists_2: - forall p gl1 id f gl2, - prog_defs p = gl1 ++ (id, Gfun f) :: gl2 -> ~In id (map fst gl2) -> - exists b, - find_symbol (globalenv p) id = Some b - /\ find_funct_ptr (globalenv p) b = Some f. +Theorem find_var_info_iff: + forall ge b v, find_var_info ge b = Some v <-> find_def ge b = Some (Gvar v). Proof. - intros; unfold globalenv. rewrite H. eapply add_globals_unique_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 PTree.gso. auto. - apply Plt_ne. eapply genv_funs_range; eauto. - auto. -(* ensures *) - intros. unfold find_symbol, find_funct_ptr in *; simpl. - exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. + intros. unfold find_var_info. destruct (find_def ge b) as [[f1|v1]|]; intuition congruence. Qed. -Corollary 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. +Theorem find_def_symbol: + forall p id g, + (prog_defmap p)!id = Some g <-> exists b, find_symbol (globalenv p) id = Some b /\ find_def (globalenv p) b = Some g. Proof. - intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). - eapply find_funct_ptr_exists_2; eauto. + intros. + set (P := fun m ge => m!id = Some g <-> exists b, find_symbol ge id = Some b /\ find_def ge b = Some g). + assert (REC: forall l m ge, + P m ge -> + P (fold_left (fun m idg => PTree.set idg#1 idg#2 m) l m) + (add_globals ge l)). + { induction l as [ | [id1 g1] l]; intros; simpl. + - auto. + - apply IHl. unfold P, add_global, find_symbol, find_def; simpl. + rewrite ! PTree.gsspec. destruct (peq id id1). + + subst id1. split; intros. + inv H0. exists (genv_next ge); split; auto. apply PTree.gss. + destruct H0 as (b & A & B). inv A. rewrite PTree.gss in B. auto. + + red in H; rewrite H. split. + intros (b & A & B). exists b; split; auto. rewrite PTree.gso; auto. + apply Plt_ne. eapply genv_symb_range; eauto. + intros (b & A & B). rewrite PTree.gso in B. exists b; auto. + apply Plt_ne. eapply genv_symb_range; eauto. + } + apply REC. unfold P, find_symbol, find_def; simpl. + rewrite ! PTree.gempty. split. + congruence. + intros (b & A & B); congruence. Qed. -Theorem find_var_exists_2: - forall p gl1 id v gl2, - prog_defs p = gl1 ++ (id, Gvar v) :: gl2 -> ~In id (map fst gl2) -> - exists b, - find_symbol (globalenv p) id = Some b - /\ find_var_info (globalenv p) b = Some v. +Theorem find_symbol_exists: + forall p id g, + In (id, g) (prog_defs p) -> + exists b, find_symbol (globalenv p) id = Some b. Proof. - intros; unfold globalenv. rewrite H. eapply add_globals_unique_ensures; eauto. + intros. unfold globalenv. eapply add_globals_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 PTree.gso. auto. - apply Plt_ne. eapply genv_vars_range; eauto. + intros. unfold find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id0). + econstructor; eauto. + auto. (* ensures *) - intros. unfold find_symbol, find_var_info in *; simpl. - exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. -Qed. - -Corollary find_var_exists: - 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 v. -Proof. - intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). - eapply find_var_exists_2; eauto. + intros. unfold find_symbol; simpl. rewrite PTree.gss. econstructor; eauto. Qed. -Lemma find_symbol_inversion : forall p x b, +Theorem find_symbol_inversion : forall p x b, find_symbol (globalenv p) x = Some b -> In x (prog_defs_names p). Proof. @@ -490,22 +432,30 @@ Proof. unfold find_symbol; simpl; intros. rewrite PTree.gempty in H. discriminate. Qed. -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). +Theorem find_def_inversion: + forall p b g, + find_def (globalenv p) b = Some g -> + exists id, In (id, g) (prog_defs p). Proof. - intros until f. unfold globalenv. apply add_globals_preserves. + intros until g. unfold globalenv. apply add_globals_preserves. (* preserves *) - unfold find_funct_ptr; simpl; intros. destruct g; auto. + unfold find_def; simpl; intros. rewrite PTree.gsspec in H1. destruct (peq b (genv_next ge)). inv H1. exists id; auto. auto. (* base *) - unfold find_funct_ptr; simpl; intros. rewrite PTree.gempty in H. discriminate. + unfold find_def; simpl; intros. rewrite PTree.gempty in H. discriminate. Qed. -Theorem find_funct_inversion: +Corollary 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. + intros. apply find_def_inversion with b. apply find_funct_ptr_iff; auto. +Qed. + +Corollary find_funct_inversion: forall p v f, find_funct (globalenv p) v = Some f -> exists id, In (id, Gfun f) (prog_defs p). @@ -533,25 +483,6 @@ Proof. 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, 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 PTree.gss in H2. inv H2. auto. - eelim Plt_strict. eapply genv_funs_range; eauto. - destruct g as [f1|v1]. rewrite PTree.gso in H2. auto. - apply Plt_ne. eapply genv_symb_range; eauto. - auto. -(* initial *) - intros. simpl in *. rewrite PTree.gempty in H. discriminate. -Qed. - - Theorem global_addresses_distinct: forall ge id1 id2 b1 b2, id1 <> id2 -> @@ -626,7 +557,7 @@ Theorem block_is_volatile_below: forall ge b, block_is_volatile ge b = true -> Plt b ge.(genv_next). Proof. unfold block_is_volatile; intros. destruct (find_var_info ge b) as [gv|] eqn:FV. - eapply genv_vars_range; eauto. + rewrite find_var_info_iff in FV. eapply genv_defs_range; eauto. discriminate. Qed. @@ -652,24 +583,6 @@ Section INITMEM. Variable ge: t. -Definition init_data_size (i: init_data) : Z := - match i with - | Init_int8 _ => 1 - | Init_int16 _ => 2 - | Init_int32 _ => 4 - | Init_int64 _ => 8 - | Init_float32 _ => 4 - | Init_float64 _ => 8 - | Init_addrof _ _ => 4 - | Init_space n => Zmax n 0 - end. - -Lemma init_data_size_pos: - forall i, init_data_size i >= 0. -Proof. - destruct i; simpl; try omega. generalize (Zle_max_r z 0). omega. -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) @@ -697,12 +610,6 @@ Fixpoint store_init_data_list (m: mem) (b: block) (p: Z) (idl: list init_data) end end. -Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := - match il with - | nil => 0 - | i :: il' => init_data_size i + init_data_list_size il' - end. - Definition perm_globvar (gv: globvar V) : permission := if gv.(gvar_volatile) then Nonempty else if gv.(gvar_readonly) then Readable @@ -818,22 +725,32 @@ Proof. congruence. Qed. -Remark store_init_data_list_perm: - forall k prm b' q idl b m p m', - store_init_data_list m b p idl = Some m' -> +Remark store_init_data_perm: + forall k prm b' q i b m p m', + store_init_data m b p i = Some m' -> (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. - induction idl; simpl; intros until m'. - intros. inv H. tauto. - caseEq (store_init_data m b p a); try congruence. intros. - rewrite <- (IHidl _ _ _ _ H0). + intros. 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)). + Mem.store chunk m b p v = Some m' -> + (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm)). intros; split; eauto with mem. - destruct a; simpl in H; eauto. + destruct i; simpl in H; eauto. inv H; tauto. - destruct (find_symbol ge i). eauto. discriminate. + destruct (find_symbol ge i); try discriminate. eauto. +Qed. + +Remark store_init_data_list_perm: + forall k prm b' q idl b m p m', + store_init_data_list m b p idl = Some m' -> + (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). +Proof. + induction idl as [ | i1 idl]; simpl; intros. +- inv H; tauto. +- destruct (store_init_data m b p i1) as [m1|] eqn:S1; try discriminate. + transitivity (Mem.perm m1 b' q k prm). + eapply store_init_data_perm; eauto. + eapply IHidl; eauto. Qed. Remark alloc_global_perm: @@ -883,36 +800,146 @@ Qed. (** Data preservation properties *) -Remark store_zeros_load_outside: - forall m b p n m', +Remark store_zeros_unchanged: + forall (P: block -> Z -> Prop) 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'. + (forall i, p <= i < p + n -> ~ P b i) -> + Mem.unchanged_on P m m'. Proof. intros until n. functional induction (store_zeros m b p n); intros. - inv H; auto. - transitivity (Mem.load chunk m' b' p'). - apply IHo. auto. intuition omega. - eapply Mem.load_store_other; eauto. simpl. intuition omega. - discriminate. +- inv H; apply Mem.unchanged_on_refl. +- apply Mem.unchanged_on_trans with m'. ++ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega. ++ apply IHo; auto. intros; apply H0; omega. +- discriminate. +Qed. + +Remark store_init_data_unchanged: + forall (P: block -> Z -> Prop) b i m p m', + store_init_data m b p i = Some m' -> + (forall ofs, p <= ofs < p + init_data_size i -> ~ P b ofs) -> + Mem.unchanged_on P m m'. +Proof. + intros. destruct i; simpl in *; + try (eapply Mem.store_unchanged_on; eauto; fail). + inv H; apply Mem.unchanged_on_refl. + destruct (find_symbol ge i); try congruence. + eapply Mem.store_unchanged_on; eauto. +Qed. + +Remark store_init_data_list_unchanged: + forall (P: block -> Z -> Prop) b il m p m', + store_init_data_list m b p il = Some m' -> + (forall ofs, p <= ofs -> ~ P b ofs) -> + Mem.unchanged_on P m m'. +Proof. + induction il; simpl; intros. +- inv H. apply Mem.unchanged_on_refl. +- destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. + apply Mem.unchanged_on_trans with m1. + eapply store_init_data_unchanged; eauto. intros; apply H0; tauto. + eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); omega. Qed. -Remark store_zeros_loadbytes_outside: +(** Properties related to [loadbytes] *) + +Definition readbytes_as_zero (m: mem) (b: block) (ofs len: Z) : Prop := + forall p n, + ofs <= p -> p + Z.of_nat n <= ofs + len -> + Mem.loadbytes m b p (Z.of_nat n) = Some (list_repeat n (Byte Byte.zero)). + +Lemma store_zeros_loadbytes: forall m b p n m', store_zeros m b p n = Some m' -> - forall b' p' n', - b' <> b \/ p' + n' <= p \/ p + n <= p' -> - Mem.loadbytes m' b' p' n' = Mem.loadbytes m b' p' n'. + readbytes_as_zero m' b p n. Proof. - intros until n. functional induction (store_zeros m b p n); intros. - inv H; auto. - transitivity (Mem.loadbytes m' b' p' n'). - apply IHo. auto. intuition omega. - eapply Mem.loadbytes_store_other; eauto. simpl. intuition omega. - discriminate. + intros until n; functional induction (store_zeros m b p n); red; intros. +- destruct n0. simpl. apply Mem.loadbytes_empty. omega. + rewrite inj_S in H1. omegaContradiction. +- destruct (zeq p0 p). + + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. omega. + rewrite inj_S in H1. rewrite inj_S. + replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by omega. + change (list_repeat (S n0) (Byte Byte.zero)) + with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)). + apply Mem.loadbytes_concat. + eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p). + eapply store_zeros_unchanged; eauto. intros; omega. + intros; omega. + change (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero). + change 1 with (size_chunk Mint8unsigned). + eapply Mem.loadbytes_store_same; eauto. + eapply IHo; eauto. omega. omega. omega. omega. + + eapply IHo; eauto. omega. omega. +- discriminate. Qed. +Definition bytes_of_init_data (i: init_data): list memval := + match i with + | Init_int8 n => inj_bytes (encode_int 1%nat (Int.unsigned n)) + | Init_int16 n => inj_bytes (encode_int 2%nat (Int.unsigned n)) + | Init_int32 n => inj_bytes (encode_int 4%nat (Int.unsigned n)) + | Init_int64 n => inj_bytes (encode_int 8%nat (Int64.unsigned n)) + | Init_float32 n => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n))) + | Init_float64 n => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n))) + | Init_space n => list_repeat (Z.to_nat n) (Byte Byte.zero) + | Init_addrof id ofs => + match find_symbol ge id with + | Some b => inj_value Q32 (Vptr b ofs) + | None => list_repeat 4%nat Undef + end + end. + +Lemma store_init_data_loadbytes: + forall m b p i m', + store_init_data m b p i = Some m' -> + readbytes_as_zero m b p (init_data_size i) -> + Mem.loadbytes m' b p (init_data_size i) = Some (bytes_of_init_data i). +Proof. + intros; destruct i; simpl in H; try apply (Mem.loadbytes_store_same _ _ _ _ _ _ H). +- inv H. simpl. + assert (EQ: Z.of_nat (Z.to_nat z) = Z.max z 0). + { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } + rewrite <- EQ. apply H0. omega. simpl. omega. +- simpl; destruct (find_symbol ge i) as [b'|]; try discriminate. + apply (Mem.loadbytes_store_same _ _ _ _ _ _ H). +Qed. + +Fixpoint bytes_of_init_data_list (il: list init_data): list memval := + match il with + | nil => nil + | i :: il => bytes_of_init_data i ++ bytes_of_init_data_list il + end. + +Lemma store_init_data_list_loadbytes: + forall b il m p m', + store_init_data_list m b p il = Some m' -> + readbytes_as_zero m b p (init_data_list_size il) -> + Mem.loadbytes m' b p (init_data_list_size il) = Some (bytes_of_init_data_list il). +Proof. + induction il as [ | i1 il]; simpl; intros. +- apply Mem.loadbytes_empty. omega. +- generalize (init_data_size_pos i1) (init_data_list_size_pos il); intros P1 PL. + destruct (store_init_data m b p i1) as [m1|] eqn:S; try discriminate. + apply Mem.loadbytes_concat. + eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 < p + init_data_size i1). + eapply store_init_data_list_unchanged; eauto. + intros; omega. + intros; omega. + eapply store_init_data_loadbytes; eauto. + red; intros; apply H0. omega. omega. + apply IHil with m1; auto. + red; intros. + eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => p + init_data_size i1 <= ofs1). + eapply store_init_data_unchanged; eauto. + intros; omega. + intros; omega. + apply H0. omega. omega. + auto. auto. +Qed. + +(** Properties related to [load] *) + Definition read_as_zero (m: mem) (b: block) (ofs len: Z) : Prop := forall chunk p, ofs <= p -> p + size_chunk chunk <= ofs + len -> @@ -926,32 +953,16 @@ Definition read_as_zero (m: mem) (b: block) (ofs len: Z) : Prop := | Many32 | Many64 => Vundef end). -Remark store_zeros_loadbytes: - forall m b p n m', - store_zeros m b p n = Some m' -> - forall p' n', - p <= p' -> p' + Z.of_nat n' <= p + n -> - Mem.loadbytes m' b p' (Z.of_nat n') = Some (list_repeat n' (Byte Byte.zero)). +Remark read_as_zero_unchanged: + forall (P: block -> Z -> Prop) m b ofs len m', + read_as_zero m b ofs len -> + Mem.unchanged_on P m m' -> + (forall i, ofs <= i < ofs + len -> P b i) -> + read_as_zero m' b ofs len. Proof. - intros until n; functional induction (store_zeros m b p n); intros. -- destruct n'. simpl. apply Mem.loadbytes_empty. omega. - rewrite inj_S in H1. omegaContradiction. -- destruct (zeq p' p). - + subst p'. destruct n'. simpl. apply Mem.loadbytes_empty. omega. - rewrite inj_S in H1. rewrite inj_S. - replace (Z.succ (Z.of_nat n')) with (1 + Z.of_nat n') by omega. - change (list_repeat (S n') (Byte Byte.zero)) - with ((Byte Byte.zero :: nil) ++ list_repeat n' (Byte Byte.zero)). - apply Mem.loadbytes_concat. - erewrite store_zeros_loadbytes_outside; eauto. - change (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero). - change 1 with (size_chunk Mint8unsigned). - eapply Mem.loadbytes_store_same; eauto. - right; omega. - eapply IHo; eauto. omega. omega. omega. omega. - + eapply IHo; eauto. omega. omega. -- discriminate. -Qed. + intros; red; intros. eapply Mem.load_unchanged_on; eauto. + intros; apply H1. omega. +Qed. Lemma store_zeros_read_as_zero: forall m b p n m', @@ -965,35 +976,6 @@ Proof. f_equal. destruct chunk; reflexivity. Qed. -Remark store_init_data_outside: - forall b i m p m', - store_init_data m b p i = Some m' -> - forall chunk b' q, - b' <> b \/ q + size_chunk chunk <= p \/ p + init_data_size i <= q -> - Mem.load chunk m' b' q = Mem.load chunk m b' q. -Proof. - intros. destruct i; simpl in *; - try (eapply Mem.load_store_other; eauto; fail). - inv H; auto. - destruct (find_symbol ge i); try congruence. - eapply Mem.load_store_other; eauto; intuition. -Qed. - -Remark store_init_data_list_outside: - forall b il m p m', - store_init_data_list m b p il = Some m' -> - forall chunk b' q, - b' <> b \/ q + size_chunk chunk <= p -> - Mem.load chunk m' b' q = Mem.load chunk m b' q. -Proof. - induction il; simpl. - intros; congruence. - 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. - eapply store_init_data_outside; eauto. tauto. -Qed. - Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {struct il} : Prop := match il with | nil => True @@ -1023,12 +1005,6 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s /\ load_store_init_data m b (p + Zmax n 0) il' end. -Remark init_data_list_size_pos: - forall il, init_data_list_size il >= 0. -Proof. - induction il; simpl. omega. generalize (init_data_size_pos a); omega. -Qed. - Lemma store_init_data_list_charact: forall b il m p m', store_init_data_list m b p il = Some m' -> @@ -1040,17 +1016,22 @@ Proof. store_init_data_list m1 b (p + size_chunk chunk) il = Some m' -> Mem.load chunk m' b p = Some(Val.load_result chunk v)). { - intros. transitivity (Mem.load chunk m1 b p). - eapply store_init_data_list_outside; eauto. right. omega. + intros. + eapply Mem.load_unchanged_on with (P := fun b' ofs' => ofs' < p + size_chunk chunk). + eapply store_init_data_list_unchanged; eauto. intros; omega. + intros; tauto. eapply Mem.load_store_same; eauto. } induction il; simpl. auto. intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. exploit IHil; eauto. - red; intros. transitivity (Mem.load chunk m b p0). - eapply store_init_data_outside. eauto. auto. - apply H0. generalize (init_data_size_pos a); omega. omega. auto. + set (P := fun (b': block) ofs' => p + init_data_size a <= ofs'). + apply read_as_zero_unchanged with (m := m) (P := P). + red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega. + eapply store_init_data_unchanged with (P := P); eauto. + intros; unfold P. omega. + intros; unfold P. omega. intro D. destruct a; simpl in Heqo; intuition. eapply (A Mint8unsigned (Vint i)); eauto. @@ -1059,56 +1040,60 @@ Proof. eapply (A Mint64 (Vlong i)); eauto. eapply (A Mfloat32 (Vsingle f)); eauto. eapply (A Mfloat64 (Vfloat f)); eauto. - inv Heqo. red; intros. transitivity (Mem.load chunk m1 b p0). - eapply store_init_data_list_outside; eauto. right. simpl. xomega. - apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega. + set (P := fun (b': block) ofs' => ofs' < p + init_data_size (Init_space z)). + inv Heqo. apply read_as_zero_unchanged with (m := m1) (P := P). + red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega. + eapply store_init_data_list_unchanged; eauto. + intros; unfold P. omega. + intros; unfold P. simpl; xomega. destruct (find_symbol ge i); try congruence. exists b0; split; auto. eapply (A Mint32 (Vptr b0 i0)); eauto. Qed. -Remark load_alloc_global: - forall chunk b p id g m m', +Remark alloc_global_unchanged: + forall (P: block -> Z -> Prop) m id g 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. + Mem.unchanged_on P m m'. Proof. 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 *) +- (* function *) + destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. + set (Q := fun b' (ofs: Z) => b' <> b). + apply Mem.unchanged_on_implies with Q. + apply Mem.unchanged_on_trans with m1. + eapply Mem.alloc_unchanged_on; eauto. + eapply Mem.drop_perm_unchanged_on; eauto. + intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem. +- (* 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. - transitivity (Mem.load chunk m1 b p). - eapply store_zeros_load_outside; eauto. - eapply Mem.load_alloc_unchanged; eauto. -Qed. - -Remark load_alloc_globals: - forall chunk b p gl m m', + 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. + set (Q := fun b' (ofs: Z) => b' <> b). + apply Mem.unchanged_on_implies with Q. + apply Mem.unchanged_on_trans with m1. + eapply Mem.alloc_unchanged_on; eauto. + apply Mem.unchanged_on_trans with m2. + eapply store_zeros_unchanged; eauto. + apply Mem.unchanged_on_trans with m3. + eapply store_init_data_list_unchanged; eauto. + eapply Mem.drop_perm_unchanged_on; eauto. + intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem. +Qed. + +Remark alloc_globals_unchanged: + forall (P: block -> Z -> Prop) 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. + Mem.unchanged_on P m m'. 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. - apply Plt_trans with (Mem.nextblock m); auto. apply Plt_succ. - destruct a as [id g]. eapply load_alloc_global; eauto. +- inv H. apply Mem.unchanged_on_refl. +- destruct (alloc_global m a) as [m''|] eqn:?; try discriminate. + destruct a as [id g]. + apply Mem.unchanged_on_trans with m''. + eapply alloc_global_unchanged; eauto. + apply IHgl; auto. Qed. Remark load_store_init_data_invariant: @@ -1119,125 +1104,101 @@ Remark load_store_init_data_invariant: Proof. induction il; intro p; simpl. auto. - repeat rewrite H. destruct a; intuition. red; intros; rewrite H; auto. -Qed. - -Definition variables_initialized (g: t) (m: mem) := - forall b gv, - find_var_info g b = Some gv -> - Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Cur (perm_globvar gv) - /\ (forall ofs k p, Mem.perm m b ofs k p -> - 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)). - -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). + rewrite ! H. destruct a; intuition. red; intros; rewrite H; auto. +Qed. + +Definition globals_initialized (g: t) (m: mem) := + forall b gd, + find_def g b = Some gd -> + match gd with + | Gfun f => + Mem.perm m b 0 Cur Nonempty + /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ p = Nonempty) + | Gvar v => + Mem.range_perm m b 0 (init_data_list_size v.(gvar_init)) Cur (perm_globvar v) + /\ (forall ofs k p, Mem.perm m b ofs k p -> + 0 <= ofs < init_data_list_size v.(gvar_init) /\ perm_order (perm_globvar v) p) + /\ (v.(gvar_volatile) = false -> load_store_init_data m b 0 v.(gvar_init)) + /\ (v.(gvar_volatile) = false -> Mem.loadbytes m b 0 (init_data_list_size v.(gvar_init)) = Some (bytes_of_init_data_list v.(gvar_init))) + end. 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'. + forall g m id gd m', + genv_next g = Mem.nextblock m -> + alloc_global m (id, gd) = Some m' -> + globals_initialized g m -> + globals_initialized (add_global g (id, gd)) m' + /\ genv_next (add_global g (id, gd)) = Mem.nextblock m'. Proof. intros. 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; auto. - 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 PTree.gsspec in H3. - destruct (peq b (genv_next ge0)). - (* same *) - inv H3. simpl in H0. - set (init := gvar_init gv) in *. +- (* globals-initialized *) + red; intros. unfold find_def in H2; simpl in H2. + rewrite PTree.gsspec in H2. destruct (peq b (genv_next g)). ++ inv H2. destruct gd0 as [f|v]; simpl in H0. +* destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC. + exploit Mem.alloc_result; eauto. intros RES. + rewrite H, <- RES. 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. } + exploit Mem.perm_drop_2; eauto. intros ORD. + split. omega. inv ORD; auto. +* 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. + 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. + replace (genv_next g) 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. + { eapply Mem.perm_alloc_3; eauto. + erewrite store_zeros_perm by eauto. + erewrite store_init_data_list_perm by eauto. + eapply Mem.perm_drop_4; eauto. } + split; auto. + eapply Mem.perm_drop_2; eauto. + split. intros NOTVOL. apply load_store_init_data_invariant with m3. + intros. eapply Mem.load_drop; eauto. right; right; right. + unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem. + eapply store_init_data_list_charact; eauto. eapply store_zeros_read_as_zero; eauto. - (* older var *) - exploit H1; eauto. intros [A [B C]]. - assert (D: Mem.valid_block m b). - red. exploit genv_vars_range; eauto. rewrite H; auto. - 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 PTree.gsspec in H3. - destruct (peq 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; auto. - 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; auto. - split. erewrite <- alloc_global_perm; eauto. - intros. eapply B. erewrite alloc_global_perm; eauto. -(* nextblock *) - rewrite NB. simpl. rewrite H. auto. + intros NOTVOL. + transitivity (Mem.loadbytes m3 b 0 sz). + eapply Mem.loadbytes_drop; eauto. right; right; right. + unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem. + eapply store_init_data_list_loadbytes; eauto. + eapply store_zeros_loadbytes; eauto. ++ assert (U: Mem.unchanged_on (fun _ _ => True) m m') by (eapply alloc_global_unchanged; eauto). + assert (VALID: Mem.valid_block m b). + { red. rewrite <- H. eapply genv_defs_range; eauto. } + exploit H1; eauto. + destruct gd0 as [f|v]. +* intros [A B]; split; intros. + eapply Mem.perm_unchanged_on; eauto. exact I. + eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I. +* intros (A & B & C & D). split; [| split; [| split]]. + red; intros. eapply Mem.perm_unchanged_on; eauto. exact I. + intros. eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I. + intros. apply load_store_init_data_invariant with m; auto. + intros. eapply Mem.load_unchanged_on_1; eauto. intros; exact I. + intros. eapply Mem.loadbytes_unchanged_on; eauto. intros; exact I. +- simpl. congruence. 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'. + genv_next ge = Mem.nextblock m -> + globals_initialized ge m -> + globals_initialized (add_globals ge gl) m'. Proof. induction gl; simpl; intros. - inv H0; auto. - 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]]. +- inv H; auto. +- destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|] eqn:?; try discriminate. + exploit alloc_global_initialized; eauto. intros [P Q]. eapply IHgl; eauto. Qed. @@ -1265,13 +1226,21 @@ Proof. eapply genv_symb_range; eauto. Qed. +Theorem find_def_not_fresh: + forall p b g m, + init_mem p = Some m -> + find_def (globalenv p) b = Some g -> Mem.valid_block m b. +Proof. + intros. red. erewrite <- init_mem_genv_next; eauto. + eapply genv_defs_range; eauto. +Qed. + 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. - intros. red. erewrite <- init_mem_genv_next; eauto. - eapply genv_funs_range; eauto. + intros. rewrite find_funct_ptr_iff in H0. eapply find_def_not_fresh; eauto. Qed. Theorem find_var_info_not_fresh: @@ -1279,8 +1248,18 @@ 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. - intros. red. erewrite <- init_mem_genv_next; eauto. - eapply genv_vars_range; eauto. + intros. rewrite find_var_info_iff in H0. eapply find_def_not_fresh; eauto. +Qed. + +Lemma init_mem_characterization_gen: + forall p m, + init_mem p = Some m -> + globals_initialized (globalenv p) (globalenv p) m. +Proof. + intros. apply alloc_globals_initialized with Mem.empty. + auto. + rewrite Mem.nextblock_empty. auto. + red; intros. unfold find_def in H0; simpl in H0; rewrite PTree.gempty in H0; discriminate. Qed. Theorem init_mem_characterization: @@ -1290,12 +1269,13 @@ Theorem init_mem_characterization: Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Cur (perm_globvar gv) /\ (forall ofs k p, Mem.perm m b ofs k p -> 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)). + /\ (gv.(gvar_volatile) = false -> + load_store_init_data (globalenv p) m b 0 gv.(gvar_init)) + /\ (gv.(gvar_volatile) = false -> + Mem.loadbytes m b 0 (init_data_list_size gv.(gvar_init)) = Some (bytes_of_init_data_list (globalenv p) gv.(gvar_init))). Proof. - intros. eapply alloc_globals_initialized; eauto. - rewrite Mem.nextblock_empty. auto. - red; intros. unfold find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence. - red; intros. unfold find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence. + intros. rewrite find_var_info_iff in H. + exploit init_mem_characterization_gen; eauto. Qed. Theorem init_mem_characterization_2: @@ -1303,12 +1283,10 @@ Theorem init_mem_characterization_2: 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). + /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ p = Nonempty). Proof. - intros. unfold init_mem in H0. eapply alloc_globals_initialized; eauto. - rewrite Mem.nextblock_empty. auto. - red; intros. unfold find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence. - red; intros. unfold find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence. + intros. rewrite find_funct_ptr_iff in H. + exploit init_mem_characterization_gen; eauto. Qed. (** ** Compatibility with memory injections *) @@ -1426,302 +1404,296 @@ Proof. apply Ple_refl. Qed. -Section INITMEM_AUGMENT_INJ. +(** ** Sufficient and necessary conditions for the initial memory to exist. *) + +(** Alignment properties *) + +Definition init_data_alignment (i: init_data) : Z := + match i with + | Init_int8 n => 1 + | Init_int16 n => 2 + | Init_int32 n => 4 + | Init_int64 n => 8 + | Init_float32 n => 4 + | Init_float64 n => 4 + | Init_addrof symb ofs => 4 + | Init_space n => 1 + end. + +Fixpoint init_data_list_aligned (p: Z) (il: list init_data) {struct il} : Prop := + match il with + | nil => True + | i1 :: il => (init_data_alignment i1 | p) /\ init_data_list_aligned (p + init_data_size i1) il + end. + +Section INITMEM_INVERSION. 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 -> - Ple thr b -> - store_zeros m2 b p n = Some m2' -> - Mem.inject (Mem.flat_inj thr) m1 m2'. +Lemma store_init_data_aligned: + forall m b p i m', + store_init_data ge m b p i = Some m' -> + (init_data_alignment i | p). 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 (plt b' thr). - inv H2. unfold Plt, Ple in *. zify; omega. - discriminate. - discriminate. + intros. + assert (DFL: forall chunk v, + Mem.store chunk m b p v = Some m' -> + align_chunk chunk = init_data_alignment i -> + (init_data_alignment i | p)). + { intros. apply Mem.store_valid_access_3 in H0. destruct H0. congruence. } + destruct i; simpl in H; eauto. + simpl. apply Z.divide_1_l. + destruct (find_symbol ge i); try discriminate. eauto. Qed. -Lemma store_init_data_augment: - forall m1 m2 b p id m2', - Mem.inject (Mem.flat_inj thr) m1 m2 -> - Ple thr b -> - store_init_data ge m2 b p id = Some m2' -> - Mem.inject (Mem.flat_inj thr) m1 m2'. -Proof. - intros until m2'. intros INJ BND ST. - assert (P: forall chunk ofs v m2', - Mem.store chunk m2 b ofs v = Some m2' -> - Mem.inject (Mem.flat_inj thr) m1 m2'). - intros. eapply Mem.store_outside_inject; eauto. - intros. unfold Mem.flat_inj in H0. - destruct (plt b' thr); inv H0. unfold Plt, Ple in *. zify; omega. - destruct id; simpl in ST; try (eapply P; eauto; fail). - congruence. - revert ST. caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. +Lemma store_init_data_list_aligned: + forall b il m p m', + store_init_data_list ge m b p il = Some m' -> + init_data_list_aligned p il. +Proof. + induction il as [ | i1 il]; simpl; intros. +- auto. +- destruct (store_init_data ge m b p i1) as [m1|] eqn:S1; try discriminate. + split; eauto. eapply store_init_data_aligned; eauto. Qed. -Lemma store_init_data_list_augment: - forall b idl m1 m2 p m2', - Mem.inject (Mem.flat_inj thr) m1 m2 -> - Ple thr b -> - store_init_data_list ge m2 b p idl = Some m2' -> - Mem.inject (Mem.flat_inj thr) m1 m2'. +Lemma store_init_data_list_free_idents: + forall b i o il m p m', + store_init_data_list ge m b p il = Some m' -> + In (Init_addrof i o) il -> + exists b', find_symbol ge i = Some b'. Proof. - induction idl; simpl. - intros; congruence. - intros until m2'; intros INJ FB. - caseEq (store_init_data ge m2 b p a); try congruence. intros. - eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto. + induction il as [ | i1 il]; simpl; intros. +- contradiction. +- destruct (store_init_data ge m b p i1) as [m1|] eqn:S1; try discriminate. + destruct H0. ++ subst i1. simpl in S1. destruct (find_symbol ge i) as [b'|]. exists b'; auto. discriminate. ++ eapply IHil; eauto. Qed. -Lemma alloc_global_augment: - forall idg m1 m2 m2', - alloc_global ge m2 idg = Some m2' -> - Mem.inject (Mem.flat_inj thr) m1 m2 -> - Ple thr (Mem.nextblock m2) -> - Mem.inject (Mem.flat_inj thr) m1 m2'. -Proof. - intros. destruct idg as [id [f|v]]; simpl in H. - (* function *) - destruct (Mem.alloc m2 0 1) as [m3 b] eqn:?. - assert (Ple thr b). 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 (plt b' thr); inv H3. - unfold Plt, Ple in *. zify; 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 (Ple thr b). 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 (plt b' thr); inv H3. - unfold Plt, Ple in *. zify; omega. -Qed. - -Lemma alloc_globals_augment: - forall gl m1 m2 m2', - alloc_globals ge m2 gl = Some m2' -> - Mem.inject (Mem.flat_inj thr) m1 m2 -> - Ple thr (Mem.nextblock m2) -> - Mem.inject (Mem.flat_inj thr) m1 m2'. -Proof. - induction gl; simpl. - intros. congruence. - 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). - apply Ple_trans with (Mem.nextblock m2); auto. apply Ple_succ. +End INITMEM_INVERSION. + +Theorem init_mem_inversion: + forall p m id v, + init_mem p = Some m -> + In (id, Gvar v) p.(prog_defs) -> + init_data_list_aligned 0 v.(gvar_init) + /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol (globalenv p) i = Some b. +Proof. + intros until v. unfold init_mem. set (ge := globalenv p). + revert m. generalize Mem.empty. generalize (prog_defs p). + induction l as [ | idg1 defs ]; simpl; intros m m'; intros. +- contradiction. +- destruct (alloc_global ge m idg1) as [m''|] eqn:A; try discriminate. + destruct H0. ++ subst idg1; simpl in A. + set (il := gvar_init v) in *. set (sz := init_data_list_size il) in *. + destruct (Mem.alloc m 0 sz) as [m1 b]. + destruct (store_zeros m1 b 0 sz) as [m2|]; try discriminate. + destruct (store_init_data_list ge m2 b 0 il) as [m3|] eqn:B; try discriminate. + split. eapply store_init_data_list_aligned; eauto. intros; eapply store_init_data_list_free_idents; eauto. ++ eapply IHdefs; eauto. +Qed. + +Section INITMEM_EXISTS. + +Variable ge: t. + +Lemma store_zeros_exists: + forall m b p n, + Mem.range_perm m b p (p + n) Cur Writable -> + exists m', store_zeros m b p n = Some m'. +Proof. + intros until n. functional induction (store_zeros m b p n); intros PERM. +- exists m; auto. +- apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. omega. +- destruct (Mem.valid_access_store m Mint8unsigned b p Vzero) as (m' & STORE). + split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega. + simpl. apply Z.divide_1_l. + congruence. Qed. -End INITMEM_AUGMENT_INJ. +Lemma store_init_data_exists: + forall m b p i, + Mem.range_perm m b p (p + init_data_size i) Cur Writable -> + (init_data_alignment i | p) -> + (forall id ofs, i = Init_addrof id ofs -> exists b, find_symbol ge id = Some b) -> + exists m', store_init_data ge m b p i = Some m'. +Proof. + intros. + assert (DFL: forall chunk v, + init_data_size i = size_chunk chunk -> + init_data_alignment i = align_chunk chunk -> + exists m', Mem.store chunk m b p v = Some m'). + { intros. destruct (Mem.valid_access_store m chunk b p v) as (m' & STORE). + split. rewrite <- H2; auto. rewrite <- H3; auto. + exists m'; auto. } + destruct i; eauto. + simpl. exists m; auto. + simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eauto. +Qed. + +Lemma store_init_data_list_exists: + forall b il m p, + Mem.range_perm m b p (p + init_data_list_size il) Cur Writable -> + init_data_list_aligned p il -> + (forall id ofs, In (Init_addrof id ofs) il -> exists b, find_symbol ge id = Some b) -> + exists m', store_init_data_list ge m b p il = Some m'. +Proof. + induction il as [ | i1 il ]; simpl; intros. +- exists m; auto. +- destruct H0. + destruct (@store_init_data_exists m b p i1) as (m1 & S1); eauto. + red; intros. apply H. generalize (init_data_list_size_pos il); omega. + rewrite S1. + apply IHil; eauto. + red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); omega. +Qed. + +Lemma alloc_global_exists: + forall m idg, + match idg with + | (id, Gfun f) => True + | (id, Gvar v) => + init_data_list_aligned 0 v.(gvar_init) + /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol ge i = Some b + end -> + exists m', alloc_global ge m idg = Some m'. +Proof. + intros m [id [f|v]]; intros; simpl. +- destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC. + destruct (Mem.range_perm_drop_2 m1 b 0 1 Nonempty) as [m2 DROP]. + red; intros; eapply Mem.perm_alloc_2; eauto. + exists m2; auto. +- destruct H as [P Q]. + set (sz := init_data_list_size (gvar_init v)). + destruct (Mem.alloc m 0 sz) as [m1 b] eqn:ALLOC. + assert (P1: Mem.range_perm m1 b 0 sz Cur Freeable) by (red; intros; eapply Mem.perm_alloc_2; eauto). + destruct (@store_zeros_exists m1 b 0 sz) as [m2 ZEROS]. + red; intros. apply Mem.perm_implies with Freeable; auto with mem. + rewrite ZEROS. + assert (P2: Mem.range_perm m2 b 0 sz Cur Freeable). + { red; intros. erewrite <- store_zeros_perm by eauto. eauto. } + destruct (@store_init_data_list_exists b (gvar_init v) m2 0) as [m3 STORE]; auto. + red; intros. apply Mem.perm_implies with Freeable; auto with mem. + rewrite STORE. + assert (P3: Mem.range_perm m3 b 0 sz Cur Freeable). + { red; intros. erewrite <- store_init_data_list_perm by eauto. eauto. } + destruct (Mem.range_perm_drop_2 m3 b 0 sz (perm_globvar v)) as [m4 DROP]; auto. + exists m4; auto. +Qed. + +End INITMEM_EXISTS. + +Theorem init_mem_exists: + forall p, + (forall id v, In (id, Gvar v) (prog_defs p) -> + init_data_list_aligned 0 v.(gvar_init) + /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol (globalenv p) i = Some b) -> + exists m, init_mem p = Some m. +Proof. + intros. set (ge := globalenv p) in *. + unfold init_mem. revert H. generalize (prog_defs p) Mem.empty. + induction l as [ | idg l]; simpl; intros. +- exists m; auto. +- destruct (@alloc_global_exists ge m idg) as [m1 A1]. + destruct idg as [id [f|v]]; eauto. + fold ge. rewrite A1. eapply IHl; eauto. +Qed. End GENV. (** * Commutation with program transformations *) -(** ** Commutation with matching between programs. *) - -Section MATCH_PROGRAMS. - -Variables A B V W: Type. -Variable match_fun: A -> B -> Prop. -Variable match_varinfo: V -> W -> Prop. +Section MATCH_GENVS. -Inductive match_globvar: globvar V -> globvar W -> Prop := - | match_globvar_intro: forall info1 info2 init ro vo, - match_varinfo info1 info2 -> - match_globvar (mkglobvar info1 init ro vo) (mkglobvar info2 init ro vo). +Context {A B V W: Type} (R: globdef A V -> globdef B W -> Prop). -Record match_genvs (new_globs : list (ident * globdef B W)) - (ge1: t A V) (ge2: t B W): Prop := { +Record match_genvs (ge1: t A V) (ge2: t B W): Prop := { mge_next: - genv_next ge2 = advance_next new_globs (genv_next ge1); + genv_next ge2 = genv_next ge1; 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, PTree.get b (genv_funs ge1) = Some f -> - exists tf, PTree.get b (genv_funs ge2) = Some tf /\ match_fun f tf; - mge_rev_funs: - forall b tf, PTree.get b (genv_funs ge2) = Some tf -> - if plt b (genv_next ge1) then - exists f, PTree.get b (genv_funs ge1) = Some f /\ match_fun f tf - else - In (Gfun tf) (map snd new_globs); - mge_vars: - forall b v, PTree.get b (genv_vars ge1) = Some v -> - exists tv, PTree.get b (genv_vars ge2) = Some tv /\ match_globvar v tv; - mge_rev_vars: - forall b tv, PTree.get b (genv_vars ge2) = Some tv -> - if plt b (genv_next ge1) then - exists v, PTree.get b (genv_vars ge1) = Some v /\ match_globvar v tv - else - In (Gvar tv) (map snd new_globs) + forall id, PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1); + mge_defs: + forall b, option_rel R (PTree.get b (genv_defs ge1)) (PTree.get b (genv_defs ge2)) }. 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_next0. - inv H0. -(* two functions *) - constructor; simpl. - congruence. - intros. rewrite mge_next0. - repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. - rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. - destruct (peq b (genv_next ge1)). - exists f2; split; congruence. - eauto. - rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. - destruct (peq b (genv_next ge1)). - subst b. rewrite pred_dec_true. exists f1; split; congruence. apply Plt_succ. - pose proof (mge_rev_funs0 b tf H0). - destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto. - contradiction. - eauto. - intros. - pose proof (mge_rev_vars0 b tv H0). - destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. - apply Plt_trans with (genv_next ge1); auto. apply Plt_succ. - contradiction. -(* two variables *) - constructor; simpl. - 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 (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto. - contradiction. - rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. - destruct (peq b (genv_next ge1)). - econstructor; split. eauto. inv H0. constructor; auto. - eauto. - rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. - destruct (peq b (genv_next ge1)). - subst b. rewrite pred_dec_true. - econstructor; split. eauto. inv H0. constructor; auto. apply Plt_succ. - pose proof (mge_rev_vars0 b tv H0). - destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto. - contradiction. + forall ge1 ge2 id g1 g2, + match_genvs ge1 ge2 -> + R g1 g2 -> + match_genvs (add_global ge1 (id, g1)) (add_global ge2 (id, g2)). +Proof. + intros. destruct H. constructor; simpl; intros. +- congruence. +- rewrite mge_next0, ! PTree.gsspec. destruct (peq id0 id); auto. +- rewrite mge_next0, ! PTree.gsspec. destruct (peq b (genv_next ge1)). + constructor; auto. + auto. Qed. 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). + forall gl1 gl2, + list_forall2 (fun idg1 idg2 => fst idg1 = fst idg2 /\ R (snd idg1) (snd idg2)) gl1 gl2 -> + forall ge1 ge2, match_genvs ge1 ge2 -> + match_genvs (add_globals ge1 gl1) (add_globals ge2 gl2). Proof. induction 1; intros; simpl. auto. + destruct a1 as [id1 g1]; destruct b1 as [id2 g2]; simpl in *; destruct H; subst id2. apply IHlist_forall2. apply add_global_match; auto. Qed. -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. - assert (LE: Ple (genv_next ge1) (genv_next ge2)). - { rewrite mge_next0; apply advance_next_le. } - constructor; simpl. - rewrite mge_next0. unfold advance_next. rewrite fold_left_app. simpl. auto. - 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 PTree.gso. eauto. - exploit genv_funs_range; eauto. intros. - unfold Plt, Ple in *; zify; omega. - intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H. - rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). - rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence. - subst b. unfold Plt, Ple in *; zify; omega. - exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. - rewrite in_app. tauto. - exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. - rewrite in_app. tauto. - intros. destruct idg as [id1 [f1|v1]]; simpl; eauto. - rewrite PTree.gso. eauto. exploit genv_vars_range; eauto. - unfold Plt, Ple in *; zify; omega. - intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H. - exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. - rewrite in_app. tauto. - rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). - rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence. - subst b. unfold Plt, Ple in *; zify; omega. - exploit mge_rev_vars0; eauto. destruct (plt 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. change (a :: gl) with ((a :: nil) ++ gl). rewrite <- app_ass. - apply IHgl. apply add_global_augment_match. auto. -Qed. - -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_globs new_main p p'. +End MATCH_GENVS. + +Section MATCH_PROGRAMS. + +Context {C F1 V1 F2 V2: Type} {LC: Linker C} {LF: Linker F1} {LV: Linker V1}. +Variable match_fundef: C -> F1 -> F2 -> Prop. +Variable match_varinfo: V1 -> V2 -> Prop. +Variable ctx: C. +Variable p: program F1 V1. +Variable tp: program F2 V2. +Hypothesis progmatch: match_program_gen match_fundef match_varinfo ctx p tp. Lemma globalenvs_match: - match_genvs new_globs (globalenv p) (globalenv p'). + match_genvs (match_globdef match_fundef match_varinfo ctx) (globalenv p) (globalenv tp). +Proof. + intros. apply add_globals_match. apply progmatch. + constructor; simpl; intros; auto. rewrite ! PTree.gempty. constructor. +Qed. + +Theorem find_def_match_2: + forall b, option_rel (match_globdef match_fundef match_varinfo ctx) + (find_def (globalenv p) b) (find_def (globalenv tp) b). +Proof (mge_defs globalenvs_match). + +Theorem find_def_match: + forall b g, + find_def (globalenv p) b = Some g -> + exists tg, + find_def (globalenv tp) b = Some tg /\ match_globdef match_fundef match_varinfo ctx g tg. 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 PTree.gempty in H; congruence. + intros. generalize (find_def_match_2 b). rewrite H; intros R; inv R. + exists y; auto. Qed. Theorem find_funct_ptr_match: - forall (b : block) (f : A), + forall b f, find_funct_ptr (globalenv p) b = Some f -> - exists tf : B, - find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf. -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 plt b (genv_next (globalenv p)) then - exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf - else - In (Gfun tf) (map snd new_globs). -Proof (mge_rev_funs globalenvs_match). + exists cunit tf, + find_funct_ptr (globalenv tp) b = Some tf /\ match_fundef cunit f tf /\ linkorder cunit ctx. +Proof. + intros. rewrite find_funct_ptr_iff in *. apply find_def_match in H. + destruct H as (tg & P & Q). inv Q. + exists ctx', f2; intuition auto. apply find_funct_ptr_iff; auto. +Qed. Theorem find_funct_match: - forall (v : val) (f : A), + forall v f, find_funct (globalenv p) v = Some f -> - exists tf : B, find_funct (globalenv p') v = Some tf /\ match_fun f tf. + exists cunit tf, + find_funct (globalenv tp) v = Some tf /\ match_fundef cunit f tf /\ linkorder cunit ctx. Proof. intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. rewrite find_funct_find_funct_ptr in H. @@ -1729,569 +1701,180 @@ Proof. apply find_funct_ptr_match. auto. Qed. -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 (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 (plt b (genv_next (globalenv p))); auto. -Qed. - Theorem find_var_info_match: - forall (b : block) (v : globvar V), + forall b v, find_var_info (globalenv p) b = Some v -> exists tv, - find_var_info (globalenv p') b = Some tv /\ match_globvar v tv. -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 plt b (genv_next (globalenv p)) then - exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv - else - In (Gvar tv) (map snd new_globs). -Proof (mge_rev_vars globalenvs_match). + find_var_info (globalenv tp) b = Some tv /\ match_globvar match_varinfo v tv. +Proof. + intros. rewrite find_var_info_iff in *. apply find_def_match in H. + destruct H as (tg & P & Q). inv Q. + exists v2; split; auto. apply find_var_info_iff; auto. +Qed. Theorem find_symbol_match: forall (s : ident), - ~In s (map fst new_globs) -> - find_symbol (globalenv p') s = find_symbol (globalenv p) s. + find_symbol (globalenv tp) s = find_symbol (globalenv p) s. Proof. - intros. destruct globalenvs_match. unfold find_symbol. auto. + intros. destruct globalenvs_match. apply mge_symb0. Qed. -Theorem public_symbol_match: - forall (s : ident), - ~In s (map fst new_globs) -> - public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Theorem senv_match: + Senv.equiv (to_senv (globalenv p)) (to_senv (globalenv tp)). Proof. - intros. unfold public_symbol. rewrite find_symbol_match by auto. - destruct (find_symbol (globalenv p) s); auto. - rewrite ! globalenv_public. + red; simpl. repeat split. +- apply find_symbol_match. +- intros. unfold public_symbol. rewrite find_symbol_match. + rewrite ! globalenv_public. destruct progmatch as (P & Q & R). rewrite R. auto. +- intros. unfold block_is_volatile. + destruct globalenvs_match as [P Q R]. specialize (R b). + unfold find_var_info, find_def. + inv R; auto. + inv H1; auto. + inv H2; auto. Qed. -Hypothesis new_ids_fresh: - forall s, In s (prog_defs_names p) -> In s (map fst new_globs) -> False. -Hypothesis new_ids_unique: - list_norepet (map fst new_globs). - Lemma store_init_data_list_match: forall idl m b ofs m', store_init_data_list (globalenv p) m b ofs idl = Some m' -> - store_init_data_list (globalenv p') m b ofs idl = Some m'. + store_init_data_list (globalenv tp) m b ofs idl = Some m'. Proof. induction idl; simpl; intros. - 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. - simpl in H. destruct (find_symbol (globalenv p) i) as [b'|] eqn:?; try discriminate. - red; intros. exploit find_symbol_inversion; eauto. - 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. +- auto. +- destruct (store_init_data (globalenv p) m b ofs a) as [m1|] eqn:S; try discriminate. + assert (X: store_init_data (globalenv tp) m b ofs a = Some m1). + { destruct a; auto. simpl; rewrite find_symbol_match; auto. } + rewrite X. auto. Qed. Lemma alloc_globals_match: - forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 -> + forall gl1 gl2, list_forall2 (match_ident_globdef match_fundef match_varinfo ctx) gl1 gl2 -> forall m m', alloc_globals (globalenv p) m gl1 = Some m' -> - alloc_globals (globalenv p') m gl2 = Some m'. + alloc_globals (globalenv tp) m gl2 = Some m'. Proof. induction 1; simpl; intros. - auto. - 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. +- auto. +- destruct (alloc_global (globalenv p) m a1) as [m1|] eqn:?; try discriminate. + assert (X: alloc_global (globalenv tp) m b1 = Some m1). + { destruct a1 as [id1 g1]; destruct b1 as [id2 g2]; destruct H; simpl in *. + subst id2. inv H2. + - auto. + - inv H; simpl in *. 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. + } + rewrite X; eauto. Qed. Theorem init_mem_match: - forall m, init_mem p = Some m -> - init_mem p' = alloc_globals (globalenv p') m new_globs. + forall m, init_mem p = Some m -> init_mem tp = Some m. Proof. unfold init_mem; intros. - destruct progmatch as [[tglob [P Q]] R]. - rewrite Q. erewrite <- alloc_globals_app; eauto. - eapply alloc_globals_match; eauto. -Qed. - -Theorem find_new_funct_ptr_match: - 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 progmatch as [[tglob [P Q]] R]. - exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T). - rewrite S in Q. rewrite <- app_ass in Q. - eapply find_funct_ptr_exists_2; eauto. -Qed. - -Theorem find_new_var_match: - forall id v, In (id, Gvar v) new_globs -> - exists b, - find_symbol (globalenv p') id = Some b - /\ find_var_info (globalenv p') b = Some v. -Proof. - intros. - destruct progmatch as [[tglob [P Q]] R]. - exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T). - rewrite S in Q. rewrite <- app_ass in Q. - eapply find_var_exists_2; eauto. + eapply alloc_globals_match; eauto. apply progmatch. Qed. End MATCH_PROGRAMS. -Section TRANSF_PROGRAM_AUGMENT. - -Variable A B V W: Type. -Variable transf_fun: A -> res B. -Variable transf_var: V -> res W. +(** Special case for partial transformations that do not depend on the compilation unit *) -Variable new_globs : list (ident * globdef B W). -Variable new_main : ident. +Section TRANSFORM_PARTIAL. -Variable p: program A V. -Variable p': program B W. - -Hypothesis transf_OK: - transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK p'. - -Let prog_match: - match_program - (fun fd tfd => transf_fun fd = OK tfd) - (fun info tinfo => transf_var info = OK tinfo) - new_globs new_main - p p'. -Proof. - apply transform_partial_augment_program_match; auto. -Qed. - -Theorem find_funct_ptr_transf_augment: - forall (b: block) (f: A), - find_funct_ptr (globalenv p) b = Some f -> - exists f', - find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'. -Proof. - intros. - exploit find_funct_ptr_match. eexact prog_match. eauto. - intros [tf [X Y]]. exists tf; auto. -Qed. - -Theorem find_funct_ptr_rev_transf_augment: - forall (b: block) (tf: B), - find_funct_ptr (globalenv p') b = Some tf -> - if plt b (genv_next (globalenv p)) then - (exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf) - else - In (Gfun tf) (map snd new_globs). -Proof. - intros. - exploit find_funct_ptr_rev_match; eauto. -Qed. - -Theorem find_funct_transf_augment: - forall (v: val) (f: A), - find_funct (globalenv p) v = Some f -> - exists f', - find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. -Proof. - intros. - 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 (Gfun tf) (map snd new_globs). -Proof. - intros. - exploit find_funct_rev_match. eexact prog_match. eauto. auto. -Qed. - -Theorem find_var_info_transf_augment: - forall (b: block) (v: globvar V), - find_var_info (globalenv p) b = Some v -> - exists v', - 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. - rewrite H0; simpl. auto. -Qed. - -Theorem find_var_info_rev_transf_augment: - forall (b: block) (v': globvar W), - find_var_info (globalenv p') b = Some v' -> - if plt 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 (Gvar v') (map snd new_globs)). -Proof. - intros. - exploit find_var_info_rev_match. eexact prog_match. eauto. - destruct (plt 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 (map fst new_globs) -> - find_symbol (globalenv p') s = find_symbol (globalenv p) s. -Proof. - intros. eapply find_symbol_match. eexact prog_match. auto. -Qed. - -Theorem public_symbol_transf_augment: - forall (s: ident), - ~ In s (map fst new_globs) -> - public_symbol (globalenv p') s = public_symbol (globalenv p) s. -Proof. - intros. eapply public_symbol_match. eexact prog_match. auto. -Qed. - -Hypothesis new_ids_fresh: - forall s, In s (prog_defs_names p) -> In s (map fst new_globs) -> False. -Hypothesis new_ids_unique: - list_norepet (map fst new_globs). - -Theorem init_mem_transf_augment: - forall m, init_mem p = Some m -> - 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 m, init_mem p = Some m -> - forall m', init_mem p' = Some m' -> - Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m'. -Proof. - intros. - pose proof (initmem_inject p H). - erewrite init_mem_transf_augment in H0; eauto. - eapply alloc_globals_augment; eauto. apply Ple_refl. -Qed. - -Theorem find_new_funct_ptr_exists: - 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. eapply find_new_funct_ptr_match; eauto. -Qed. - -Theorem find_new_var_exists: - 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. eapply find_new_var_match; eauto. -Qed. - -End TRANSF_PROGRAM_AUGMENT. - -Section TRANSF_PROGRAM_PARTIAL2. - -Variable A B V W: Type. -Variable transf_fun: A -> res B. -Variable transf_var: V -> res W. -Variable p: program A V. -Variable p': program B W. -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 p.(prog_main) p = OK p'. -Proof. - rewrite <- transf_OK. symmetry. apply transform_partial_program2_augment. -Qed. - -Theorem find_funct_ptr_transf_partial2: - forall (b: block) (f: A), - find_funct_ptr (globalenv p) b = Some f -> - 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). -Qed. - -Theorem find_funct_ptr_rev_transf_partial2: - forall (b: block) (tf: B), - 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). - intros. pose proof (H b tf H0). - destruct (plt b (genv_next (globalenv p))). auto. contradiction. -Qed. - -Theorem find_funct_transf_partial2: - forall (v: val) (f: A), - find_funct (globalenv p) v = Some f -> - exists f', - find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. -Proof. - exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). -Qed. - -Theorem find_funct_rev_transf_partial2: - 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. -Proof. - pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). - intros. pose proof (H v tf H0). - destruct H1. auto. contradiction. -Qed. - -Theorem find_var_info_transf_partial2: - forall (b: block) (v: globvar V), - find_var_info (globalenv p) b = Some v -> - 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). -Qed. - -Theorem find_var_info_rev_transf_partial2: - forall (b: block) (v': globvar W), - find_var_info (globalenv p') b = Some v' -> - 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). - intros. pose proof (H b v' H0). - destruct (plt 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). - auto. -Qed. - -Theorem public_symbol_transf_partial2: - forall (s: ident), - public_symbol (globalenv p') s = public_symbol (globalenv p) s. -Proof. - pose proof (@public_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). - auto. -Qed. - -Theorem block_is_volatile_transf_partial2: - forall (b: block), - block_is_volatile (globalenv p') b = block_is_volatile (globalenv p) b. -Proof. - unfold block_is_volatile; intros. - destruct (find_var_info (globalenv p) b) as [v|] eqn:FV. - exploit find_var_info_transf_partial2; eauto. intros (v' & P & Q). - rewrite P. monadInv Q. auto. - destruct (find_var_info (globalenv p') b) as [v'|] eqn:FV'. - exploit find_var_info_rev_transf_partial2; eauto. intros (v & P & Q). congruence. - 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). - intros. simpl in H. apply H; auto. -Qed. - -End TRANSF_PROGRAM_PARTIAL2. - -Section TRANSF_PROGRAM_PARTIAL. - -Variable A B V: Type. -Variable transf: A -> res B. -Variable p: program A V. -Variable p': program B V. -Hypothesis transf_OK: transform_partial_program transf p = OK p'. +Context {A B V: Type} {LA: Linker A} {LV: Linker V}. +Context {transf: A -> res B} {p: program A V} {tp: program B V}. +Hypothesis progmatch: match_program (fun cu f tf => transf f = OK tf) eq p tp. Theorem find_funct_ptr_transf_partial: - forall (b: block) (f: A), + forall b f, 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 _ _ _ _ _ _ _ _ transf_OK). -Qed. - -Theorem find_funct_ptr_rev_transf_partial: - forall (b: block) (tf: B), - find_funct_ptr (globalenv p') b = Some tf -> - exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf. + exists tf, + find_funct_ptr (globalenv tp) b = Some tf /\ transf f = OK tf. Proof. - exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). + intros. exploit (find_funct_ptr_match progmatch); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. Qed. Theorem find_funct_transf_partial: - forall (v: val) (f: A), + forall v f, find_funct (globalenv p) v = Some f -> - exists f', - find_funct (globalenv p') v = Some f' /\ transf f = OK f'. -Proof. - exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). -Qed. - -Theorem find_funct_rev_transf_partial: - forall (v: val) (tf: B), - find_funct (globalenv p') v = Some tf -> - exists f, find_funct (globalenv p) v = Some f /\ transf f = OK tf. + exists tf, + find_funct (globalenv tp) v = Some tf /\ transf f = OK tf. Proof. - exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). + intros. exploit (find_funct_match progmatch); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. 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 _ _ _ _ _ _ _ _ transf_OK). -Qed. - -Theorem public_symbol_transf_partial: - forall (s: ident), - public_symbol (globalenv p') s = public_symbol (globalenv p) s. -Proof. - exact (@public_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). -Qed. - -Theorem find_var_info_transf_partial: - forall (b: block), - find_var_info (globalenv p') b = find_var_info (globalenv p) b. + forall (s : ident), + find_symbol (globalenv tp) s = find_symbol (globalenv p) s. Proof. - intros. case_eq (find_var_info (globalenv p) b); intros. - 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 transf_OK. eauto. - intros [v' [P Q]]. monadInv Q. inv EQ. congruence. - auto. + intros. eapply (find_symbol_match progmatch). Qed. -Theorem block_is_volatile_transf_partial: - forall (b: block), - block_is_volatile (globalenv p') b = block_is_volatile (globalenv p) b. +Theorem senv_transf_partial: + Senv.equiv (to_senv (globalenv p)) (to_senv (globalenv tp)). Proof. - exact (@block_is_volatile_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). + intros. eapply (senv_match progmatch). Qed. Theorem init_mem_transf_partial: - forall m, init_mem p = Some m -> init_mem p' = Some m. + forall m, init_mem p = Some m -> init_mem tp = Some m. Proof. - exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). + eapply (init_mem_match progmatch). Qed. -End TRANSF_PROGRAM_PARTIAL. +End TRANSFORM_PARTIAL. -Section TRANSF_PROGRAM. +(** Special case for total transformations that do not depend on the compilation unit *) -Variable A B V: Type. -Variable transf: A -> B. -Variable p: program A V. -Let tp := transform_program transf p. +Section TRANSFORM_TOTAL. -Remark transf_OK: - transform_partial_program (fun x => OK (transf x)) p = OK tp. -Proof. - unfold tp. apply transform_program_partial_program. -Qed. +Context {A B V: Type} {LA: Linker A} {LV: Linker V}. +Context {transf: A -> B} {p: program A V} {tp: program B V}. +Hypothesis progmatch: match_program (fun cu f tf => tf = transf f) eq p tp. Theorem find_funct_ptr_transf: - forall (b: block) (f: A), + forall b f, find_funct_ptr (globalenv p) b = Some f -> find_funct_ptr (globalenv tp) b = Some (transf f). Proof. - intros. - destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK _ _ H) - as [f' [X Y]]. congruence. -Qed. - -Theorem find_funct_ptr_rev_transf: - forall (b: block) (tf: B), - find_funct_ptr (globalenv tp) b = Some tf -> - exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf. -Proof. - intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto. - intros [f [X Y]]. exists f; split. auto. congruence. + intros. exploit (find_funct_ptr_match progmatch); eauto. + intros (cu & tf & P & Q & R). congruence. Qed. Theorem find_funct_transf: - forall (v: val) (f: A), + forall v f, find_funct (globalenv p) v = Some f -> find_funct (globalenv tp) v = Some (transf f). Proof. - intros. - destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK _ _ H) - as [f' [X Y]]. congruence. -Qed. - -Theorem find_funct_rev_transf: - forall (v: val) (tf: B), - find_funct (globalenv tp) v = Some tf -> - exists f, find_funct (globalenv p) v = Some f /\ transf f = tf. -Proof. - intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto. - intros [f [X Y]]. exists f; split. auto. congruence. + intros. exploit (find_funct_match progmatch); eauto. + intros (cu & tf & P & Q & R). congruence. Qed. Theorem find_symbol_transf: - forall (s: ident), + forall (s : ident), find_symbol (globalenv tp) s = find_symbol (globalenv p) s. Proof. - exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). -Qed. - -Theorem public_symbol_transf: - forall (s: ident), - public_symbol (globalenv tp) s = public_symbol (globalenv p) s. -Proof. - exact (@public_symbol_transf_partial _ _ _ _ _ _ transf_OK). -Qed. - -Theorem find_var_info_transf: - forall (b: block), - find_var_info (globalenv tp) b = find_var_info (globalenv p) b. -Proof. - exact (@find_var_info_transf_partial _ _ _ _ _ _ transf_OK). + intros. eapply (find_symbol_match progmatch). Qed. -Theorem block_is_volatile_transf: - forall (b: block), - block_is_volatile (globalenv tp) b = block_is_volatile (globalenv p) b. +Theorem senv_transf: + Senv.equiv (to_senv (globalenv p)) (to_senv (globalenv tp)). Proof. - exact (@block_is_volatile_transf_partial _ _ _ _ _ _ transf_OK). + intros. eapply (senv_match progmatch). Qed. Theorem init_mem_transf: forall m, init_mem p = Some m -> init_mem tp = Some m. Proof. - exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK). + eapply (init_mem_match progmatch). Qed. -End TRANSF_PROGRAM. +End TRANSFORM_TOTAL. End Genv. diff --git a/common/Linking.v b/common/Linking.v new file mode 100644 index 00000000..52e774db --- /dev/null +++ b/common/Linking.v @@ -0,0 +1,905 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Separate compilation and syntactic linking *) + +Require Import Coqlib Maps Errors AST. + +(** This file follows "approach A" from the paper + "Lightweight Verification of Separate Compilation" + by Kang, Kim, Hur, Dreyer and Vafeiadis, POPL 2016. *) + + +(** * Syntactic linking *) + +(** A syntactic element [A] supports syntactic linking if it is equipped with the following: +- a partial binary operator [link] that produces the result of linking two elements, + or fails if they cannot be linked (e.g. two definitions that are incompatible); +- a preorder [linkorder] with the meaning that [linkorder a1 a2] holds + if [a2] can be obtained by linking [a1] with some other syntactic element. +*) + +Class Linker (A: Type) := { + link: A -> A -> option A; + linkorder: A -> A -> Prop; + linkorder_refl: forall x, linkorder x x; + linkorder_trans: forall x y z, linkorder x y -> linkorder y z -> linkorder x z; + link_linkorder: forall x y z, link x y = Some z -> linkorder x z /\ linkorder y z +}. + +(** Linking function definitions. External functions of the [EF_external] + kind can link with internal function definitions; the result of + linking is the internal definition. Two external functions can link + if they are identical. *) + +Definition link_fundef {F: Type} (fd1 fd2: fundef F) := + match fd1, fd2 with + | Internal _, Internal _ => None + | External ef1, External ef2 => + if external_function_eq ef1 ef2 then Some (External ef1) else None + | Internal f, External ef => + match ef with EF_external id sg => Some (Internal f) | _ => None end + | External ef, Internal f => + match ef with EF_external id sg => Some (Internal f) | _ => None end + end. + +Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop := + | linkorder_fundef_refl: forall fd, linkorder_fundef fd fd + | linkorder_fundef_ext_int: forall f id sg, linkorder_fundef (External (EF_external id sg)) (Internal f). + +Instance Linker_fundef (F: Type): Linker (fundef F) := { + link := link_fundef; + linkorder := linkorder_fundef +}. +Proof. +- intros; constructor. +- intros. inv H; inv H0; constructor. +- intros x y z EQ. destruct x, y; simpl in EQ. ++ discriminate. ++ destruct e; inv EQ. split; constructor. ++ destruct e; inv EQ. split; constructor. ++ destruct (external_function_eq e e0); inv EQ. split; constructor. +Defined. + +Global Opaque Linker_fundef. + +(** Linking variable initializers. We adopt the following conventions: +- an "extern" variable has an empty initialization list; +- a "common" variable has an initialization list of the form [Init_space sz]; +- all other initialization lists correspond to fully defined variables, neither "common" nor "extern". +*) + +Inductive init_class : list init_data -> Type := + | Init_extern: init_class nil + | Init_common: forall sz, init_class (Init_space sz :: nil) + | Init_definitive: forall il, init_class il. + +Definition classify_init (i: list init_data) : init_class i := + match i with + | nil => Init_extern + | Init_space sz :: nil => Init_common sz + | i => Init_definitive i + end. + +Definition link_varinit (i1 i2: list init_data) := + match classify_init i1, classify_init i2 with + | Init_extern, _ => Some i2 + | _, Init_extern => Some i1 + | Init_common sz1, _ => if zeq sz1 (init_data_list_size i2) then Some i2 else None + | _, Init_common sz2 => if zeq sz2 (init_data_list_size i1) then Some i1 else None + | _, _ => None + end. + +Inductive linkorder_varinit: list init_data -> list init_data -> Prop := + | linkorder_varinit_refl: forall il, linkorder_varinit il il + | linkorder_varinit_extern: forall il, linkorder_varinit nil il + | linkorder_varinit_common: forall sz il, + il <> nil -> init_data_list_size il = sz -> + linkorder_varinit (Init_space sz :: nil) il. + +Instance Linker_varinit : Linker (list init_data) := { + link := link_varinit; + linkorder := linkorder_varinit +}. +Proof. +- intros. constructor. +- intros. inv H; inv H0; constructor; auto. + congruence. + simpl. generalize (init_data_list_size_pos z). xomega. +- unfold link_varinit; intros until z. + destruct (classify_init x) eqn:Cx, (classify_init y) eqn:Cy; intros E; inv E; try (split; constructor; fail). ++ destruct (zeq sz (Z.max sz0 0 + 0)); inv H0. + split; constructor. congruence. auto. ++ destruct (zeq sz (init_data_list_size il)); inv H0. + split; constructor. red; intros; subst z; discriminate. auto. ++ destruct (zeq sz (init_data_list_size il)); inv H0. + split; constructor. red; intros; subst z; discriminate. auto. +Defined. + +Global Opaque Linker_varinit. + +(** Linking variable definitions. *) + +Definition link_vardef {V: Type} {LV: Linker V} (v1 v2: globvar V) := + match link v1.(gvar_info) v2.(gvar_info) with + | None => None + | Some info => + match link v1.(gvar_init) v2.(gvar_init) with + | None => None + | Some init => + if eqb v1.(gvar_readonly) v2.(gvar_readonly) + && eqb v1.(gvar_volatile) v2.(gvar_volatile) + then Some {| gvar_info := info; gvar_init := init; + gvar_readonly := v1.(gvar_readonly); + gvar_volatile := v1.(gvar_volatile) |} + else None + end + end. + +Inductive linkorder_vardef {V: Type} {LV: Linker V}: globvar V -> globvar V -> Prop := + | linkorder_vardef_intro: forall info1 info2 i1 i2 ro vo, + linkorder info1 info2 -> + linkorder i1 i2 -> + linkorder_vardef (mkglobvar info1 i1 ro vo) (mkglobvar info2 i2 ro vo). + +Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := { + link := link_vardef; + linkorder := linkorder_vardef +}. +Proof. +- intros. destruct x; constructor; apply linkorder_refl. +- intros. inv H; inv H0. constructor; eapply linkorder_trans; eauto. +- unfold link_vardef; intros until z. + destruct x as [f1 i1 r1 v1], y as [f2 i2 r2 v2]; simpl. + destruct (link f1 f2) as [f|] eqn:LF; try discriminate. + destruct (link i1 i2) as [i|] eqn:LI; try discriminate. + destruct (eqb r1 r2) eqn:ER; try discriminate. + destruct (eqb v1 v2) eqn:EV; intros EQ; inv EQ. + apply eqb_prop in ER; apply eqb_prop in EV; subst r2 v2. + apply link_linkorder in LF. apply link_linkorder in LI. + split; constructor; tauto. +Defined. + +Global Opaque Linker_vardef. + +(** A trivial linker for the trivial var info [unit]. *) + +Instance Linker_unit: Linker unit := { + link := fun x y => Some tt; + linkorder := fun x y => True +}. +Proof. +- auto. +- auto. +- auto. +Defined. + +Global Opaque Linker_unit. + +(** Linking global definitions *) + +Definition link_def {F V: Type} {LF: Linker F} {LV: Linker V} (gd1 gd2: globdef F V) := + match gd1, gd2 with + | Gfun f1, Gfun f2 => + match link f1 f2 with Some f => Some (Gfun f) | None => None end + | Gvar v1, Gvar v2 => + match link v1 v2 with Some v => Some (Gvar v) | None => None end + | _, _ => None + end. + +Inductive linkorder_def {F V: Type} {LF: Linker F} {LV: Linker V}: globdef F V -> globdef F V -> Prop := + | linkorder_def_fun: forall fd1 fd2, + linkorder fd1 fd2 -> + linkorder_def (Gfun fd1) (Gfun fd2) + | linkorder_def_var: forall v1 v2, + linkorder v1 v2 -> + linkorder_def (Gvar v1) (Gvar v2). + +Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := { + link := link_def; + linkorder := linkorder_def +}. +Proof. +- intros. destruct x; constructor; apply linkorder_refl. +- intros. inv H; inv H0; constructor; eapply linkorder_trans; eauto. +- unfold link_def; intros. + destruct x as [f1|v1], y as [f2|v2]; try discriminate. ++ destruct (link f1 f2) as [f|] eqn:L; inv H. apply link_linkorder in L. + split; constructor; tauto. ++ destruct (link v1 v2) as [v|] eqn:L; inv H. apply link_linkorder in L. + split; constructor; tauto. +Defined. + +Global Opaque Linker_def. + +(** Linking two compilation units. Compilation units are represented like + whole programs using the type [program F V]. If a name has + a global definition in one unit but not in the other, this definition + is left unchanged in the result of the link. If a name has + global definitions in both units, and is public (not static) in both, + the two definitions are linked as per [Linker_def] above. + + If one or both definitions are static (not public), we should ideally + rename it so that it can be kept unchanged in the result of the link. + This would require a general notion of renaming of global identifiers + in programs that we do not have yet. Hence, as a first step, linking + is undefined if static definitions with the same name appear in both + compilation units. *) + +Section LINKER_PROG. + +Context {F V: Type} {LF: Linker F} {LV: Linker V} (p1 p2: program F V). + +Let dm1 := prog_defmap p1. +Let dm2 := prog_defmap p2. + +Definition link_prog_check (x: ident) (gd1: globdef F V) := + match dm2!x with + | None => true + | Some gd2 => + In_dec peq x p1.(prog_public) + && In_dec peq x p2.(prog_public) + && match link gd1 gd2 with Some _ => true | None => false end + end. + +Definition link_prog_merge (o1 o2: option (globdef F V)) := + match o1, o2 with + | None, _ => o2 + | _, None => o1 + | Some gd1, Some gd2 => link gd1 gd2 + end. + +Definition link_prog := + if ident_eq p1.(prog_main) p2.(prog_main) + && PTree_Properties.for_all dm1 link_prog_check then + Some {| prog_main := p1.(prog_main); + prog_public := p1.(prog_public) ++ p2.(prog_public); + prog_defs := PTree.elements (PTree.combine link_prog_merge dm1 dm2) |} + else + None. + +Lemma link_prog_inv: + forall p, + link_prog = Some p -> + p1.(prog_main) = p2.(prog_main) + /\ (forall id gd1 gd2, + dm1!id = Some gd1 -> dm2!id = Some gd2 -> + In id p1.(prog_public) /\ In id p2.(prog_public) /\ exists gd, link gd1 gd2 = Some gd) + /\ p = {| prog_main := p1.(prog_main); + prog_public := p1.(prog_public) ++ p2.(prog_public); + prog_defs := PTree.elements (PTree.combine link_prog_merge dm1 dm2) |}. +Proof. + unfold link_prog; intros p E. + destruct (ident_eq (prog_main p1) (prog_main p2)); try discriminate. + destruct (PTree_Properties.for_all dm1 link_prog_check) eqn:C; inv E. + rewrite PTree_Properties.for_all_correct in C. + split; auto. split; auto. + intros. exploit C; eauto. unfold link_prog_check. rewrite H0. intros. + destruct (in_dec peq id (prog_public p1)); try discriminate. + destruct (in_dec peq id (prog_public p2)); try discriminate. + destruct (link gd1 gd2) eqn:L; try discriminate. + intuition auto. exists g; auto. +Qed. + +Lemma link_prog_succeeds: + p1.(prog_main) = p2.(prog_main) -> + (forall id gd1 gd2, + dm1!id = Some gd1 -> dm2!id = Some gd2 -> + In id p1.(prog_public) /\ In id p2.(prog_public) /\ link gd1 gd2 <> None) -> + link_prog = + Some {| prog_main := p1.(prog_main); + prog_public := p1.(prog_public) ++ p2.(prog_public); + prog_defs := PTree.elements (PTree.combine link_prog_merge dm1 dm2) |}. +Proof. + intros. unfold link_prog. unfold proj_sumbool. rewrite H, dec_eq_true. simpl. + replace (PTree_Properties.for_all dm1 link_prog_check) with true; auto. + symmetry. apply PTree_Properties.for_all_correct; intros. rename a into gd1. + unfold link_prog_check. destruct dm2!x as [gd2|] eqn:G2; auto. + exploit H0; eauto. intros (P & Q & R). unfold proj_sumbool; rewrite ! pred_dec_true by auto. + destruct (link gd1 gd2); auto; discriminate. +Qed. + +Lemma prog_defmap_elements: + forall (m: PTree.t (globdef F V)) pub mn x, + (prog_defmap {| prog_defs := PTree.elements m; prog_public := pub; prog_main := mn |})!x = m!x. +Proof. + intros. unfold prog_defmap; simpl. apply PTree_Properties.of_list_elements. +Qed. + +End LINKER_PROG. + +Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := { + link := link_prog; + linkorder := fun p1 p2 => + p1.(prog_main) = p2.(prog_main) + /\ incl p1.(prog_public) p2.(prog_public) + /\ forall id gd1, + (prog_defmap p1)!id = Some gd1 -> + exists gd2, + (prog_defmap p2)!id = Some gd2 + /\ linkorder gd1 gd2 + /\ (~In id p2.(prog_public) -> gd2 = gd1) +}. +Proof. +- intros; split; auto. split. apply incl_refl. intros. + exists gd1; split; auto. split; auto. apply linkorder_refl. + +- intros x y z (A1 & B1 & C1) (A2 & B2 & C2). + split. congruence. split. red; eauto. + intros. exploit C1; eauto. intros (gd2 & P & Q & R). + exploit C2; eauto. intros (gd3 & U & X & Y). + exists gd3. split; auto. split. eapply linkorder_trans; eauto. + intros. transitivity gd2. apply Y. auto. apply R. red; intros; elim H0; auto. + +- intros. apply link_prog_inv in H. destruct H as (L1 & L2 & L3). + subst z; simpl. intuition auto. ++ red; intros; apply in_app_iff; auto. ++ rewrite prog_defmap_elements, PTree.gcombine, H by auto. + destruct (prog_defmap y)!id as [gd2|] eqn:GD2; simpl. +* exploit L2; eauto. intros (P & Q & gd & R). + exists gd; split. auto. split. apply link_linkorder in R; tauto. + rewrite in_app_iff; tauto. +* exists gd1; split; auto. split. apply linkorder_refl. auto. ++ red; intros; apply in_app_iff; auto. ++ rewrite prog_defmap_elements, PTree.gcombine, H by auto. + destruct (prog_defmap x)!id as [gd2|] eqn:GD2; simpl. +* exploit L2; eauto. intros (P & Q & gd & R). + exists gd; split. auto. split. apply link_linkorder in R; tauto. + rewrite in_app_iff; tauto. +* exists gd1; split; auto. split. apply linkorder_refl. auto. +Defined. + +Lemma prog_defmap_linkorder: + forall {F V: Type} {LF: Linker F} {LV: Linker V} (p1 p2: program F V) id gd1, + linkorder p1 p2 -> + (prog_defmap p1)!id = Some gd1 -> + exists gd2, (prog_defmap p2)!id = Some gd2 /\ linkorder gd1 gd2. +Proof. + intros. destruct H as (A & B & C). + exploit C; eauto. intros (gd2 & P & Q & R). exists gd2; auto. +Qed. + +Global Opaque Linker_prog. + +(** * Matching between two programs *) + +(** The following is a relational presentation of program transformations, + e.g. [transf_partial_program] from module [AST]. *) + +(** To capture the possibility of separate compilation, we parameterize + the [match_fundef] relation between function definitions with + a context, e.g. the compilation unit from which the function definition comes. + This unit is characterized as any program that is in the [linkorder] + relation with the final, whole program. *) + +Section MATCH_PROGRAM_GENERIC. + +Context {C F1 V1 F2 V2: Type} {LC: Linker C} {LF: Linker F1} {LV: Linker V1}. +Variable match_fundef: C -> F1 -> F2 -> Prop. +Variable match_varinfo: V1 -> V2 -> Prop. + +Inductive match_globvar: globvar V1 -> globvar V2 -> Prop := + | match_globvar_intro: forall i1 i2 init ro vo, + match_varinfo i1 i2 -> + match_globvar (mkglobvar i1 init ro vo) (mkglobvar i2 init ro vo). + +Inductive match_globdef (ctx: C): globdef F1 V1 -> globdef F2 V2 -> Prop := + | match_globdef_fun: forall ctx' f1 f2, + linkorder ctx' ctx -> + match_fundef ctx' f1 f2 -> + match_globdef ctx (Gfun f1) (Gfun f2) + | match_globdef_var: forall v1 v2, + match_globvar v1 v2 -> + match_globdef ctx (Gvar v1) (Gvar v2). + +Definition match_ident_globdef + (ctx: C) (ig1: ident * globdef F1 V1) (ig2: ident * globdef F2 V2) : Prop := + fst ig1 = fst ig2 /\ match_globdef ctx (snd ig1) (snd ig2). + +Definition match_program_gen (ctx: C) (p1: program F1 V1) (p2: program F2 V2) : Prop := + list_forall2 (match_ident_globdef ctx) p1.(prog_defs) p2.(prog_defs) + /\ p2.(prog_main) = p1.(prog_main) + /\ p2.(prog_public) = p1.(prog_public). + +Theorem match_program_defmap: + forall ctx p1 p2, match_program_gen ctx p1 p2 -> + forall id, option_rel (match_globdef ctx) (prog_defmap p1)!id (prog_defmap p2)!id. +Proof. + intros. apply PTree_Properties.of_list_related. apply H. +Qed. + +Lemma match_program_gen_main: + forall ctx p1 p2, match_program_gen ctx p1 p2 -> p2.(prog_main) = p1.(prog_main). +Proof. + intros. apply H. +Qed. + +Lemma match_program_public: + forall ctx p1 p2, match_program_gen ctx p1 p2 -> p2.(prog_public) = p1.(prog_public). +Proof. + intros. apply H. +Qed. + +End MATCH_PROGRAM_GENERIC. + +(** In many cases, the context for [match_program_gen] is the source program or + source compilation unit itself. We provide a specialized definition for this case. *) + +Definition match_program {F1 V1 F2 V2: Type} {LF: Linker F1} {LV: Linker V1} + (match_fundef: program F1 V1 -> F1 -> F2 -> Prop) + (match_varinfo: V1 -> V2 -> Prop) + (p1: program F1 V1) (p2: program F2 V2) : Prop := + match_program_gen match_fundef match_varinfo p1 p1 p2. + +Lemma match_program_main: + forall {F1 V1 F2 V2: Type} {LF: Linker F1} {LV: Linker V1} + {match_fundef: program F1 V1 -> F1 -> F2 -> Prop} + {match_varinfo: V1 -> V2 -> Prop} + {p1: program F1 V1} {p2: program F2 V2}, + match_program match_fundef match_varinfo p1 p2 -> p2.(prog_main) = p1.(prog_main). +Proof. + intros. apply H. +Qed. + +(* +Lemma match_program_implies: + forall (A B V W: Type) (LA: Linker A) (LV: Linker V) + (match_fundef1 match_fundef2: program A V -> A -> B -> Prop) + (match_varinfo1 match_varinfo2: V -> W -> Prop) + p p', + match_program match_fundef1 match_varinfo1 p p' -> + (forall cu a b, match_fundef1 cu a b -> linkorder cu p -> match_fundef2 cu a b) -> + (forall v w, match_varinfo1 v w -> match_varinfo2 v w) -> + match_program match_fundef2 match_varinfo2 p p'. +Proof. + intros. destruct H as [P Q]. split; auto. + eapply list_forall2_imply; eauto. + intros. inv H3. split; auto. inv H5. + econstructor; eauto. + constructor. inv H7; constructor; auto. +Qed. +*) + +(** Relation between the program transformation functions from [AST] + and the [match_program] predicate. *) + +Theorem match_transform_partial_program2: + forall {C F1 V1 F2 V2: Type} {LC: Linker C} {LF: Linker F1} {LV: Linker V1} + (match_fundef: C -> F1 -> F2 -> Prop) + (match_varinfo: V1 -> V2 -> Prop) + (transf_fun: ident -> F1 -> res F2) + (transf_var: ident -> V1 -> res V2) + (ctx: C) (p: program F1 V1) (tp: program F2 V2), + transform_partial_program2 transf_fun transf_var p = OK tp -> + (forall i f tf, transf_fun i f = OK tf -> match_fundef ctx f tf) -> + (forall i v tv, transf_var i v = OK tv -> match_varinfo v tv) -> + match_program_gen match_fundef match_varinfo ctx p tp. +Proof. + unfold transform_partial_program2; intros. monadInv H. + red; simpl; split; auto. + revert x EQ. generalize (prog_defs p). + induction l as [ | [i g] l]; simpl; intros. +- monadInv EQ. constructor. +- destruct g as [f|v]. ++ destruct (transf_fun i f) as [tf|?] eqn:TF; monadInv EQ. + constructor; auto. split; simpl; auto. econstructor. apply linkorder_refl. eauto. ++ destruct (transf_globvar transf_var i v) as [tv|?] eqn:TV; monadInv EQ. + constructor; auto. split; simpl; auto. constructor. + monadInv TV. destruct v; simpl; constructor. eauto. +Qed. + +Theorem match_transform_partial_program_contextual: + forall {A B V: Type} {LA: Linker A} {LV: Linker V} + (match_fundef: program A V -> A -> B -> Prop) + (transf_fun: A -> res B) + (p: program A V) (tp: program B V), + transform_partial_program transf_fun p = OK tp -> + (forall f tf, transf_fun f = OK tf -> match_fundef p f tf) -> + match_program match_fundef eq p tp. +Proof. + intros. + eapply match_transform_partial_program2. eexact H. + auto. + simpl; intros. congruence. +Qed. + +Theorem match_transform_program_contextual: + forall {A B V: Type} {LA: Linker A} {LV: Linker V} + (match_fundef: program A V -> A -> B -> Prop) + (transf_fun: A -> B) + (p: program A V), + (forall f, match_fundef p f (transf_fun f)) -> + match_program match_fundef eq p (transform_program transf_fun p). +Proof. + intros. + eapply match_transform_partial_program_contextual. + apply transform_program_partial_program with (transf_fun := transf_fun). + simpl; intros. inv H0. auto. +Qed. + +(** The following two theorems are simpler versions for the case where the + function transformation does not depend on the compilation unit. *) + +Theorem match_transform_partial_program: + forall {A B V: Type} {LA: Linker A} {LV: Linker V} + (transf_fun: A -> res B) + (p: program A V) (tp: program B V), + transform_partial_program transf_fun p = OK tp -> + match_program (fun cu f tf => transf_fun f = OK tf) eq p tp. +Proof. + intros. + eapply match_transform_partial_program2. eexact H. + auto. + simpl; intros. congruence. +Qed. + +Theorem match_transform_program: + forall {A B V: Type} {LA: Linker A} {LV: Linker V} + (transf: A -> B) + (p: program A V), + match_program (fun cu f tf => tf = transf f) eq p (transform_program transf p). +Proof. + intros. apply match_transform_program_contextual. auto. +Qed. + +(** * Commutation between linking and program transformations *) + +Section LINK_MATCH_PROGRAM. + +Context {C F1 V1 F2 V2: Type} {LC: Linker C} {LF1: Linker F1} {LF2: Linker F2} {LV1: Linker V1} {LV2: Linker V2}. +Variable match_fundef: C -> F1 -> F2 -> Prop. +Variable match_varinfo: V1 -> V2 -> Prop. + +Local Transparent Linker_vardef Linker_def Linker_prog. + +Hypothesis link_match_fundef: + forall ctx1 ctx2 f1 tf1 f2 tf2 f, + link f1 f2 = Some f -> + match_fundef ctx1 f1 tf1 -> match_fundef ctx2 f2 tf2 -> + exists tf, link tf1 tf2 = Some tf /\ (match_fundef ctx1 f tf \/ match_fundef ctx2 f tf). + +Hypothesis link_match_varinfo: + forall v1 tv1 v2 tv2 v, + link v1 v2 = Some v -> + match_varinfo v1 tv1 -> match_varinfo v2 tv2 -> + exists tv, link tv1 tv2 = Some tv /\ match_varinfo v tv. + +Lemma link_match_globvar: + forall v1 tv1 v2 tv2 v, + link v1 v2 = Some v -> + match_globvar match_varinfo v1 tv1 -> match_globvar match_varinfo v2 tv2 -> + exists tv, link tv1 tv2 = Some tv /\ match_globvar match_varinfo v tv. +Proof. + simpl; intros. unfold link_vardef in *. inv H0; inv H1; simpl in *. + destruct (link i1 i0) as [info'|] eqn:LINFO; try discriminate. + destruct (link init init0) as [init'|] eqn:LINIT; try discriminate. + destruct (eqb ro ro0 && eqb vo vo0); inv H. + exploit link_match_varinfo; eauto. intros (tinfo & P & Q). rewrite P. + econstructor; split. eauto. constructor. auto. +Qed. + +Lemma link_match_globdef: + forall ctx1 ctx2 ctx g1 tg1 g2 tg2 g, + linkorder ctx1 ctx -> linkorder ctx2 ctx -> + link g1 g2 = Some g -> + match_globdef match_fundef match_varinfo ctx1 g1 tg1 -> + match_globdef match_fundef match_varinfo ctx2 g2 tg2 -> + exists tg, link tg1 tg2 = Some tg /\ match_globdef match_fundef match_varinfo ctx g tg. +Proof. + simpl link. unfold link_def. intros. inv H2; inv H3; try discriminate. +- destruct (link f1 f0) as [f|] eqn:LF; inv H1. + exploit link_match_fundef; eauto. intros (tf & P & Q). + assert (X: exists ctx', linkorder ctx' ctx /\ match_fundef ctx' f tf). + { destruct Q as [Q|Q]; econstructor; (split; [|eassumption]). + apply linkorder_trans with ctx1; auto. + apply linkorder_trans with ctx2; auto. } + destruct X as (cu & X & Y). + exists (Gfun tf); split. rewrite P; auto. econstructor; eauto. +- destruct (link v1 v0) as [v|] eqn:LVAR; inv H1. + exploit link_match_globvar; eauto. intros (tv & P & Q). + exists (Gvar tv); split. rewrite P; auto. constructor; auto. +Qed. + +Lemma match_globdef_linkorder: + forall ctx ctx' g tg, + match_globdef match_fundef match_varinfo ctx g tg -> + linkorder ctx ctx' -> + match_globdef match_fundef match_varinfo ctx' g tg. +Proof. + intros. inv H. +- econstructor. eapply linkorder_trans; eauto. auto. +- constructor; auto. +Qed. + +Theorem link_match_program: + forall ctx1 ctx2 ctx p1 p2 tp1 tp2 p, + link p1 p2 = Some p -> + match_program_gen match_fundef match_varinfo ctx1 p1 tp1 -> + match_program_gen match_fundef match_varinfo ctx2 p2 tp2 -> + linkorder ctx1 ctx -> linkorder ctx2 ctx -> + exists tp, link tp1 tp2 = Some tp /\ match_program_gen match_fundef match_varinfo ctx p tp. +Proof. + intros. destruct (link_prog_inv _ _ _ H) as (P & Q & R). + generalize H0; intros (A1 & B1 & C1). + generalize H1; intros (A2 & B2 & C2). + econstructor; split. +- apply link_prog_succeeds. ++ congruence. ++ intros. + generalize (match_program_defmap _ _ _ _ _ H0 id) (match_program_defmap _ _ _ _ _ H1 id). + rewrite H4, H5. intros R1 R2; inv R1; inv R2. + exploit Q; eauto. intros (X & Y & gd & Z). + exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto. + intros (tg & TL & _). intuition congruence. +- split; [|split]. ++ rewrite R. apply PTree.elements_canonical_order'. intros id. + rewrite ! PTree.gcombine by auto. + generalize (match_program_defmap _ _ _ _ _ H0 id) (match_program_defmap _ _ _ _ _ H1 id). + clear R. intros R1 R2; inv R1; inv R2; unfold link_prog_merge. +* constructor. +* constructor. apply match_globdef_linkorder with ctx2; auto. +* constructor. apply match_globdef_linkorder with ctx1; auto. +* exploit Q; eauto. intros (X & Y & gd & Z). + exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto. + intros (tg & TL & MG). rewrite Z, TL. constructor; auto. ++ rewrite R; simpl; auto. ++ rewrite R; simpl. congruence. +Qed. + +End LINK_MATCH_PROGRAM. + +(** We now wrap this commutation diagram into a class, and provide some common instances. *) + +Class TransfLink {A B: Type} {LA: Linker A} {LB: Linker B} (transf: A -> B -> Prop) := + transf_link: + forall (p1 p2: A) (tp1 tp2: B) (p: A), + link p1 p2 = Some p -> + transf p1 tp1 -> transf p2 tp2 -> + exists tp, link tp1 tp2 = Some tp /\ transf p tp. + +Remark link_transf_partial_fundef: + forall (A B: Type) (tr1 tr2: A -> res B) (f1 f2: fundef A) (tf1 tf2: fundef B) (f: fundef A), + link f1 f2 = Some f -> + transf_partial_fundef tr1 f1 = OK tf1 -> + transf_partial_fundef tr2 f2 = OK tf2 -> + exists tf, + link tf1 tf2 = Some tf + /\ (transf_partial_fundef tr1 f = OK tf \/ transf_partial_fundef tr2 f = OK tf). +Proof. +Local Transparent Linker_fundef. + simpl; intros. destruct f1 as [f1|ef1], f2 as [f2|ef2]; simpl in *; monadInv H0; monadInv H1. +- discriminate. +- destruct ef2; inv H. exists (Internal x); split; auto. left; simpl; rewrite EQ; auto. +- destruct ef1; inv H. exists (Internal x); split; auto. right; simpl; rewrite EQ; auto. +- destruct (external_function_eq ef1 ef2); inv H. exists (External ef2); split; auto. simpl. rewrite dec_eq_true; auto. +Qed. + +Instance TransfPartialContextualLink + {A B C V: Type} {LV: Linker V} + (tr_fun: C -> A -> res B) + (ctx_for: program (fundef A) V -> C): + TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) => + match_program + (fun cu f tf => AST.transf_partial_fundef (tr_fun (ctx_for cu)) f = OK tf) + eq p1 p2). +Proof. + red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. + eapply link_match_program; eauto. +- intros. eapply link_transf_partial_fundef; eauto. +- intros; subst. exists v; auto. +Qed. + +Instance TransfPartialLink + {A B V: Type} {LV: Linker V} + (tr_fun: A -> res B): + TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) => + match_program + (fun cu f tf => AST.transf_partial_fundef tr_fun f = OK tf) + eq p1 p2). +Proof. + red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. + eapply link_match_program; eauto. +- intros. eapply link_transf_partial_fundef; eauto. +- intros; subst. exists v; auto. +Qed. + +Instance TransfTotallContextualLink + {A B C V: Type} {LV: Linker V} + (tr_fun: C -> A -> B) + (ctx_for: program (fundef A) V -> C): + TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) => + match_program + (fun cu f tf => tf = AST.transf_fundef (tr_fun (ctx_for cu)) f) + eq p1 p2). +Proof. + red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. + eapply link_match_program; eauto. +- intros. subst. destruct f1, f2; simpl in *. ++ discriminate. ++ destruct e; inv H2. econstructor; eauto. ++ destruct e; inv H2. econstructor; eauto. ++ destruct (external_function_eq e e0); inv H2. econstructor; eauto. +- intros; subst. exists v; auto. +Qed. + +Instance TransfTotalLink + {A B V: Type} {LV: Linker V} + (tr_fun: A -> B): + TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) => + match_program + (fun cu f tf => tf = AST.transf_fundef tr_fun f) + eq p1 p2). +Proof. + red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. + eapply link_match_program; eauto. +- intros. subst. destruct f1, f2; simpl in *. ++ discriminate. ++ destruct e; inv H2. econstructor; eauto. ++ destruct e; inv H2. econstructor; eauto. ++ destruct (external_function_eq e e0); inv H2. econstructor; eauto. +- intros; subst. exists v; auto. +Qed. + +(** * Linking a set of compilation units *) + +(** Here, we take a more general view of linking as taking a nonempty list of compilation units + and producing a whole program. *) + +Section LINK_LIST. + +Context {A: Type} {LA: Linker A}. + +Fixpoint link_list (l: nlist A) : option A := + match l with + | nbase a => Some a + | ncons a l => + match link_list l with None => None | Some b => link a b end + end. + +Lemma link_list_linkorder: + forall a l b, link_list l = Some b -> nIn a l -> linkorder a b. +Proof. + induction l; simpl; intros. +- inv H. subst. apply linkorder_refl. +- destruct (link_list l) as [b'|]; try discriminate. + apply link_linkorder in H. destruct H0. ++ subst a0. tauto. ++ apply linkorder_trans with b'. auto. tauto. +Qed. + +End LINK_LIST. + +(** List linking commutes with program transformations, provided the + transformation commutes with simple (binary) linking. *) + +Section LINK_LIST_MATCH. + +Context {A B: Type} {LA: Linker A} {LB: Linker B} (prog_match: A -> B -> Prop) {TL: TransfLink prog_match}. + +Theorem link_list_match: + forall al bl, nlist_forall2 prog_match al bl -> + forall a, link_list al = Some a -> + exists b, link_list bl = Some b /\ prog_match a b. +Proof. + induction 1; simpl; intros a' L. +- inv L. exists b; auto. +- destruct (link_list l) as [a1|] eqn:LL; try discriminate. + exploit IHnlist_forall2; eauto. intros (b' & P & Q). + red in TL. exploit TL; eauto. intros (b'' & U & V). + rewrite P; exists b''; auto. +Qed. + +End LINK_LIST_MATCH. + +(** * Linking and composition of compilation passes *) + +Set Implicit Arguments. + +(** A generic language is a type of programs and a linker. *) + +Structure Language := mklang { lang_prog :> Type; lang_link: Linker lang_prog }. + +Canonical Structure Language_gen (A: Type) (L: Linker A) : Language := @mklang A L. + +(** A compilation pass from language [S] (source) to language [T] (target) + is a matching relation between [S] programs and [T] programs, + plus two linkers, one for [S] and one for [T], + and a property of commutation with linking. *) + +Record Pass (S T: Language) := mkpass { + pass_match :> lang_prog S -> lang_prog T -> Prop; + pass_match_link: @TransfLink (lang_prog S) (lang_prog T) (lang_link S) (lang_link T) pass_match +}. + +Arguments mkpass {S} {T} (pass_match) {pass_match_link}. + +Program Definition pass_identity (l: Language): Pass l l := + {| pass_match := fun p1 p2 => p1 = p2; + pass_match_link := _ |}. +Next Obligation. + red; intros. subst. exists p; auto. +Defined. + +Program Definition pass_compose {l1 l2 l3: Language} (pass: Pass l1 l2) (pass': Pass l2 l3) : Pass l1 l3 := + {| pass_match := fun p1 p3 => exists p2, pass_match pass p1 p2 /\ pass_match pass' p2 p3; + pass_match_link := _ |}. +Next Obligation. + red; intros. + destruct H0 as (p1' & A1 & B1). + destruct H1 as (p2' & A2 & B2). + edestruct (pass_match_link pass) as (p' & A & B); eauto. + edestruct (pass_match_link pass') as (tp & C & D); eauto. +Defined. + +(** A list of compilation passes that can be composed. *) + +Inductive Passes: Language -> Language -> Type := + | pass_nil: forall l, Passes l l + | pass_cons: forall l1 l2 l3, Pass l1 l2 -> Passes l2 l3 -> Passes l1 l3. + +Infix ":::" := pass_cons (at level 60, right associativity) : linking_scope. + +(** The pass corresponding to the composition of a list of passes. *) + +Fixpoint compose_passes (l l': Language) (passes: Passes l l') : Pass l l' := + match passes in Passes l l' return Pass l l' with + | pass_nil l => pass_identity l + | pass_cons l1 l2 l3 pass1 passes => pass_compose pass1 (compose_passes passes) + end. + +(** Some more lemmas about [nlist_forall2]. *) + +Lemma nlist_forall2_identity: + forall (A: Type) (la lb: nlist A), + nlist_forall2 (fun a b => a = b) la lb -> la = lb. +Proof. + induction 1; congruence. +Qed. + +Lemma nlist_forall2_compose_inv: + forall (A B C: Type) (R1: A -> B -> Prop) (R2: B -> C -> Prop) + (la: nlist A) (lc: nlist C), + nlist_forall2 (fun a c => exists b, R1 a b /\ R2 b c) la lc -> + exists lb: nlist B, nlist_forall2 R1 la lb /\ nlist_forall2 R2 lb lc. +Proof. + induction 1. +- rename b into c. destruct H as (b & P & Q). + exists (nbase b); split; constructor; auto. +- rename b into c. destruct H as (b & P & Q). destruct IHnlist_forall2 as (lb & U & V). + exists (ncons b lb); split; constructor; auto. +Qed. + +(** List linking with a composition of compilation passes. *) + +Theorem link_list_compose_passes: + forall (src tgt: Language) (passes: Passes src tgt) + (src_units: nlist src) (tgt_units: nlist tgt), + nlist_forall2 (pass_match (compose_passes passes)) src_units tgt_units -> + forall src_prog, + @link_list _ (lang_link src) src_units = Some src_prog -> + exists tgt_prog, + @link_list _ (lang_link tgt) tgt_units = Some tgt_prog + /\ pass_match (compose_passes passes) src_prog tgt_prog. +Proof. + induction passes; simpl; intros src_units tgt_units F2 src_prog LINK. +- apply nlist_forall2_identity in F2. subst tgt_units. exists src_prog; auto. +- apply nlist_forall2_compose_inv in F2. destruct F2 as (interm_units & P & Q). + edestruct (@link_list_match _ _ (lang_link l1) (lang_link l2) (pass_match p)) + as (interm_prog & U & V). + apply pass_match_link. eauto. eauto. + exploit IHpasses; eauto. intros (tgt_prog & X & Y). + exists tgt_prog; split; auto. exists interm_prog; auto. +Qed. + diff --git a/common/Memory.v b/common/Memory.v index 93d0e432..0ea9e3b0 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -4143,6 +4143,8 @@ Section UNCHANGED_ON. Variable P: block -> Z -> Prop. Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on { + unchanged_on_nextblock: + Ple (nextblock m_before) (nextblock m_after); unchanged_on_perm: forall b ofs k p, P b ofs -> valid_block m_before b -> @@ -4157,15 +4159,22 @@ Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on { Lemma unchanged_on_refl: forall m, unchanged_on m m. Proof. - intros; constructor; tauto. + intros; constructor. apply Ple_refl. tauto. tauto. +Qed. + +Lemma valid_block_unchanged_on: + forall m m' b, + unchanged_on m m' -> valid_block m b -> valid_block m' b. +Proof. + unfold valid_block; intros. apply unchanged_on_nextblock in H. xomega. Qed. Lemma perm_unchanged_on: forall m m' b ofs k p, - unchanged_on m m' -> P b ofs -> valid_block m b -> + unchanged_on m m' -> P b ofs -> perm m b ofs k p -> perm m' b ofs k p. Proof. - intros. destruct H. apply unchanged_on_perm0; auto. + intros. destruct H. apply unchanged_on_perm0; auto. eapply perm_valid_block; eauto. Qed. Lemma perm_unchanged_on_2: @@ -4176,6 +4185,17 @@ Proof. intros. destruct H. apply unchanged_on_perm0; auto. Qed. +Lemma unchanged_on_trans: + forall m1 m2 m3, unchanged_on m1 m2 -> unchanged_on m2 m3 -> unchanged_on m1 m3. +Proof. + intros; constructor. +- apply Ple_trans with (nextblock m2); apply unchanged_on_nextblock; auto. +- intros. transitivity (perm m2 b ofs k p); apply unchanged_on_perm; auto. + eapply valid_block_unchanged_on; eauto. +- intros. transitivity (ZMap.get ofs (mem_contents m2)#b); apply unchanged_on_contents; auto. + eapply perm_unchanged_on; eauto. +Qed. + Lemma loadbytes_unchanged_on_1: forall m m' b ofs n, unchanged_on m m' -> @@ -4243,6 +4263,7 @@ Lemma store_unchanged_on: unchanged_on m m'. Proof. intros; constructor; intros. +- rewrite (nextblock_store _ _ _ _ _ _ H). apply Ple_refl. - split; intros; eauto with mem. - erewrite store_mem_contents; eauto. rewrite PMap.gsspec. destruct (peq b0 b); auto. subst b0. apply setN_outside. @@ -4259,6 +4280,7 @@ Lemma storebytes_unchanged_on: unchanged_on m m'. Proof. intros; constructor; intros. +- rewrite (nextblock_storebytes _ _ _ _ _ H). apply Ple_refl. - split; intros. eapply perm_storebytes_1; eauto. eapply perm_storebytes_2; eauto. - erewrite storebytes_mem_contents; eauto. rewrite PMap.gsspec. destruct (peq b0 b); auto. subst b0. apply setN_outside. @@ -4273,6 +4295,7 @@ Lemma alloc_unchanged_on: unchanged_on m m'. Proof. intros; constructor; intros. +- rewrite (nextblock_alloc _ _ _ _ _ H). apply Ple_succ. - split; intros. eapply perm_alloc_1; eauto. eapply perm_alloc_4; eauto. @@ -4288,6 +4311,7 @@ Lemma free_unchanged_on: unchanged_on m m'. Proof. intros; constructor; intros. +- rewrite (nextblock_free _ _ _ _ _ H). apply Ple_refl. - split; intros. eapply perm_free_1; eauto. destruct (eq_block b0 b); auto. destruct (zlt ofs lo); auto. destruct (zle hi ofs); auto. @@ -4297,8 +4321,39 @@ Proof. simpl. auto. Qed. +Lemma drop_perm_unchanged_on: + forall m b lo hi p m', + drop_perm m b lo hi p = Some m' -> + (forall i, lo <= i < hi -> ~ P b i) -> + unchanged_on m m'. +Proof. + intros; constructor; intros. +- rewrite (nextblock_drop _ _ _ _ _ _ H). apply Ple_refl. +- split; intros. eapply perm_drop_3; eauto. + destruct (eq_block b0 b); auto. + subst b0. + assert (~ (lo <= ofs < hi)). { red; intros; eelim H0; eauto. } + right; omega. + eapply perm_drop_4; eauto. +- unfold drop_perm in H. + destruct (range_perm_dec m b lo hi Cur Freeable); inv H; simpl. auto. +Qed. + End UNCHANGED_ON. +Lemma unchanged_on_implies: + forall (P Q: block -> Z -> Prop) m m', + unchanged_on P m m' -> + (forall b ofs, Q b ofs -> valid_block m b -> P b ofs) -> + unchanged_on Q m m'. +Proof. + intros. destruct H. constructor; intros. +- auto. +- apply unchanged_on_perm0; auto. +- apply unchanged_on_contents0; auto. + apply H0; auto. eapply perm_valid_block; eauto. +Qed. + End Mem. Notation mem := Mem.mem. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 39481bfb..48172dfd 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -39,6 +39,7 @@ let name_of_chunk = function let name_of_external = function | EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name) | EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name) + | EF_runtime(name, sg) -> sprintf "runtime %S" (camlstring_of_coqstring name) | EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk) | EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk) | EF_malloc -> "malloc" @@ -55,8 +56,8 @@ let rec print_builtin_arg px oc = function | BA x -> px oc x | BA_int n -> fprintf oc "int %ld" (camlint_of_coqint n) | BA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n) - | BA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n) - | BA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n) + | BA_float n -> fprintf oc "float %.15F" (camlfloat_of_coqfloat n) + | BA_single n -> fprintf oc "single %.15F" (camlfloat_of_coqfloat32 n) | BA_loadstack(chunk, ofs) -> fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs) | BA_addrstack(ofs) -> diff --git a/common/Smallstep.v b/common/Smallstep.v index 71cef35f..9c91243a 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -513,43 +513,49 @@ Open Scope smallstep_scope. (** The general form of a forward simulation. *) -Record forward_simulation (L1 L2: semantics) : Type := - Forward_simulation { - fsim_index: Type; - fsim_order: fsim_index -> fsim_index -> Prop; - fsim_order_wf: well_founded fsim_order; - fsim_match_states :> fsim_index -> state L1 -> state L2 -> Prop; +Record fsim_properties (L1 L2: semantics) (index: Type) + (order: index -> index -> Prop) + (match_states: index -> state L1 -> state L2 -> Prop) : Prop := { + fsim_order_wf: well_founded order; fsim_match_initial_states: forall s1, initial_state L1 s1 -> - exists i, exists s2, initial_state L2 s2 /\ fsim_match_states i s1 s2; + exists i, exists s2, initial_state L2 s2 /\ match_states i s1 s2; fsim_match_final_states: forall i s1 s2 r, - fsim_match_states i s1 s2 -> final_state L1 s1 r -> final_state L2 s2 r; + match_states i s1 s2 -> final_state L1 s1 r -> final_state L2 s2 r; fsim_simulation: forall s1 t s1', Step L1 s1 t s1' -> - forall i s2, fsim_match_states i s1 s2 -> + forall i s2, match_states i s1 s2 -> exists i', exists s2', - (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ fsim_order i' i)) - /\ fsim_match_states i' s1' s2'; + (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ order i' i)) + /\ match_states i' s1' s2'; fsim_public_preserved: forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id }. -Implicit Arguments forward_simulation []. +Arguments fsim_properties: clear implicits. + +Inductive forward_simulation (L1 L2: semantics) : Prop := + Forward_simulation (index: Type) + (order: index -> index -> Prop) + (match_states: index -> state L1 -> state L2 -> Prop) + (props: fsim_properties L1 L2 index order match_states). + +Arguments Forward_simulation {L1 L2 index} order match_states props. (** An alternate form of the simulation diagram *) Lemma fsim_simulation': - forall L1 L2 (S: forward_simulation L1 L2), + forall L1 L2 index order match_states, fsim_properties L1 L2 index order match_states -> forall i s1 t s1', Step L1 s1 t s1' -> - forall s2, S i s1 s2 -> - (exists i', exists s2', Plus L2 s2 t s2' /\ S i' s1' s2') - \/ (exists i', fsim_order S i' i /\ t = E0 /\ S i' s1' s2). + forall s2, match_states i s1 s2 -> + (exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2') + \/ (exists i', order i' i /\ t = E0 /\ match_states i' s1' s2). Proof. intros. exploit fsim_simulation; eauto. intros [i' [s2' [A B]]]. intuition. left; exists i'; exists s2'; auto. - inv H2. + inv H3. right; exists i'; auto. left; exists i'; exists s2'; split; auto. econstructor; eauto. Qed. @@ -602,15 +608,15 @@ Hypothesis simulation: Lemma forward_simulation_star_wf: forward_simulation L1 L2. Proof. - apply Forward_simulation with - (fsim_order := order) - (fsim_match_states := fun idx s1 s2 => idx = s1 /\ match_states s1 s2); - auto. - intros. exploit match_initial_states; eauto. intros [s2 [A B]]. + apply Forward_simulation with order (fun idx s1 s2 => idx = s1 /\ match_states s1 s2); + constructor. +- auto. +- intros. exploit match_initial_states; eauto. intros [s2 [A B]]. exists s1; exists s2; auto. - intros. destruct H. eapply match_final_states; eauto. - intros. destruct H0. subst i. exploit simulation; eauto. intros [s2' [A B]]. - exists s1'; exists s2'; intuition. +- intros. destruct H. eapply match_final_states; eauto. +- intros. destruct H0. subst i. exploit simulation; eauto. intros [s2' [A B]]. + exists s1'; exists s2'; intuition auto. +- auto. Qed. End SIMULATION_STAR_WF. @@ -709,28 +715,26 @@ End FORWARD_SIMU_DIAGRAMS. Section SIMULATION_SEQUENCES. -Variable L1: semantics. -Variable L2: semantics. -Variable S: forward_simulation L1 L2. +Context L1 L2 index order match_states (S: fsim_properties L1 L2 index order match_states). Lemma simulation_star: forall s1 t s1', Star L1 s1 t s1' -> - forall i s2, S i s1 s2 -> - exists i', exists s2', Star L2 s2 t s2' /\ S i' s1' s2'. + forall i s2, match_states i s1 s2 -> + exists i', exists s2', Star L2 s2 t s2' /\ match_states i' s1' s2'. Proof. induction 1; intros. exists i; exists s2; split; auto. apply star_refl. exploit fsim_simulation; eauto. intros [i' [s2' [A B]]]. exploit IHstar; eauto. intros [i'' [s2'' [C D]]]. exists i''; exists s2''; split; auto. eapply star_trans; eauto. - intuition. apply plus_star; auto. + intuition auto. apply plus_star; auto. Qed. Lemma simulation_plus: forall s1 t s1', Plus L1 s1 t s1' -> - forall i s2, S i s1 s2 -> - (exists i', exists s2', Plus L2 s2 t s2' /\ S i' s1' s2') - \/ (exists i', clos_trans _ (fsim_order S) i' i /\ t = E0 /\ S i' s1' s2). + forall i s2, match_states i s1 s2 -> + (exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2') + \/ (exists i', clos_trans _ order i' i /\ t = E0 /\ match_states i' s1' s2). Proof. induction 1 using plus_ind2; intros. (* base case *) @@ -744,34 +748,34 @@ Proof. left; exists i''; exists s2''; split; auto. eapply plus_star_trans; eauto. exploit IHplus; eauto. intros [[i'' [s2'' [P Q]]] | [i'' [P [Q R]]]]. subst. simpl. left; exists i''; exists s2''; auto. - subst. simpl. right; exists i''; intuition. + subst. simpl. right; exists i''; intuition auto. eapply t_trans; eauto. eapply t_step; eauto. Qed. Lemma simulation_forever_silent: forall i s1 s2, - Forever_silent L1 s1 -> S i s1 s2 -> + Forever_silent L1 s1 -> match_states i s1 s2 -> Forever_silent L2 s2. Proof. assert (forall i s1 s2, - Forever_silent L1 s1 -> S i s1 s2 -> - forever_silent_N (step L2) (fsim_order S) (globalenv L2) i s2). + Forever_silent L1 s1 -> match_states i s1 s2 -> + forever_silent_N (step L2) order (globalenv L2) i s2). cofix COINDHYP; intros. inv H. destruct (fsim_simulation S _ _ _ H1 _ _ H0) as [i' [s2' [A B]]]. destruct A as [C | [C D]]. eapply forever_silent_N_plus; eauto. eapply forever_silent_N_star; eauto. - intros. eapply forever_silent_N_forever; eauto. apply fsim_order_wf. + intros. eapply forever_silent_N_forever; eauto. eapply fsim_order_wf; eauto. Qed. Lemma simulation_forever_reactive: forall i s1 s2 T, - Forever_reactive L1 s1 T -> S i s1 s2 -> + Forever_reactive L1 s1 T -> match_states i s1 s2 -> Forever_reactive L2 s2 T. Proof. cofix COINDHYP; intros. inv H. - destruct (simulation_star H1 i _ H0) as [i' [st2' [A B]]]. + edestruct simulation_star as [i' [st2' [A B]]]; eauto. econstructor; eauto. Qed. @@ -779,56 +783,48 @@ End SIMULATION_SEQUENCES. (** ** Composing two forward simulations *) -Section COMPOSE_SIMULATIONS. - -Variable L1: semantics. -Variable L2: semantics. -Variable L3: semantics. -Variable S12: forward_simulation L1 L2. -Variable S23: forward_simulation L2 L3. - -Let ff_index : Type := (fsim_index S23 * fsim_index S12)%type. - -Let ff_order : ff_index -> ff_index -> Prop := - lex_ord (clos_trans _ (fsim_order S23)) (fsim_order S12). - -Let ff_match_states (i: ff_index) (s1: state L1) (s3: state L3) : Prop := - exists s2, S12 (snd i) s1 s2 /\ S23 (fst i) s2 s3. - -Lemma compose_forward_simulation: forward_simulation L1 L3. -Proof. - apply Forward_simulation with (fsim_order := ff_order) (fsim_match_states := ff_match_states). -(* well founded *) - unfold ff_order. apply wf_lex_ord. apply wf_clos_trans. apply fsim_order_wf. apply fsim_order_wf. -(* initial states *) - intros. exploit (fsim_match_initial_states S12); eauto. intros [i [s2 [A B]]]. - exploit (fsim_match_initial_states S23); eauto. intros [i' [s3 [C D]]]. +Lemma compose_forward_simulations: + forall L1 L2 L3, forward_simulation L1 L2 -> forward_simulation L2 L3 -> forward_simulation L1 L3. +Proof. + intros L1 L2 L3 S12 S23. + destruct S12 as [index order match_states props]. + destruct S23 as [index' order' match_states' props']. + + set (ff_index := (index' * index)%type). + set (ff_order := lex_ord (clos_trans _ order') order). + set (ff_match_states := fun (i: ff_index) (s1: state L1) (s3: state L3) => + exists s2, match_states (snd i) s1 s2 /\ match_states' (fst i) s2 s3). + apply Forward_simulation with ff_order ff_match_states; constructor. +- (* well founded *) + unfold ff_order. apply wf_lex_ord. apply wf_clos_trans. + eapply fsim_order_wf; eauto. eapply fsim_order_wf; eauto. +- (* initial states *) + intros. exploit (fsim_match_initial_states props); eauto. intros [i [s2 [A B]]]. + exploit (fsim_match_initial_states props'); eauto. intros [i' [s3 [C D]]]. exists (i', i); exists s3; split; auto. exists s2; auto. -(* final states *) +- (* final states *) intros. destruct H as [s3 [A B]]. - eapply (fsim_match_final_states S23); eauto. - eapply (fsim_match_final_states S12); eauto. -(* simulation *) + eapply (fsim_match_final_states props'); eauto. + eapply (fsim_match_final_states props); eauto. +- (* simulation *) intros. destruct H0 as [s3 [A B]]. destruct i as [i2 i1]; simpl in *. - exploit (fsim_simulation' S12); eauto. intros [[i1' [s3' [C D]]] | [i1' [C [D E]]]]. - (* L2 makes one or several steps. *) + exploit (fsim_simulation' props); eauto. intros [[i1' [s3' [C D]]] | [i1' [C [D E]]]]. ++ (* L2 makes one or several steps. *) exploit simulation_plus; eauto. intros [[i2' [s2' [P Q]]] | [i2' [P [Q R]]]]. - (* L3 makes one or several steps *) +* (* L3 makes one or several steps *) exists (i2', i1'); exists s2'; split. auto. exists s3'; auto. - (* L3 makes no step *) +* (* L3 makes no step *) exists (i2', i1'); exists s2; split. right; split. subst t; apply star_refl. red. left. auto. exists s3'; auto. - (* L2 makes no step *) ++ (* L2 makes no step *) exists (i2, i1'); exists s2; split. right; split. subst t; apply star_refl. red. right. auto. exists s3; auto. -(* symbols *) - intros. transitivity (Senv.public_symbol (symbolenv L2) id); apply fsim_public_preserved; auto. +- (* symbols *) + intros. transitivity (Senv.public_symbol (symbolenv L2) id); eapply fsim_public_preserved; eauto. Qed. -End COMPOSE_SIMULATIONS. - (** * Receptiveness and determinacy *) Definition single_events (L: semantics) : Prop := @@ -916,49 +912,57 @@ Qed. (** The general form of a backward simulation. *) -Record backward_simulation (L1 L2: semantics) : Type := - Backward_simulation { - bsim_index: Type; - bsim_order: bsim_index -> bsim_index -> Prop; - bsim_order_wf: well_founded bsim_order; - bsim_match_states :> bsim_index -> state L1 -> state L2 -> Prop; +Record bsim_properties (L1 L2: semantics) (index: Type) + (order: index -> index -> Prop) + (match_states: index -> state L1 -> state L2 -> Prop) : Prop := { + bsim_order_wf: well_founded order; bsim_initial_states_exist: forall s1, initial_state L1 s1 -> exists s2, initial_state L2 s2; bsim_match_initial_states: forall s1 s2, initial_state L1 s1 -> initial_state L2 s2 -> - exists i, exists s1', initial_state L1 s1' /\ bsim_match_states i s1' s2; + exists i, exists s1', initial_state L1 s1' /\ match_states i s1' s2; bsim_match_final_states: forall i s1 s2 r, - bsim_match_states i s1 s2 -> safe L1 s1 -> final_state L2 s2 r -> + match_states i s1 s2 -> safe L1 s1 -> final_state L2 s2 r -> exists s1', Star L1 s1 E0 s1' /\ final_state L1 s1' r; bsim_progress: forall i s1 s2, - bsim_match_states i s1 s2 -> safe L1 s1 -> + match_states i s1 s2 -> safe L1 s1 -> (exists r, final_state L2 s2 r) \/ (exists t, exists s2', Step L2 s2 t s2'); bsim_simulation: forall s2 t s2', Step L2 s2 t s2' -> - forall i s1, bsim_match_states i s1 s2 -> safe L1 s1 -> + forall i s1, match_states i s1 s2 -> safe L1 s1 -> exists i', exists s1', - (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order i' i)) - /\ bsim_match_states i' s1' s2'; + (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ order i' i)) + /\ match_states i' s1' s2'; bsim_public_preserved: forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id }. +Arguments bsim_properties: clear implicits. + +Inductive backward_simulation (L1 L2: semantics) : Prop := + Backward_simulation (index: Type) + (order: index -> index -> Prop) + (match_states: index -> state L1 -> state L2 -> Prop) + (props: bsim_properties L1 L2 index order match_states). + +Arguments Backward_simulation {L1 L2 index} order match_states props. + (** An alternate form of the simulation diagram *) Lemma bsim_simulation': - forall L1 L2 (S: backward_simulation L1 L2), + forall L1 L2 index order match_states, bsim_properties L1 L2 index order match_states -> forall i s2 t s2', Step L2 s2 t s2' -> - forall s1, S i s1 s2 -> safe L1 s1 -> - (exists i', exists s1', Plus L1 s1 t s1' /\ S i' s1' s2') - \/ (exists i', bsim_order S i' i /\ t = E0 /\ S i' s1 s2'). + forall s1, match_states i s1 s2 -> safe L1 s1 -> + (exists i', exists s1', Plus L1 s1 t s1' /\ match_states i' s1' s2') + \/ (exists i', order i' i /\ t = E0 /\ match_states i' s1 s2'). Proof. intros. exploit bsim_simulation; eauto. intros [i' [s1' [A B]]]. intuition. left; exists i'; exists s1'; auto. - inv H3. + inv H4. right; exists i'; auto. left; exists i'; exists s1'; split; auto. econstructor; eauto. Qed. @@ -1004,13 +1008,13 @@ Hypothesis simulation: Lemma backward_simulation_plus: backward_simulation L1 L2. Proof. apply Backward_simulation with - (bsim_order := fun (x y: unit) => False) - (bsim_match_states := fun (i: unit) s1 s2 => match_states s1 s2); - auto. - red; intros; constructor; intros. contradiction. - intros. exists tt; eauto. - intros. exists s1; split. apply star_refl. eauto. - intros. exploit simulation; eauto. intros [s1' [A B]]. + (fun (x y: unit) => False) + (fun (i: unit) s1 s2 => match_states s1 s2); + constructor; auto. +- red; intros; constructor; intros. contradiction. +- intros. exists tt; eauto. +- intros. exists s1; split. apply star_refl. eauto. +- intros. exploit simulation; eauto. intros [s1' [A B]]. exists tt; exists s1'; auto. Qed. @@ -1022,19 +1026,17 @@ End BACKWARD_SIMU_DIAGRAMS. Section BACKWARD_SIMULATION_SEQUENCES. -Variable L1: semantics. -Variable L2: semantics. -Variable S: backward_simulation L1 L2. +Context L1 L2 index order match_states (S: bsim_properties L1 L2 index order match_states). Lemma bsim_E0_star: forall s2 s2', Star L2 s2 E0 s2' -> - forall i s1, S i s1 s2 -> safe L1 s1 -> - exists i', exists s1', Star L1 s1 E0 s1' /\ S i' s1' s2'. + forall i s1, match_states i s1 s2 -> safe L1 s1 -> + exists i', exists s1', Star L1 s1 E0 s1' /\ match_states i' s1' s2'. Proof. intros s20 s20' STAR0. pattern s20, s20'. eapply star_E0_ind; eauto. -(* base case *) +- (* base case *) intros. exists i; exists s1; split; auto. apply star_refl. -(* inductive case *) +- (* inductive case *) intros. exploit bsim_simulation; eauto. intros [i' [s1' [A B]]]. assert (Star L1 s0 E0 s1'). intuition. apply plus_star; auto. exploit H0. eauto. eapply star_safe; eauto. intros [i'' [s1'' [C D]]]. @@ -1043,7 +1045,7 @@ Qed. Lemma bsim_safe: forall i s1 s2, - S i s1 s2 -> safe L1 s1 -> safe L2 s2. + match_states i s1 s2 -> safe L1 s1 -> safe L2 s2. Proof. intros; red; intros. exploit bsim_E0_star; eauto. intros [i' [s1' [A B]]]. @@ -1052,22 +1054,22 @@ Qed. Lemma bsim_E0_plus: forall s2 t s2', Plus L2 s2 t s2' -> t = E0 -> - forall i s1, S i s1 s2 -> safe L1 s1 -> - (exists i', exists s1', Plus L1 s1 E0 s1' /\ S i' s1' s2') - \/ (exists i', clos_trans _ (bsim_order S) i' i /\ S i' s1 s2'). + forall i s1, match_states i s1 s2 -> safe L1 s1 -> + (exists i', exists s1', Plus L1 s1 E0 s1' /\ match_states i' s1' s2') + \/ (exists i', clos_trans _ order i' i /\ match_states i' s1 s2'). Proof. induction 1 using plus_ind2; intros; subst t. -(* base case *) +- (* base case *) exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]]. - left; exists i'; exists s1'; auto. - right; exists i'; intuition. -(* inductive case *) ++ left; exists i'; exists s1'; auto. ++ right; exists i'; intuition. +- (* inductive case *) exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst. exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]]. - exploit bsim_E0_star. apply plus_star; eauto. eauto. eapply star_safe; eauto. apply plus_star; auto. ++ exploit bsim_E0_star. apply plus_star; eauto. eauto. eapply star_safe; eauto. apply plus_star; auto. intros [i'' [s1'' [P Q]]]. left; exists i''; exists s1''; intuition. eapply plus_star_trans; eauto. - exploit IHplus; eauto. intros [P | [i'' [P Q]]]. ++ exploit IHplus; eauto. intros [P | [i'' [P Q]]]. left; auto. right; exists i''; intuition. eapply t_trans; eauto. apply t_step; auto. Qed. @@ -1098,21 +1100,20 @@ Variable L1: semantics. Variable L2: semantics. Variable L3: semantics. Hypothesis L3_single_events: single_events L3. -Variable S12: backward_simulation L1 L2. -Variable S23: backward_simulation L2 L3. +Context index order match_states (S12: bsim_properties L1 L2 index order match_states). +Context index' order' match_states' (S23: bsim_properties L2 L3 index' order' match_states'). -Let bb_index : Type := (bsim_index S12 * bsim_index S23)%type. +Let bb_index : Type := (index * index')%type. -Let bb_order : bb_index -> bb_index -> Prop := - lex_ord (clos_trans _ (bsim_order S12)) (bsim_order S23). +Definition bb_order : bb_index -> bb_index -> Prop := lex_ord (clos_trans _ order) order'. Inductive bb_match_states: bb_index -> state L1 -> state L3 -> Prop := | bb_match_later: forall i1 i2 s1 s3 s2x s2y, - S12 i1 s1 s2x -> Star L2 s2x E0 s2y -> S23 i2 s2y s3 -> + match_states i1 s1 s2x -> Star L2 s2x E0 s2y -> match_states' i2 s2y s3 -> bb_match_states (i1, i2) s1 s3. Lemma bb_match_at: forall i1 i2 s1 s3 s2, - S12 i1 s1 s2 -> S23 i2 s2 s3 -> + match_states i1 s1 s2 -> match_states' i2 s2 s3 -> bb_match_states (i1, i2) s1 s3. Proof. intros. econstructor; eauto. apply star_refl. @@ -1120,7 +1121,7 @@ Qed. Lemma bb_simulation_base: forall s3 t s3', Step L3 s3 t s3' -> - forall i1 s1 i2 s2, S12 i1 s1 s2 -> S23 i2 s2 s3 -> safe L1 s1 -> + forall i1 s1 i2 s2, match_states i1 s1 s2 -> match_states' i2 s2 s3 -> safe L1 s1 -> exists i', exists s1', (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bb_order i' (i1, i2))) /\ bb_match_states i' s1' s3'. @@ -1128,29 +1129,29 @@ Proof. intros. exploit (bsim_simulation' S23); eauto. eapply bsim_safe; eauto. intros [ [i2' [s2' [PLUS2 MATCH2]]] | [i2' [ORD2 [EQ MATCH2]]]]. - (* 1 L2 makes one or several transitions *) +- (* 1 L2 makes one or several transitions *) assert (EITHER: t = E0 \/ (length t = 1)%nat). - exploit L3_single_events; eauto. - destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. + { exploit L3_single_events; eauto. + destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. } destruct EITHER. - (* 1.1 these are silent transitions *) - subst t. exploit bsim_E0_plus; eauto. ++ (* 1.1 these are silent transitions *) + subst t. exploit (bsim_E0_plus S12); eauto. intros [ [i1' [s1' [PLUS1 MATCH1]]] | [i1' [ORD1 MATCH1]]]. - (* 1.1.1 L1 makes one or several transitions *) +* (* 1.1.1 L1 makes one or several transitions *) exists (i1', i2'); exists s1'; split. auto. eapply bb_match_at; eauto. - (* 1.1.2 L1 makes no transitions *) +* (* 1.1.2 L1 makes no transitions *) exists (i1', i2'); exists s1; split. right; split. apply star_refl. left; auto. eapply bb_match_at; eauto. - (* 1.2 non-silent transitions *) ++ (* 1.2 non-silent transitions *) exploit star_non_E0_split. apply plus_star; eauto. auto. intros [s2x [s2y [P [Q R]]]]. - exploit bsim_E0_star. eexact P. eauto. auto. intros [i1' [s1x [X Y]]]. - exploit bsim_simulation'. eexact Q. eauto. eapply star_safe; eauto. + exploit (bsim_E0_star S12). eexact P. eauto. auto. intros [i1' [s1x [X Y]]]. + exploit (bsim_simulation' S12). eexact Q. eauto. eapply star_safe; eauto. intros [[i1'' [s1y [U V]]] | [i1'' [U [V W]]]]; try (subst t; discriminate). exists (i1'', i2'); exists s1y; split. left. eapply star_plus_trans; eauto. eapply bb_match_later; eauto. - (* 2. L2 makes no transitions *) +- (* 2. L2 makes no transitions *) subst. exists (i1, i2'); exists s1; split. right; split. apply star_refl. right; auto. eapply bb_match_at; eauto. @@ -1165,12 +1166,12 @@ Lemma bb_simulation: Proof. intros. inv H0. exploit star_inv; eauto. intros [[EQ1 EQ2] | PLUS]. - (* 1. match at *) +- (* 1. match at *) subst. eapply bb_simulation_base; eauto. - (* 2. match later *) - exploit bsim_E0_plus; eauto. +- (* 2. match later *) + exploit (bsim_E0_plus S12); eauto. intros [[i1' [s1' [A B]]] | [i1' [A B]]]. - (* 2.1 one or several silent transitions *) ++ (* 2.1 one or several silent transitions *) exploit bb_simulation_base. eauto. auto. eexact B. eauto. eapply star_safe; eauto. eapply plus_star; eauto. intros [i'' [s1'' [C D]]]. @@ -1178,7 +1179,7 @@ Proof. left. eapply plus_star_trans; eauto. destruct C as [P | [P Q]]. apply plus_star; eauto. eauto. traceEq. - (* 2.2 no silent transition *) ++ (* 2.2 no silent transition *) exploit bb_simulation_base. eauto. auto. eexact B. eauto. auto. intros [i'' [s1'' [C D]]]. exists i''; exists s1''; split; auto. @@ -1186,48 +1187,53 @@ Proof. inv H6. left. eapply t_trans; eauto. left; auto. Qed. -Lemma compose_backward_simulation: backward_simulation L1 L3. -Proof. - apply Backward_simulation with (bsim_order := bb_order) (bsim_match_states := bb_match_states). -(* well founded *) - unfold bb_order. apply wf_lex_ord. apply wf_clos_trans. apply bsim_order_wf. apply bsim_order_wf. -(* initial states exist *) - intros. exploit (bsim_initial_states_exist S12); eauto. intros [s2 A]. - eapply (bsim_initial_states_exist S23); eauto. -(* match initial states *) +End COMPOSE_BACKWARD_SIMULATIONS. + +Lemma compose_backward_simulation: + forall L1 L2 L3, + single_events L3 -> backward_simulation L1 L2 -> backward_simulation L2 L3 -> + backward_simulation L1 L3. +Proof. + intros L1 L2 L3 L3single S12 S23. + destruct S12 as [index order match_states props]. + destruct S23 as [index' order' match_states' props']. + apply Backward_simulation with (bb_order order order') (bb_match_states L1 L2 L3 match_states match_states'); + constructor. +- (* well founded *) + unfold bb_order. apply wf_lex_ord. apply wf_clos_trans. eapply bsim_order_wf; eauto. eapply bsim_order_wf; eauto. +- (* initial states exist *) + intros. exploit (bsim_initial_states_exist props); eauto. intros [s2 A]. + eapply (bsim_initial_states_exist props'); eauto. +- (* match initial states *) intros s1 s3 INIT1 INIT3. - exploit (bsim_initial_states_exist S12); eauto. intros [s2 INIT2]. - exploit (bsim_match_initial_states S23); eauto. intros [i2 [s2' [INIT2' M2]]]. - exploit (bsim_match_initial_states S12); eauto. intros [i1 [s1' [INIT1' M1]]]. - exists (i1, i2); exists s1'; intuition. eapply bb_match_at; eauto. -(* match final states *) + exploit (bsim_initial_states_exist props); eauto. intros [s2 INIT2]. + exploit (bsim_match_initial_states props'); eauto. intros [i2 [s2' [INIT2' M2]]]. + exploit (bsim_match_initial_states props); eauto. intros [i1 [s1' [INIT1' M1]]]. + exists (i1, i2); exists s1'; intuition auto. eapply bb_match_at; eauto. +- (* match final states *) intros i s1 s3 r MS SAFE FIN. inv MS. - exploit (bsim_match_final_states S23); eauto. + exploit (bsim_match_final_states props'); eauto. eapply star_safe; eauto. eapply bsim_safe; eauto. intros [s2' [A B]]. - exploit bsim_E0_star. eapply star_trans. eexact H0. eexact A. auto. eauto. auto. + exploit (bsim_E0_star props). eapply star_trans. eexact H0. eexact A. auto. eauto. auto. intros [i1' [s1' [C D]]]. - exploit (bsim_match_final_states S12); eauto. eapply star_safe; eauto. + exploit (bsim_match_final_states props); eauto. eapply star_safe; eauto. intros [s1'' [P Q]]. exists s1''; split; auto. eapply star_trans; eauto. -(* progress *) +- (* progress *) intros i s1 s3 MS SAFE. inv MS. - eapply (bsim_progress S23). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto. -(* simulation *) - exact bb_simulation. -(* symbols *) - intros. transitivity (Senv.public_symbol (symbolenv L2) id); apply bsim_public_preserved; auto. + eapply (bsim_progress props'). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto. +- (* simulation *) + apply bb_simulation; auto. +- (* symbols *) + intros. transitivity (Senv.public_symbol (symbolenv L2) id); eapply bsim_public_preserved; eauto. Qed. -End COMPOSE_BACKWARD_SIMULATIONS. - (** ** Converting a forward simulation to a backward simulation *) Section FORWARD_TO_BACKWARD. -Variable L1: semantics. -Variable L2: semantics. -Variable FS: forward_simulation L1 L2. +Context L1 L2 index order match_states (FS: fsim_properties L1 L2 index order match_states). Hypothesis L1_receptive: receptive L1. Hypothesis L2_determinate: determinate L2. @@ -1243,38 +1249,38 @@ Inductive f2b_transitions: state L1 -> state L2 -> Prop := Star L1 s1 E0 s1' -> Step L1 s1' t s1'' -> Plus L2 s2 t s2' -> - FS i' s1' s2 -> - FS i'' s1'' s2' -> + match_states i' s1' s2 -> + match_states i'' s1'' s2' -> f2b_transitions s1 s2. Lemma f2b_progress: - forall i s1 s2, FS i s1 s2 -> safe L1 s1 -> f2b_transitions s1 s2. + forall i s1 s2, match_states i s1 s2 -> safe L1 s1 -> f2b_transitions s1 s2. Proof. - intros i0; pattern i0. apply well_founded_ind with (R := fsim_order FS). - apply fsim_order_wf. + intros i0; pattern i0. apply well_founded_ind with (R := order). + eapply fsim_order_wf; eauto. intros i REC s1 s2 MATCH SAFE. destruct (SAFE s1) as [[r FINAL] | [t [s1' STEP1]]]. apply star_refl. - (* final state reached *) +- (* final state reached *) eapply f2b_trans_final; eauto. apply star_refl. eapply fsim_match_final_states; eauto. - (* L1 can make one step *) +- (* L1 can make one step *) exploit (fsim_simulation FS); eauto. intros [i' [s2' [A MATCH']]]. - assert (B: Plus L2 s2 t s2' \/ (s2' = s2 /\ t = E0 /\ fsim_order FS i' i)). - intuition. - destruct (star_inv H0); intuition. + assert (B: Plus L2 s2 t s2' \/ (s2' = s2 /\ t = E0 /\ order i' i)). + intuition auto. + destruct (star_inv H0); intuition auto. clear A. destruct B as [PLUS2 | [EQ1 [EQ2 ORDER]]]. - eapply f2b_trans_step; eauto. apply star_refl. - subst. exploit REC; eauto. eapply star_safe; eauto. apply star_one; auto. ++ eapply f2b_trans_step; eauto. apply star_refl. ++ subst. exploit REC; eauto. eapply star_safe; eauto. apply star_one; auto. intros TRANS; inv TRANS. - eapply f2b_trans_final; eauto. eapply star_left; eauto. - eapply f2b_trans_step; eauto. eapply star_left; eauto. +* eapply f2b_trans_final; eauto. eapply star_left; eauto. +* eapply f2b_trans_step; eauto. eapply star_left; eauto. Qed. Lemma fsim_simulation_not_E0: forall s1 t s1', Step L1 s1 t s1' -> t <> E0 -> - forall i s2, FS i s1 s2 -> - exists i', exists s2', Plus L2 s2 t s2' /\ FS i' s1' s2'. + forall i s2, match_states i s1 s2 -> + exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2'. Proof. intros. exploit (fsim_simulation FS); eauto. intros [i' [s2' [A B]]]. exists i'; exists s2'; split; auto. @@ -1363,23 +1369,23 @@ Qed. Inductive f2b_match_states: f2b_index -> state L1 -> state L2 -> Prop := | f2b_match_at: forall i s1 s2, - FS i s1 s2 -> + match_states i s1 s2 -> f2b_match_states (F2BI_after O) s1 s2 | f2b_match_before: forall s1 t s1' s2b s2 n s2a i, Step L1 s1 t s1' -> t <> E0 -> Star L2 s2b E0 s2 -> starN (step L2) (globalenv L2) n s2 t s2a -> - FS i s1 s2b -> + match_states i s1 s2b -> f2b_match_states (F2BI_before n) s1 s2 | f2b_match_after: forall n s2 s2a s1 i, starN (step L2) (globalenv L2) (S n) s2 E0 s2a -> - FS i s1 s2a -> + match_states i s1 s2a -> f2b_match_states (F2BI_after (S n)) s1 s2. Remark f2b_match_after': forall n s2 s2a s1 i, starN (step L2) (globalenv L2) n s2 E0 s2a -> - FS i s1 s2a -> + match_states i s1 s2a -> f2b_match_states (F2BI_after n) s1 s2. Proof. intros. inv H. @@ -1398,15 +1404,15 @@ Lemma f2b_simulation_step: Proof. intros s2 t s2' STEP2 i s1 MATCH SAFE. inv MATCH. -(* 1. At matching states *) +- (* 1. At matching states *) exploit f2b_progress; eauto. intros TRANS; inv TRANS. - (* 1.1 L1 can reach final state and L2 is at final state: impossible! *) ++ (* 1.1 L1 can reach final state and L2 is at final state: impossible! *) exploit (sd_final_nostep L2_determinate); eauto. contradiction. - (* 1.2 L1 can make 0 or several steps; L2 can make 1 or several matching steps. *) ++ (* 1.2 L1 can make 0 or several steps; L2 can make 1 or several matching steps. *) inv H2. exploit f2b_determinacy_inv. eexact H5. eexact STEP2. intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]]. - (* 1.2.1 L2 makes a silent transition *) +* (* 1.2.1 L2 makes a silent transition *) destruct (silent_or_not_silent t2). (* 1.2.1.1 L1 makes a silent transition too: perform transition now and go to "after" state *) subst. simpl in *. destruct (star_starN H6) as [n STEPS2]. @@ -1418,7 +1424,7 @@ Proof. exists (F2BI_before n); exists s1'; split. right; split. auto. constructor. econstructor. eauto. auto. apply star_one; eauto. eauto. eauto. - (* 1.2.2 L2 makes a non-silent transition, and so does L1 *) +* (* 1.2.2 L2 makes a non-silent transition, and so does L1 *) exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. congruence. subst t2. rewrite E0_right in H1. @@ -1437,15 +1443,15 @@ Proof. left. eapply plus_right; eauto. eapply f2b_match_after'; eauto. -(* 2. Before *) +- (* 2. Before *) inv H2. congruence. exploit f2b_determinacy_inv. eexact H4. eexact STEP2. intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]]. - (* 2.1 L2 makes a silent transition: remain in "before" state *) ++ (* 2.1 L2 makes a silent transition: remain in "before" state *) subst. simpl in *. exists (F2BI_before n0); exists s1; split. right; split. apply star_refl. constructor. omega. econstructor; eauto. eapply star_right; eauto. - (* 2.2 L2 make a non-silent transition *) ++ (* 2.2 L2 make a non-silent transition *) exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. congruence. subst. rewrite E0_right in *. @@ -1466,7 +1472,7 @@ Proof. left. apply plus_one; auto. eapply f2b_match_after'; eauto. -(* 3. After *) +- (* 3. After *) inv H. exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst. exploit f2b_determinacy_inv. eexact H2. eexact STEP2. intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]]. @@ -1476,20 +1482,28 @@ Proof. congruence. Qed. +End FORWARD_TO_BACKWARD. + (** The backward simulation *) -Lemma forward_to_backward_simulation: backward_simulation L1 L2. +Lemma forward_to_backward_simulation: + forall L1 L2, + forward_simulation L1 L2 -> receptive L1 -> determinate L2 -> + backward_simulation L1 L2. Proof. - apply Backward_simulation with (bsim_order := f2b_order) (bsim_match_states := f2b_match_states). + intros L1 L2 FS L1_receptive L2_determinate. + destruct FS as [index order match_states FS]. + apply Backward_simulation with f2b_order (f2b_match_states L1 L2 match_states); constructor. +- (* well founded *) apply wf_f2b_order. -(* initial states exist *) +- (* initial states exist *) intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2 [A B]]]. exists s2; auto. -(* initial states *) +- (* initial states *) intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2' [A B]]]. assert (s2 = s2') by (eapply sd_initial_determ; eauto). subst s2'. exists (F2BI_after O); exists s1; split; auto. econstructor; eauto. -(* final states *) +- (* final states *) intros. inv H. exploit f2b_progress; eauto. intros TRANS; inv TRANS. assert (r0 = r) by (eapply (sd_final_determ L2_determinate); eauto). subst r0. @@ -1497,21 +1511,19 @@ Proof. inv H4. exploit (sd_final_nostep L2_determinate); eauto. contradiction. inv H5. congruence. exploit (sd_final_nostep L2_determinate); eauto. contradiction. inv H2. exploit (sd_final_nostep L2_determinate); eauto. contradiction. -(* progress *) +- (* progress *) intros. inv H. exploit f2b_progress; eauto. intros TRANS; inv TRANS. left; exists r; auto. inv H3. right; econstructor; econstructor; eauto. inv H4. congruence. right; econstructor; econstructor; eauto. inv H1. right; econstructor; econstructor; eauto. -(* simulation *) - exact f2b_simulation_step. -(* symbols preserved *) +- (* simulation *) + eapply f2b_simulation_step; eauto. +- (* symbols preserved *) exact (fsim_public_preserved FS). Qed. -End FORWARD_TO_BACKWARD. - (** * Transforming a semantics into a single-event, equivalent semantics *) Definition well_behaved_traces (L: semantics) : Prop := @@ -1554,15 +1566,15 @@ Section FACTOR_FORWARD_SIMULATION. Variable L1: semantics. Variable L2: semantics. -Variable sim: forward_simulation L1 L2. +Context index order match_states (sim: fsim_properties L1 L2 index order match_states). Hypothesis L2single: single_events L2. -Inductive ffs_match: fsim_index sim -> (trace * state L1) -> state L2 -> Prop := +Inductive ffs_match: index -> (trace * state L1) -> state L2 -> Prop := | ffs_match_at: forall i s1 s2, - sim i s1 s2 -> + match_states i s1 s2 -> ffs_match i (E0, s1) s2 | ffs_match_buffer: forall i ev t s1 s2 s2', - Star L2 s2 (ev :: t) s2' -> sim i s1 s2' -> + Star L2 s2 (ev :: t) s2' -> match_states i s1 s2' -> ffs_match i (ev :: t, s1) s2. Lemma star_non_E0_split': @@ -1585,27 +1597,27 @@ Lemma ffs_simulation: forall s1 t s1', Step (atomic L1) s1 t s1' -> forall i s2, ffs_match i s1 s2 -> exists i', exists s2', - (Plus L2 s2 t s2' \/ (Star L2 s2 t s2') /\ fsim_order sim i' i) + (Plus L2 s2 t s2' \/ (Star L2 s2 t s2') /\ order i' i) /\ ffs_match i' s1' s2'. Proof. induction 1; intros. -(* silent step *) +- (* silent step *) inv H0. exploit (fsim_simulation sim); eauto. intros [i' [s2' [A B]]]. exists i'; exists s2'; split. auto. constructor; auto. -(* start step *) +- (* start step *) inv H0. exploit (fsim_simulation sim); eauto. intros [i' [s2' [A B]]]. destruct t as [ | ev' t]. - (* single event *) ++ (* single event *) exists i'; exists s2'; split. auto. constructor; auto. - (* multiple events *) ++ (* multiple events *) assert (C: Star L2 s2 (ev :: ev' :: t) s2'). intuition. apply plus_star; auto. exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. exists i'; exists s2x; split. auto. econstructor; eauto. -(* continue step *) +- (* continue step *) inv H0. exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. destruct t. @@ -1613,27 +1625,31 @@ Proof. exists i; exists s2x; split. auto. econstructor; eauto. Qed. +End FACTOR_FORWARD_SIMULATION. + Theorem factor_forward_simulation: + forall L1 L2, + forward_simulation L1 L2 -> single_events L2 -> forward_simulation (atomic L1) L2. Proof. - apply Forward_simulation with (fsim_match_states := ffs_match) (fsim_order := fsim_order sim). -(* wf *) - apply fsim_order_wf. -(* initial states *) + intros L1 L2 FS L2single. + destruct FS as [index order match_states sim]. + apply Forward_simulation with order (ffs_match L1 L2 match_states); constructor. +- (* wf *) + eapply fsim_order_wf; eauto. +- (* initial states *) intros. destruct s1 as [t1 s1]. simpl in H. destruct H. subst. exploit (fsim_match_initial_states sim); eauto. intros [i [s2 [A B]]]. exists i; exists s2; split; auto. constructor; auto. -(* final states *) +- (* final states *) intros. destruct s1 as [t1 s1]. simpl in H0; destruct H0; subst. inv H. eapply (fsim_match_final_states sim); eauto. -(* simulation *) - exact ffs_simulation. -(* symbols preserved *) +- (* simulation *) + eapply ffs_simulation; eauto. +- (* symbols preserved *) simpl. exact (fsim_public_preserved sim). Qed. -End FACTOR_FORWARD_SIMULATION. - (** Likewise, a backward simulation from a single-event semantics [L1] to a semantics [L2] can be "factored" as a backward simulation from [L1] to [atomic L2]. *) @@ -1641,13 +1657,13 @@ Section FACTOR_BACKWARD_SIMULATION. Variable L1: semantics. Variable L2: semantics. -Variable sim: backward_simulation L1 L2. +Context index order match_states (sim: bsim_properties L1 L2 index order match_states). Hypothesis L1single: single_events L1. Hypothesis L2wb: well_behaved_traces L2. -Inductive fbs_match: bsim_index sim -> state L1 -> (trace * state L2) -> Prop := +Inductive fbs_match: index -> state L1 -> (trace * state L2) -> Prop := | fbs_match_intro: forall i s1 t s2 s1', - Star L1 s1 t s1' -> sim i s1' s2 -> + Star L1 s1 t s1' -> match_states i s1' s2 -> t = E0 \/ output_trace t -> fbs_match i s1 (t, s2). @@ -1655,18 +1671,18 @@ Lemma fbs_simulation: forall s2 t s2', Step (atomic L2) s2 t s2' -> forall i s1, fbs_match i s1 s2 -> safe L1 s1 -> exists i', exists s1', - (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order sim i' i)) + (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ order i' i)) /\ fbs_match i' s1' s2'. Proof. induction 1; intros. -(* silent step *) +- (* silent step *) inv H0. exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. intros [i' [s1'' [A B]]]. exists i'; exists s1''; split. destruct A as [P | [P Q]]. left. eapply star_plus_trans; eauto. right; split; auto. eapply star_trans; eauto. econstructor. apply star_refl. auto. auto. -(* start step *) +- (* start step *) inv H0. exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. intros [i' [s1'' [A B]]]. @@ -1677,7 +1693,7 @@ Proof. left; auto. econstructor; eauto. exploit L2wb; eauto. -(* continue step *) +- (* continue step *) inv H0. unfold E0 in H8; destruct H8; try congruence. exploit star_non_E0_split'; eauto. simpl. intros [s1x [P Q]]. exists i; exists s1x; split. left; auto. econstructor; eauto. simpl in H0; tauto. @@ -1690,47 +1706,51 @@ Lemma fbs_progress: (exists t, exists s2', Step (atomic L2) s2 t s2'). Proof. intros. inv H. destruct t. -(* 1. no buffered events *) +- (* 1. no buffered events *) exploit (bsim_progress sim); eauto. eapply star_safe; eauto. intros [[r A] | [t [s2' A]]]. -(* final state *) ++ (* final state *) left; exists r; simpl; auto. -(* L2 can step *) ++ (* L2 can step *) destruct t. right; exists E0; exists (nil, s2'). constructor. auto. right; exists (e :: nil); exists (t, s2'). constructor. auto. -(* 2. some buffered events *) +- (* 2. some buffered events *) unfold E0 in H3; destruct H3. congruence. right; exists (e :: nil); exists (t, s3). constructor. auto. Qed. +End FACTOR_BACKWARD_SIMULATION. + Theorem factor_backward_simulation: + forall L1 L2, + backward_simulation L1 L2 -> single_events L1 -> well_behaved_traces L2 -> backward_simulation L1 (atomic L2). Proof. - apply Backward_simulation with (bsim_match_states := fbs_match) (bsim_order := bsim_order sim). -(* wf *) - apply bsim_order_wf. -(* initial states exist *) + intros L1 L2 BS L1single L2wb. + destruct BS as [index order match_states sim]. + apply Backward_simulation with order (fbs_match L1 L2 match_states); constructor. +- (* wf *) + eapply bsim_order_wf; eauto. +- (* initial states exist *) intros. exploit (bsim_initial_states_exist sim); eauto. intros [s2 A]. exists (E0, s2). simpl; auto. -(* initial states match *) +- (* initial states match *) intros. destruct s2 as [t s2]; simpl in H0; destruct H0; subst. exploit (bsim_match_initial_states sim); eauto. intros [i [s1' [A B]]]. exists i; exists s1'; split. auto. econstructor. apply star_refl. auto. auto. -(* final states match *) +- (* final states match *) intros. destruct s2 as [t s2]; simpl in H1; destruct H1; subst. inv H. exploit (bsim_match_final_states sim); eauto. eapply star_safe; eauto. intros [s1'' [A B]]. exists s1''; split; auto. eapply star_trans; eauto. -(* progress *) - exact fbs_progress. -(* simulation *) - exact fbs_simulation. -(* symbols *) +- (* progress *) + eapply fbs_progress; eauto. +- (* simulation *) + eapply fbs_simulation; eauto. +- (* symbols *) simpl. exact (bsim_public_preserved sim). Qed. -End FACTOR_BACKWARD_SIMULATION. - (** Receptiveness of [atomic L]. *) Record strongly_receptive (L: semantics) : Prop := |