diff options
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | mppa_k1c/lib/RTLpathSE_theory.v | 60 | ||||
| -rw-r--r-- | mppa_k1c/lib/RTLpathScheduler.v | 390 |
3 files changed, 353 insertions, 99 deletions
@@ -849,7 +849,7 @@ ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure EXECUTE=k1-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __K1C_COS__ SIMU=k1-cluster -- -BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v RTLpath.v\\ +BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v RTLpath.v RTLpathSE_theory.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v index cc2d2fde..b7674916 100644 --- a/mppa_k1c/lib/RTLpathSE_theory.v +++ b/mppa_k1c/lib/RTLpathSE_theory.v @@ -841,31 +841,31 @@ Qed. *) -Inductive smatch_state: state -> state -> Prop := - | smatch_state_refl s: smatch_state s s - | State_smatch stack f sp pc rs1 m rs2: +Inductive equiv_state: state -> state -> Prop := + | equiv_state_refl s: equiv_state s s + | State_equiv stack f sp pc rs1 m rs2: (forall r, rs1#r = rs2#r) -> - smatch_state (State stack f sp pc rs1 m) + equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m) - | Callstate_smatch stack res f sp pc rs1 m rs2 fd args: + | Callstate_equiv stack res f sp pc rs1 m rs2 fd args: (forall r, rs1#r = rs2#r) -> - smatch_state (Callstate (Stackframe res f sp pc rs1 :: stack) fd args m) - (Callstate (Stackframe res f sp pc rs2 :: stack) fd args m). + equiv_state (Callstate (Stackframe res f sp pc rs1 :: stack) fd args m) + (Callstate (Stackframe res f sp pc rs2 :: stack) fd args m). -Lemma sfval_sem_smatch sge (f:function) st sv stack rs0 m0 t rs1 rs2 m s: +Lemma sfval_sem_equiv sge (f:function) st sv stack rs0 m0 t rs1 rs2 m s: sfval_sem sge st stack f rs0 m0 sv rs1 m t s -> (forall r, rs1#r = rs2#r) -> - exists s', smatch_state s s' /\ sfval_sem sge st stack f rs0 m0 sv rs2 m t s'. + exists s', equiv_state s s' /\ sfval_sem sge st stack f rs0 m0 sv rs2 m t s'. Proof. destruct 1. - (* Snone *) intros; eexists; econstructor. - + eapply State_smatch; eauto. + + eapply State_equiv; eauto. + eapply exec_Snone. - (* Scall *) intros; eexists; econstructor. - + eapply Callstate_smatch; eauto. + + eapply Callstate_equiv; eauto. + eapply exec_Scall; eauto. - (* Sreturn *) intros; eexists; econstructor. - + eapply smatch_state_refl; eauto. + + eapply equiv_state_refl; eauto. + eapply exec_Sreturn; eauto. Qed. @@ -874,7 +874,7 @@ Theorem symb_step_exact f pc pge ge sp path stack st rs m t s1: symb_step f pc = Some st -> sem_state (Build_sgenv pge ge sp) st stack f rs m t s1 -> exists s2, path_step ge pge path stack f sp rs m pc t s2 /\ - smatch_state s1 s2. + equiv_state s1 s2. Proof. Local Hint Resolve init_sem_istate. unfold symb_step; intros PATH SSTEP SEM; rewrite PATH in SSTEP. @@ -892,7 +892,8 @@ Proof. rewrite Hi in SSTEP. intros ISTEPS. try_simplify_someHyps. destruct (symb_istep i st0) as [st'|] eqn: Hst'; simpl. - + admit. + + (* normal exit on Snone instruction *) + admit. + destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *. - (* early exit *) intros. @@ -900,14 +901,14 @@ Proof. destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4). eexists. econstructor 1. * eapply exec_early_exit; eauto. - * rewrite EQ2, EQ4; eapply State_smatch. auto. - - (* normal exit *) + * rewrite EQ2, EQ4; eapply State_equiv. auto. + - (* normal exit non-Snone instruction *) intros. exploit sem_option_istate_determ; eauto. destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4). unfold sem_istate in SEM1. rewrite CONT in SEM1. destruct SEM1 as (SEM1 & PC0 & NYE0). - exploit sfval_sem_smatch; eauto. + exploit sfval_sem_equiv; eauto. clear SEM2; destruct 1 as (s' & Ms' & SEM2). rewrite ! EQ4 in * |-; clear EQ4. rewrite ! EQ2 in * |-; clear EQ2. @@ -918,5 +919,30 @@ Proof. * unfold sem_local_istate in * |- *. intuition try congruence. Admitted. +(** * Simulation of RTLpath code w.r.t symbolic execution *) +Definition istate_simu (srce: node -> option node) ist1 ist2 := + ist1.(continue) = ist2.(continue) /\ + srce (ist2.(RTLpath.the_pc)) = Some ist1.(RTLpath.the_pc) /\ + (forall r, (ist1.(the_rs)#r) = ist2.(the_rs)#r) /\ + ist1.(the_mem) = ist2.(the_mem). + +Definition s_istate_simu (srce: node -> option node) (st1 st2: s_istate): Prop := + forall sge1 sge2 rs0 m0 is1 is2, istate_simu srce is1 is2 -> sem_istate sge1 st1 rs0 m0 is1 -> sem_istate sge2 st2 rs0 m0 is2. + +Inductive sfval_simu (srce: node -> option node): sfval -> sfval -> Prop := + | Snone_simu: sfval_simu srce Snone Snone + | Scall_simu sig svos lsv res pc1 pc2: + srce pc2 = Some pc1 -> + sfval_simu srce (Scall sig svos lsv res pc1) (Scall sig svos lsv res pc2) + | Sreturn_simu os: + sfval_simu srce (Sreturn os) (Sreturn os). + +Definition s_state_simu (srce: node -> option node) (s1 s2: s_state): Prop := + s_istate_simu srce s1.(internal) s2.(internal) + /\ sfval_simu srce s1.(final) s2.(final). + +Definition path_simu (srce: node -> option node) (f1 f2: RTLpath.function) pc1 pc2: Prop := + forall st1, symb_step f1 pc1 = Some st1 -> exists st2, symb_step f2 pc2 = Some st2 /\ s_state_simu srce st1 st2. +(** See usage of [path_simu] in [RTLpathScheduler] *)
\ No newline at end of file diff --git a/mppa_k1c/lib/RTLpathScheduler.v b/mppa_k1c/lib/RTLpathScheduler.v index 76795fa4..c27d5317 100644 --- a/mppa_k1c/lib/RTLpathScheduler.v +++ b/mppa_k1c/lib/RTLpathScheduler.v @@ -1,11 +1,13 @@ (** RTLpath Scheduling from an external oracle. -This module is inspired from [Duplicate] +This module is inspired from [Duplicate] and [Duplicateproof] *) -Require Import AST Values RTL RTLpath Maps Globalenvs. -Require Import Coqlib Errors Op. +Require Import AST Linking Values Maps Globalenvs Smallstep. +Require Import Coqlib Maps Events Errors Op. +Require Import RTL RTLpath RTLpathSE_theory. + Local Open Scope error_monad_scope. Local Open Scope positive_scope. @@ -25,7 +27,7 @@ Extract Constant untrusted_scheduler => "TODO". *) Record xfunction : Type := - { fn_RTL: RTLpath.function; + { fn_RTL:> RTLpath.function; fn_revmap: PTree.t node; }. @@ -39,109 +41,335 @@ Definition fundef_RTL (fu: xfundef) : fundef := | External ef => External ef end. -(* auxiliary definitions that should be use in [verify_match_path] implementation below ! *) +(* Definition verify_is_copy revmap n n' := match revmap!n' with | None => Error(msg "verify_is_copy None") | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end end. -Fixpoint verify_is_copy_list revmap ln ln' := - match ln with - | n::ln => match ln' with - | n'::ln' => do u <- verify_is_copy revmap n n'; - verify_is_copy_list revmap ln ln' - | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end - | nil => match ln' with - | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") - | nil => OK tt end - end. - Definition verify_mapping_entrypoint (f: function) (xf: xfunction): res unit := verify_is_copy (fn_revmap xf) (fn_entrypoint f) (fn_entrypoint (fn_RTL xf)). +*) +Record match_function (f1: RTLpath.function) (f2: xfunction): Prop := { + preserv_fnsig: fn_sig f1 = fn_sig f2; + preserv_fnparams: fn_params f1 = fn_params f2; + preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2; + preserv_entrypoint: f2.(fn_revmap)!(fn_entrypoint f2) = Some (fn_entrypoint f1); + pathentry_simu: + forall pc1 pc2, f2.(fn_revmap)!pc2 = Some pc1 -> path_entry (fn_code f1) (fn_path f1) pc1 -> path_entry (fn_code f2) (fn_path f2) pc2 /\ path_simu (fun n' => (fn_revmap f2)!n') f1 f2 pc1 pc2 +}. -(* This verifier remains to be implemented by symbolic execution *) -Parameter verify_match_path: function -> xfunction -> node -> node -> bool. +(* TODO: remove these two stub parameters *) +Parameter transf_function_aux: RTLpath.function -> res xfunction. -(* -Lemma product_eq {A B: Type} : - (forall (a b: A), {a=b} + {a<>b}) -> - (forall (c d: B), {c=d} + {c<>d}) -> - forall (x y: A+B), {x=y} + {x<>y}. +Parameter transf_function_correct: forall f xf, transf_function_aux f = OK xf -> match_function f xf. + +Definition transf_function (f: function) : res function := + do xf <- transf_function_aux f; + OK (fn_RTL xf). + +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. + + +(** * Preservation proof *) + + +Inductive match_fundef: RTLpath.fundef -> RTLpath.fundef -> Prop := + | match_Internal f xf: match_function f xf -> match_fundef (Internal f) (Internal (fn_RTL xf)) + | match_External ef: match_fundef (External ef) (External ef). + + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + | match_stackframe_intro: + forall res f sp pc rs xf pc' + (TRANSF: match_function f xf) + (DUPLIC: (fn_revmap xf)!pc' = Some pc), + match_stackframes (Stackframe res f sp pc rs) (Stackframe res (fn_RTL xf) sp pc' rs). + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall st f sp pc rs m st' xf pc' + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function f xf) + (DUPLIC: (fn_revmap xf)!pc' = Some pc), + match_states (State st f sp pc rs m) (State st' (fn_RTL xf) sp pc' rs m) + | match_states_call: + forall st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f'), + match_states (Callstate st f args m) (Callstate st' f' args m) + | match_states_return: + forall st st' v m + (STACKS: list_forall2 match_stackframes st st'), + match_states (Returnstate st v m) (Returnstate st' v m). + + +Lemma transf_fundef_correct f f': + transf_fundef f = OK f' -> match_fundef f f'. Proof. - intros H H'. intros. decide equality. + intros TRANSF; destruct f; simpl; monadInv TRANSF. + + monadInv EQ. + eapply match_Internal; eapply transf_function_correct; eauto. + + eapply match_External. Qed. -(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application" - * error when doing so *) -Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}. +Definition match_prog (p tp: program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. Proof. - intros. - apply (builtin_arg_eq Pos.eq_dec). -Defined. -Global Opaque builtin_arg_eq_pos. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. -Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}. -Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed. -Global Opaque builtin_res_eq_pos. -*) +Section PRESERVATION. -Fixpoint verify_mapping_mn_rec f xf lm := - match lm with - | nil => OK tt - | (pc2,pc1) :: lm => - if verify_match_path f xf pc1 pc2 - then - do u2 <- verify_mapping_mn_rec f xf lm; - OK tt - else - Error (msg "verify_match_path fails") - end. +Variable prog: program. +Variable tprog: program. -Definition verify_mapping_match_paths (f: function) (xf: xfunction) : res unit := - verify_mapping_mn_rec f xf (PTree.elements (fn_revmap xf)). +Hypothesis TRANSL: match_prog prog tprog. -(** Verifies that the [fn_revmap] of the translated function [xf] is giving correct information in regards to [f] *) -Definition verify_mapping (f: function) (xf: xfunction) : res unit := - do u <- verify_mapping_entrypoint f xf; - do v <- verify_mapping_match_paths f xf; OK tt. -(* TODO - verify the other axiom *) +Let pge := Genv.globalenv prog. +Let tpge := Genv.globalenv tprog. +Let ge := Genv.globalenv (program_RTL prog). +Let tge := Genv.globalenv (program_RTL tprog). -(** * Entry points *) +Lemma symbols_preserved_pge s: Genv.find_symbol tpge s = Genv.find_symbol pge s. +Proof. + rewrite <- (Genv.find_symbol_match TRANSL). reflexivity. +Qed. -(* TODO: à finir... +Lemma senv_sym x y: Senv.equiv x y -> Senv.equiv y x. +Proof. + unfold Senv.equiv. intuition congruence. +Qed. -Definition transf_function_aux (f: function) : res xfunction := - let (tcte, mp) := duplicate_aux f in - let (tc, te) := tcte in - let xf := {| fn_RTL := (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te); fn_revmap := mp |} in - do u <- verify_mapping f xf; - OK xf. +Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z. +Proof. + unfold Senv.equiv. intuition congruence. +Qed. -Theorem transf_function_aux_preserves: - forall f xf, - transf_function_aux f = OK xf -> - fn_sig f = fn_sig (fn_RTL xf) /\ fn_params f = fn_params (fn_RTL xf) /\ fn_stacksize f = fn_stacksize (fn_RTL xf). +Lemma senv_preserved_pge: + Senv.equiv pge tpge. Proof. - intros. unfold transf_function_aux in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H. - repeat (split; try reflexivity). + eapply (Genv.senv_match TRANSL). Qed. -Remark transf_function_aux_fnsig: forall f xf, transf_function_aux f = OK xf -> fn_sig f = fn_sig (fn_RTL xf). - Proof. apply transf_function_aux_preserves. Qed. -Remark transf_function_aux_fnparams: forall f xf, transf_function_aux f = OK xf -> fn_params f = fn_params (fn_RTL xf). - Proof. apply transf_function_aux_preserves. Qed. -Remark transf_function_aux_fnstacksize: forall f xf, transf_function_aux f = OK xf -> fn_stacksize f = fn_stacksize (fn_RTL xf). - Proof. apply transf_function_aux_preserves. Qed. +Lemma senv_preserved: + Senv.equiv ge tge. +Proof. + eapply senv_transitivity. { eapply senv_sym; eapply RTLpath.senv_preserved. } + eapply senv_transitivity. { eapply senv_preserved_pge. } + eapply RTLpath.senv_preserved. +Qed. -Definition transf_function (f: function) : res function := - do xf <- transf_function_aux f; - OK (fn_RTL xf). -Definition transf_fundef (f: fundef) : res fundef := - transf_partial_fundef transf_function f. +Lemma functions_translated: + forall (v: val) (f: fundef), + Genv.find_funct pge v = Some f -> + exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tpge v = Some tf /\ linkorder cunit prog. +Proof. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & A & B & C). + repeat eexists; intuition eauto. + + unfold incl; auto. + + eapply linkorder_refl. +Qed. -Definition transf_program (p: program) : res program := - transform_partial_program transf_fundef p. -*)
\ No newline at end of file +Lemma function_ptr_translated_pge: + forall v f, + Genv.find_funct_ptr pge v = Some f -> + exists tf, + Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf. +Proof. + intros. + exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto. +Qed. + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + exists f0 tf, + Genv.find_funct_ptr pge v = Some f0 /\ Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f0 = OK tf. +Proof. + intros; exploit find_funct_ptr_RTL_preserv; eauto. + intros (f0 & X & Y); subst. + exploit function_ptr_translated_pge; eauto. + intros (tf & Y & Z); eauto. +Qed. + +Lemma function_sig_translated: + forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f. +Proof. + intros. destruct f. + - simpl in H. monadInv H. simpl. symmetry. monadInv EQ. + eapply preserv_fnsig. + eapply transf_function_correct. + assumption. + - simpl in H. monadInv H. (* monadInv EQ. *) reflexivity. +Qed. + +Theorem transf_initial_states: + forall s1, initial_state prog s1 -> + exists s2, initial_state tprog s2 /\ match_states s1 s2. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros (f0 & tf & FIND1 & FIND2 & TRANSF). + exists (RTL.Callstate nil (fn_RTL tf nil m0) nil m0). + eexists. split. + 2: { eapply match_states_call. eauto. + - unfold initial_state. econstructor. + + eapply (Genv.init_mem_transf_partial TRANSL); eauto. + + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main. eauto. + + exploit function_ptr_translated; eauto. + + destruct f. + * monadInv TRANSF. monadInv EQ. rewrite <- H3. symmetry; eapply transf_function_aux_preserves. assumption. + * monadInv TRANSF. (* monadInv EQ. *) assumption. + - constructor; eauto. constructor. apply transf_fundef_correct; auto. +Qed. + +(* TODO +Theorem transf_final_states: + forall s1 s2 r, + match_states s1 s2 -> final_state s1 r -> final_state s2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem step_simulation: + forall s1 t s1', step pge s1 t s1' -> + forall s2 (MS: match_states s1 s2), + exists s2', + step tge s2 t s2' + /\ match_states s1' s2'. +Proof. + Local Hint Resolve transf_fundef_correct. + induction 1; intros; inv MS. +(* Inop *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). + inv H3. + eexists. split. + + eapply exec_Inop; eauto. + + constructor; eauto. +(* Iop *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Iop; eauto. erewrite eval_operation_preserved; eauto. + + constructor; eauto. +(* Iload *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto. + + constructor; auto. +(* Istore *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto. + + constructor; auto. +(* Icall *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + destruct ros. + * simpl in H0. apply functions_translated in H0. + destruct H0 as (tf & cunit & TFUN & GFIND & LO). + eexists. split. + + eapply exec_Icall. eassumption. simpl. eassumption. + apply function_sig_translated. assumption. + + repeat (constructor; auto). + * simpl in H0. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. + apply function_ptr_translated in H0. destruct H0 as (tf & GFF & TF). + eexists. split. + + eapply exec_Icall. eassumption. simpl. rewrite symbols_preserved. rewrite GFS. + eassumption. apply function_sig_translated. assumption. + + repeat (constructor; auto). +(* Itailcall *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H10 & H11). inv H11. + pose symbols_preserved as SYMPRES. + destruct ros. + * simpl in H0. apply functions_translated in H0. + destruct H0 as (tf & cunit & TFUN & GFIND & LO). + eexists. split. + + eapply exec_Itailcall. eassumption. simpl. eassumption. + apply function_sig_translated. assumption. + erewrite <- preserv_fnstacksize; eauto. + + repeat (constructor; auto). + * simpl in H0. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. + apply function_ptr_translated in H0. destruct H0 as (tf & GFF & TF). + eexists. split. + + eapply exec_Itailcall. eassumption. simpl. rewrite symbols_preserved. rewrite GFS. + eassumption. apply function_sig_translated. assumption. + erewrite <- preserv_fnstacksize; eauto. + + repeat (constructor; auto). +(* Ibuiltin *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + + constructor; auto. +(* Icond *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Icond; eauto. + + constructor; auto. destruct b; auto. +(* Ijumptable *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + exploit list_nth_z_revmap; eauto. intros (pc'1 & LNZ & REVM). + eexists. split. + + eapply exec_Ijumptable; eauto. + + constructor; auto. +(* Ireturn *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Ireturn; eauto. erewrite <- preserv_fnstacksize; eauto. + + constructor; auto. +(* exec_function_internal *) + - inversion TRANSF as [f0 xf MATCHF|]; subst. eexists. split. + + eapply exec_function_internal. erewrite <- preserv_fnstacksize; eauto. + + erewrite preserv_fnparams; eauto. + econstructor; eauto. apply revmap_entrypoint. assumption. +(* exec_function_external *) + - inversion TRANSF as [|]; subst. eexists. split. + + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor. assumption. +(* exec_return *) + - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split. + + constructor. + + inv H1. constructor; assumption. +Qed. + +Theorem transf_program_correct: + forward_simulation (semantics prog) (semantics tprog). +Proof. + eapply forward_simulation_step with match_states. + - eapply senv_preserved. + - eapply transf_initial_states. + - eapply transf_final_states. + - eapply step_simulation. +Qed. +*) + +End PRESERVATION. |