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/Stackingproof.v | 143 ++++++++++++++++++++++++++++++++---------------- 1 file changed, 97 insertions(+), 46 deletions(-) (limited to 'backend/Stackingproof.v') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 68d179a..5b06c71 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -32,6 +32,7 @@ Require Import Events. Require Import Globalenvs. Require Import Smallstep. Require Import Locations. +Require LTL. Require Import Linear. Require Import Lineartyping. Require Import Mach. @@ -575,6 +576,58 @@ Proof. intros. rewrite get_set_index_val_other; eauto with stacking. red; auto. Qed. +Lemma agree_undef_regs: + forall rl ls ls0 rs fr cs, + agree ls ls0 rs fr cs -> + (forall r, In r rl -> In (R r) temporaries) -> + agree (Locmap.undef (List.map R rl) ls) ls0 (undef_regs rl rs) fr cs. +Proof. + induction rl; intros; simpl. + auto. + eapply IHrl; eauto. + apply agree_set_reg; auto with coqlib. + assert (In (R a) temporaries) by auto with coqlib. + red. destruct (mreg_type a). + destruct (zlt (index_int_callee_save a) 0). + generalize (bound_int_callee_save_pos b). omega. + elim (int_callee_save_not_destroyed a). auto. apply index_int_callee_save_pos2; auto. + destruct (zlt (index_float_callee_save a) 0). + generalize (bound_float_callee_save_pos b). omega. + elim (float_callee_save_not_destroyed a). auto. apply index_float_callee_save_pos2; auto. + intros. apply H0. auto with coqlib. +Qed. + +Lemma agree_undef_temps: + forall ls ls0 rs fr cs, + agree ls ls0 rs fr cs -> + agree (LTL.undef_temps ls) ls0 (Mach.undef_temps rs) fr cs. +Proof. + intros. unfold undef_temps, LTL.undef_temps. + change temporaries with (List.map R (int_temporaries ++ float_temporaries)). + apply agree_undef_regs; auto. + intros. + change temporaries with (List.map R (int_temporaries ++ float_temporaries)). + apply List.in_map. auto. +Qed. + +Lemma agree_undef_op: + forall op env ls ls0 rs fr cs, + agree ls ls0 rs fr cs -> + agree (Linear.undef_op op ls) ls0 (Mach.undef_op (transl_op env op) rs) fr cs. +Proof. + intros. exploit agree_undef_temps; eauto. intro. + destruct op; simpl; auto. +Qed. + +Lemma agree_undef_getparam: + forall ls ls0 rs fr cs, + agree ls ls0 rs fr cs -> + agree (Locmap.set (R IT1) Vundef ls) ls0 (rs#IT1 <- Vundef) fr cs. +Proof. + intros. exploit (agree_undef_regs (IT1 :: nil)); eauto. + simpl; intros. intuition congruence. +Qed. + Lemma agree_return_regs: forall ls ls0 rs fr cs rs', agree ls ls0 rs fr cs -> @@ -831,9 +884,10 @@ Proof. intros until idx. destruct idx; simpl; auto. congruence. apply incl_refl. apply float_callee_save_norepet. eauto. - intros [fr' [A [B C]]]. - exists fr'; intuition. unfold save_callee_save_float; eauto. - apply C. auto. intros; subst idx. auto. + intros [fr' [A [B C]]]. + exists fr'. split. unfold save_callee_save_float; eauto. + split. auto. + intros. apply C. auto. intros; subst. red; intros; subst idx. contradiction. Qed. Lemma save_callee_save_correct: @@ -1216,24 +1270,15 @@ Qed. Definition shift_sp (tf: Mach.function) (sp: val) := Val.add sp (Vint (Int.repr (-tf.(fn_framesize)))). -Remark shift_offset_sp: - forall f tf sp n v, +Remark shift_sp_eq: + forall f tf sp, transf_function f = OK tf -> - offset_sp sp n = Some v -> - offset_sp (shift_sp tf sp) - (Int.add (Int.repr (fe_size (make_env (function_bounds f)))) n) = Some v. + shift_sp tf sp = Val.sub sp (Vint (Int.repr (fe_size (make_env (function_bounds f))))). Proof. - intros. destruct sp; try discriminate. - unfold offset_sp in *. - unfold shift_sp. - rewrite (unfold_transf_function _ _ H). unfold fn_framesize. - unfold Val.add. rewrite <- Int.neg_repr. - set (p := Int.repr (fe_size (make_env (function_bounds f)))). - inversion H0. decEq. decEq. - rewrite Int.add_assoc. decEq. - rewrite <- Int.add_assoc. - rewrite (Int.add_commut (Int.neg p) p). rewrite Int.add_neg_zero. - rewrite Int.add_commut. apply Int.add_zero. + intros. unfold shift_sp. + replace (fe_size (make_env (function_bounds f))) with (fn_framesize tf). + rewrite <- Int.neg_repr. destruct sp; simpl; auto; rewrite Int.sub_add_opp; auto. + rewrite (unfold_transf_function _ _ H). auto. Qed. Lemma shift_eval_operation: @@ -1243,10 +1288,10 @@ Lemma shift_eval_operation: eval_operation tge (shift_sp tf sp) (transl_op (make_env (function_bounds f)) op) args = Some v. Proof. - intros until v. destruct op; intros; auto. - simpl in *. rewrite symbols_preserved. auto. - destruct args; auto. unfold eval_operation in *. unfold transl_op. - apply shift_offset_sp; auto. + intros. rewrite <- H0. rewrite (shift_sp_eq f tf sp H). unfold transl_op. + rewrite (eval_operation_preserved ge tge). + apply shift_stack_eval_operation. + exact symbols_preserved. Qed. Lemma shift_eval_addressing: @@ -1257,11 +1302,10 @@ Lemma shift_eval_addressing: (transl_addr (make_env (function_bounds f)) addr) args = Some v. Proof. - intros. - unfold transl_addr, eval_addressing in *; - destruct addr; try (rewrite symbols_preserved); auto. - destruct args; try discriminate. - apply shift_offset_sp; auto. + intros. rewrite <- H0. rewrite (shift_sp_eq f tf sp H). unfold transl_addr. + rewrite (eval_addressing_preserved ge tge). + apply shift_stack_eval_addressing. + exact symbols_preserved. Qed. (** Preservation of the arguments to an external call. *) @@ -1389,23 +1433,29 @@ Proof. intro BOUND; simpl in BOUND); unfold transl_instr. (* Lgetstack *) - inv WTI. destruct BOUND. - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) - (rs0#r <- (rs (S sl))) fr m). - split. destruct sl. + inv WTI. destruct BOUND. unfold undef_getstack; destruct sl. (* Lgetstack, local *) + exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) + (rs0#r <- (rs (S (Local z t)))) fr m); split. apply plus_one. apply exec_Mgetstack. apply get_slot_index. auto. apply index_local_valid. auto. congruence. congruence. auto. eapply agree_locals; eauto. + econstructor; eauto with coqlib. + apply agree_set_reg; auto. (* Lgetstack, incoming *) - apply plus_one; apply exec_Mgetparam. + exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) + (rs0 # IT1 <- Vundef # r <- (rs (S (Incoming z t)))) fr m); split. + apply plus_one. apply exec_Mgetparam. change (get_parent_slot ts z t (rs (S (Incoming z t)))). eapply agree_incoming; eauto. + econstructor; eauto with coqlib. + apply agree_set_reg; auto. apply agree_undef_getparam; auto. (* Lgetstack, outgoing *) - apply plus_one; apply exec_Mgetstack. - apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto. + exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) + (rs0#r <- (rs (S (Outgoing z t)))) fr m); split. + apply plus_one. apply exec_Mgetstack. + apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto. eapply agree_outgoing; eauto. - (* Lgetstack, common *) econstructor; eauto with coqlib. apply agree_set_reg; auto. @@ -1432,22 +1482,23 @@ Proof. symmetry. eapply agree_reg; eauto. (* Lop *) - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) (rs0#res <- v) fr m); split. + set (op' := transl_op (make_env (function_bounds f)) op). + exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) ((undef_op op' rs0)#res <- v) fr m); split. apply plus_one. apply exec_Mop. apply shift_eval_operation. auto. change mreg with RegEq.t. rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). auto. econstructor; eauto with coqlib. - apply agree_set_reg; auto. + apply agree_set_reg; auto. apply agree_undef_op; auto. (* Lload *) - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) (rs0#dst <- v) fr m); split. + exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) ((undef_temps rs0)#dst <- v) fr m); split. apply plus_one; eapply exec_Mload; eauto. apply shift_eval_addressing; auto. change mreg with RegEq.t. rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eauto. econstructor; eauto with coqlib. - apply agree_set_reg; auto. + apply agree_set_reg; auto. apply agree_undef_temps; auto. (* Lstore *) econstructor; split. @@ -1456,7 +1507,7 @@ Proof. change mreg with RegEq.t. rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eauto. rewrite (agree_eval_reg _ _ _ _ _ _ _ src AG). eauto. - econstructor; eauto with coqlib. + econstructor; eauto with coqlib. apply agree_undef_temps; auto. (* Lcall *) assert (WTF': wt_fundef f'). eapply find_function_well_typed; eauto. @@ -1504,14 +1555,14 @@ Proof. apply agree_callee_save_return_regs. (* Lbuiltin *) - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) (rs0#res <- v) fr m'); split. + econstructor; split. apply plus_one. apply exec_Mbuiltin. change mreg with RegEq.t. rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto with coqlib. - apply agree_set_reg; auto. + apply agree_set_reg; auto. apply agree_undef_temps; auto. (* Llabel *) econstructor; split. @@ -1530,14 +1581,14 @@ Proof. apply plus_one; apply exec_Mcond_true. rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; eauto. apply transl_find_label; eauto. - econstructor; eauto. + econstructor; eauto. apply agree_undef_temps; auto. eapply find_label_incl; eauto. (* Lcond, false *) econstructor; split. apply plus_one; apply exec_Mcond_false. rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; auto. - econstructor; eauto with coqlib. + econstructor; eauto with coqlib. apply agree_undef_temps; auto. (* Ljumptable *) econstructor; split. @@ -1545,7 +1596,7 @@ Proof. rewrite <- (agree_eval_reg _ _ _ _ _ _ _ arg AG) in H; eauto. eauto. apply transl_find_label; eauto. - econstructor; eauto. + econstructor; eauto. apply agree_undef_temps; auto. eapply find_label_incl; eauto. (* Lreturn *) -- cgit v1.2.3