From 0cb770c9d2dcad16afdd8129558e356f31202803 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 2 May 2010 07:43:49 +0000 Subject: In compilation of Sassign, avoid systematic move from a fresh temp. Those moves are not always coalesced during coloring. The resulting smaller RTL code also reduces the load on the rest of the back-end. RTLgenspec.v: use spiffy saturateTrans tactic to speed up proof search. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1330 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenspec.v | 224 ++++++++++++++++++++++++++++++++++----------------- 1 file changed, 152 insertions(+), 72 deletions(-) (limited to 'backend/RTLgenspec.v') diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 51fb945e..5690bb29 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -132,6 +132,8 @@ Ltac monadInv H := (** * Monotonicity properties of the state *) +Hint Resolve state_incr_refl: rtlg. + Lemma instr_at_incr: forall s1 s2 n i, state_incr s1 s2 -> s1.(st_code)!n = Some i -> s2.(st_code)!n = Some i. @@ -141,7 +143,23 @@ Proof. Qed. Hint Resolve instr_at_incr: rtlg. -Hint Resolve state_incr_refl state_incr_trans: rtlg. +(** The following tactic saturates the hypotheses with + [state_incr] properties that follow by transitivity from + the known hypotheses. *) + +Ltac saturateTrans := + match goal with + | H1: state_incr ?x ?y, H2: state_incr ?y ?z |- _ => + match goal with + | H: state_incr x z |- _ => + fail 1 + | _ => + let i := fresh "INCR" in + (generalize (state_incr_trans x y z H1 H2); intro i; + saturateTrans) + end + | _ => idtac + end. (** * Validity and freshness of registers *) @@ -619,49 +637,69 @@ Inductive tr_move (c: code): c!ns = Some (Iop Omove (rs :: nil) rd nd) -> tr_move c ns rs nd rd. -(** [tr_expr c map pr expr ns nd rd] holds if the graph [c], +(** [reg_map_ok map r optid] characterizes the destination register + for an expression: if [optid] is [None], the destination is + a fresh register (not associated with any variable); + if [optid] is [Some id], the destination is the register + associated with local variable [id]. *) + +Inductive reg_map_ok: mapping -> reg -> option ident -> Prop := + | reg_map_ok_novar: forall map rd, + ~reg_in_map map rd -> + reg_map_ok map rd None + | reg_map_ok_somevar: forall map rd id, + map.(map_vars)!id = Some rd -> + reg_map_ok map rd (Some id). + +Hint Resolve reg_map_ok_novar: rtlg. + +(** [tr_expr c map pr expr ns nd rd optid] holds if the graph [c], between nodes [ns] and [nd], contains instructions that compute the value of the Cminor expression [expr] and deposit this value in register [rd]. [map] is a mapping from Cminor variables to the corresponding RTL registers. [pr] is a list of RTL registers whose values must be preserved during this computation. All registers mentioned in [map] must also be preserved during this computation. - To ensure this, we demand that the result registers of the instructions - appearing on the path from [ns] to [nd] are neither in [pr] nor in [map]. + (Exception: if [optid = Some id], the register associated with + local variable [id] can be assigned, but only at the end of the + expression evaluation.) + To ensure this property, we demand that the result registers of the + instructions appearing on the path from [ns] to [nd] are not in [pr], + and moreover that they satisfy the [reg_map_ok] predicate. *) Inductive tr_expr (c: code): - mapping -> list reg -> expr -> node -> node -> reg -> Prop := - | tr_Evar: forall map pr id ns nd r rd, + mapping -> list reg -> expr -> node -> node -> reg -> option ident -> Prop := + | tr_Evar: forall map pr id ns nd r rd dst, map.(map_vars)!id = Some r -> - (rd = r \/ ~reg_in_map map rd /\ ~In rd pr) -> + ((rd = r /\ dst = None) \/ (reg_map_ok map rd dst /\ ~In rd pr)) -> tr_move c ns r nd rd -> - tr_expr c map pr (Evar id) ns nd rd - | tr_Eop: forall map pr op al ns nd rd n1 rl, + tr_expr c map pr (Evar id) ns nd rd dst + | tr_Eop: forall map pr op al ns nd rd n1 rl dst, tr_exprlist c map pr al ns n1 rl -> c!n1 = Some (Iop op rl rd nd) -> - ~reg_in_map map rd -> ~In rd pr -> - tr_expr c map pr (Eop op al) ns nd rd - | tr_Eload: forall map pr chunk addr al ns nd rd n1 rl, + reg_map_ok map rd dst -> ~In rd pr -> + tr_expr c map pr (Eop op al) ns nd rd dst + | tr_Eload: forall map pr chunk addr al ns nd rd n1 rl dst, tr_exprlist c map pr al ns n1 rl -> c!n1 = Some (Iload chunk addr rl rd nd) -> - ~reg_in_map map rd -> ~In rd pr -> - tr_expr c map pr (Eload chunk addr al) ns nd rd - | tr_Econdition: forall map pr b ifso ifnot ns nd rd ntrue nfalse, + reg_map_ok map rd dst -> ~In rd pr -> + tr_expr c map pr (Eload chunk addr al) ns nd rd dst + | tr_Econdition: forall map pr b ifso ifnot ns nd rd ntrue nfalse dst, tr_condition c map pr b ns ntrue nfalse -> - tr_expr c map pr ifso ntrue nd rd -> - tr_expr c map pr ifnot nfalse nd rd -> - tr_expr c map pr (Econdition b ifso ifnot) ns nd rd - | tr_Elet: forall map pr b1 b2 ns nd rd n1 r, + tr_expr c map pr ifso ntrue nd rd dst -> + tr_expr c map pr ifnot nfalse nd rd dst -> + tr_expr c map pr (Econdition b ifso ifnot) ns nd rd dst + | tr_Elet: forall map pr b1 b2 ns nd rd n1 r dst, ~reg_in_map map r -> - tr_expr c map pr b1 ns n1 r -> - tr_expr c (add_letvar map r) pr b2 n1 nd rd -> - tr_expr c map pr (Elet b1 b2) ns nd rd - | tr_Eletvar: forall map pr n ns nd rd r, + tr_expr c map pr b1 ns n1 r None -> + tr_expr c (add_letvar map r) pr b2 n1 nd rd dst -> + tr_expr c map pr (Elet b1 b2) ns nd rd dst + | tr_Eletvar: forall map pr n ns nd rd r dst, List.nth_error map.(map_letvars) n = Some r -> - (rd = r \/ ~reg_in_map map rd /\ ~In rd pr) -> + ((rd = r /\ dst = None) \/ (reg_map_ok map rd dst /\ ~In rd pr)) -> tr_move c ns r nd rd -> - tr_expr c map pr (Eletvar n) ns nd rd + tr_expr c map pr (Eletvar n) ns nd rd dst (** [tr_condition c map pr cond ns ntrue nfalse rd] holds if the graph [c], starting at node [ns], contains instructions that compute the truth @@ -694,7 +732,7 @@ with tr_exprlist (c: code): | tr_Enil: forall map pr n, tr_exprlist c map pr Enil n n nil | tr_Econs: forall map pr a1 al ns nd r1 rl n1, - tr_expr c map pr a1 ns n1 r1 -> + tr_expr c map pr a1 ns n1 r1 None -> tr_exprlist c map (r1 :: pr) al n1 nd rl -> tr_exprlist c map pr (Econs a1 al) ns nd (r1 :: rl). @@ -757,24 +795,24 @@ Inductive tr_stmt (c: code) (map: mapping): stmt -> node -> node -> list node -> labelmap -> node -> option reg -> Prop := | tr_Sskip: forall ns nexits ngoto nret rret, tr_stmt c map Sskip ns ns nexits ngoto nret rret - | tr_Sassign: forall id a ns nd nexits ngoto nret rret rt n, - tr_expr c map nil a ns n rt -> - tr_store_var c map rt id n nd -> + | tr_Sassign: forall id a ns nd nexits ngoto nret rret r, + map.(map_vars)!id = Some r -> + tr_expr c map nil a ns nd r (Some id) -> tr_stmt c map (Sassign id a) ns nd nexits ngoto nret rret | tr_Sstore: forall chunk addr al b ns nd nexits ngoto nret rret rd n1 rl n2, tr_exprlist c map nil al ns n1 rl -> - tr_expr c map rl b n1 n2 rd -> + tr_expr c map rl b n1 n2 rd None -> c!n2 = Some (Istore chunk addr rl rd nd) -> tr_stmt c map (Sstore chunk addr al b) ns nd nexits ngoto nret rret | tr_Scall: forall optid sig b cl ns nd nexits ngoto nret rret rd n1 rf n2 n3 rargs, - tr_expr c map nil b ns n1 rf -> + tr_expr c map nil b ns n1 rf None -> tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> c!n2 = Some (Icall sig (inl _ rf) rargs rd n3) -> tr_store_optvar c map rd optid n3 nd -> ~reg_in_map map rd -> tr_stmt c map (Scall optid sig b cl) ns nd nexits ngoto nret rret | tr_Stailcall: forall sig b cl ns nd nexits ngoto nret rret n1 rf n2 rargs, - tr_expr c map nil b ns n1 rf -> + tr_expr c map nil b ns n1 rf None -> tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> c!n2 = Some (Itailcall sig (inl _ rf) rargs) -> tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret @@ -799,13 +837,13 @@ Inductive tr_stmt (c: code) (map: mapping): tr_stmt c map (Sexit n) ns nd nexits ngoto nret rret | tr_Sswitch: forall a cases default ns nd nexits ngoto nret rret n r t, validate_switch default cases t = true -> - tr_expr c map nil a ns n r -> + tr_expr c map nil a ns n r None -> tr_switch c map r nexits t n -> tr_stmt c map (Sswitch a cases default) ns nd nexits ngoto nret rret | tr_Sreturn_none: forall nret nd nexits ngoto, tr_stmt c map (Sreturn None) nret nd nexits ngoto nret None | tr_Sreturn_some: forall a ns nd nexits ngoto nret rret, - tr_expr c map nil a ns nret rret -> + tr_expr c map nil a ns nret rret None -> tr_stmt c map (Sreturn (Some a)) ns nd nexits ngoto nret (Some rret) | tr_Slabel: forall lbl s ns nd nexits ngoto nret rret n, ngoto!lbl = Some n -> @@ -850,9 +888,9 @@ Qed. Lemma tr_expr_incr: forall s1 s2, state_incr s1 s2 -> - forall map pr a ns nd rd, - tr_expr s1.(st_code) map pr a ns nd rd -> - tr_expr s2.(st_code) map pr a ns nd rd + forall map pr a ns nd rd dst, + tr_expr s1.(st_code) map pr a ns nd rd dst -> + tr_expr s2.(st_code) map pr a ns nd rd dst with tr_condition_incr: forall s1 s2, state_incr s1 s2 -> forall map pr a ns ntrue nfalse, @@ -894,7 +932,7 @@ Lemma transl_expr_charact: (OK: target_reg_ok map pr a rd) (VALID: regs_valid pr s) (VALID2: reg_valid rd s), - tr_expr s'.(st_code) map pr a ns nd rd + tr_expr s'.(st_code) map pr a ns nd rd None with transl_condexpr_charact: forall a map ntrue nfalse s ns s' pr INCR @@ -913,11 +951,11 @@ with transl_exprlist_charact: tr_exprlist s'.(st_code) map pr al ns nd rl. Proof. - induction a; intros; try (monadInv TR). + induction a; intros; try (monadInv TR); saturateTrans. (* Evar *) generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1. econstructor; eauto. - inv OK. left; congruence. right; eauto. + inv OK. left; split; congruence. right; eauto with rtlg. eapply add_move_charact; eauto. (* Eop *) inv OK. @@ -930,15 +968,14 @@ Proof. (* Econdition *) inv OK. econstructor; eauto with rtlg. - eapply transl_condexpr_charact; eauto with rtlg. apply tr_expr_incr with s1; auto. - eapply transl_expr_charact; eauto with rtlg. constructor; auto. + eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. apply tr_expr_incr with s0; auto. - eapply transl_expr_charact; eauto with rtlg. constructor; auto. + eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. (* Elet *) inv OK. econstructor. eapply new_reg_not_in_map; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. + eapply transl_expr_charact; eauto 3 with rtlg. apply tr_expr_incr with s1; auto. eapply transl_expr_charact. eauto. apply add_letvar_valid; eauto with rtlg. @@ -952,12 +989,12 @@ Proof. generalize EQ; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros; inv EQ0. monadInv EQ1. econstructor; eauto with rtlg. - inv OK. left; congruence. right; eauto. + inv OK. left; split; congruence. right; eauto with rtlg. eapply add_move_charact; eauto. monadInv EQ1. (* Conditions *) - induction a; intros; try (monadInv TR). + induction a; intros; try (monadInv TR); saturateTrans. (* CEtrue *) constructor. @@ -976,7 +1013,7 @@ Proof. (* Lists *) - induction al; intros; try (monadInv TR). + induction al; intros; try (monadInv TR); saturateTrans. (* Enil *) destruct rl; inv TR. constructor. @@ -991,6 +1028,49 @@ Proof. red; intros; apply VALID2; auto with coqlib. Qed. +(** A variant of [transl_expr_charact], for use when the destination + register is the one associated with a variable. *) + +Lemma transl_expr_assign_charact: + forall id a map rd nd s ns s' INCR + (TR: transl_expr map a rd nd s = OK ns s' INCR) + (WF: map_valid map s) + (OK: reg_map_ok map rd (Some id)), + tr_expr s'.(st_code) map nil a ns nd rd (Some id). +Proof. + induction a; intros; monadInv TR; saturateTrans. + (* Evar *) + generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1. + econstructor; eauto. + eapply add_move_charact; eauto. + (* Eop *) + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. + (* Eload *) + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. + (* Econdition *) + econstructor; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. + apply tr_expr_incr with s1; auto. + eapply IHa1; eauto 2 with rtlg. + apply tr_expr_incr with s0; auto. + eapply IHa2; eauto 2 with rtlg. + (* Elet *) + econstructor. eapply new_reg_not_in_map; eauto with rtlg. + eapply transl_expr_charact; eauto 3 with rtlg. + apply tr_expr_incr with s1; auto. + eapply IHa2; eauto. + apply add_letvar_valid; eauto with rtlg. + inv OK. constructor. auto. + (* Eletvar *) + generalize EQ; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros; inv EQ0. + monadInv EQ1. + econstructor; eauto with rtlg. + eapply add_move_charact; eauto. + monadInv EQ1. +Qed. + Lemma tr_store_var_incr: forall s1 s2, state_incr s1 s2 -> forall map rs id ns nd, @@ -1084,17 +1164,18 @@ Lemma transl_switch_charact: transl_switch r nexits t s = OK ns s' incr -> tr_switch s'.(st_code) map r nexits t ns. Proof. - induction t; simpl; intros. + induction t; simpl; intros; saturateTrans. + exploit transl_exit_charact; eauto. intros [A B]. econstructor; eauto. monadInv H1. exploit transl_exit_charact; eauto. intros [A B]. subst s1. - econstructor; eauto with rtlg. + econstructor; eauto 2 with rtlg. apply tr_switch_incr with s0; eauto with rtlg. monadInv H1. - econstructor; eauto with rtlg. + econstructor; eauto 2 with rtlg. apply tr_switch_incr with s1; eauto with rtlg. apply tr_switch_incr with s0; eauto with rtlg. @@ -1115,39 +1196,38 @@ Lemma transl_stmt_charact: (OK: return_reg_ok s map rret), tr_stmt s'.(st_code) map stmt ns nd nexits ngoto nret rret. Proof. - induction stmt; intros; simpl in TR; try (monadInv TR). + induction stmt; intros; simpl in TR; try (monadInv TR); saturateTrans. (* Sskip *) constructor. (* Sassign *) - econstructor. eapply transl_expr_charact; eauto with rtlg. - apply tr_store_var_incr with s1; auto with rtlg. - eapply store_var_charact; eauto. + revert EQ. unfold find_var. case_eq (map_vars map)!i; intros; monadInv EQ. + econstructor. eauto. + eapply transl_expr_assign_charact; eauto with rtlg. + constructor. auto. (* Sstore *) econstructor; eauto with rtlg. - eapply transl_exprlist_charact; eauto with rtlg. - apply tr_expr_incr with s3; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. + eapply transl_exprlist_charact; eauto 3 with rtlg. + apply tr_expr_incr with s3; auto. + eapply transl_expr_charact; eauto 4 with rtlg. (* Scall *) - assert (state_incr s0 s2) by eauto with rtlg. - assert (state_incr s2 s4) by eauto with rtlg. - assert (state_incr s4 s6) by eauto with rtlg. - econstructor; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. + econstructor; eauto 4 with rtlg. + eapply transl_expr_charact; eauto 3 with rtlg. apply tr_exprlist_incr with s6. auto. - eapply transl_exprlist_charact; eauto with rtlg. - eapply alloc_regs_target_ok with (s1 := s1); eauto with rtlg. - apply regs_valid_cons; eauto with rtlg. - apply regs_valid_incr with s1; eauto with rtlg. - apply regs_valid_cons; eauto with rtlg. - apply tr_store_optvar_incr with s4; eauto with rtlg. + eapply transl_exprlist_charact; eauto 3 with rtlg. + eapply alloc_regs_target_ok with (s1 := s1); eauto 3 with rtlg. + apply regs_valid_cons; eauto 3 with rtlg. + apply regs_valid_incr with s1; eauto 3 with rtlg. + apply regs_valid_cons; eauto 3 with rtlg. + apply regs_valid_incr with s2; eauto 3 with rtlg. + apply tr_store_optvar_incr with s4; auto. eapply store_optvar_charact; eauto with rtlg. (* Stailcall *) assert (RV: regs_valid (x :: nil) s1). - apply regs_valid_cons; eauto with rtlg. - econstructor; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. + apply regs_valid_cons; eauto 3 with rtlg. + econstructor; eauto 3 with rtlg. + eapply transl_expr_charact; eauto 3 with rtlg. apply tr_exprlist_incr with s4; auto. - eapply transl_exprlist_charact; eauto with rtlg. + eapply transl_exprlist_charact; eauto 4 with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. -- cgit