From bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 11 Jan 2009 11:57:02 +0000 Subject: - Added alignment constraints to memory loads and stores. - In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Stackingproof.v | 148 ++++++++++++++---------------------------------- 1 file changed, 44 insertions(+), 104 deletions(-) (limited to 'backend/Stackingproof.v') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index e17f67a..a7560d0 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -172,6 +172,45 @@ Proof. assert (z <> z0). intuition auto. omega. Qed. +Remark aligned_4_4x: forall x, (4 | 4 * x). +Proof. intro. exists x; ring. Qed. + +Remark aligned_4_8x: forall x, (4 | 8 * x). +Proof. intro. exists (x * 2); ring. Qed. + +Remark aligned_4_align8: forall x, (4 | align x 8). +Proof. + intro. apply Zdivides_trans with 8. exists 2; auto. apply align_divides. omega. +Qed. + +Hint Resolve Zdivide_0 Zdivide_refl Zdivide_plus_r + aligned_4_4x aligned_4_8x aligned_4_align8: align_4. + +Hint Extern 4 (?X | ?Y) => (exists (Y/X); reflexivity) : align_4. + +Lemma offset_of_index_aligned: + forall idx, (4 | offset_of_index fe idx). +Proof. + intros. + destruct idx; + unfold offset_of_index, fe, make_env, + fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, + fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg; + auto with align_4. + destruct t; auto with align_4. +Qed. + +Lemma frame_size_aligned: + (4 | fe_size fe). +Proof. + unfold offset_of_index, fe, make_env, + fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, + fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg; + auto with align_4. +Qed. + (** The following lemmas give sufficient conditions for indices of various kinds to be valid. *) @@ -232,7 +271,7 @@ Proof. fe_ofs_float_local, fe_ofs_float_callee_save, fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg, type_of_index, typesize; - simpl in H5; + unfold index_valid in H5; simpl typesize in H5; omega. Qed. @@ -287,6 +326,7 @@ Proof. auto. exact I. red. destruct idx; auto || congruence. intro. rewrite typesize_typesize. assumption. exact I. + apply offset_of_index_aligned. Qed. Lemma get_slot_index: @@ -535,96 +575,6 @@ Proof. intros. rewrite get_set_index_val_other; eauto with stacking. red; auto. Qed. -(* -Lemma agree_set_int_callee_save: - forall ls ls0 rs fr r v, - agree ls ls0 rs fr -> - In r int_callee_save_regs -> - index_int_callee_save r < fe.(fe_num_int_callee_save) -> - exists fr', - set_slot tf fr Tint - (Int.signed (Int.repr - (offset_of_index fe (FI_saved_int (index_int_callee_save r))))) - v fr' /\ - agree ls (Locmap.set (R r) v ls0) rs fr'. -Proof. - intros. - set (idx := FI_saved_int (index_int_callee_save r)). - exists (set_index_val idx v fr); split. - change Tint with (type_of_index idx). - apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. - constructor; eauto with stacking. - (* agree_unused_reg *) - intros. rewrite Locmap.gso. eauto with stacking. - red; red; intro. subst r0. elim H2. red. - rewrite (int_callee_save_type r H0). auto. - (* agree_local *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_outgoing *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_incoming *) - intros. rewrite Locmap.gso. eauto with stacking. red. auto. - (* saved ints *) - intros. destruct (mreg_eq r r0). - subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. - rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking. - unfold idx. auto with stacking. auto with stacking. - unfold idx; red. apply index_int_callee_save_inj; auto. - red; auto. - (* saved floats *) - intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. - unfold idx. auto with stacking. - unfold idx; red; auto. - red. apply int_float_callee_save_disjoint; auto. -Qed. - -Lemma agree_set_float_callee_save: - forall ls ls0 rs fr r v, - agree ls ls0 rs fr -> - In r float_callee_save_regs -> - index_float_callee_save r < fe.(fe_num_float_callee_save) -> - exists fr', - set_slot tf fr Tfloat - (Int.signed (Int.repr - (offset_of_index fe (FI_saved_float (index_float_callee_save r))))) - v fr' /\ - agree ls (Locmap.set (R r) v ls0) rs fr'. -Proof. - intros. - set (idx := FI_saved_float (index_float_callee_save r)). - exists (set_index_val idx v fr); split. - change Tfloat with (type_of_index idx). - apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. - constructor; eauto with stacking. - (* agree_unused_reg *) - intros. rewrite Locmap.gso. eauto with stacking. - red; red; intro. subst r0. elim H2. red. - rewrite (float_callee_save_type r H0). auto. - (* agree_local *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_outgoing *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_incoming *) - intros. rewrite Locmap.gso. eauto with stacking. red. auto. - (* saved ints *) - intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. - unfold idx. auto with stacking. - unfold idx; red; auto. - red. apply sym_not_equal. apply int_float_callee_save_disjoint; auto. - (* saved floats *) - intros. destruct (mreg_eq r r0). - subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. - rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking. - unfold idx. auto with stacking. auto with stacking. - unfold idx; red. apply index_float_callee_save_inj; auto. - red; auto. -Qed. -*) - Lemma agree_return_regs: forall ls ls0 rs fr cs rs', agree ls ls0 rs fr cs -> @@ -1270,12 +1220,11 @@ Proof. Qed. Lemma shift_eval_operation: - forall f tf sp op args m v, + forall f tf sp op args v, transf_function f = OK tf -> - eval_operation ge sp op args m = Some v -> + eval_operation ge sp op args = Some v -> eval_operation tge (shift_sp tf sp) - (transl_op (make_env (function_bounds f)) op) args m = - Some v. + (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. @@ -1535,15 +1484,6 @@ Proof. intros. inv WTI. generalize (H3 _ H0). tauto. apply agree_callee_save_return_regs. - (* Lalloc *) - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) - (rs0#loc_alloc_result <- (Vptr blk Int.zero)) fr m'); split. - apply plus_one; eapply exec_Malloc; eauto. - rewrite (agree_eval_reg _ _ _ _ _ _ _ loc_alloc_argument AG). auto. - econstructor; eauto with coqlib. - apply agree_set_reg; auto. - red. simpl. generalize (max_over_regs_of_funct_pos f int_callee_save). omega. - (* Llabel *) econstructor; split. apply plus_one; apply exec_Mlabel. -- cgit v1.2.3