From e4723d142aa7b1229cdf5989340342d7c5ce870c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:31:26 +0100 Subject: Update the back-end proofs to the new linking framework. --- backend/Inliningspec.v | 122 ++++++++++++++++++++++++++----------------------- 1 file changed, 66 insertions(+), 56 deletions(-) (limited to 'backend/Inliningspec.v') diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index ba62313f..23770cb7 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -12,64 +12,60 @@ (** RTL function inlining: relational specification *) -Require Import Coqlib. -Require Import Wfsimpl. -Require Import Errors. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Globalenvs. -Require Import Op. -Require Import Registers. -Require Import RTL. +Require Import Coqlib Wfsimpl Maps Errors Integers. +Require Import AST Linking. +Require Import Op Registers RTL. Require Import Inlining. (** ** Soundness of function environments. *) -(** A (compile-time) function environment is compatible with a - (run-time) global environment if the following condition holds. *) +(** A compile-time function environment is compatible with a whole + program if the following condition holds. *) -Definition fenv_compat (ge: genv) (fenv: funenv) : Prop := - forall id b f, - fenv!id = Some f -> Genv.find_symbol ge id = Some b -> - Genv.find_funct_ptr ge b = Some (Internal f). +Definition fenv_compat (p: program) (fenv: funenv) : Prop := + forall id f, + fenv!id = Some f -> (prog_defmap p)!id = Some (Gfun (Internal f)). -Remark add_globdef_compat: - forall ge fenv idg, - fenv_compat ge fenv -> - fenv_compat (Genv.add_global ge idg) (Inlining.add_globdef fenv idg). +Lemma funenv_program_compat: + forall p, fenv_compat p (funenv_program p). Proof. - intros. destruct idg as [id gd]. red; simpl; intros. - unfold Genv.find_symbol in H1; simpl in H1. - unfold Genv.find_funct_ptr; simpl. - rewrite PTree.gsspec in H1. destruct (peq id0 id). - (* same *) - subst id0. inv H1. destruct gd. destruct f0. - destruct (should_inline id f0). - rewrite PTree.gss in H0. rewrite PTree.gss. inv H0; auto. - rewrite PTree.grs in H0; discriminate. - rewrite PTree.grs in H0; discriminate. - rewrite PTree.grs in H0; discriminate. - (* different *) - destruct gd. rewrite PTree.gso. eapply H; eauto. - destruct f0. destruct (should_inline id f0). - rewrite PTree.gso in H0; auto. - rewrite PTree.gro in H0; auto. - rewrite PTree.gro in H0; auto. - red; intros; subst b. eelim Plt_strict. eapply Genv.genv_symb_range; eauto. - rewrite PTree.gro in H0; auto. eapply H; eauto. + set (P := fun (dm: PTree.t (globdef fundef unit)) (fenv: funenv) => + forall id f, + fenv!id = Some f -> dm!id = Some (Gfun (Internal f))). + assert (REMOVE: forall dm fenv id g, + P dm fenv -> + P (PTree.set id g dm) (PTree.remove id fenv)). + { unfold P; intros. rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id). + discriminate. + rewrite PTree.gso; auto. + } + assert (ADD: forall dm fenv idg, + P dm fenv -> + P (PTree.set (fst idg) (snd idg) dm) (add_globdef fenv idg)). + { intros dm fenv [id g]; simpl; intros. + destruct g as [ [f|ef] | v]; auto. + destruct (should_inline id f); auto. + red; intros. rewrite ! PTree.gsspec in *. + destruct (peq id0 id); auto. inv H0; auto. + } + assert (REC: forall l dm fenv, + P dm fenv -> + P (fold_left (fun x idg => PTree.set (fst idg) (snd idg) x) l dm) + (fold_left add_globdef l fenv)). + { induction l; simpl; intros. + - auto. + - apply IHl. apply ADD; auto. + } + intros. apply REC. red; intros. rewrite PTree.gempty in H; discriminate. Qed. -Lemma funenv_program_compat: - forall p, fenv_compat (Genv.globalenv p) (funenv_program p). +Lemma fenv_compat_linkorder: + forall cunit prog fenv, + linkorder cunit prog -> fenv_compat cunit fenv -> fenv_compat prog fenv. Proof. - intros. - unfold Genv.globalenv, funenv_program. - assert (forall gl ge fenv, - fenv_compat ge fenv -> - fenv_compat (Genv.add_globals ge gl) (fold_left add_globdef gl fenv)). - induction gl; simpl; intros. auto. apply IHgl. apply add_globdef_compat; auto. - apply H. red; intros. rewrite PTree.gempty in H0; discriminate. + intros; red; intros. apply H0 in H1. + destruct (prog_defmap_linkorder _ _ _ _ H H1) as (gd' & P & Q). + inv Q. inv H3. auto. Qed. (** ** Properties of shifting *) @@ -684,29 +680,45 @@ Qed. End INLINING_BODY_SPEC. +End INLINING_SPEC. + (** ** Relational specification of the translation of a function *) -Inductive tr_function: function -> function -> Prop := - | tr_function_intro: forall f f' ctx, - tr_funbody f'.(fn_stacksize) ctx f f'.(fn_code) -> +Inductive tr_function: program -> function -> function -> Prop := + | tr_function_intro: forall p fenv f f' ctx, + fenv_compat p fenv -> + tr_funbody fenv f'.(fn_stacksize) ctx f f'.(fn_code) -> ctx.(dstk) = 0 -> ctx.(retinfo) = None -> f'.(fn_sig) = f.(fn_sig) -> f'.(fn_params) = sregs ctx f.(fn_params) -> f'.(fn_entrypoint) = spc ctx f.(fn_entrypoint) -> 0 <= fn_stacksize f' < Int.max_unsigned -> - tr_function f f'. + tr_function p f f'. + +Lemma tr_function_linkorder: + forall cunit prog f f', + linkorder cunit prog -> + tr_function cunit f f' -> + tr_function prog f f'. +Proof. + intros. inv H0. econstructor; eauto. eapply fenv_compat_linkorder; eauto. +Qed. Lemma transf_function_spec: - forall f f', transf_function fenv f = OK f' -> tr_function f f'. + forall cunit f f', + transf_function (funenv_program cunit) f = OK f' -> + tr_function cunit f f'. Proof. intros. unfold transf_function in H. + set (fenv := funenv_program cunit) in *. destruct (expand_function fenv f initstate) as [ctx s i] eqn:?. destruct (zlt (st_stksize s) Int.max_unsigned); inv H. monadInv Heqr. set (ctx := initcontext x x0 (max_reg_function f) (fn_stacksize f)) in *. Opaque initstate. destruct INCR3. inversion EQ1. inversion EQ. - apply tr_function_intro with ctx; auto. + apply tr_function_intro with fenv ctx; auto. + apply funenv_program_compat. eapply expand_cfg_spec with (fe := fenv); eauto. red; auto. unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega. @@ -718,5 +730,3 @@ Opaque initstate. simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR. simpl. change 0 with (st_stksize initstate). omega. Qed. - -End INLINING_SPEC. -- cgit