From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenspec.v | 76 ++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 68 insertions(+), 8 deletions(-) (limited to 'backend/RTLgenspec.v') diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 22a1e79d..44e7c418 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -504,6 +504,32 @@ 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 @@ -606,7 +632,24 @@ Proof. apply regs_valid_cons; eauto with rtlg. Qed. -Hint Resolve new_reg_target_ok alloc_reg_target_ok alloc_regs_target_ok: rtlg. +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. (** The following predicate is a variant of [target_reg_ok] used to characterize registers that are adequate for holding the return @@ -804,9 +847,14 @@ 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 -> + 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_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 None -> @@ -970,7 +1018,9 @@ Proof. inv OK. left; split; congruence. right; eauto with rtlg. eapply add_move_charact; eauto. (* Eop *) - inv OK. + inv OK. destruct (two_address_op o). + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. (* Eload *) @@ -1047,21 +1097,25 @@ 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)), + (OK: reg_map_ok map rd (Some id)) + (NOT2ADDR: expr_is_2addr_op a = false), 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 *) - econstructor; eauto with rtlg. + 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. eapply transl_condexpr_charact; eauto with rtlg. apply tr_expr_incr with s1; auto. @@ -1069,6 +1123,7 @@ Proof. apply tr_expr_incr with s0; 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. @@ -1112,8 +1167,9 @@ Proof. intros s1 s2 EXT. 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; econstructor; eauto. - eapply tr_switch_incr; eauto. + induction 1; try (econstructor; eauto; fail). + eapply tr_Sassign_2; eauto. eapply tr_move_incr; eauto. + econstructor; eauto. eapply tr_switch_incr; eauto. Qed. Lemma transl_exit_charact: @@ -1181,7 +1237,11 @@ Proof. constructor. (* Sassign *) revert EQ. unfold find_var. case_eq (map_vars map)!i; intros; monadInv EQ. - econstructor. eauto. + 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. (* Sstore *) -- cgit