diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | backend/CSE2.v | 829 | ||||
| -rw-r--r-- | backend/CSE2proof.v | 835 |
3 files changed, 838 insertions, 827 deletions
@@ -83,6 +83,7 @@ BACKEND=\ ValueDomain.v ValueAOp.v ValueAnalysis.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ + CSE2.v CSE2proof.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ 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 diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v new file mode 100644 index 00000000..a14988a0 --- /dev/null +++ b/backend/CSE2proof.v @@ -0,0 +1,835 @@ +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. +Require Import CSE2. + +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. + +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. + + +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. + + +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. + *) + +End PRESERVATION.
\ No newline at end of file |