From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Constpropproof.v | 496 +++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 410 insertions(+), 86 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 9affea88..406e6133 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -31,11 +31,18 @@ Require Import ConstpropOp. Require Import Constprop. Require Import ConstpropOpproof. +Section PRESERVATION. + +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_vars). + (** * Correctness of the static analysis *) Section ANALYSIS. -Variable ge: genv. Variable sp: val. Definition regs_match_approx (a: D.t) (rs: regset) : Prop := @@ -97,14 +104,14 @@ 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 f pc (analyze f)!!pc) rs -> - regs_match_approx (analyze f)!!pc' rs. + regs_match_approx (transfer gapp f pc (analyze gapp f)!!pc) rs -> + regs_match_approx (analyze gapp f)!!pc' rs. Proof. intros until i. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer f) + caseEq (DS.fixpoint (successors f) (transfer gapp f) ((fn_entrypoint f, D.top) :: nil)). intros approxs; intros. - apply regs_match_approx_increasing with (transfer f pc approxs!!pc). + apply regs_match_approx_increasing with (transfer gapp f pc approxs!!pc). eapply DS.fixpoint_solution; eauto. unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto. auto. @@ -113,10 +120,10 @@ Qed. Lemma analyze_correct_3: forall f rs, - regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs. + regs_match_approx (analyze gapp f)!!(f.(fn_entrypoint)) rs. Proof. intros. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer f) + caseEq (DS.fixpoint (successors f) (transfer gapp f) ((fn_entrypoint f, D.top) :: nil)). intros approxs; intros. apply regs_match_approx_increasing with D.top. @@ -125,6 +132,301 @@ Proof. 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_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 zeq_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 (zeq 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 vl g ga, + global_approx_charact g ga -> + global_approx_charact (Genv.add_variables g vl) (make_global_approx ga vl). +Proof. + induction vl; simpl; intros. + auto. + destruct a as [id gv]. apply IHvl. + red; intros. + assert (EITHER: id0 = id /\ gv = mkglobvar tt il true false + \/ id0 <> id /\ ga!id0 = Some il). + destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn. + rewrite PTree.gsspec in H0. destruct (peq id0 id). + inv H0. left. split; auto. + destruct gv; simpl in *. + destruct gvar_readonly; try discriminate. + destruct gvar_volatile; try discriminate. + destruct gvar_info. auto. + right; auto. + rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); try discriminate. + right; auto. + unfold Genv.add_variable, 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 ZMap.gss. auto. + rewrite PTree.gso in H1; auto. rewrite ZMap.gso. eapply H. eauto. auto. + exploit Genv.genv_symb_range; eauto. unfold ZIndexed.t. omega. +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. + +(********************** +Definition mem_match_approx_gen (g: genv) (ga: global_approx) (m: mem) : Prop := + forall id il b, + ga!id = Some il -> Genv.find_symbol g 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 mem_match_approx_alloc_variables: + forall vl g ga m m', + mem_match_approx_gen g ga m -> + Genv.genv_nextvar g = Mem.nextblock m -> + Genv.alloc_variables ge m vl = Some m' -> + mem_match_approx_gen (Genv.add_variables g vl) (make_global_approx ga vl) m'. +Proof. + induction vl; simpl; intros. +(* base case *) + inv H1. auto. +(* inductive case *) + destruct a as [id gv]. + set (ga1 := if gv.(gvar_readonly) && negb gv.(gvar_volatile) + then PTree.set id gv.(gvar_init) ga + else PTree.remove id ga). + revert H1. unfold Genv.alloc_variable. simpl. + set (il := gvar_init gv) in *. + set (sz := Genv.init_data_list_size il) in *. + destruct (Mem.alloc m 0 sz) as [m1 b]_eqn. + destruct (Genv.store_zeros m1 b sz) as [m2|]_eqn; try congruence. + destruct (Genv.store_init_data_list ge m2 b 0 il) as [m3|]_eqn; try congruence. + destruct (Mem.drop_perm m3 b 0 sz (Genv.perm_globvar gv)) as [m4|]_eqn; try congruence. + intros. + exploit Mem.alloc_result; eauto. intro NB. + assert (NB': Mem.nextblock m4 = Mem.nextblock m1). + rewrite (Mem.nextblock_drop _ _ _ _ _ _ Heqo1). + rewrite (Genv.store_init_data_list_nextblock _ _ _ _ _ Heqo0). + rewrite (Genv.store_zeros_nextblock _ _ _ Heqo). + auto. + apply IHvl with m4. + (* mem_match_approx for intermediate state *) + red; intros. + unfold Genv.find_symbol in H3. simpl in H3. + rewrite H0 in H3. rewrite <- NB in H3. + assert (EITHER: id0 <> id /\ ga!id0 = Some il0 + \/ id0 = id /\ il0 = il /\ gvar_readonly gv = true /\ gvar_volatile gv = false). + unfold ga1 in H2. destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn. + rewrite PTree.gsspec in H2. destruct (peq id0 id). + inv H2. right. split; auto. split; auto. + destruct (gvar_readonly gv); simpl in Heqb1; try discriminate. + destruct (gvar_volatile gv); simpl in Heqb1; try discriminate. + auto. auto. + rewrite PTree.grspec in H2. destruct (PTree.elt_eq id0 id); try discriminate. + auto. + destruct EITHER as [[A B] | [A [B [C D]]]]. + (* older blocks *) + rewrite PTree.gso in H3; auto. exploit H; eauto. intros [P [Q R]]. + assert (b0 <> b). eapply Mem.valid_not_valid_diff; eauto with mem. + split. apply Genv.load_store_init_data_invariant with m; auto. + intros. transitivity (Mem.load chunk m3 b0 ofs). eapply Mem.load_drop; eauto. + transitivity (Mem.load chunk m2 b0 ofs). eapply Genv.store_init_data_list_outside; eauto. + transitivity (Mem.load chunk m1 b0 ofs). eapply Genv.store_zeros_outside; eauto. + eapply Mem.load_alloc_unchanged; eauto. + split. red. rewrite NB'. change (Mem.valid_block m1 b0). eauto with mem. + intros; red; intros. elim (R ofs). + eapply Mem.perm_alloc_4; eauto. + rewrite Genv.store_zeros_perm; [idtac|eauto]. + rewrite Genv.store_init_data_list_perm; [idtac|eauto]. + eapply Mem.perm_drop_4; eauto. + (* same block *) + subst id0 il0. rewrite PTree.gss in H3. injection H3; intro EQ; subst b0. + unfold Genv.perm_globvar in Heqo1. + rewrite D in Heqo1. rewrite C in Heqo1. + split. apply Genv.load_store_init_data_invariant with m3. + intros. eapply Mem.load_drop; eauto. do 3 right. auto with mem. + eapply Genv.store_init_data_list_charact; eauto. + split. red. rewrite NB'. change (Mem.valid_block m1 b). eauto with mem. + intros; red; intros. + assert (0 <= ofs < sz). + eapply Mem.perm_alloc_3; eauto. + rewrite Genv.store_zeros_perm; [idtac|eauto]. + rewrite Genv.store_init_data_list_perm; [idtac|eauto]. + eapply Mem.perm_drop_4; eauto. + assert (PO: perm_order Readable Writable). + eapply Mem.perm_drop_2; eauto. + inv PO. + (* nextvar hyp *) + simpl. rewrite NB'. rewrite (Mem.nextblock_alloc _ _ _ _ _ Heqp). + unfold block in *; omega. + (* alloc vars hyp *) + auto. +Qed. + +Theorem mem_match_approx_init: + forall m, Genv.init_mem prog = Some m -> mem_match_approx m. +Proof. + intros. unfold Genv.init_mem in H. + eapply mem_match_approx_alloc_variables; eauto. +(* mem_match_approx on empty list *) + red; intros. rewrite PTree.gempty in H0. discriminate. +(* nextvar *) + rewrite Genv.add_functions_nextvar. auto. +Qed. +********************************) + End ANALYSIS. (** * Correctness of the code transformation *) @@ -132,13 +434,6 @@ End ANALYSIS. (** We now show that the transformed code after constant propagation has the same semantics as the original code. *) -Section PRESERVATION. - -Variable prog: program. -Let tprog := transf_program prog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. @@ -156,24 +451,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 f). + Genv.find_funct tge v = Some (transf_fundef gapp f). Proof. intros. - exact (Genv.find_funct_transf transf_fundef _ _ H). + exact (Genv.find_funct_transf (transf_fundef gapp) _ _ 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 f). + Genv.find_funct_ptr tge b = Some (transf_fundef gapp f). Proof. intros. - exact (Genv.find_funct_ptr_transf transf_fundef _ _ H). + exact (Genv.find_funct_ptr_transf (transf_fundef gapp) _ _ H). Qed. Lemma sig_function_translated: forall f, - funsig (transf_fundef f) = funsig f. + funsig (transf_fundef gapp f) = funsig f. Proof. intros. destruct f; reflexivity. Qed. @@ -209,17 +504,17 @@ Qed. Lemma transf_ros_correct: forall sp ros rs rs' f approx, - regs_match_approx ge sp approx rs -> + regs_match_approx sp approx rs -> find_function ge ros rs = Some f -> regs_lessdef rs rs' -> - find_function tge (transf_ros approx ros) rs' = Some (transf_fundef f). + 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 f)). + 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. @@ -230,6 +525,20 @@ Proof. apply function_ptr_translated; auto. Qed. +Lemma const_for_result_correct: + forall a op sp v 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. + (** The proof of semantic preservation is a simulation argument based on diagrams of the following form: << @@ -259,29 +568,32 @@ 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 ge sp (analyze f)!!pc (rs#res <- v)) -> + (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 f) sp pc rs'). + (Stackframe res (transf_function gapp f) sp pc rs'). Inductive match_states: state -> state -> Prop := | match_states_intro: forall s sp pc rs m f s' rs' m' - (MATCH: regs_match_approx ge sp (analyze f)!!pc rs) + (MATCH: regs_match_approx sp (analyze gapp f)!!pc rs) + (GMATCH: mem_match_approx m) (STACKS: list_forall2 match_stackframes s s') (REGS: regs_lessdef rs rs') (MEM: Mem.extends m m'), match_states (State s f sp pc rs m) - (State s' (transf_function f) sp pc rs' m') + (State s' (transf_function gapp 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 (Callstate s f args m) - (Callstate s' (transf_fundef f) args' m') + (Callstate s' (transf_fundef gapp 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'), @@ -292,7 +604,7 @@ Inductive match_states: state -> state -> Prop := Ltac TransfInstr := match goal with | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ => - cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr)); + cut ((transf_function gapp f).(fn_code)!pc = Some(transf_instr gapp (analyze gapp f)!!pc instr)); [ simpl transf_instr | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; unfold option_map; rewrite H1; reflexivity ] @@ -310,7 +622,7 @@ Proof. induction 1; intros; inv MS. (* Inop *) - exists (State s' (transf_function f) sp pc' rs' m'); split. + exists (State s' (transf_function gapp f) sp pc' rs' m'); split. TransfInstr; intro. eapply exec_Inop; eauto. econstructor; eauto. eapply analyze_correct_1 with (pc := pc); eauto. @@ -318,70 +630,73 @@ Proof. unfold transfer; rewrite H. auto. (* Iop *) - assert (MATCH': regs_match_approx ge sp (analyze f) # pc' rs # res <- v). + TransfInstr. + set (a := eval_static_operation op (approx_regs (analyze gapp f)#pc args)). + 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 (analyze gapp f) # pc' rs # res <- v). eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto. unfold transfer; rewrite H. apply regs_match_approx_update; auto. - eapply eval_static_operation_correct; eauto. - apply approx_regs_val_list; auto. - TransfInstr. - exploit eval_static_operation_correct; eauto. eapply approx_regs_val_list; eauto. intros VM. - destruct (eval_static_operation op (approx_regs (analyze f) # pc args)); intros; simpl in VM. - (* Novalue *) - contradiction. - (* Unknown *) + destruct (const_for_result a) as [cop|]_eqn; intros. + (* constant is propagated *) + exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v) m'); split. + eapply exec_Iop; eauto. + eapply const_for_result_correct; eauto. + econstructor; eauto. + apply set_reg_lessdef; auto. + (* operator is strength-reduced *) exploit op_strength_reduction_correct. eexact MATCH. reflexivity. eauto. - destruct (op_strength_reduction op args (approx_regs (analyze f) # pc args)) as [op' args']. + destruct (op_strength_reduction op args (approx_regs (analyze gapp f) # pc 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. + eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto. destruct EV'' as [v'' [EV'' LD'']]. - exists (State s' (transf_function f) sp pc' (rs'#res <- v'') m'); split. + exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v'') m'); split. econstructor. eauto. rewrite <- EV''. apply eval_operation_preserved. exact symbols_preserved. econstructor; eauto. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. - (* I i *) - subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vint i)) m'); split. - econstructor; eauto. - econstructor; eauto. apply set_reg_lessdef; auto. - (* F *) - subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vfloat f0)) m'); split. - econstructor; eauto. - econstructor; eauto. apply set_reg_lessdef; auto. - (* G *) - subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (symbol_address tge i i0)) m'); split. - econstructor; eauto. - econstructor; eauto. apply set_reg_lessdef; auto. - unfold symbol_address. rewrite symbols_preserved; auto. - (* S *) - subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Val.add sp (Vint i))) m'); split. - econstructor; eauto. - econstructor; eauto. apply set_reg_lessdef; auto. (* Iload *) TransfInstr. - generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs - MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)). - destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args']. - intros P Q. rewrite H0 in P. + 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. + assert (MATCH': regs_match_approx sp (analyze gapp f) # pc' rs # dst <- v). + eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. + destruct (const_for_result ap2) as [cop|]_eqn; intros. + (* constant-propagated *) + exists (State s' (transf_function gapp f) sp pc' (rs'#dst <- v) m'); split. + eapply exec_Iop; eauto. eapply const_for_result_correct; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. + (* strength-reduced *) + generalize (addr_strength_reduction_correct ge sp (analyze gapp f)!!pc rs + MATCH 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]]. - exists (State s' (transf_function f) sp pc' (rs'#dst <- v') m'); split. + exists (State s' (transf_function gapp f) sp pc' (rs'#dst <- v') m'); split. eapply exec_Iload; eauto. econstructor; eauto. - eapply analyze_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. simpl; auto. apply set_reg_lessdef; auto. (* Istore *) TransfInstr. - generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs - MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)). - destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args']. + generalize (addr_strength_reduction_correct ge sp (analyze gapp f)!!pc rs + MATCH 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. @@ -389,11 +704,12 @@ Proof. 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]]. - exists (State s' (transf_function f) sp pc' rs' m2'); split. + exists (State s' (transf_function gapp f) sp pc' rs' m2'); split. eapply exec_Istore; eauto. econstructor; eauto. eapply analyze_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. auto. + eapply mem_match_approx_store; eauto. (* Icall *) exploit transf_ros_correct; eauto. intro FIND'. @@ -413,18 +729,20 @@ Proof. TransfInstr; intro. econstructor; split. eapply exec_Itailcall; eauto. apply sig_function_translated; auto. - constructor; auto. apply regs_lessdef_regs; auto. + constructor; auto. + eapply mem_match_approx_free; eauto. + apply regs_lessdef_regs; auto. (* Ibuiltin *) Opaque builtin_strength_reduction. - destruct (builtin_strength_reduction ef args (approx_regs (analyze f)#pc args)) as [ef' args']_eqn. - generalize (builtin_strength_reduction_correct ge sp (analyze f)!!pc rs - MATCH ef args (approx_regs (analyze f) # pc args) _ _ _ _ (refl_equal _) H0). + destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args']_eqn. + generalize (builtin_strength_reduction_correct ge sp (analyze gapp f)!!pc rs + MATCH ef args (approx_regs (analyze gapp f) # pc args) _ _ _ _ (refl_equal _) H0). rewrite Heqp. intros P. exploit external_call_mem_extends; eauto. instantiate (1 := rs'##args'). apply regs_lessdef_regs; auto. intros [v' [m2' [A [B [C D]]]]]. - exists (State s' (transf_function f) sp pc' (rs'#res <- v') m2'); split. + exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v') m2'); split. eapply exec_Ibuiltin. TransfInstr. rewrite Heqp. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. @@ -432,16 +750,17 @@ Opaque builtin_strength_reduction. eapply analyze_correct_1; 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 *) TransfInstr. - generalize (cond_strength_reduction_correct ge sp (analyze f)#pc rs m - MATCH cond args (approx_regs (analyze f) # pc args) (refl_equal _)). - destruct (cond_strength_reduction cond args (approx_regs (analyze f) # pc args)) as [cond' args']. + generalize (cond_strength_reduction_correct ge sp (analyze gapp f)#pc rs m + MATCH 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']. intros EV1. - exists (State s' (transf_function f) sp (if b then ifso else ifnot) rs' m'); split. - destruct (eval_static_condition cond (approx_regs (analyze f) # pc args)) as []_eqn. + 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)) as []_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. @@ -453,14 +772,14 @@ Opaque builtin_strength_reduction. unfold transfer; rewrite H. auto. (* Ijumptable *) - assert (A: (fn_code (transf_function f))!pc = Some(Ijumptable arg tbl) - \/ (fn_code (transf_function f))!pc = Some(Inop pc')). - TransfInstr. destruct (approx_reg (analyze f) # pc arg) as []_eqn; auto. + 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) as []_eqn; auto. generalize (MATCH 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. - exists (State s' (transf_function f) sp pc' rs' m'); split. + exists (State s' (transf_function gapp f) sp pc' rs' m'); split. destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto. econstructor; eauto. eapply analyze_correct_1; eauto. @@ -472,6 +791,7 @@ Opaque builtin_strength_reduction. 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 *) @@ -482,6 +802,7 @@ Opaque builtin_strength_reduction. eapply exec_function_internal; simpl; eauto. simpl. econstructor; eauto. apply analyze_correct_3; auto. + eapply mem_match_approx_alloc; eauto. apply init_regs_lessdef; auto. (* external function *) @@ -492,6 +813,7 @@ 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 *) inv H3. inv H1. @@ -506,14 +828,16 @@ Lemma transf_initial_states: Proof. intros. inversion H. exploit function_ptr_translated; eauto. intro FIND. - exists (Callstate nil (transf_fundef f) nil m0); split. + exists (Callstate nil (transf_fundef gapp 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. constructor. constructor. apply Mem.extends_refl. + constructor. + eapply mem_match_approx_init; eauto. + constructor. constructor. apply Mem.extends_refl. Qed. Lemma transf_final_states: -- cgit