From 7698300cfe2d3f944ce2e1d4a60a263620487718 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 20 Dec 2013 13:05:53 +0000 Subject: Merge of branch value-analysis. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Constpropproof.v | 782 +++++++++++++++-------------------------------- 1 file changed, 241 insertions(+), 541 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 898c4df..41afe8c 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -26,7 +26,9 @@ Require Import Registers. Require Import RTL. Require Import Lattice. Require Import Kildall. -Require Import Liveness. +Require Import ValueDomain. +Require Import ValueAOp. +Require Import ValueAnalysis. Require Import ConstpropOp. Require Import Constprop. Require Import ConstpropOpproof. @@ -37,316 +39,7 @@ Variable prog: program. Let tprog := transf_program prog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Let gapp := make_global_approx (PTree.empty _) prog.(prog_defs). - -(** * Correctness of the static analysis *) - -Section ANALYSIS. - -Variable sp: val. - -Definition regs_match_approx (a: D.t) (rs: regset) : Prop := - forall r, val_match_approx ge sp (D.get r a) rs#r. - -Lemma regs_match_approx_top: - forall rs, regs_match_approx D.top rs. -Proof. - intros. red; intros. simpl. rewrite PTree.gempty. - unfold Approx.top, val_match_approx. auto. -Qed. - -Lemma val_match_approx_increasing: - forall a1 a2 v, - Approx.ge a1 a2 -> val_match_approx ge sp a2 v -> val_match_approx ge sp a1 v. -Proof. - intros until v. - intros [A|[B|C]]. - subst a1. simpl. auto. - subst a2. simpl. tauto. - subst a2. auto. -Qed. - -Lemma regs_match_approx_increasing: - forall a1 a2 rs, - D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs. -Proof. - unfold D.ge, regs_match_approx. intros. - apply val_match_approx_increasing with (D.get r a2); auto. -Qed. - -Lemma regs_match_approx_update: - forall ra rs a v r, - val_match_approx ge sp a v -> - regs_match_approx ra rs -> - regs_match_approx (D.set r a ra) (rs#r <- v). -Proof. - intros; red; intros. - rewrite D.gsspec. rewrite Regmap.gsspec. destruct (peq r0 r); auto. - red; intros; subst ra. specialize (H0 xH). rewrite D.get_bot in H0. inv H0. - unfold Approx.eq. red; intros; subst a. inv H. -Qed. - -Lemma approx_regs_val_list: - forall ra rs rl, - regs_match_approx ra rs -> - val_list_match_approx ge sp (approx_regs ra rl) rs##rl. -Proof. - induction rl; simpl; intros. - constructor. - constructor. apply H. auto. -Qed. - -Lemma regs_match_approx_forget: - forall rs rl ra, - regs_match_approx ra rs -> - regs_match_approx (List.fold_left (fun a r => D.set r Unknown a) rl ra) rs. -Proof. - induction rl; simpl; intros. - auto. - apply IHrl. - red; intros. rewrite D.gsspec. destruct (peq r a). constructor. auto. - red; intros; subst ra. specialize (H xH). inv H. - unfold Approx.eq, Approx.bot. congruence. -Qed. - -(** The correctness of the static analysis follows from the results - of module [ConstpropOpproof] and the fact that the result of - the static analysis is a solution of the forward dataflow inequations. *) - -Lemma analyze_correct_1: - forall f pc rs pc' i, - f.(fn_code)!pc = Some i -> - In pc' (successors_instr i) -> - regs_match_approx (transfer gapp f pc (analyze gapp f)!!pc) rs -> - regs_match_approx (analyze gapp f)!!pc' rs. -Proof. - unfold analyze; intros. - set (lu := last_uses f) in *. - destruct (DS.fixpoint (fn_code f) successors_instr (transfer' gapp f lu) - ((fn_entrypoint f, D.top) :: nil)) as [approxs|] eqn:FIX. - apply regs_match_approx_increasing with (transfer' gapp f lu pc approxs!!pc). - eapply DS.fixpoint_solution; eauto. - unfold transfer'. destruct (lu!pc) as [regs|]. - apply regs_match_approx_forget; auto. - auto. - intros. rewrite PMap.gi. apply regs_match_approx_top. -Qed. - -Lemma analyze_correct_3: - forall f rs, - regs_match_approx (analyze gapp f)!!(f.(fn_entrypoint)) rs. -Proof. - intros. unfold analyze. - set (lu := last_uses f) in *. - destruct (DS.fixpoint (fn_code f) successors_instr (transfer' gapp f lu) - ((fn_entrypoint f, D.top) :: nil)) as [approxs|] eqn:FIX. - apply regs_match_approx_increasing with D.top. - eapply DS.fixpoint_entry; eauto. auto with coqlib. - apply regs_match_approx_top. - intros. rewrite PMap.gi. apply regs_match_approx_top. -Qed. - -(** eval_static_load *) - -Definition mem_match_approx (m: mem) : Prop := - forall id il b, - gapp!id = Some il -> Genv.find_symbol ge id = Some b -> - Genv.load_store_init_data ge m b 0 il /\ - Mem.valid_block m b /\ - (forall ofs, ~Mem.perm m b ofs Max Writable). - -Lemma eval_load_init_sound: - forall chunk m b il base ofs pos v, - Genv.load_store_init_data ge m b base il -> - Mem.load chunk m b ofs = Some v -> - ofs = base + pos -> - val_match_approx ge sp (eval_load_init chunk pos il) v. -Proof. - induction il; simpl; intros. -(* base case il = nil *) - auto. -(* inductive case *) - destruct a. - (* Init_int8 *) - destruct H. destruct (zeq pos 0). subst. rewrite Zplus_0_r in H0. - destruct chunk; simpl; auto. - rewrite Mem.load_int8_signed_unsigned in H0. rewrite H in H0. simpl in H0. - inv H0. decEq. apply Int.sign_ext_zero_ext. compute; auto. - congruence. - eapply IHil; eauto. omega. - (* Init_int16 *) - destruct H. destruct (zeq pos 0). subst. rewrite Zplus_0_r in H0. - destruct chunk; simpl; auto. - rewrite Mem.load_int16_signed_unsigned in H0. rewrite H in H0. simpl in H0. - inv H0. decEq. apply Int.sign_ext_zero_ext. compute; auto. - congruence. - eapply IHil; eauto. omega. - (* Init_int32 *) - destruct H. destruct (zeq pos 0). subst. rewrite Zplus_0_r in H0. - destruct chunk; simpl; auto. - congruence. - eapply IHil; eauto. omega. - (* Init_int64 *) - destruct H. destruct (zeq pos 0). subst. rewrite Zplus_0_r in H0. - destruct chunk; simpl; auto. - congruence. - eapply IHil; eauto. omega. - (* Init_float32 *) - destruct H. destruct (zeq pos 0). subst. rewrite Zplus_0_r in H0. - destruct chunk; simpl; auto. destruct (propagate_float_constants tt); simpl; auto. - congruence. - eapply IHil; eauto. omega. - (* Init_float64 *) - destruct H. destruct (zeq pos 0). subst. rewrite Zplus_0_r in H0. - destruct chunk; simpl; auto. destruct (propagate_float_constants tt); simpl; auto. - congruence. - eapply IHil; eauto. omega. - (* Init_space *) - eapply IHil; eauto. omega. - (* Init_symbol *) - destruct H as [[b' [A B]] C]. - destruct (zeq pos 0). subst. rewrite Zplus_0_r in H0. - destruct chunk; simpl; auto. - unfold symbol_address. rewrite A. congruence. - eapply IHil; eauto. omega. -Qed. - -Lemma eval_static_load_sound: - forall chunk m addr vaddr v, - Mem.loadv chunk m vaddr = Some v -> - mem_match_approx m -> - val_match_approx ge sp addr vaddr -> - val_match_approx ge sp (eval_static_load gapp chunk addr) v. -Proof. - intros. unfold eval_static_load. destruct addr; simpl; auto. - destruct (gapp!i) as [il|] eqn:?; auto. - red in H1. subst vaddr. unfold symbol_address in H. - destruct (Genv.find_symbol ge i) as [b'|] eqn:?; simpl in H; try discriminate. - exploit H0; eauto. intros [A [B C]]. - eapply eval_load_init_sound; eauto. - red; auto. -Qed. - -Lemma mem_match_approx_store: - forall chunk m addr v m', - mem_match_approx m -> - Mem.storev chunk m addr v = Some m' -> - mem_match_approx m'. -Proof. - intros; red; intros. exploit H; eauto. intros [A [B C]]. - destruct addr; simpl in H0; try discriminate. - exploit Mem.store_valid_access_3; eauto. intros [P Q]. - split. apply Genv.load_store_init_data_invariant with m; auto. - intros. eapply Mem.load_store_other; eauto. left; red; intro; subst b0. - eapply C. apply Mem.perm_cur_max. eapply P. instantiate (1 := Int.unsigned i). - generalize (size_chunk_pos chunk). omega. - split. eauto with mem. - intros; red; intros. eapply C. eapply Mem.perm_store_2; eauto. -Qed. - -Lemma mem_match_approx_alloc: - forall m lo hi b m', - mem_match_approx m -> - Mem.alloc m lo hi = (m', b) -> - mem_match_approx m'. -Proof. - intros; red; intros. exploit H; eauto. intros [A [B C]]. - split. apply Genv.load_store_init_data_invariant with m; auto. - intros. eapply Mem.load_alloc_unchanged; eauto. - split. eauto with mem. - intros; red; intros. exploit Mem.perm_alloc_inv; eauto. - rewrite dec_eq_false. apply C. eapply Mem.valid_not_valid_diff; eauto with mem. -Qed. - -Lemma mem_match_approx_free: - forall m lo hi b m', - mem_match_approx m -> - Mem.free m b lo hi = Some m' -> - mem_match_approx m'. -Proof. - intros; red; intros. exploit H; eauto. intros [A [B C]]. - split. apply Genv.load_store_init_data_invariant with m; auto. - intros. eapply Mem.load_free; eauto. - destruct (eq_block b0 b); auto. subst b0. - right. destruct (zlt lo hi); auto. - elim (C lo). apply Mem.perm_cur_max. - exploit Mem.free_range_perm; eauto. instantiate (1 := lo); omega. - intros; eapply Mem.perm_implies; eauto with mem. - split. eauto with mem. - intros; red; intros. eapply C. eauto with mem. -Qed. - -Lemma mem_match_approx_extcall: - forall ef vargs m t vres m', - mem_match_approx m -> - external_call ef ge vargs m t vres m' -> - mem_match_approx m'. -Proof. - intros; red; intros. exploit H; eauto. intros [A [B C]]. - split. apply Genv.load_store_init_data_invariant with m; auto. - intros. eapply external_call_readonly; eauto. - split. eapply external_call_valid_block; eauto. - intros; red; intros. elim (C ofs). eapply external_call_max_perm; eauto. -Qed. - -(* Show that mem_match_approx holds initially *) - -Definition global_approx_charact (g: genv) (ga: global_approx) : Prop := - forall id il b, - ga!id = Some il -> - Genv.find_symbol g id = Some b -> - Genv.find_var_info g b = Some (mkglobvar tt il true false). - -Lemma make_global_approx_correct: - forall gdl g ga, - global_approx_charact g ga -> - global_approx_charact (Genv.add_globals g gdl) (make_global_approx ga gdl). -Proof. - induction gdl; simpl; intros. - auto. - destruct a as [id gd]. apply IHgdl. - red; intros. - assert (EITHER: id0 = id /\ gd = Gvar(mkglobvar tt il true false) - \/ id0 <> id /\ ga!id0 = Some il). - destruct gd. - rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto]. - destruct (gvar_readonly v && negb (gvar_volatile v)) eqn:?. - rewrite PTree.gsspec in H0. destruct (peq id0 id). - inv H0. left. split; auto. - destruct v; simpl in *. - destruct gvar_readonly; try discriminate. - destruct gvar_volatile; try discriminate. - destruct gvar_info. auto. - auto. - rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto]. - - unfold Genv.add_global, Genv.find_symbol, Genv.find_var_info in *; - simpl in *. - destruct EITHER as [[A B] | [A B]]. - subst id0. rewrite PTree.gss in H1. inv H1. rewrite PTree.gss. auto. - rewrite PTree.gso in H1; auto. destruct gd. eapply H; eauto. - rewrite PTree.gso. eapply H; eauto. - red; intros; subst b. eelim Plt_strict; eapply Genv.genv_symb_range; eauto. -Qed. - -Theorem mem_match_approx_init: - forall m, Genv.init_mem prog = Some m -> mem_match_approx m. -Proof. - intros. - assert (global_approx_charact ge gapp). - unfold ge, gapp. unfold Genv.globalenv. - apply make_global_approx_correct. - red; intros. rewrite PTree.gempty in H0; discriminate. - red; intros. - exploit Genv.init_mem_characterization. - unfold ge in H0. eapply H0; eauto. eauto. - unfold Genv.perm_globvar; simpl. - intros [A [B C]]. - split. auto. split. eapply Genv.find_symbol_not_fresh; eauto. - intros; red; intros. exploit B; eauto. intros [P Q]. inv Q. -Qed. - -End ANALYSIS. +Let rm := romem_for_program prog. (** * Correctness of the code transformation *) @@ -370,24 +63,24 @@ Qed. Lemma functions_translated: forall (v: val) (f: fundef), Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (transf_fundef gapp f). + Genv.find_funct tge v = Some (transf_fundef rm f). Proof. intros. - exact (Genv.find_funct_transf (transf_fundef gapp) _ _ H). + exact (Genv.find_funct_transf (transf_fundef rm) _ _ H). Qed. Lemma function_ptr_translated: forall (b: block) (f: fundef), Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (transf_fundef gapp f). + Genv.find_funct_ptr tge b = Some (transf_fundef rm f). Proof. intros. - exact (Genv.find_funct_ptr_transf (transf_fundef gapp) _ _ H). + exact (Genv.find_funct_ptr_transf (transf_fundef rm) _ _ H). Qed. Lemma sig_function_translated: forall f, - funsig (transf_fundef gapp f) = funsig f. + funsig (transf_fundef rm f) = funsig f. Proof. intros. destruct f; reflexivity. Qed. @@ -422,82 +115,103 @@ Proof. Qed. Lemma transf_ros_correct: - forall sp ros rs rs' f approx, - regs_match_approx sp approx rs -> + forall bc rs ae ros f rs', + genv_match bc ge -> + ematch bc rs ae -> find_function ge ros rs = Some f -> regs_lessdef rs rs' -> - find_function tge (transf_ros approx ros) rs' = Some (transf_fundef gapp f). -Proof. - intros. destruct ros; simpl in *. - generalize (H r); intro MATCH. generalize (H1 r); intro LD. - destruct (rs#r); simpl in H0; try discriminate. - destruct (Int.eq_dec i Int.zero); try discriminate. - inv LD. - assert (find_function tge (inl _ r) rs' = Some (transf_fundef gapp f)). - simpl. rewrite <- H4. simpl. rewrite dec_eq_true. apply function_ptr_translated. auto. - destruct (D.get r approx); auto. - predSpec Int.eq Int.eq_spec i0 Int.zero; intros; auto. - simpl in *. unfold symbol_address in MATCH. rewrite symbols_preserved. - destruct (Genv.find_symbol ge i); try discriminate. - inv MATCH. apply function_ptr_translated; auto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try discriminate. + find_function tge (transf_ros ae ros) rs' = Some (transf_fundef rm f). +Proof. + intros until rs'; intros GE EM FF RLD. destruct ros; simpl in *. +- (* function pointer *) + generalize (EM r); fold (areg ae r); intro VM. generalize (RLD r); intro LD. + assert (DEFAULT: find_function tge (inl _ r) rs' = Some (transf_fundef rm f)). + { + simpl. inv LD. apply functions_translated; auto. rewrite <- H0 in FF; discriminate. + } + destruct (areg ae r); auto. destruct p; auto. + predSpec Int.eq Int.eq_spec ofs Int.zero; intros; auto. + subst ofs. exploit vmatch_ptr_gl; eauto. intros LD'. inv LD'; try discriminate. + rewrite H1 in FF. unfold symbol_address in FF. + simpl. rewrite symbols_preserved. + destruct (Genv.find_symbol ge id) as [b|]; try discriminate. + simpl in FF. rewrite dec_eq_true in FF. + apply function_ptr_translated; auto. + rewrite <- H0 in FF; discriminate. +- (* function symbol *) + rewrite symbols_preserved. + destruct (Genv.find_symbol ge i) as [b|]; try discriminate. apply function_ptr_translated; auto. Qed. Lemma const_for_result_correct: - forall a op sp v m, + forall a op bc v sp m, const_for_result a = Some op -> - val_match_approx ge sp a v -> - eval_operation tge sp op nil m = Some v. -Proof. - unfold const_for_result; intros. - destruct a; inv H; simpl in H0. - simpl. congruence. - destruct (generate_float_constants tt); inv H2. simpl. congruence. - simpl. subst v. unfold symbol_address. rewrite symbols_preserved. auto. - simpl. congruence. -Qed. - -Inductive match_pc (f: function) (app: D.t): nat -> node -> node -> Prop := + vmatch bc v a -> + bc sp = BCstack -> + genv_match bc ge -> + exists v', eval_operation tge (Vptr sp Int.zero) op nil m = Some v' /\ Val.lessdef v v'. +Proof. + unfold const_for_result; intros. + destruct a; try discriminate. +- (* integer *) + inv H. inv H0. exists (Vint n); auto. +- (* float *) + destruct (generate_float_constants tt); inv H. inv H0. exists (Vfloat f); auto. +- (* pointer *) + destruct p; try discriminate. + + (* global *) + inv H. exists (symbol_address ge id ofs); split. + unfold symbol_address. rewrite <- symbols_preserved. reflexivity. + eapply vmatch_ptr_gl; eauto. + + (* stack *) + inv H. exists (Vptr sp ofs); split. + simpl; rewrite Int.add_zero_l; auto. + eapply vmatch_ptr_stk; eauto. +Qed. + +Inductive match_pc (f: function) (ae: AE.t): nat -> node -> node -> Prop := | match_pc_base: forall n pc, - match_pc f app n pc pc + match_pc f ae n pc pc | match_pc_nop: forall n pc s pcx, f.(fn_code)!pc = Some (Inop s) -> - match_pc f app n s pcx -> - match_pc f app (Datatypes.S n) pc pcx - | match_pc_cond: forall n pc cond args s1 s2 b, + match_pc f ae n s pcx -> + match_pc f ae (S n) pc pcx + | match_pc_cond: forall n pc cond args s1 s2 b pcx, f.(fn_code)!pc = Some (Icond cond args s1 s2) -> - eval_static_condition cond (approx_regs app args) = Some b -> - match_pc f app (Datatypes.S n) pc (if b then s1 else s2). + resolve_branch (eval_static_condition cond (aregs ae args)) = Some b -> + match_pc f ae n (if b then s1 else s2) pcx -> + match_pc f ae (S n) pc pcx. Lemma match_successor_rec: - forall f app n pc, match_pc f app n pc (successor_rec n f app pc). + forall f ae n pc, match_pc f ae n pc (successor_rec n f ae pc). Proof. induction n; simpl; intros. - apply match_pc_base. - destruct (fn_code f)!pc as [i|] eqn:?; try apply match_pc_base. - destruct i; try apply match_pc_base. - eapply match_pc_nop; eauto. - destruct (eval_static_condition c (approx_regs app l)) as [b|] eqn:?. +- apply match_pc_base. +- destruct (fn_code f)!pc as [[]|] eqn:INSTR; try apply match_pc_base. + eapply match_pc_nop; eauto. + destruct (resolve_branch (eval_static_condition c (aregs ae l))) as [b|] eqn:COND. eapply match_pc_cond; eauto. apply match_pc_base. Qed. Lemma match_successor: - forall f app pc, match_pc f app num_iter pc (successor f app pc). + forall f ae pc, match_pc f ae num_iter pc (successor f ae pc). Proof. unfold successor; intros. apply match_successor_rec. Qed. Section BUILTIN_STRENGTH_REDUCTION. -Variable app: D.t. -Variable sp: val. + +Variable bc: block_classification. +Hypothesis GE: genv_match bc ge. +Variable ae: AE.t. Variable rs: regset. -Hypothesis MATCH: forall r, val_match_approx ge sp (approx_reg app r) rs#r. +Hypothesis MATCH: ematch bc rs ae. Lemma annot_strength_reduction_correct: forall targs args targs' args' eargs, - annot_strength_reduction app targs args = (targs', args') -> + annot_strength_reduction ae targs args = (targs', args') -> eventval_list_match ge eargs (annot_args_typ targs) rs##args -> exists eargs', eventval_list_match ge eargs' (annot_args_typ targs') rs##args' @@ -507,7 +221,7 @@ Proof. - inv H. simpl. exists eargs; auto. - destruct a. + destruct args as [ | arg args0]; simpl in H0; inv H0. - destruct (annot_strength_reduction app targs args0) as [targs'' args''] eqn:E. + destruct (annot_strength_reduction ae targs args0) as [targs'' args''] eqn:E. exploit IHtargs; eauto. intros [eargs'' [A B]]. assert (DFL: exists eargs', @@ -517,41 +231,48 @@ Proof. exists (ev1 :: eargs''); split. simpl; constructor; auto. simpl. congruence. } - destruct ty; destruct (approx_reg app arg) as [] eqn:E2; inv H; auto. - * exists eargs''; split; auto; simpl; f_equal; auto. - generalize (MATCH arg); rewrite E2; simpl; intros E3; - rewrite E3 in H5; inv H5; auto. + destruct ty; destruct (areg ae arg) as [] eqn:E2; inv H; auto. + * exists eargs''; split; auto; simpl; f_equal; auto. + generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM. + inv VM. rewrite <- H0 in *. inv H5; auto. * destruct (generate_float_constants tt); inv H1; auto. - exists eargs''; split; auto; simpl; f_equal; auto. - generalize (MATCH arg); rewrite E2; simpl; intros E3; - rewrite E3 in H5; inv H5; auto. - + destruct (annot_strength_reduction app targs args) as [targs'' args''] eqn:E. + exists eargs''; split; auto; simpl; f_equal; auto. + generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM. + inv VM. rewrite <- H0 in *. inv H5; auto. + + destruct (annot_strength_reduction ae targs args) as [targs'' args''] eqn:E. inv H. exploit IHtargs; eauto. intros [eargs'' [A B]]. exists eargs''; simpl; split; auto. congruence. - + destruct (annot_strength_reduction app targs args) as [targs'' args''] eqn:E. + + destruct (annot_strength_reduction ae targs args) as [targs'' args''] eqn:E. inv H. exploit IHtargs; eauto. intros [eargs'' [A B]]. exists eargs''; simpl; split; auto. congruence. Qed. +Lemma vmatch_ptr_gl': + forall v id ofs, + vmatch bc v (Ptr (Gl id ofs)) -> + v = Vundef \/ exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b ofs. +Proof. + intros. inv H; auto. inv H2. right; exists b; split; auto. eapply GE; eauto. +Qed. + Lemma builtin_strength_reduction_correct: forall ef args m t vres m', external_call ef ge rs##args m t vres m' -> - let (ef', args') := builtin_strength_reduction app ef args in + let (ef', args') := builtin_strength_reduction ae ef args in external_call ef' ge rs##args' m t vres m'. Proof. - intros until m'. functional induction (builtin_strength_reduction app ef args); intros; auto. -+ generalize (MATCH r1); rewrite e1; simpl; intros E. simpl in H. - unfold symbol_address in E. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite E in H. - rewrite volatile_load_global_charact. exists b; auto. - inv H. -+ generalize (MATCH r1); rewrite e1; simpl; intros E. simpl in H. - unfold symbol_address in E. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite E in H. - rewrite volatile_store_global_charact. exists b; auto. - inv H. -+ inv H. exploit annot_strength_reduction_correct; eauto. - intros [eargs' [A B]]. + intros until m'. functional induction (builtin_strength_reduction ae ef args); intros; auto. ++ simpl in H. assert (V: vmatch bc (rs#r1) (Ptr (Gl symb n1))) by (rewrite <- e1; apply MATCH). + exploit vmatch_ptr_gl'; eauto. intros [A | [b [A B]]]. + * simpl in H; rewrite A in H; inv H. + * simpl; rewrite volatile_load_global_charact. exists b; split; congruence. ++ simpl in H. assert (V: vmatch bc (rs#r1) (Ptr (Gl symb n1))) by (rewrite <- e1; apply MATCH). + exploit vmatch_ptr_gl'; eauto. intros [A | [b [A B]]]. + * simpl in H; rewrite A in H; inv H. + * simpl; rewrite volatile_store_global_charact. exists b; split; congruence. ++ inv H. exploit annot_strength_reduction_correct; eauto. intros [eargs' [A B]]. rewrite <- B. econstructor; eauto. Qed. @@ -575,9 +296,8 @@ End BUILTIN_STRENGTH_REDUCTION. and an initial state [st2] in the transformed code. This invariant expresses that all code fragments appearing in [st2] are obtained by [transf_code] transformation of the corresponding - fragments in [st1]. Moreover, the values of registers in [st1] - must match their compile-time approximations at the current program - point. + fragments in [st1]. Moreover, the state [st1] must match its compile-time + approximations at the current program point. These two parts of the diagram are the hypotheses. In conclusions, we want to prove the other two parts: the right vertical arrow, which is a transition in the transformed RTL code, and the bottom @@ -588,72 +308,63 @@ Inductive match_stackframes: stackframe -> stackframe -> Prop := match_stackframe_intro: forall res sp pc rs f rs', regs_lessdef rs rs' -> - (forall v, regs_match_approx sp (analyze gapp f)!!pc (rs#res <- v)) -> match_stackframes (Stackframe res f sp pc rs) - (Stackframe res (transf_function gapp f) sp pc rs'). + (Stackframe res (transf_function rm f) sp pc rs'). Inductive match_states: nat -> state -> state -> Prop := | match_states_intro: - forall s sp pc rs m f s' pc' rs' m' app n - (MATCH1: regs_match_approx sp app rs) - (MATCH2: regs_match_approx sp (analyze gapp f)!!pc rs) - (GMATCH: mem_match_approx m) + forall s sp pc rs m f s' pc' rs' m' bc ae n + (MATCH: ematch bc rs ae) (STACKS: list_forall2 match_stackframes s s') - (PC: match_pc f app n pc pc') + (PC: match_pc f ae n pc pc') (REGS: regs_lessdef rs rs') (MEM: Mem.extends m m'), match_states n (State s f sp pc rs m) - (State s' (transf_function gapp f) sp pc' rs' m') + (State s' (transf_function rm f) sp pc' rs' m') | match_states_call: forall s f args m s' args' m' - (GMATCH: mem_match_approx m) (STACKS: list_forall2 match_stackframes s s') (ARGS: Val.lessdef_list args args') (MEM: Mem.extends m m'), match_states O (Callstate s f args m) - (Callstate s' (transf_fundef gapp f) args' m') + (Callstate s' (transf_fundef rm f) args' m') | match_states_return: forall s v m s' v' m' - (GMATCH: mem_match_approx m) (STACKS: list_forall2 match_stackframes s s') (RES: Val.lessdef v v') (MEM: Mem.extends m m'), list_forall2 match_stackframes s s' -> match_states O (Returnstate s v m) - (Returnstate s' v' m'). + (Returnstate s' v' m'). Lemma match_states_succ: - forall s f sp pc2 rs m s' rs' m' pc1 i, - f.(fn_code)!pc1 = Some i -> - In pc2 (successors_instr i) -> - regs_match_approx sp (transfer gapp f pc1 (analyze gapp f)!!pc1) rs -> - mem_match_approx m -> + forall s f sp pc rs m s' rs' m', + sound_state prog (State s f sp pc rs m) -> list_forall2 match_stackframes s s' -> regs_lessdef rs rs' -> Mem.extends m m' -> - match_states O (State s f sp pc2 rs m) - (State s' (transf_function gapp f) sp pc2 rs' m'). + match_states O (State s f sp pc rs m) + (State s' (transf_function rm f) sp pc rs' m'). Proof. - intros. - assert (regs_match_approx sp (analyze gapp f)!!pc2 rs). - eapply analyze_correct_1; eauto. - apply match_states_intro with (app := (analyze gapp f)!!pc2); auto. + intros. inv H. + apply match_states_intro with (bc := bc) (ae := ae); auto. constructor. Qed. Lemma transf_instr_at: forall f pc i, f.(fn_code)!pc = Some i -> - (transf_function gapp f).(fn_code)!pc = Some(transf_instr gapp f (analyze gapp f) pc i). + (transf_function rm f).(fn_code)!pc = Some(transf_instr f (analyze rm f) rm pc i). Proof. - intros. simpl. unfold transf_code. rewrite PTree.gmap. rewrite H. auto. + intros. simpl. rewrite PTree.gmap. rewrite H. auto. Qed. Ltac TransfInstr := match goal with - | H: (PTree.get ?pc (fn_code ?f) = Some ?instr) |- _ => - generalize (transf_instr_at _ _ _ H); simpl + | H1: (PTree.get ?pc (fn_code ?f) = Some ?instr), + H2: (analyze (romem_for_program prog) ?f)#?pc = VA.State ?ae ?am |- _ => + fold rm in H2; generalize (transf_instr_at _ _ _ H1); unfold transf_instr; rewrite H2 end. (** The proof of simulation proceeds by case analysis on the transition @@ -662,113 +373,107 @@ Ltac TransfInstr := Lemma transf_step_correct: forall s1 t s2, step ge s1 t s2 -> - forall n1 s1' (MS: match_states n1 s1 s1'), + forall n1 s1' (SS1: sound_state prog s1) (SS2: sound_state prog s2) (MS: match_states n1 s1 s1'), (exists n2, exists s2', step tge s1' t s2' /\ match_states n2 s2 s2') \/ (exists n2, n2 < n1 /\ t = E0 /\ match_states n2 s2 s1')%nat. Proof. - induction 1; intros; inv MS; try (inv PC; try congruence). + induction 1; intros; inv SS1; inv MS; try (inv PC; try congruence). (* Inop, preserved *) - rename pc'0 into pc. TransfInstr; intro. + rename pc'0 into pc. TransfInstr; intros. left; econstructor; econstructor; split. eapply exec_Inop; eauto. - eapply match_states_succ; eauto. simpl; auto. - unfold transfer; rewrite H. auto. + eapply match_states_succ; eauto. (* Inop, skipped over *) - rewrite H0 in H; inv H. + assert (s0 = pc') by congruence. subst s0. right; exists n; split. omega. split. auto. - apply match_states_intro with app; auto. - eapply analyze_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H0. auto. + apply match_states_intro with bc0 ae0; auto. (* Iop *) rename pc'0 into pc. TransfInstr. - set (app_before := (analyze gapp f)#pc). - set (a := eval_static_operation op (approx_regs app_before args)). - set (app_after := D.set res a app_before). - assert (VMATCH: val_match_approx ge sp a v). - eapply eval_static_operation_correct; eauto. - apply approx_regs_val_list; auto. - assert (MATCH': regs_match_approx sp app_after rs#res <- v). - apply regs_match_approx_update; auto. - assert (MATCH'': regs_match_approx sp (analyze gapp f) # pc' rs # res <- v). - eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto. - unfold transfer; rewrite H. auto. + set (a := eval_static_operation op (aregs ae args)). + set (ae' := AE.set res a ae). + assert (VMATCH: vmatch bc v a) by (eapply eval_static_operation_sound; eauto with va). + assert (MATCH': ematch bc (rs#res <- v) ae') by (eapply ematch_update; eauto). destruct (const_for_result a) as [cop|] eqn:?; intros. (* constant is propagated *) + exploit const_for_result_correct; eauto. intros (v' & A & B). left; econstructor; econstructor; split. eapply exec_Iop; eauto. - eapply const_for_result_correct; eauto. - apply match_states_intro with app_after; auto. + apply match_states_intro with bc ae'; auto. apply match_successor. apply set_reg_lessdef; auto. (* operator is strength-reduced *) - exploit op_strength_reduction_correct. eexact MATCH2. reflexivity. eauto. - fold app_before. - destruct (op_strength_reduction op args (approx_regs app_before args)) as [op' args']. - intros [v' [EV' LD']]. - assert (EV'': exists v'', eval_operation ge sp op' rs'##args' m' = Some v'' /\ Val.lessdef v' v''). - eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto. + assert(OP: + let (op', args') := op_strength_reduction op args (aregs ae args) in + exists v', + eval_operation ge (Vptr sp0 Int.zero) op' rs ## args' m = Some v' /\ + Val.lessdef v v'). + { eapply op_strength_reduction_correct with (ae := ae); eauto with va. } + destruct (op_strength_reduction op args (aregs ae args)) as [op' args']. + destruct OP as [v' [EV' LD']]. + assert (EV'': exists v'', eval_operation ge (Vptr sp0 Int.zero) op' rs'##args' m' = Some v'' /\ Val.lessdef v' v''). + { eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto. } destruct EV'' as [v'' [EV'' LD'']]. left; econstructor; econstructor; split. eapply exec_Iop; eauto. erewrite eval_operation_preserved. eexact EV''. exact symbols_preserved. - apply match_states_intro with app_after; auto. + apply match_states_intro with bc ae'; auto. apply match_successor. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. (* Iload *) - rename pc'0 into pc. TransfInstr. - set (ap1 := eval_static_addressing addr - (approx_regs (analyze gapp f) # pc args)). - set (ap2 := eval_static_load gapp chunk ap1). - assert (VM1: val_match_approx ge sp ap1 a). - eapply eval_static_addressing_correct; eauto. - eapply approx_regs_val_list; eauto. - assert (VM2: val_match_approx ge sp ap2 v). - eapply eval_static_load_sound; eauto. - destruct (const_for_result ap2) as [cop|] eqn:?; intros. + rename pc'0 into pc. TransfInstr. + set (aa := eval_static_addressing addr (aregs ae args)). + assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va). + set (av := loadv chunk rm am aa). + assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto). + destruct (const_for_result av) as [cop|] eqn:?; intros. (* constant-propagated *) + exploit const_for_result_correct; eauto. intros (v' & A & B). left; econstructor; econstructor; split. - eapply exec_Iop; eauto. eapply const_for_result_correct; eauto. - eapply match_states_succ; eauto. simpl; auto. - unfold transfer; rewrite H. apply regs_match_approx_update; auto. + eapply exec_Iop; eauto. + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. (* strength-reduced *) - generalize (addr_strength_reduction_correct ge sp (analyze gapp f)!!pc rs - MATCH2 addr args (approx_regs (analyze gapp f) # pc args) (refl_equal _)). - destruct (addr_strength_reduction addr args (approx_regs (analyze gapp f) # pc args)) as [addr' args']. - rewrite H0. intros P. - assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a'). - eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto. - destruct ADDR' as [a' [A B]]. - assert (C: eval_addressing tge sp addr' rs'##args' = Some a'). - rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. - exploit Mem.loadv_extends; eauto. intros [v' [D E]]. + assert (ADDR: + let (addr', args') := addr_strength_reduction addr args (aregs ae args) in + exists a', + eval_addressing ge (Vptr sp0 Int.zero) addr' rs ## args' = Some a' /\ + Val.lessdef a a'). + { eapply addr_strength_reduction_correct with (ae := ae); eauto with va. } + destruct (addr_strength_reduction addr args (aregs ae args)) as [addr' args']. + destruct ADDR as (a' & P & Q). + exploit eval_addressing_lessdef. eapply regs_lessdef_regs; eauto. eexact P. + intros (a'' & U & V). + assert (W: eval_addressing tge (Vptr sp0 Int.zero) addr' rs'##args' = Some a''). + { rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. } + exploit Mem.loadv_extends. eauto. eauto. apply Val.lessdef_trans with a'; eauto. + intros (v' & X & Y). left; econstructor; econstructor; split. eapply exec_Iload; eauto. - eapply match_states_succ; eauto. simpl; auto. - unfold transfer; rewrite H. apply regs_match_approx_update; auto. - apply set_reg_lessdef; auto. + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. (* Istore *) rename pc'0 into pc. TransfInstr. - generalize (addr_strength_reduction_correct ge sp (analyze gapp f)!!pc rs - MATCH2 addr args (approx_regs (analyze gapp f) # pc args) (refl_equal _)). - destruct (addr_strength_reduction addr args (approx_regs (analyze gapp f) # pc args)) as [addr' args']. - intros P Q. rewrite H0 in P. - assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a'). - eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto. - destruct ADDR' as [a' [A B]]. - assert (C: eval_addressing tge sp addr' rs'##args' = Some a'). - rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. - exploit Mem.storev_extends; eauto. intros [m2' [D E]]. + assert (ADDR: + let (addr', args') := addr_strength_reduction addr args (aregs ae args) in + exists a', + eval_addressing ge (Vptr sp0 Int.zero) addr' rs ## args' = Some a' /\ + Val.lessdef a a'). + { eapply addr_strength_reduction_correct with (ae := ae); eauto with va. } + destruct (addr_strength_reduction addr args (aregs ae args)) as [addr' args']. + destruct ADDR as (a' & P & Q). + exploit eval_addressing_lessdef. eapply regs_lessdef_regs; eauto. eexact P. + intros (a'' & U & V). + assert (W: eval_addressing tge (Vptr sp0 Int.zero) addr' rs'##args' = Some a''). + { rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. } + exploit Mem.storev_extends. eauto. eauto. apply Val.lessdef_trans with a'; eauto. apply REGS. + intros (m2' & X & Y). left; econstructor; econstructor; split. eapply exec_Istore; eauto. - eapply match_states_succ; eauto. simpl; auto. - unfold transfer; rewrite H. auto. - eapply mem_match_approx_store; eauto. + eapply match_states_succ; eauto. (* Icall *) rename pc'0 into pc. @@ -777,10 +482,7 @@ Proof. left; econstructor; econstructor; split. eapply exec_Icall; eauto. apply sig_function_translated; auto. constructor; auto. constructor; auto. - econstructor; eauto. - intros. eapply analyze_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. simpl. auto. + econstructor; eauto. apply regs_lessdef_regs; auto. (* Itailcall *) @@ -790,7 +492,6 @@ Proof. left; econstructor; econstructor; split. eapply exec_Itailcall; eauto. apply sig_function_translated; auto. constructor; auto. - eapply mem_match_approx_free; eauto. apply regs_lessdef_regs; auto. (* Ibuiltin *) @@ -798,7 +499,7 @@ Proof. Opaque builtin_strength_reduction. exploit builtin_strength_reduction_correct; eauto. TransfInstr. - destruct (builtin_strength_reduction (analyze gapp f)#pc ef args) as [ef' args']. + destruct (builtin_strength_reduction ae ef args) as [ef' args']. intros P Q. exploit external_call_mem_extends; eauto. instantiate (1 := rs'##args'). apply regs_lessdef_regs; auto. @@ -808,74 +509,68 @@ Opaque builtin_strength_reduction. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. eapply match_states_succ; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. simpl; auto. - eapply mem_match_approx_extcall; eauto. apply set_reg_lessdef; auto. (* Icond, preserved *) - rename pc'0 into pc. TransfInstr. - generalize (cond_strength_reduction_correct ge sp (analyze gapp f)#pc rs m - MATCH2 cond args (approx_regs (analyze gapp f) # pc args) (refl_equal _)). - destruct (cond_strength_reduction cond args (approx_regs (analyze gapp f) # pc args)) as [cond' args']. + rename pc' into pc. TransfInstr. + set (ac := eval_static_condition cond (aregs ae args)). + assert (C: cmatch (eval_condition cond rs ## args m) ac) + by (eapply eval_static_condition_sound; eauto with va). + rewrite H0 in C. + generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (refl_equal _)). + destruct (cond_strength_reduction cond args (aregs ae args)) as [cond' args']. intros EV1 TCODE. - left; exists O; exists (State s' (transf_function gapp f) sp (if b then ifso else ifnot) rs' m'); split. - destruct (eval_static_condition cond (approx_regs (analyze gapp f) # pc args)) eqn:?. - assert (eval_condition cond rs ## args m = Some b0). - eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto. - assert (b = b0) by congruence. subst b0. + left; exists O; exists (State s' (transf_function rm f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split. + destruct (resolve_branch ac) eqn: RB. + assert (b0 = b) by (eapply resolve_branch_sound; eauto). subst b0. destruct b; eapply exec_Inop; eauto. eapply exec_Icond; eauto. eapply eval_condition_lessdef with (vl1 := rs##args'); eauto. eapply regs_lessdef_regs; eauto. congruence. eapply match_states_succ; eauto. - destruct b; simpl; auto. - unfold transfer; rewrite H. auto. (* Icond, skipped over *) rewrite H1 in H; inv H. - assert (eval_condition cond rs ## args m = Some b0). - eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto. - assert (b = b0) by congruence. subst b0. - right; exists n; split. omega. split. auto. - assert (MATCH': regs_match_approx sp (analyze gapp f) # (if b then ifso else ifnot) rs). - eapply analyze_correct_1; eauto. destruct b; simpl; auto. - unfold transfer; rewrite H1; auto. - econstructor; eauto. constructor. + set (ac := eval_static_condition cond (aregs ae0 args)) in *. + assert (C: cmatch (eval_condition cond rs ## args m) ac) + by (eapply eval_static_condition_sound; eauto with va). + rewrite H0 in C. + assert (b0 = b) by (eapply resolve_branch_sound; eauto). subst b0. + right; exists n; split. omega. split. auto. + econstructor; eauto. (* Ijumptable *) rename pc'0 into pc. - assert (A: (fn_code (transf_function gapp f))!pc = Some(Ijumptable arg tbl) - \/ (fn_code (transf_function gapp f))!pc = Some(Inop pc')). - TransfInstr. destruct (approx_reg (analyze gapp f) # pc arg) eqn:?; auto. - generalize (MATCH2 arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. - simpl. intro EQ; inv EQ. rewrite H1. auto. - assert (B: rs'#arg = Vint n). - generalize (REGS arg); intro LD; inv LD; congruence. - left; exists O; exists (State s' (transf_function gapp f) sp pc' rs' m'); split. + assert (A: (fn_code (transf_function rm f))!pc = Some(Ijumptable arg tbl) + \/ (fn_code (transf_function rm f))!pc = Some(Inop pc')). + { TransfInstr. + destruct (areg ae arg) eqn:A; auto. + generalize (EM arg). fold (areg ae arg); rewrite A. + intros V; inv V. replace n0 with n by congruence. + rewrite H1. auto. } + assert (rs'#arg = Vint n). + { generalize (REGS arg). rewrite H0. intros LD; inv LD; auto. } + left; exists O; exists (State s' (transf_function rm f) (Vptr sp0 Int.zero) pc' rs' m'); split. destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto. eapply match_states_succ; eauto. - simpl. eapply list_nth_z_in; eauto. - unfold transfer; rewrite H; auto. (* Ireturn *) exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. left; exists O; exists (Returnstate s' (regmap_optget or Vundef rs') m2'); split. eapply exec_Ireturn; eauto. TransfInstr; auto. constructor; auto. - eapply mem_match_approx_free; eauto. destruct or; simpl; auto. (* internal function *) exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m2' [A B]]. + assert (X: exists bc ae, ematch bc (init_regs args (fn_params f)) ae). + { inv SS2. exists bc0; exists ae; auto. } + destruct X as (bc1 & ae1 & MATCH). simpl. unfold transf_function. left; exists O; econstructor; split. eapply exec_function_internal; simpl; eauto. simpl. econstructor; eauto. - apply analyze_correct_3; auto. - apply analyze_correct_3; auto. - eapply mem_match_approx_alloc; eauto. - instantiate (1 := f). constructor. + constructor. apply init_regs_lessdef; auto. (* external function *) @@ -886,9 +581,11 @@ Opaque builtin_strength_reduction. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. constructor; auto. - eapply mem_match_approx_extcall; eauto. (* return *) + assert (X: exists bc ae, ematch bc (rs#res <- vres) ae). + { inv SS2. exists bc0; exists ae; auto. } + destruct X as (bc1 & ae1 & MATCH). inv H4. inv H1. left; exists O; econstructor; split. eapply exec_return; eauto. @@ -901,16 +598,14 @@ Lemma transf_initial_states: Proof. intros. inversion H. exploit function_ptr_translated; eauto. intro FIND. - exists O; exists (Callstate nil (transf_fundef gapp f) nil m0); split. + exists O; exists (Callstate nil (transf_fundef rm f) nil m0); split. econstructor; eauto. apply Genv.init_mem_transf; auto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. reflexivity. rewrite <- H3. apply sig_function_translated. - constructor. - eapply mem_match_approx_init; eauto. - constructor. constructor. apply Mem.extends_refl. + constructor. constructor. constructor. apply Mem.extends_refl. Qed. Lemma transf_final_states: @@ -926,16 +621,21 @@ Qed. Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. - eapply Forward_simulation with (fsim_order := lt); simpl. - apply lt_wf. - eexact transf_initial_states. - eexact transf_final_states. - fold ge; fold tge. intros. - exploit transf_step_correct; eauto. - intros [ [n2 [s2' [A B]]] | [n2 [A [B C]]]]. - exists n2; exists s2'; split; auto. left; apply plus_one; auto. - exists n2; exists s2; split; auto. right; split; auto. subst t; apply star_refl. - eexact symbols_preserved. + apply Forward_simulation with + (fsim_order := lt) + (fsim_match_states := fun n s1 s2 => sound_state prog s1 /\ match_states n s1 s2). +- apply lt_wf. +- simpl; intros. exploit transf_initial_states; eauto. intros (n & st2 & A & B). + exists n, st2; intuition. eapply sound_initial; eauto. +- simpl; intros. destruct H. eapply transf_final_states; eauto. +- simpl; intros. destruct H0. + assert (sound_state prog s1') by (eapply sound_step; eauto). + fold ge; fold tge. + exploit transf_step_correct; eauto. + intros [ [n2 [s2' [A B]]] | [n2 [A [B C]]]]. + exists n2; exists s2'; split; auto. left; apply plus_one; auto. + exists n2; exists s2; split; auto. right; split; auto. subst t; apply star_refl. +- eexact symbols_preserved. Qed. End PRESERVATION. -- cgit v1.2.3