From 57f18784d1fac0123cdb51ed67ae761100509c1f Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 27 Mar 2014 13:44:24 +0000 Subject: Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of machine registers that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report by D. Dickman whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2435 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Allocproof.v | 264 ++++++++++++++++++++++++--------------------------- 1 file changed, 126 insertions(+), 138 deletions(-) (limited to 'backend/Allocproof.v') diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 4c39fee..bbe9ba3 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -451,7 +451,7 @@ Lemma add_equations_args_lessdef: forall rs ls rl tyl ll e e', add_equations_args rl tyl ll e = Some e' -> satisf rs ls e' -> - Val.has_type_list (rs##rl) tyl -> + Val.has_type_list (rs##rl) (normalize_list tyl) -> Val.lessdef_list (rs##rl) (decode_longs tyl (map ls ll)). Proof. intros until e'. functional induction (add_equations_args rl tyl ll e); simpl; intros. @@ -648,7 +648,7 @@ Lemma loc_unconstrained_satisf: Proof. intros; red; intros. destruct (OrderedEquation.eq_dec q (Eq k r l)). - subst q; simpl. unfold l; rewrite Locmap.gss_reg. auto. + subst q; simpl. unfold l; rewrite Locmap.gss. auto. assert (EqSet.In q (remove_equation (Eq k r l) e)). simpl. ESD.fsetdec. rewrite Locmap.gso. apply H; auto. eapply loc_unconstrained_sound; eauto. @@ -674,7 +674,7 @@ Lemma parallel_assignment_satisf: Proof. intros; red; intros. destruct (OrderedEquation.eq_dec q (Eq k r l)). - subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss_reg; auto. + subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss; auto. assert (EqSet.In q (remove_equation {| ekind := k; ereg := r; eloc := l |} e)). simpl. ESD.fsetdec. exploit reg_loc_unconstrained_sound; eauto. intros [A B]. @@ -702,11 +702,11 @@ Proof. rewrite <- H5 in H2. simpl in H2. InvBooleans. simpl. destruct (OrderedEquation.eq_dec q (Eq Low res l2)). subst q; simpl. rewrite Regmap.gss. - destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg. + destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss. apply Val.loword_lessdef; auto. destruct (OrderedEquation.eq_dec q (Eq High res l1)). subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto. - destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg. + destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss. apply Val.hiword_lessdef; auto. assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. rewrite Regmap.gso. rewrite ! Locmap.gso. auto. @@ -719,7 +719,7 @@ Proof. set (e' := remove_equation {| ekind := Full; ereg := res; eloc := l1 |} e) in *. destruct (OrderedEquation.eq_dec q (Eq Full res l1)). subst q; simpl. rewrite Regmap.gss. - destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg. + destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss. auto. assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec. simpl. rewrite Regmap.gso. rewrite Locmap.gso. auto. @@ -969,6 +969,7 @@ Proof. split. apply eqs_same; auto. auto. Qed. +(* Lemma loc_type_compat_charact: forall env l e q, loc_type_compat env l e = true -> @@ -1008,7 +1009,8 @@ Proof. destruct (rs#r); exact I. eelim Loc.diff_not_eq. eexact A. auto. Qed. - +*) +(* Remark val_lessdef_normalize: forall v v' ty, Val.has_type v ty -> Val.lessdef v v' -> @@ -1016,23 +1018,19 @@ Remark val_lessdef_normalize: Proof. intros. inv H0. rewrite Val.load_result_same; auto. auto. Qed. +*) Lemma subst_loc_satisf: forall env src dst rs ls e e', subst_loc dst src e = Some e' -> - well_typed_move env dst e = true -> + (*well_typed_move env dst e = true ->*) wt_regset env rs -> satisf rs ls e' -> satisf rs (Locmap.set dst (ls src) ls) e. Proof. intros; red; intros. exploit in_subst_loc; eauto. intros [[A B] | [A B]]. - subst dst. rewrite Locmap.gss. - destruct q as [k r l]; simpl in *. - exploit well_typed_move_charact; eauto. - destruct l as [mr | sl ofs ty]; intros. - apply (H2 _ B). - apply val_lessdef_normalize; auto. apply (H2 _ B). + subst dst. rewrite Locmap.gss. apply (H1 _ B). rewrite Locmap.gso; auto. Qed. @@ -1079,22 +1077,18 @@ Proof. Qed. Lemma subst_loc_undef_satisf: - forall env src dst rs ls ml e e', + forall src dst rs ls ml e e', subst_loc dst src e = Some e' -> - well_typed_move env dst e = true -> + (*well_typed_move env dst e = true ->*) can_undef_except dst ml e = true -> - wt_regset env rs -> + (*wt_regset env rs ->*) satisf rs ls e' -> satisf rs (Locmap.set dst (ls src) (undef_regs ml ls)) e. Proof. intros; red; intros. exploit in_subst_loc; eauto. intros [[A B] | [A B]]. subst dst. rewrite Locmap.gss. - destruct q as [k r l]; simpl in *. - exploit well_typed_move_charact; eauto. - destruct l as [mr | sl ofs ty]; intros. - apply (H3 _ B). - apply val_lessdef_normalize; auto. apply (H3 _ B). + destruct q as [k r l]; simpl in *. apply (H1 _ B). rewrite Locmap.gso; auto. rewrite undef_regs_outside. eauto. eapply can_undef_except_sound; eauto. apply Loc.diff_sym; auto. Qed. @@ -1336,27 +1330,27 @@ Qed. (** * Properties of the dataflow analysis *) Lemma analyze_successors: - forall f env bsh an pc bs s e, - analyze f env bsh = Some an -> + forall f bsh an pc bs s e, + analyze f bsh = Some an -> bsh!pc = Some bs -> In s (successors_block_shape bs) -> an!!pc = OK e -> - exists e', transfer f env bsh s an!!s = OK e' /\ EqSet.Subset e' e. + exists e', transfer f bsh s an!!s = OK e' /\ EqSet.Subset e' e. Proof. unfold analyze; intros. exploit DS.fixpoint_allnodes_solution; eauto. - rewrite H2. unfold DS.L.ge. destruct (transfer f env bsh s an#s); intros. + rewrite H2. unfold DS.L.ge. destruct (transfer f bsh s an#s); intros. exists e0; auto. contradiction. Qed. Lemma satisf_successors: - forall f env bsh an pc bs s e rs ls, - analyze f env bsh = Some an -> + forall f bsh an pc bs s e rs ls, + analyze f bsh = Some an -> bsh!pc = Some bs -> In s (successors_block_shape bs) -> an!!pc = OK e -> satisf rs ls e -> - exists e', transfer f env bsh s an!!s = OK e' /\ satisf rs ls e'. + exists e', transfer f bsh s an!!s = OK e' /\ satisf rs ls e'. Proof. intros. exploit analyze_successors; eauto. intros [e' [A B]]. exists e'; split; auto. eapply satisf_incr; eauto. @@ -1366,13 +1360,12 @@ Qed. Inductive transf_function_spec (f: RTL.function) (tf: LTL.function) : Prop := | transf_function_spec_intro: - forall env an mv k e1 e2, - wt_function f env -> - analyze f env (pair_codes f tf) = Some an -> + forall an mv k e1 e2, + analyze f (pair_codes f tf) = Some an -> (LTL.fn_code tf)!(LTL.fn_entrypoint tf) = Some(expand_moves mv (Lbranch (RTL.fn_entrypoint f) :: k)) -> wf_moves mv -> - transfer f env (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 -> - track_moves env mv e1 = Some e2 -> + transfer f (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 -> + track_moves mv e1 = Some e2 -> compat_entry (RTL.fn_params f) (sig_args (RTL.fn_sig f)) (loc_parameters (fn_sig tf)) e2 = true -> can_undef destroyed_at_function_entry e2 = true -> RTL.fn_stacksize f = LTL.fn_stacksize tf -> @@ -1387,36 +1380,33 @@ Proof. unfold transf_function; intros. destruct (type_function f) as [env|] eqn:TY; try discriminate. destruct (regalloc f); try discriminate. - destruct (check_function f f0 env) as [] eqn:?; inv H. + destruct (check_function f f0) as [] eqn:?; inv H. unfold check_function in Heqr. - destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate. + destruct (analyze f (pair_codes f tf)) as [an|] eqn:?; try discriminate. monadInv Heqr. - destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate. + destruct (check_entrypoints_aux f tf x) as [y|] eqn:?; try discriminate. unfold check_entrypoints_aux, pair_entrypoints in Heqo0. MonadInv. exploit extract_moves_sound; eauto. intros [A B]. subst b. exploit check_succ_sound; eauto. intros [k EQ1]. subst b0. - econstructor; eauto. eapply type_function_correct; eauto. congruence. + econstructor; eauto. congruence. Qed. Lemma invert_code: - forall f env tf pc i opte e, - wt_function f env -> + forall f tf pc i opte e, (RTL.fn_code f)!pc = Some i -> - transfer f env (pair_codes f tf) pc opte = OK e -> + transfer f (pair_codes f tf) pc opte = OK e -> exists eafter, exists bsh, exists bb, opte = OK eafter /\ (pair_codes f tf)!pc = Some bsh /\ (LTL.fn_code tf)!pc = Some bb /\ expand_block_shape bsh i bb /\ - transfer_aux f env bsh eafter = Some e /\ - wt_instr f env i. + transfer_aux f bsh eafter = Some e. Proof. - intros. destruct opte as [eafter|]; simpl in H1; try discriminate. exists eafter. + intros. destruct opte as [eafter|]; simpl in H0; try discriminate. exists eafter. destruct (pair_codes f tf)!pc as [bsh|] eqn:?; try discriminate. exists bsh. exploit matching_instr_block; eauto. intros [bb [A B]]. - destruct (transfer_aux f env bsh eafter) as [e1|] eqn:?; inv H1. - exists bb. exploit wt_instr_at; eauto. - tauto. + destruct (transfer_aux f bsh eafter) as [e1|] eqn:?; inv H0. + exists bb. tauto. Qed. (** * Semantic preservation *) @@ -1490,11 +1480,10 @@ Proof. Qed. Lemma exec_moves: - forall mv env rs s f sp bb m e e' ls, - track_moves env mv e = Some e' -> + forall mv rs s f sp bb m e e' ls, + track_moves mv e = Some e' -> wf_moves mv -> satisf rs ls e' -> - wt_regset env rs -> exists ls', star step tge (Block s f sp (expand_moves mv bb) ls m) E0 (Block s f sp bb ls' m) @@ -1506,7 +1495,7 @@ Opaque destroyed_by_op. - unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. auto. (* step *) - destruct a as [src dst]. unfold expand_moves. simpl. - destruct (track_moves env mv e) as [e1|] eqn:?; MonadInv. + destruct (track_moves mv e) as [e1|] eqn:?; MonadInv. assert (wf_moves mv). red; intros. apply H0; auto with coqlib. destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst]. (* reg-reg *) @@ -1532,17 +1521,13 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa sg.(sig_res) = Some Tint -> match_stackframes nil nil sg | match_stackframes_cons: - forall res f sp pc rs s tf bb ls ts sg an e env + forall res f sp pc rs s tf bb ls ts sg an e (STACKS: match_stackframes s ts (fn_sig tf)) (FUN: transf_function f = OK tf) - (ANL: analyze f env (pair_codes f tf) = Some an) - (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e) - (WTF: wt_function f env) - (WTRS: wt_regset env rs) - (WTRES: subtype (proj_sig_res sg) (env res) = true) + (ANL: analyze f (pair_codes f tf) = Some an) + (EQ: transfer f (pair_codes f tf) pc an!!pc = OK e) (STEPS: forall v ls1 m, Val.lessdef_list (encode_long (sig_res sg) v) (map ls1 (map R (loc_result sg))) -> - Val.has_type v (env res) -> agree_callee_save ls ls1 -> exists ls2, star LTL.step tge (Block ts tf sp bb ls1 m) @@ -1555,15 +1540,13 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa Inductive match_states: RTL.state -> LTL.state -> Prop := | match_states_intro: - forall s f sp pc rs m ts tf ls m' an e env + forall s f sp pc rs m ts tf ls m' an e (STACKS: match_stackframes s ts (fn_sig tf)) (FUN: transf_function f = OK tf) - (ANL: analyze f env (pair_codes f tf) = Some an) - (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e) + (ANL: analyze f (pair_codes f tf) = Some an) + (EQ: transfer f (pair_codes f tf) pc an!!pc = OK e) (SAT: satisf rs ls e) - (MEM: Mem.extends m m') - (WTF: wt_function f env) - (WTRS: wt_regset env rs), + (MEM: Mem.extends m m'), match_states (RTL.State s f sp pc rs m) (LTL.State ts tf sp pc ls m') | match_states_call: @@ -1572,8 +1555,7 @@ Inductive match_states: RTL.state -> LTL.state -> Prop := (FUN: transf_fundef f = OK tf) (ARGS: Val.lessdef_list args (decode_longs (sig_args (funsig tf)) (map ls (loc_arguments (funsig tf))))) (AG: agree_callee_save (parent_locset ts) ls) - (MEM: Mem.extends m m') - (WTARGS: Val.has_type_list args (sig_args (funsig tf))), + (MEM: Mem.extends m m'), match_states (RTL.Callstate s f args m) (LTL.Callstate ts tf ls m') | match_states_return: @@ -1581,8 +1563,7 @@ Inductive match_states: RTL.state -> LTL.state -> Prop := (STACKS: match_stackframes s ts sg) (RES: Val.lessdef_list (encode_long (sig_res sg) res) (map ls (map R (loc_result sg)))) (AG: agree_callee_save (parent_locset ts) ls) - (MEM: Mem.extends m m') - (WTRES: Val.has_type res (proj_sig_res sg)), + (MEM: Mem.extends m m'), match_states (RTL.Returnstate s res m) (LTL.Returnstate ts ls m'). @@ -1595,14 +1576,13 @@ Proof. intros. inv H. constructor. congruence. econstructor; eauto. - unfold proj_sig_res in *. rewrite H0; auto. intros. unfold loc_result in H; rewrite H0 in H; eauto. Qed. Ltac UseShape := match goal with - | [ WT: wt_function _ _, CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ _ = OK _ |- _ ] => - destruct (invert_code _ _ _ _ _ _ _ WT CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR & WTI); + | [ CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ = OK _ |- _ ] => + destruct (invert_code _ _ _ _ _ _ CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR); inv EBS; unfold transfer_aux in TR; MonadInv end. @@ -1619,24 +1599,32 @@ Proof. { generalize args (type_of_addressing addr) H0 H1 H5. induction args0; simpl; intros. contradiction. - destruct l. discriminate. InvBooleans. - destruct H2. subst a. - assert (t = Tint) by auto with coqlib. subst t. - destruct (env r); auto || discriminate. + destruct l. discriminate. inv H4. + destruct H2. subst a. apply H3; auto with coqlib. eauto with coqlib. } red; intros; subst r. rewrite H in H8; discriminate. Qed. +Lemma wt_instr_inv: + forall s f sp pc rs m i, + wt_state (RTL.State s f sp pc rs m) -> + f.(RTL.fn_code)!pc = Some i -> + exists env, wt_instr f env i /\ wt_regset env rs. +Proof. + intros. inv H. exists env; split; auto. + inv WT_FN. eauto. +Qed. + (** The proof of semantic preservation is a simulation argument of the "plus" kind. *) Lemma step_simulation: - forall S1 t S2, RTL.step ge S1 t S2 -> + forall S1 t S2, RTL.step ge S1 t S2 -> wt_state S1 -> forall S1', match_states S1 S1' -> exists S2', plus LTL.step tge S1' t S2' /\ match_states S2 S2'. Proof. - induction 1; intros S1' MS; inv MS; try UseShape. + induction 1; intros WT S1' MS; inv MS; try UseShape. (* nop *) exploit exec_moves; eauto. intros [ls1 [X Y]]. @@ -1648,8 +1636,7 @@ Proof. econstructor; eauto. (* op move *) -- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - simpl in H0. inv H0. +- simpl in H0. inv H0. exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -1660,8 +1647,7 @@ Proof. econstructor; eauto. (* op makelong *) -- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - simpl in H0. inv H0. +- simpl in H0. inv H0. exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -1673,8 +1659,7 @@ Proof. econstructor; eauto. (* op lowlong *) -- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - simpl in H0. inv H0. +- simpl in H0. inv H0. exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -1686,8 +1671,7 @@ Proof. econstructor; eauto. (* op highlong *) -- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - simpl in H0. inv H0. +- simpl in H0. inv H0. exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -1699,8 +1683,7 @@ Proof. econstructor; eauto. (* op regular *) -- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. +- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. exploit transfer_use_def_satisf; eauto. intros [X Y]. exploit eval_operation_lessdef; eauto. intros [v' [F G]]. exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. @@ -1724,11 +1707,9 @@ Proof. eapply reg_unconstrained_satisf; eauto. intros [enext [U V]]. econstructor; eauto. - eapply wt_exec_Iop; eauto. (* load regular *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. +- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. exploit transfer_use_def_satisf; eauto. intros [X Y]. exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. exploit Mem.loadv_extends; eauto. intros [v' [P Q]]. @@ -1744,8 +1725,7 @@ Proof. econstructor; eauto. (* load pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. - exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). +- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. @@ -1766,7 +1746,8 @@ Proof. assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')). { replace (rs##args) with ((rs#dst<-v)##args). eapply add_equations_lessdef; eauto. - apply list_map_exten; intros. rewrite Regmap.gso; auto. + apply list_map_exten; intros. rewrite Regmap.gso; auto. + exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). eapply addressing_not_long; eauto. } exploit eval_addressing_lessdef. eexact LD3. @@ -1798,8 +1779,7 @@ Proof. econstructor; eauto. (* load first word of a pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. - exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). +- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. @@ -1829,8 +1809,7 @@ Proof. econstructor; eauto. (* load second word of a pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. - exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). +- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. @@ -1870,7 +1849,6 @@ Proof. eapply reg_unconstrained_satisf; eauto. intros [enext [U V]]. econstructor; eauto. - eapply wt_exec_Iload; eauto. (* store *) - exploit exec_moves; eauto. intros [ls1 [X Y]]. @@ -1950,21 +1928,19 @@ Proof. exploit analyze_successors; eauto. simpl. left; eauto. intros [enext [U V]]. econstructor; eauto. econstructor; eauto. - inv WTI. rewrite SIG. auto. intros. exploit (exec_moves mv2). eauto. eauto. eapply function_return_satisf with (v := v) (ls_before := ls1) (ls_after := ls0); eauto. eapply add_equation_ros_satisf; eauto. eapply add_equations_args_satisf; eauto. congruence. - apply wt_regset_assign; auto. intros [ls2 [A2 B2]]. exists ls2; split. eapply star_right. eexact A2. constructor. traceEq. apply satisf_incr with eafter; auto. rewrite SIG. eapply add_equations_args_lessdef; eauto. - inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. + exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). + inv WTI. rewrite <- H7. apply wt_regset_list; auto. simpl. red; auto. - inv WTI. rewrite SIG. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. (* tailcall *) - set (sg := RTL.funsig fd) in *. @@ -1985,16 +1961,16 @@ Proof. eapply match_stackframes_change_sig; eauto. rewrite SIG. rewrite e0. decEq. destruct (transf_function_inv _ _ FUN); auto. rewrite SIG. rewrite return_regs_arg_values; auto. eapply add_equations_args_lessdef; eauto. - inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. + exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). + inv WTI. rewrite <- H6. apply wt_regset_list; auto. apply return_regs_agree_callee_save. - rewrite SIG. inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. (* builtin *) -- assert (WTRS': wt_regset env (rs#res <- v)) by (eapply wt_exec_Ibuiltin; eauto). - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. +- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. exploit external_call_mem_extends; eauto. eapply add_equations_args_lessdef; eauto. - inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. + exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). + inv WTI. rewrite <- H4. apply wt_regset_list; auto. intros [v' [m'' [F [G [J K]]]]]. assert (E: map ls1 (map R args') = reglist ls1 args'). { unfold reglist. rewrite list_map_compose. auto. } @@ -2024,7 +2000,8 @@ Proof. (* annot *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. exploit external_call_mem_extends; eauto. eapply add_equations_args_lessdef; eauto. - inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. + exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). + inv WTI. simpl in H4. rewrite <- H4. apply wt_regset_list; auto. intros [v' [m'' [F [G [J K]]]]]. assert (v = Vundef). red in H0; inv H0. auto. econstructor; split. @@ -2042,7 +2019,6 @@ Proof. econstructor; eauto. change (destroyed_by_builtin (EF_annot txt typ)) with (@nil mreg). simpl. subst v. assumption. - apply wt_regset_assign; auto. subst v. constructor. (* cond *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. @@ -2074,45 +2050,43 @@ Proof. (* return *) - destruct (transf_function_inv _ _ FUN). - exploit Mem.free_parallel_extends; eauto. rewrite H10. intros [m'' [P Q]]. - inv WTI; MonadInv. - (* without an argument *) -+ exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact A1. - econstructor. eauto. eauto. traceEq. - simpl. econstructor; eauto. - unfold encode_long, loc_result. rewrite <- H11; rewrite H13. simpl; auto. - apply return_regs_agree_callee_save. - constructor. + exploit Mem.free_parallel_extends; eauto. rewrite H9. intros [m'' [P Q]]. + destruct or as [r|]; MonadInv. (* with an argument *) + exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact A1. econstructor. eauto. eauto. traceEq. - simpl. econstructor; eauto. rewrite <- H11. + simpl. econstructor; eauto. rewrite <- H10. replace (map (return_regs (parent_locset ts) ls1) (map R (loc_result (RTL.fn_sig f)))) with (map ls1 (map R (loc_result (RTL.fn_sig f)))). eapply add_equations_res_lessdef; eauto. rewrite !list_map_compose. apply list_map_exten; intros. unfold return_regs. apply pred_dec_true. eapply loc_result_caller_save; eauto. apply return_regs_agree_callee_save. - unfold proj_sig_res. rewrite <- H11; rewrite H13. - eapply Val.has_subtype; eauto. + + (* without an argument *) ++ assert (SG: f.(RTL.fn_sig).(sig_res) = None). + { exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). + inv WTI; auto. } + exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact A1. + econstructor. eauto. eauto. traceEq. + simpl. econstructor; eauto. + unfold encode_long, loc_result. rewrite <- H10. rewrite SG. simpl; auto. + apply return_regs_agree_callee_save. (* internal function *) - monadInv FUN. simpl in *. destruct (transf_function_inv _ _ EQ). - exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H8; apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H7; apply Zle_refl. intros [m'' [U V]]. - assert (WTRS: wt_regset env (init_regs args (fn_params f))). - { apply wt_init_regs. inv H0. eapply Val.has_subtype_list; eauto. congruence. } exploit (exec_moves mv). eauto. eauto. eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto. - rewrite call_regs_param_values. rewrite H9. eexact ARGS. - exact WTRS. + rewrite call_regs_param_values. rewrite H8. eexact ARGS. intros [ls1 [A B]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -2144,15 +2118,13 @@ Proof. exploit list_in_map_inv; eauto. intros [r [A B]]; subst l'. destruct l; simpl; auto. red; intros; subst r0; elim H0. eapply loc_result_caller_save; eauto. - simpl. eapply external_call_well_typed; eauto. (* return *) - inv STACKS. - exploit STEPS; eauto. eapply Val.has_subtype; eauto. intros [ls2 [A B]]. + exploit STEPS; eauto. intros [ls2 [A B]]. econstructor; split. eapply plus_left. constructor. eexact A. traceEq. econstructor; eauto. - apply wt_regset_assign; auto. eapply Val.has_subtype; eauto. Qed. Lemma initial_states_simulation: @@ -2173,7 +2145,6 @@ Proof. rewrite SIG; rewrite H3; simpl; auto. red; auto. apply Mem.extends_refl. - rewrite SIG; rewrite H3; simpl; auto. Qed. Lemma final_states_simulation: @@ -2185,14 +2156,31 @@ Proof. unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. inv H3; auto. Qed. +Lemma wt_prog: wt_program prog. +Proof. + red; intros. exploit transform_partial_program_succeeds; eauto. + intros [tfd TF]. destruct f; simpl in *. +- monadInv TF. unfold transf_function in EQ. + destruct (type_function f) as [env|] eqn:TF; try discriminate. + econstructor. eapply type_function_correct; eauto. +- constructor. +Qed. + Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (LTL.semantics tprog). Proof. - eapply forward_simulation_plus. - eexact symbols_preserved. - eexact initial_states_simulation. - eexact final_states_simulation. - exact step_simulation. + set (ms := fun s s' => wt_state s /\ match_states s s'). + eapply forward_simulation_plus with (match_states := ms). +- exact symbols_preserved. +- intros. exploit initial_states_simulation; eauto. intros [st2 [A B]]. + exists st2; split; auto. split; auto. + apply wt_initial_state with (p := prog); auto. exact wt_prog. +- intros. destruct H. eapply final_states_simulation; eauto. +- intros. destruct H0. + exploit step_simulation; eauto. intros [s2' [A B]]. + exists s2'; split. exact A. split. + eapply subject_reduction; eauto. eexact wt_prog. eexact H. + auto. Qed. End PRESERVATION. -- cgit v1.2.3