diff options
Diffstat (limited to 'backend/RTLTunnelingproof.v')
| -rw-r--r-- | backend/RTLTunnelingproof.v | 613 |
1 files changed, 613 insertions, 0 deletions
diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v new file mode 100644 index 00000000..aa21fc06 --- /dev/null +++ b/backend/RTLTunnelingproof.v @@ -0,0 +1,613 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Pierre Goutagny ENS-Lyon, VERIMAG *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness proof for the branch tunneling optimization for RTL. *) +(* This is a port of Tunnelingproof.v, the same optimisation for LTL. *) + +Require Import Coqlib Maps Errors. +Require Import AST Linking. +Require Import Values Memory Registers Events Globalenvs Smallstep. +Require Import Op Locations RTL. +Require Import RTLTunneling. +Require Import Conventions1. + +Local Open Scope nat. + +Definition check_included_spec (c:code) (td:UF) (ok: option instruction) := + ok <> None -> forall pc, c!pc = None -> td!pc = None. + +Lemma check_included_correct (td:UF) (c:code): + check_included_spec c td (check_included td c). +Proof. + apply PTree_Properties.fold_rec with (P:=check_included_spec c); unfold check_included_spec. + - intros m m' oi EQ IND N pc. rewrite <- EQ. apply IND. apply N. + - intros N pc. rewrite PTree.gempty. auto. + - intros m oi pc v N S IND. destruct oi. + + intros. rewrite PTree.gsspec. destruct (peq _ _); try congruence. apply IND. congruence. apply H0. + + contradiction. +Qed. + +Inductive target_bounds (target: node -> node) (bound: node -> nat) (pc: node) : option instruction -> Prop := + | TB_default (TB: target pc = pc) oi: + target_bounds target bound pc oi + | TB_nop s + (EQ: target pc = target s) + (DEC: bound s < bound pc): + target_bounds target bound pc (Some (Inop s)) + | TB_cond cond args ifso ifnot info + (EQSO: target pc = target ifso) + (EQNOT: target pc = target ifnot) + (DECSO: bound ifso < bound pc) + (DECNOT: bound ifnot < bound pc): + target_bounds target bound pc (Some (Icond cond args ifso ifnot info)) +. +Local Hint Resolve TB_default: core. + +Lemma target_None (td: UF) (pc: node): td!pc = None -> td pc = pc. +Proof. + unfold target, get. intro EQ. rewrite EQ. auto. +Qed. +Local Hint Resolve target_None Z.abs_nonneg: core. + +Lemma get_nonneg td pc t d: get td pc = (t,d) -> (0 <= d)%Z. +Proof. + unfold get. destruct td!pc as [(tpc,dpc)|]; intro H; inv H; lia. +Qed. +Local Hint Resolve get_nonneg: core. + +Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)). + + +(* TODO: à réécrire proprement *) +Lemma check_instr_correct (td: UF) (pc: node) (i: instruction): + check_instr td pc i = OK tt -> + target_bounds (target td) (bound td) pc (Some i). +Proof. + unfold check_instr. destruct (td!pc) as [(tpc,dpc)|] eqn:EQ. + assert (DPC: snd (get td pc) = Z.abs dpc). { unfold get. rewrite EQ. auto. } + - destruct i; try congruence. + + destruct (get td n) as (ts,ds) eqn:EQs. + destruct (peq _ _); try congruence. + destruct (zlt _ _); try congruence. intros _. + apply TB_nop. replace (td pc) with tpc. + unfold target. rewrite EQs. auto. + unfold target. unfold get. rewrite EQ. auto. + unfold bound. rewrite DPC. rewrite EQs; simpl. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n ts. apply EQs. + + destruct (get td n) as (tso,dso) eqn:EQSO. + destruct (get td n0) as (tnot,dnot) eqn:EQNOT. + intro H. + repeat ((destruct (peq _ _) in H || destruct (zlt _ _) in H); try congruence). + apply TB_cond; subst. + * unfold target. replace (fst (get td pc)) with tnot. rewrite EQSO. auto. + unfold get. rewrite EQ. auto. + * unfold target. replace (fst (get td pc)) with tnot. rewrite EQNOT. auto. + unfold get. rewrite EQ. auto. + * unfold bound. rewrite DPC. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n tnot. rewrite EQSO. auto. rewrite EQSO. auto. + * unfold bound. rewrite DPC. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n0 tnot. rewrite EQNOT; auto. rewrite EQNOT; auto. + - intros _. apply TB_default. unfold target. unfold get. rewrite EQ. auto. +Qed. + +Definition check_code_spec (td:UF) (c:code) (ok: res unit) := + ok = OK tt -> forall pc i, c!pc = Some i -> target_bounds (target td) (bound td) pc (Some i). + +Lemma check_code_correct (td:UF) c: + check_code_spec td c (check_code td c). +Proof. + unfold check_code. apply PTree_Properties.fold_rec; unfold check_code_spec. + - intros. rewrite <- H in H2. apply H0; auto. + - intros. rewrite PTree.gempty in H0. congruence. + - intros m [[]|e] pc i N S IND; simpl; try congruence. + intros H pc0 i0. rewrite PTree.gsspec. destruct (peq _ _). + subst. intro. inv H0. apply check_instr_correct. apply H. + auto. +Qed. + +Theorem branch_target_bounds: + forall f tf pc, + tunnel_function f = OK tf -> + target_bounds (branch_target f) (bound (branch_target f)) pc (f.(fn_code)!pc). +Proof. + intros. unfold tunnel_function in H. + destruct (check_included _ _) eqn:EQinc; try congruence. + monadInv H. rename EQ into EQcode. + destruct (_ ! _) eqn:EQ. + - exploit check_code_correct. destruct x. apply EQcode. apply EQ. auto. + - exploit check_included_correct. + rewrite EQinc. congruence. + apply EQ. + intro. apply TB_default. apply target_None. apply H. +Qed. + +(** Preservation of semantics *) + +Definition match_prog (p tp: program) := + match_program (fun _ f tf => tunnel_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. eapply match_transform_partial_program_contextual; eauto. +Qed. + + +Section PRESERVATION. + + +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma functions_translated: + forall (v: val) (f: fundef), + Genv.find_funct ge v = Some f -> + exists tf, tunnel_fundef f = OK tf /\ Genv.find_funct tge v = Some tf. +Proof. + intros. + exploit (Genv.find_funct_match TRANSL). apply H. + intros (cu & tf & A & B & C). + eexists. eauto. +Qed. + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + exists tf, + Genv.find_funct_ptr tge v = Some tf /\ tunnel_fundef f = OK tf. +Proof. + intros. exploit (Genv.find_funct_ptr_match TRANSL). + - apply H. + - intros (cu & tf & A & B & C). exists tf. split. apply A. apply B. +Qed. + +Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + apply (Genv.find_symbol_match TRANSL). +Qed. + +Lemma sig_preserved: + forall f tf, tunnel_fundef f = OK tf -> funsig tf = funsig f. +Proof. + intros. destruct f; simpl in H. + - monadInv H. + unfold tunnel_function in EQ. + destruct (check_included _ _) in EQ; try congruence. + monadInv EQ. auto. + - monadInv H. auto. +Qed. + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof. + eapply (Genv.senv_match TRANSL). (* Il y a déjà une preuve de cette propriété très exactement, je ne vais pas réinventer la roue ici *) +Qed. + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + | match_stackframes_intro: + forall res f tf sp pc rs trs + (TF: tunnel_function f = OK tf) + (RS: Registers.regs_lessdef rs trs), + match_stackframes + (Stackframe res f sp pc rs) + (Stackframe res tf sp (branch_target f pc) trs). + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall s ts f tf sp pc rs trs m tm + (STK: list_forall2 match_stackframes s ts) + (TF: tunnel_function f = OK tf) + (RS: Registers.regs_lessdef rs trs) + (MEM: Mem.extends m tm), + match_states + (State s f sp pc rs m) + (State ts tf sp (branch_target f pc) trs tm) + | match_states_call: + forall s ts f tf a ta m tm + (STK: list_forall2 match_stackframes s ts) + (TF: tunnel_fundef f = OK tf) + (ARGS: list_forall2 Val.lessdef a ta) + (MEM: Mem.extends m tm), + match_states + (Callstate s f a m) + (Callstate ts tf ta tm) + | match_states_return: + forall s ts v tv m tm + (STK: list_forall2 match_stackframes s ts) + (VAL: Val.lessdef v tv) + (MEM: Mem.extends m tm), + match_states + (Returnstate s v m) + (Returnstate ts tv tm). + +Definition measure (st: state): nat := + match st with + | State s f sp pc rs m => bound (branch_target f) pc + | Callstate s f v m => 0 + | Returnstate s v m => 0 + end. + + +Lemma transf_initial_states: + forall s1: state, initial_state prog s1 -> + exists s2: state, initial_state tprog s2 /\ match_states s1 s2. +Proof. + intros. inversion H as [b f m0 ge0 MEM SYM PTR SIG CALL]. + exploit function_ptr_translated. + - apply PTR. + - intros (tf & TPTR & TUN). + exists (Callstate nil tf nil m0). split. + + apply initial_state_intro with b. + * apply (Genv.init_mem_match TRANSL). apply MEM. + * rewrite (match_program_main TRANSL). + rewrite symbols_preserved. apply SYM. + * apply TPTR. + * rewrite <- SIG. apply sig_preserved. apply TUN. + + apply match_states_call. + * apply list_forall2_nil. + * apply TUN. + * apply list_forall2_nil. + * apply Mem.extends_refl. +Qed. + +Lemma transf_final_states: + forall (s1 : state) + (s2 : state) (r : Integers.Int.int), + match_states s1 s2 -> + final_state s1 r -> + final_state s2 r. +Proof. + intros. inv H0. inv H. inv VAL. inversion STK. apply final_state_intro. +Qed. + +Lemma tunnel_function_unfold: + forall f tf pc, + tunnel_function f = OK tf -> + (fn_code tf) ! pc = + option_map (tunnel_instr (branch_target f)) (fn_code f) ! pc. +Proof. + intros f tf pc. + unfold tunnel_function. + destruct (check_included _ _) eqn:EQinc; try congruence. + destruct (check_code _ _) eqn:EQcode; simpl; try congruence. + intro. inv H. simpl. rewrite PTree.gmap1. reflexivity. +Qed. + +Lemma reglist_lessdef: + forall (rs trs: Registers.Regmap.t val) (args: list Registers.reg), + regs_lessdef rs trs -> Val.lessdef_list (rs##args) (trs##args). +Proof. + intros. induction args; simpl; constructor. + apply H. apply IHargs. +Qed. + +Lemma instruction_type_preserved: + forall (f tf:function) (pc:node) (i ti:instruction) + (TF: tunnel_function f = OK tf) + (FATPC: (fn_code f) ! pc = Some i) + (NOTINOP: forall s, i <> Inop s) + (NOTICOND: forall cond args ifso ifnot info, i <> Icond cond args ifso ifnot info) + (TI: ti = tunnel_instr (branch_target f) i), + (fn_code tf) ! (branch_target f pc) = Some ti. +Proof. + intros. + assert ((fn_code tf) ! pc = Some (tunnel_instr (branch_target f) i)) as TFATPC. + rewrite (tunnel_function_unfold f tf pc); eauto. + rewrite FATPC; eauto. + exploit branch_target_bounds; eauto. + intro TB. inversion TB as [BT|s|cond args ifso ifnot info]; try (rewrite FATPC in H; congruence). +Qed. + +Lemma find_function_translated: + forall ros rs trs fd, + regs_lessdef rs trs -> + find_function ge ros rs = Some fd -> + exists tfd, tunnel_fundef fd = OK tfd /\ find_function tge ros trs = Some tfd. +Proof. + intros. destruct ros; simpl in *. + - (* reg *) + assert (E: trs # r = rs # r). + { exploit Genv.find_funct_inv. apply H0. intros (b & EQ). + generalize (H r) . rewrite EQ. intro LD. inv LD. auto. } + rewrite E. exploit functions_translated; eauto. + - (* ident *) + rewrite symbols_preserved. destruct (Genv.find_symbol ge i); inv H0. + exploit function_ptr_translated; eauto. + intros (tf & X1 & X2). exists tf; intuition. +Qed. + +Lemma list_forall2_lessdef_rs: + forall rs trs args, + regs_lessdef rs trs -> + list_forall2 Val.lessdef rs ## args trs ## args. +Proof. + intros rs trs args LD. + exploit (reglist_lessdef rs trs args). apply LD. + induction args; simpl; intros H; try constructor; inv H. + apply H3. apply IHargs. apply H5. +Qed. + +Lemma fn_stacksize_preserved: + forall f tf + (TF: tunnel_function f = OK tf), + fn_stacksize f = fn_stacksize tf. +Proof. + intros f tf. unfold tunnel_function. + destruct (check_included _ _); try congruence. + intro H. monadInv H. simpl. reflexivity. +Qed. + +Lemma regs_setres_lessdef: + forall res vres tvres rs trs, + regs_lessdef rs trs -> Val.lessdef vres tvres -> + regs_lessdef (regmap_setres res vres rs) (regmap_setres res tvres trs). +Proof. + induction res; intros; simpl; try auto using set_reg_lessdef. +Qed. + +Lemma regmap_optget_lessdef: + forall or rs trs, + regs_lessdef rs trs -> Val.lessdef (regmap_optget or Vundef rs) (regmap_optget or Vundef trs). +Proof. + intros or rs trs RS. + induction or; simpl; auto using set_reg_lessdef. +Qed. + +Lemma tunnel_fundef_Internal: + forall (f: function) (tf: fundef) + (TF: tunnel_fundef (Internal f) = OK tf), + exists (tf': function), tf = (Internal tf') /\ tunnel_function f = OK tf'. +Proof. + intros f tf. + unfold tunnel_fundef. simpl. intro H. monadInv H. exists x. + split. reflexivity. apply EQ. +Qed. + +Lemma tunnel_fundef_External: + forall (ef: external_function) (tf: fundef) + (TF: tunnel_fundef (External ef) = OK tf), + tf = (External ef). +Proof. + intros f tf. + unfold tunnel_fundef. simpl. intro H. monadInv H. reflexivity. +Qed. + + +Lemma fn_entrypoint_preserved: + forall f tf + (TF: tunnel_function f = OK tf), + fn_entrypoint tf = branch_target f (fn_entrypoint f). +Proof. + intros f tf. + unfold tunnel_function. destruct (check_included _ _); try congruence. + intro TF. monadInv TF. simpl. reflexivity. +Qed. + +Lemma init_regs_lessdef: + forall f tf args targs + (ARGS: list_forall2 Val.lessdef args targs) + (TF: tunnel_function f = OK tf), + regs_lessdef (init_regs args (fn_params f)) (init_regs targs (fn_params tf)). +Proof. + assert (regs_lessdef (Regmap.init Vundef) (Regmap.init Vundef)) as Hundef. + { unfold Regmap.init. unfold regs_lessdef. intro. unfold Regmap.get. rewrite PTree.gempty. apply Val.lessdef_undef. } + + intros f tf args targs ARGS. + + unfold tunnel_function. destruct (check_included _ _) eqn:EQinc; try congruence. + intro TF. monadInv TF. simpl. + (* + induction ARGS. + - induction (fn_params f) eqn:EQP; apply Hundef. + - induction (fn_params f) eqn:EQP. + * simpl. apply Hundef. + * simpl. apply set_reg_lessdef. apply H. + *) + + generalize (fn_params f) as l. induction ARGS; induction l; try (simpl; apply Hundef). + simpl. apply set_reg_lessdef; try assumption. apply IHARGS. +Qed. + +Lemma lessdef_forall2_list: + forall args ta, + list_forall2 Val.lessdef args ta -> Val.lessdef_list args ta. +Proof. + intros args ta H. induction H. apply Val.lessdef_list_nil. apply Val.lessdef_list_cons. apply H. apply IHlist_forall2. +Qed. + +Lemma tunnel_step_correct: + forall st1 t st2, step ge st1 t st2 -> + forall st1' (MS: match_states st1 st1'), + (exists st2', step tge st1' t st2' /\ match_states st2 st2') + \/ (measure st2 < measure st1 /\ t = E0 /\ match_states st2 st1')%nat. +Proof. + intros st1 t st2 H. induction H; intros; try (inv MS). + - (* Inop *) + exploit branch_target_bounds. apply TF. + rewrite H. intro. inv H0. + + (* TB_default *) + rewrite TB. left. eexists. split. + * apply exec_Inop. rewrite (tunnel_function_unfold f tf pc). rewrite H. simpl. eauto. apply TF. + * constructor; try assumption. + + (* TB_nop *) + simpl. right. repeat split. apply DEC. + rewrite EQ. apply match_states_intro; assumption. + - (* Iop *) + exploit eval_operation_lessdef; try eassumption. + apply reglist_lessdef. apply RS. + intros (tv & EVAL & LD). + left; eexists; split. + + eapply exec_Iop with (v:=tv). + apply instruction_type_preserved with (Iop op args res pc'); (simpl; auto)||congruence. + rewrite <- EVAL. apply eval_operation_preserved. apply symbols_preserved. + + apply match_states_intro; eauto. apply set_reg_lessdef. apply LD. apply RS. + - (* Iload *) + inv H0. + + exploit eval_addressing_lessdef; try eassumption. + apply reglist_lessdef. apply RS. + intros (ta & EVAL' & LD). + exploit Mem.loadv_extends; try eassumption. + intros (tv & LOAD' & LD'). + left. eexists. split. + * eapply exec_Iload. + -- exploit instruction_type_preserved; (simpl; eauto)||congruence. + -- try (eapply has_loaded_normal; eauto; rewrite <- EVAL'; apply eval_addressing_preserved; apply symbols_preserved). + * apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + exploit eval_addressing_lessdef; try eassumption. + apply reglist_lessdef; apply RS. + intros (ta & ADDR & LD). + (* TODO: on peut sans doute factoriser ça *) + destruct (Mem.loadv chunk tm ta) eqn:Htload. + -- left; eexists; split. + eapply exec_Iload. + ++ exploit instruction_type_preserved; (simpl; eauto)||congruence. + ++ try (eapply has_loaded_normal; eauto; rewrite <- ADDR; apply eval_addressing_preserved; apply symbols_preserved). + ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto. + -- left; eexists; split. + eapply exec_Iload. + ++ exploit instruction_type_preserved; (simpl; eauto)||congruence. + ++ eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1:=ge). + intros a EVAL'; rewrite ADDR in EVAL'; inv EVAL'. auto. + apply symbols_preserved. + ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto. + * exploit eval_addressing_lessdef_none; try eassumption. + apply reglist_lessdef; apply RS. + left. eexists. split. + -- eapply exec_Iload. + ++ exploit instruction_type_preserved; (simpl; eauto)||congruence. + ++ eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1:=ge). + intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. + apply symbols_preserved. + -- apply match_states_intro; try assumption. apply set_reg_lessdef. apply Val.lessdef_undef. apply RS. + - (* Lstore *) + exploit eval_addressing_lessdef; try eassumption. + apply reglist_lessdef; apply RS. + intros (ta & EVAL & LD). + exploit Mem.storev_extends; try eassumption. apply RS. + intros (tm' & STORE & MEM'). + left. eexists. split. + + eapply exec_Istore. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved. + * rewrite STORE. reflexivity. + + apply match_states_intro; try eassumption. + - (* Icall *) + left. + exploit find_function_translated; try eassumption. + intros (tfd & TFD & FIND). + eexists. split. + + eapply exec_Icall. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * apply FIND. + * apply sig_preserved. apply TFD. + + apply match_states_call; try assumption. + * apply list_forall2_cons; try assumption. apply match_stackframes_intro; try assumption. + * apply list_forall2_lessdef_rs. apply RS. + - (* Itailcall *) + exploit find_function_translated; try eassumption. + intros (tfd & TFD & FIND). + exploit Mem.free_parallel_extends; try eassumption. + intros (tm' & FREE & MEM'). + left. eexists. split. + + eapply exec_Itailcall. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * apply FIND. + * apply sig_preserved. apply TFD. + * erewrite <- fn_stacksize_preserved; try eassumption. + + apply match_states_call; try assumption. + apply list_forall2_lessdef_rs. apply RS. + - (* Ibuiltin *) + exploit eval_builtin_args_lessdef; try eassumption. apply RS. + intros (vl2 & EVAL & LD). + exploit external_call_mem_extends; try eassumption. + intros (tvres & tm' & EXT & LDRES & MEM' & UNCHGD). + left. eexists. split. + + eapply exec_Ibuiltin. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * eapply eval_builtin_args_preserved. eapply symbols_preserved. eapply EVAL. + * eapply external_call_symbols_preserved. eapply senv_preserved. eapply EXT. + + apply match_states_intro; try assumption. apply regs_setres_lessdef; try assumption. + - (* Icond *) + simpl. exploit branch_target_bounds. apply TF. rewrite H. intro. inv H1. + + (* TB_default *) + rewrite TB. + destruct (fn_code tf)!pc as [[]|] eqn:EQ; + assert (tunnel_function f = OK tf) as TF'; auto; + unfold tunnel_function in TF; destruct (check_included _ _) in TF; monadInv TF; + simpl in EQ; rewrite PTree.gmap1 in EQ; rewrite H in EQ; simpl in EQ; destruct (peq _ _) eqn: EQpeq in EQ; try congruence. + * left. eexists. split. + -- eapply exec_Inop. simpl. rewrite PTree.gmap1. rewrite H. simpl. rewrite EQpeq. reflexivity. + -- destruct b. apply match_states_intro; eauto. rewrite e. apply match_states_intro; eauto. + * left. eexists. split. + -- eapply exec_Icond; auto. simpl. rewrite PTree.gmap1. rewrite H. simpl. rewrite EQpeq. reflexivity. eapply eval_condition_lessdef; try eassumption. apply reglist_lessdef. apply RS. + -- destruct b; apply match_states_intro; auto. + + (* TB_cond *) right; repeat split; destruct b; try assumption. + * rewrite EQSO. apply match_states_intro; try assumption. + * rewrite EQNOT. apply match_states_intro; try assumption. + - (* Ijumptable *) + left. eexists. split. + + eapply exec_Ijumptable. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * generalize (RS arg). rewrite H0. intro. inv H2. reflexivity. + * rewrite list_nth_z_map. rewrite H1. simpl. reflexivity. + + apply match_states_intro; try eassumption. + - (* Ireturn *) + exploit Mem.free_parallel_extends; try eassumption. + intros (tm' & FREE & MEM'). + left. eexists. split. + + eapply exec_Ireturn. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * erewrite <- fn_stacksize_preserved. eapply FREE. eapply TF. + + apply match_states_return; try eassumption. + apply regmap_optget_lessdef. apply RS. + - (* internal function *) + exploit tunnel_fundef_Internal; try eassumption. + intros (tf' & EQ & TF'). subst. + exploit Mem.alloc_extends; try eassumption. reflexivity. reflexivity. + intros (m2' & ALLOC & EXT). + left. eexists. split. + + eapply exec_function_internal. + rewrite <- (fn_stacksize_preserved f tf'). eapply ALLOC. eapply TF'. + + rewrite (fn_entrypoint_preserved f tf'); try eassumption. apply match_states_intro; try eassumption. + apply init_regs_lessdef. apply ARGS. apply TF'. + - (* external function *) + exploit external_call_mem_extends. eapply H. eapply MEM. eapply lessdef_forall2_list. eapply ARGS. + intros (tvres & tm' & EXTCALL & LD & EXT & MEMUNCHGD). + left. eexists. split. + + erewrite (tunnel_fundef_External ef tf); try eassumption. + eapply exec_function_external. eapply external_call_symbols_preserved. eapply senv_preserved. eapply EXTCALL. + + eapply match_states_return; try assumption. + - (* return *) + inv STK. inv H1. + left. eexists. split. + + eapply exec_return. + + eapply match_states_intro; try assumption. + apply set_reg_lessdef; try assumption. +Qed. + + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). +Proof. + eapply forward_simulation_opt. + apply senv_preserved. + apply transf_initial_states. + apply transf_final_states. + exact tunnel_step_correct. +Qed. + +End PRESERVATION. |