diff options
Diffstat (limited to 'backend/CSE2.v')
-rw-r--r-- | backend/CSE2.v | 829 |
1 files changed, 2 insertions, 827 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index 011806cc..0bd5bf81 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -2,10 +2,6 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps. -Require Import Globalenvs Values. -Require Import Linking Values Memory Globalenvs Events Smallstep. -Require Import Registers Op RTL. - (* Static analysis *) Inductive sym_val : Type := @@ -269,27 +265,6 @@ Definition kill_sym_val_mem (sv: sym_val) := Definition kill_mem (rel : RELATION.t) := PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel. -Lemma args_unaffected: - forall rs : regset, - forall dst : reg, - forall v, - forall args : list reg, - existsb (fun y : reg => peq dst y) args = false -> - (rs # dst <- v ## args) = (rs ## args). -Proof. - induction args; simpl; trivial. - destruct (peq dst a) as [EQ | NEQ]; simpl. - { discriminate. - } - intro EXIST. - f_equal. - { - apply Regmap.gso. - congruence. - } - apply IHargs. - assumption. -Qed. Definition forward_move (rel : RELATION.t) (x : reg) : reg := match rel ! x with @@ -318,258 +293,6 @@ Definition gen_oper (op: operation) (dst : reg) (args : list reg) | _, _ => oper op dst args rel end. -Section SOUNDNESS. - Variable F V : Type. - Variable genv: Genv.t F V. - Variable sp : val. - -Section SAME_MEMORY. - Variable m : mem. - -Definition sem_sym_val sym rs := - match sym with - | SMove src => Some (rs # src) - | SOp op args => - eval_operation genv sp op (rs ## args) m - end. - -Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) : option val := - match rel ! x with - | None => Some (rs # x) - | Some sym => sem_sym_val sym rs - end. - -Definition sem_rel (rel : RELATION.t) (rs : regset) := - forall x : reg, (sem_reg rel x rs) = Some (rs # x). - -Lemma kill_reg_sound : - forall rel : RELATION.t, - forall dst : reg, - forall rs, - forall v, - sem_rel rel rs -> - sem_rel (kill_reg dst rel) (rs # dst <- v). -Proof. - unfold sem_rel, kill_reg, sem_reg, sem_sym_val. - intros until v. - intros REL x. - rewrite PTree.gfilter1. - destruct (Pos.eq_dec dst x). - { - subst x. - rewrite PTree.grs. - rewrite Regmap.gss. - reflexivity. - } - rewrite PTree.gro by congruence. - rewrite Regmap.gso by congruence. - destruct (rel ! x) as [relx | ] eqn:RELx. - 2: reflexivity. - unfold kill_sym_val. - pose proof (REL x) as RELinstx. - rewrite RELx in RELinstx. - destruct relx eqn:SYMVAL. - { - destruct (peq dst src); simpl. - { reflexivity. } - rewrite Regmap.gso by congruence. - assumption. - } - { destruct existsb eqn:EXISTS; simpl. - { reflexivity. } - rewrite args_unaffected by exact EXISTS. - assumption. - } -Qed. - -Lemma write_same: - forall rs : regset, - forall src dst : reg, - (rs # dst <- (rs # src)) # src = rs # src. -Proof. - intros. - destruct (peq src dst). - { - subst dst. - apply Regmap.gss. - } - rewrite Regmap.gso by congruence. - reflexivity. -Qed. - -Lemma move_sound : - forall rel : RELATION.t, - forall src dst : reg, - forall rs, - sem_rel rel rs -> - sem_rel (move src dst rel) (rs # dst <- (rs # src)). -Proof. - intros until rs. intros REL x. - pose proof (kill_reg_sound rel dst rs (rs # src) REL x) as KILL. - pose proof (REL src) as RELsrc. - unfold move. - destruct (peq x dst). - { - subst x. - unfold sem_reg. - rewrite PTree.gss. - rewrite Regmap.gss. - unfold sem_reg in RELsrc. - simpl. - unfold forward_move. - destruct (rel ! src) as [ sv |]; simpl. - destruct sv; simpl in *. - { - destruct (peq dst src0). - { - subst src0. - rewrite Regmap.gss. - reflexivity. - } - rewrite Regmap.gso by congruence. - assumption. - } - all: f_equal; apply write_same. - } - rewrite Regmap.gso by congruence. - unfold sem_reg. - rewrite PTree.gso by congruence. - rewrite Regmap.gso in KILL by congruence. - exact KILL. -Qed. - -Lemma move_cases_neq: - forall dst rel a, - a <> dst -> - (forward_move (kill_reg dst rel) a) <> dst. -Proof. - intros until a. intro NEQ. - unfold kill_reg, forward_move. - rewrite PTree.gfilter1. - rewrite PTree.gro by congruence. - destruct (rel ! a); simpl. - 2: congruence. - destruct s. - { - unfold kill_sym_val. - destruct peq; simpl; congruence. - } - all: simpl; - destruct negb; simpl; congruence. -Qed. - -Lemma args_replace_dst : - forall rel, - forall args : list reg, - forall dst : reg, - forall rs : regset, - forall v, - (sem_rel rel rs) -> - not (In dst args) -> - (rs # dst <- v) - ## (map - (forward_move (kill_reg dst rel)) args) = rs ## args. -Proof. - induction args; simpl. - 1: reflexivity. - intros until v. - intros REL NOT_IN. - rewrite IHargs by auto. - f_equal. - pose proof (REL a) as RELa. - rewrite Regmap.gso by (apply move_cases_neq; auto). - unfold kill_reg. - unfold sem_reg in RELa. - unfold forward_move. - rewrite PTree.gfilter1. - rewrite PTree.gro by auto. - destruct (rel ! a); simpl; trivial. - destruct s; simpl in *; destruct negb; simpl; congruence. -Qed. - -Lemma oper1_sound : - forall rel : RELATION.t, - forall op : operation, - forall dst : reg, - forall args: list reg, - forall rs : regset, - forall v, - sem_rel rel rs -> - not (In dst args) -> - eval_operation genv sp op (rs ## args) m = Some v -> - sem_rel (oper1 op dst args rel) (rs # dst <- v). -Proof. - intros until v. - intros REL NOT_IN EVAL x. - pose proof (kill_reg_sound rel dst rs v REL x) as KILL. - unfold oper1. - destruct (peq x dst). - { - subst x. - unfold sem_reg. - rewrite PTree.gss. - rewrite Regmap.gss. - simpl. - rewrite args_replace_dst by auto. - assumption. - } - rewrite Regmap.gso by congruence. - unfold sem_reg. - rewrite PTree.gso by congruence. - rewrite Regmap.gso in KILL by congruence. - exact KILL. -Qed. - -Lemma oper_sound : - forall rel : RELATION.t, - forall op : operation, - forall dst : reg, - forall args: list reg, - forall rs : regset, - forall v, - sem_rel rel rs -> - eval_operation genv sp op (rs ## args) m = Some v -> - sem_rel (oper op dst args rel) (rs # dst <- v). -Proof. - intros until v. - intros REL EVAL. - unfold oper. - destruct in_dec. - { - apply kill_reg_sound; auto. - } - apply oper1_sound; auto. -Qed. - -Lemma gen_oper_sound : - forall rel : RELATION.t, - forall op : operation, - forall dst : reg, - forall args: list reg, - forall rs : regset, - forall v, - sem_rel rel rs -> - eval_operation genv sp op (rs ## args) m = Some v -> - sem_rel (gen_oper op dst args rel) (rs # dst <- v). -Proof. - intros until v. - intros REL EVAL. - unfold gen_oper. - destruct op. - { destruct args as [ | h0 t0]. - apply oper_sound; auto. - destruct t0. - { - simpl in *. - replace v with (rs # h0) by congruence. - apply move_sound; auto. - } - apply oper_sound; auto. - } - all: apply oper_sound; auto. -Qed. - - Definition find_op_fold op args (already : option reg) x sv := match already with | Some found => already @@ -586,6 +309,7 @@ Definition find_op_fold op args (already : option reg) x sv := Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) := PTree.fold (find_op_fold op args) rel None. +(* NO LONGER NEEDED Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop := match l with | nil => True @@ -610,100 +334,7 @@ Proof. } apply IHl; auto. Qed. - -Lemma find_op_sound : - forall rel : RELATION.t, - forall op : operation, - forall src dst : reg, - forall args: list reg, - forall rs : regset, - sem_rel rel rs -> - find_op rel op args = Some src -> - (eval_operation genv sp op (rs ## args) m) = Some (rs # src). -Proof. - intros until rs. - unfold find_op. - rewrite PTree.fold_spec. - intro REL. - assert ( - forall start, - match start with - | None => True - | Some src => eval_operation genv sp op rs ## args m = Some rs # src - end -> fold_left - (fun (a : option reg) (p : positive * sym_val) => - find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start = - Some src -> - eval_operation genv sp op rs ## args m = Some rs # src) as REC. - { - unfold sem_rel, sem_reg in REL. - generalize (PTree.elements_complete rel). - generalize (PTree.elements rel). - induction l; simpl. - { - intros. - subst start. - assumption. - } - destruct a as [r sv]; simpl. - intros COMPLETE start GEN. - apply IHl. - { - intros. - apply COMPLETE. - right. - assumption. - } - unfold find_op_fold. - destruct start. - assumption. - destruct sv. - { trivial. } - destruct eq_operation; trivial. - subst op0. - destruct eq_args; trivial. - subst args0. - simpl. - assert ((rel ! r) = Some (SOp op args)) as RELatr. - { - apply COMPLETE. - left. - reflexivity. - } - pose proof (REL r) as RELr. - rewrite RELatr in RELr. - simpl in RELr. - assumption. - } - apply REC; auto. -Qed. - -End SAME_MEMORY. - -Lemma kill_mem_sound : - forall m m' : mem, - forall rel : RELATION.t, - forall rs, - sem_rel m rel rs -> sem_rel m' (kill_mem rel) rs. -Proof. - unfold sem_rel, sem_reg. - intros until rs. - intros SEM x. - pose proof (SEM x) as SEMx. - unfold kill_mem. - rewrite PTree.gfilter1. - unfold kill_sym_val_mem. - destruct (rel ! x) as [ sv | ]. - 2: reflexivity. - destruct sv; simpl in *; trivial. - { - destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial. - rewrite <- SEMx. - apply op_depends_on_memory_correct; auto. - } -Qed. - -End SOUNDNESS. +*) Definition apply_instr instr (rel : RELATION.t) : RB.t := match instr with @@ -809,459 +440,3 @@ Lemma transf_program_match: Proof. intros. eapply match_transform_program; 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 f, - Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (transf_fundef f). -Proof (Genv.find_funct_transf TRANSL). - -Lemma function_ptr_translated: - forall v f, - Genv.find_funct_ptr ge v = Some f -> - Genv.find_funct_ptr tge v = Some (transf_fundef f). -Proof (Genv.find_funct_ptr_transf TRANSL). - -Lemma symbols_preserved: - forall id, - Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof (Genv.find_symbol_transf TRANSL). - -Lemma senv_preserved: - Senv.equiv ge tge. -Proof (Genv.senv_transf TRANSL). - -Lemma sig_preserved: - forall f, funsig (transf_fundef f) = funsig f. -Proof. - destruct f; trivial. -Qed. - -Lemma find_function_translated: - forall ros rs fd, - find_function ge ros rs = Some fd -> - find_function tge ros rs = Some (transf_fundef fd). -Proof. - unfold find_function; intros. destruct ros as [r|id]. - eapply functions_translated; eauto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence. - eapply function_ptr_translated; eauto. -Qed. - -Lemma transf_function_at: - forall (f : function) (pc : node) (i : instruction), - (fn_code f)!pc = Some i -> - (fn_code (transf_function f))!pc = - Some(transf_instr (forward_map f) pc i). -Proof. - intros until i. intro CODE. - unfold transf_function; simpl. - rewrite PTree.gmap. - unfold option_map. - rewrite CODE. - reflexivity. -Qed. - -Definition sem_rel_b (relb : RB.t) sp m (rs : regset) := - match relb with - | Some rel => sem_rel fundef unit ge sp m rel rs - | None => True - end. - -Definition fmap_sem (fmap : option (PMap.t RB.t)) - sp m (pc : node) (rs : regset) := - match fmap with - | None => True - | Some map => sem_rel_b (PMap.get pc map) sp m rs - end. - -(* -Lemma step_simulation: - forall S1 t S2, RTL.step ge S1 t S2 -> - forall S1', match_states S1 S1' -> - exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. -Proof. - induction 1; intros S1' MS; inv MS; try TR_AT. -- (* nop *) - econstructor; split. eapply exec_Inop; eauto. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply get_rb_sem_ge with (rb2 := map # pc); trivial. - replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - unfold get_rb_sem in *. - destruct (map # pc) in *; try contradiction. - rewrite H. - reflexivity. -- (* op *) - econstructor; split. - eapply exec_Iop with (v := v); eauto. - rewrite <- H0. - rewrite subst_args_ok by assumption. - apply eval_operation_preserved. exact symbols_preserved. - constructor; auto. - - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - assert (RB.ge (map # pc') (apply_instr' (fn_code f) pc (map # pc))) as GE. - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr' in GE. - rewrite MPC in GE. - rewrite H in GE. - - destruct (op_cases op args res pc' mpc) as [[src [OP [ARGS MOVE]]] | KILL]. - { - subst op. - subst args. - rewrite MOVE in GE. - simpl in H0. - simpl in GE. - apply get_rb_sem_ge with (rb2 := Some (move src res mpc)). - assumption. - replace v with (rs # src) by congruence. - apply move_ok. - assumption. - } - rewrite KILL in GE. - apply get_rb_sem_ge with (rb2 := Some (kill res mpc)). - assumption. - apply kill_ok. - assumption. - -(* load *) -- econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. - apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). - { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_ok. - assumption. - -- (* load notrap1 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = None). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap1; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). - { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_ok. - assumption. - -- (* load notrap2 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap2; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). - { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_ok. - assumption. - -- (* store *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Istore; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply get_rb_sem_ge with (rb2 := map # pc); trivial. - replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - unfold get_rb_sem in *. - destruct (map # pc) in *; try contradiction. - rewrite H. - reflexivity. - -(* call *) -- econstructor; split. - eapply exec_Icall with (fd := transf_fundef fd); eauto. - eapply find_function_translated; eauto. - apply sig_preserved. - rewrite subst_args_ok by assumption. - constructor. constructor; auto. constructor. - - { - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill res mpc)). - { - replace (Some (kill res mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_weaken. - assumption. - } - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - assert (RB.ge (map # pc') (apply_instr' (fn_code f) pc (map # pc))) as GE. - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr' in GE. - unfold fmap_sem in *. - destruct (map # pc) as [mpc |] in *; try contradiction. - rewrite H in GE. - simpl in GE. - unfold is_killed_in_fmap, is_killed_in_map. - unfold RB.ge in GE. - destruct (map # pc') as [mpc'|] eqn:MPC' in *; trivial. - eauto. - -(* tailcall *) -- econstructor; split. - eapply exec_Itailcall with (fd := transf_fundef fd); eauto. - eapply find_function_translated; eauto. - apply sig_preserved. - rewrite subst_args_ok by assumption. - constructor. auto. - -(* builtin *) -- econstructor; split. - eapply exec_Ibuiltin; eauto. - eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - - apply get_rb_sem_ge with (rb2 := Some RELATION.top). - { - replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply top_ok. - -(* cond *) -- econstructor; split. - eapply exec_Icond; eauto. - rewrite subst_args_ok; eassumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply get_rb_sem_ge with (rb2 := map # pc); trivial. - replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. - destruct b; tauto. - } - unfold apply_instr'. - unfold get_rb_sem in *. - destruct (map # pc) in *; try contradiction. - rewrite H. - reflexivity. - -(* jumptbl *) -- econstructor; split. - eapply exec_Ijumptable; eauto. - rewrite subst_arg_ok; eassumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply get_rb_sem_ge with (rb2 := map # pc); trivial. - replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. - apply list_nth_z_in with (n := Int.unsigned n). - assumption. - } - unfold apply_instr'. - unfold get_rb_sem in *. - destruct (map # pc) in *; try contradiction. - rewrite H. - reflexivity. - -(* return *) -- destruct or as [arg | ]. - { - econstructor; split. - eapply exec_Ireturn; eauto. - unfold regmap_optget. - rewrite subst_arg_ok by eassumption. - constructor; auto. - } - econstructor; split. - eapply exec_Ireturn; eauto. - constructor; auto. - - -(* internal function *) -- simpl. econstructor; split. - eapply exec_function_internal; eauto. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - apply get_rb_sem_ge with (rb2 := Some RELATION.top). - { - eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption. - } - apply top_ok. - -(* external function *) -- econstructor; split. - eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - constructor; auto. - -(* return *) -- inv STACKS. inv H1. - econstructor; split. - eapply exec_return; eauto. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - unfold is_killed_in_fmap in H8. - unfold is_killed_in_map in H8. - destruct (map # pc) as [mpc |] in *; try contradiction. - destruct H8 as [rel' RGE]. - eapply get_rb_killed; eauto. -Qed. - - -Lemma transf_initial_states: - forall S1, RTL.initial_state prog S1 -> - exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. -Proof. - intros. inv H. econstructor; split. - econstructor. - eapply (Genv.init_mem_transf TRANSL); eauto. - rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto. - eapply function_ptr_translated; eauto. - rewrite <- H3; apply sig_preserved. - constructor. constructor. -Qed. - -Lemma transf_final_states: - forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r. -Proof. - intros. inv H0. inv H. inv STACKS. constructor. -Qed. - -Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (RTL.semantics tprog). -Proof. - eapply forward_simulation_step. - apply senv_preserved. - eexact transf_initial_states. - eexact transf_final_states. - exact step_simulation. -Qed. -*)
\ No newline at end of file |