From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenspec.v | 92 +++++++++++++++++----------------------------------- 1 file changed, 29 insertions(+), 63 deletions(-) (limited to 'backend/RTLgenspec.v') diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index c50c7023..d8d5dc8c 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -500,32 +500,6 @@ Proof. right; eauto with rtlg. Qed. -Lemma alloc_regs_2addr_valid: - forall al rd s1 s2 map rl i, - map_valid map s1 -> - reg_valid rd s1 -> - alloc_regs_2addr map al rd s1 = OK rl s2 i -> - regs_valid rl s2. -Proof. - unfold alloc_regs_2addr; intros. - destruct al; monadInv H1. - apply regs_valid_nil. - apply regs_valid_cons. eauto with rtlg. eauto with rtlg. -Qed. -Hint Resolve alloc_regs_2addr_valid: rtlg. - -Lemma alloc_regs_2addr_fresh_or_in_map: - forall map al rd s rl s' i, - map_valid map s -> - alloc_regs_2addr map al rd s = OK rl s' i -> - forall r, In r rl -> r = rd \/ reg_in_map map r \/ reg_fresh r s. -Proof. - unfold alloc_regs_2addr; intros. - destruct al; monadInv H0. - elim H1. - simpl in H1; destruct H1. auto. right. eapply alloc_regs_fresh_or_in_map; eauto. -Qed. - (** A register is an adequate target for holding the value of an expression if - either the register is associated with a Cminor let-bound variable @@ -628,24 +602,8 @@ Proof. apply regs_valid_cons; eauto with rtlg. Qed. -Lemma alloc_regs_2addr_target_ok: - forall map al rd pr s1 rl s2 i, - map_valid map s1 -> - regs_valid pr s1 -> - reg_valid rd s1 -> - ~(reg_in_map map rd) -> ~In rd pr -> - alloc_regs_2addr map al rd s1 = OK rl s2 i -> - target_regs_ok map pr al rl. -Proof. - unfold alloc_regs_2addr; intros. destruct al; monadInv H4. - constructor. - constructor. constructor; auto. - eapply alloc_regs_target_ok; eauto. - apply regs_valid_cons; auto. -Qed. - Hint Resolve new_reg_target_ok alloc_reg_target_ok - alloc_regs_target_ok alloc_regs_2addr_target_ok: rtlg. + alloc_regs_target_ok: rtlg. (** The following predicate is a variant of [target_reg_ok] used to characterize registers that are adequate for holding the return @@ -760,6 +718,17 @@ Inductive tr_expr (c: code): ((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 dst + | tr_Ebuiltin: forall map pr ef al ns nd rd dst n1 rl, + tr_exprlist c map pr al ns n1 rl -> + c!n1 = Some (Ibuiltin ef rl rd nd) -> + reg_map_ok map rd dst -> ~In rd pr -> + tr_expr c map pr (Ebuiltin ef al) ns nd rd dst + | tr_Eexternal: forall map pr id sg al ns nd rd dst n1 rl, + tr_exprlist c map pr al ns n1 rl -> + c!n1 = Some (Icall sg (inr _ id) rl rd nd) -> + reg_map_ok map rd dst -> ~In rd pr -> + tr_expr c map pr (Eexternal id sg al) ns nd rd dst + (** [tr_condition c map pr cond al ns ntrue nfalse rd] holds if the graph [c], starting at node [ns], contains instructions that compute the truth @@ -834,13 +803,8 @@ Inductive tr_stmt (c: code) (map: mapping): | 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 r, - map.(map_vars)!id = Some r -> expr_is_2addr_op a = false -> - 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_Sassign_2: forall id a ns n1 nd nexits ngoto nret rret rd r, map.(map_vars)!id = Some r -> - tr_expr c map nil a ns n1 rd None -> - tr_move c n1 rd nd 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 -> @@ -1008,9 +972,7 @@ Proof. inv OK. left; split; congruence. right; eauto with rtlg. eapply add_move_charact; eauto. (* Eop *) - inv OK. destruct (two_address_op o). - econstructor; eauto with rtlg. - eapply transl_exprlist_charact; eauto with rtlg. + inv OK. econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. (* Eload *) @@ -1045,6 +1007,14 @@ Proof. inv OK. left; split; congruence. right; eauto with rtlg. eapply add_move_charact; eauto. monadInv EQ1. + (* Ebuiltin *) + inv OK. + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. + (* Eexternal *) + inv OK. + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. (* Lists *) @@ -1070,25 +1040,21 @@ 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)) - (NOT2ADDR: expr_is_2addr_op a = false), + (OK: reg_map_ok map rd (Some id)), tr_expr s'.(st_code) map nil a ns nd rd (Some id). Proof. -Opaque two_address_op. 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 *) - simpl in NOT2ADDR. rewrite NOT2ADDR in EQ. econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. (* Eload *) econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. (* Econdition *) - simpl in NOT2ADDR. destruct (orb_false_elim _ _ NOT2ADDR). econstructor; eauto with rtlg. econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. apply tr_expr_incr with s2; auto. @@ -1096,7 +1062,6 @@ Opaque two_address_op. apply tr_expr_incr with s1; auto. eapply IHa2; eauto 2 with rtlg. (* Elet *) - simpl in NOT2ADDR. 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. @@ -1109,6 +1074,12 @@ Opaque two_address_op. econstructor; eauto with rtlg. eapply add_move_charact; eauto. monadInv EQ1. + (* Ebuiltin *) + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. + (* Eexternal *) + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. Qed. Lemma alloc_optreg_map_ok: @@ -1141,7 +1112,6 @@ Proof. generalize tr_expr_incr tr_condition_incr tr_exprlist_incr; intros I1 I2 I3. pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). induction 1; try (econstructor; eauto; fail). - eapply tr_Sassign_2; eauto. eapply tr_move_incr; eauto. econstructor; eauto. eapply tr_switch_incr; eauto. Qed. @@ -1210,10 +1180,6 @@ Proof. constructor. (* Sassign *) revert EQ. unfold find_var. case_eq (map_vars map)!i; intros; monadInv EQ. - remember (expr_is_2addr_op e) as is2a. destruct is2a. - monadInv EQ0. eapply tr_Sassign_2; eauto. - eapply transl_expr_charact; eauto with rtlg. - apply tr_move_incr with s1; auto. eapply add_move_charact; eauto. eapply tr_Sassign; eauto. eapply transl_expr_assign_charact; eauto with rtlg. constructor. auto. -- cgit