From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/Bounds.v | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'backend/Bounds.v') diff --git a/backend/Bounds.v b/backend/Bounds.v index beb29965..2a63b1d5 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -161,7 +161,7 @@ Proof. intros until valu. unfold max_over_list. assert (forall l z, fold_left (fun x y => Zmax x (valu y)) l z >= z). induction l; simpl; intros. - omega. apply Zge_trans with (Zmax z (valu a)). + omega. apply Zge_trans with (Zmax z (valu a)). auto. apply Zle_ge. apply Zmax1. auto. Qed. @@ -193,7 +193,7 @@ Program Definition function_bounds := _ _. Next Obligation. apply Zle_ge. eapply Zle_trans. 2: apply Zmax2. - apply Zge_le. apply max_over_slots_of_funct_pos. + apply Zge_le. apply max_over_slots_of_funct_pos. Qed. Next Obligation. apply Zle_ge. apply Zmax2. @@ -211,10 +211,10 @@ Proof. z <= f /\ (In x c -> valu x <= f)). induction c; simpl; intros. split. omega. tauto. - elim (IHc (Zmax z (valu a))); intros. - split. apply Zle_trans with (Zmax z (valu a)). apply Zmax1. auto. - intro H1; elim H1; intro. - subst a. apply Zle_trans with (Zmax z (valu x)). + elim (IHc (Zmax z (valu a))); intros. + split. apply Zle_trans with (Zmax z (valu a)). apply Zmax1. auto. + intro H1; elim H1; intro. + subst a. apply Zle_trans with (Zmax z (valu x)). apply Zmax2. auto. auto. intro. elim (H l 0); intros. auto. Qed. @@ -231,7 +231,7 @@ Lemma max_over_regs_of_funct_bound: In i f.(fn_code) -> In r (regs_of_instr i) -> valu r <= max_over_regs_of_funct valu. Proof. - intros. unfold max_over_regs_of_funct. + intros. unfold max_over_regs_of_funct. apply Zle_trans with (max_over_regs_of_instr valu i). unfold max_over_regs_of_instr. apply max_over_list_bound. auto. apply max_over_instrs_bound. auto. @@ -242,7 +242,7 @@ Lemma max_over_slots_of_funct_bound: In i f.(fn_code) -> In s (slots_of_instr i) -> valu s <= max_over_slots_of_funct valu. Proof. - intros. unfold max_over_slots_of_funct. + intros. unfold max_over_slots_of_funct. apply Zle_trans with (max_over_slots_of_instr valu i). unfold max_over_slots_of_instr. apply max_over_list_bound. auto. apply max_over_instrs_bound. auto. @@ -255,7 +255,7 @@ Lemma int_callee_save_bound: Proof. intros. apply Zlt_le_trans with (int_callee_save r). unfold int_callee_save. omega. - unfold function_bounds, bound_int_callee_save. + unfold function_bounds, bound_int_callee_save. eapply max_over_regs_of_funct_bound; eauto. Qed. @@ -266,7 +266,7 @@ Lemma float_callee_save_bound: Proof. intros. apply Zlt_le_trans with (float_callee_save r). unfold float_callee_save. omega. - unfold function_bounds, bound_float_callee_save. + unfold function_bounds, bound_float_callee_save. eapply max_over_regs_of_funct_bound; eauto. Qed. @@ -315,11 +315,11 @@ Proof. Qed. Lemma slot_is_within_bounds: - forall i, In i f.(fn_code) -> + forall i, In i f.(fn_code) -> forall sl ty ofs, In (sl, ofs, ty) (slots_of_instr i) -> slot_within_bounds function_bounds sl ofs ty. Proof. - intros. unfold slot_within_bounds. + intros. unfold slot_within_bounds. destruct sl. eapply local_slot_bound; eauto. auto. @@ -329,12 +329,12 @@ Qed. Lemma slots_of_locs_charact: forall sl ofs ty l, In (sl, ofs, ty) (slots_of_locs l) <-> In (S sl ofs ty) l. Proof. - induction l; simpl; intros. + induction l; simpl; intros. tauto. destruct a; simpl; intuition congruence. Qed. -(** It follows that every instruction in the function is within bounds, +(** It follows that every instruction in the function is within bounds, in the sense of the [instr_within_bounds] predicate. *) Lemma instr_is_within_bounds: @@ -342,16 +342,16 @@ Lemma instr_is_within_bounds: In i f.(fn_code) -> instr_within_bounds function_bounds i. Proof. - intros; + intros; destruct i; - generalize (mreg_is_within_bounds _ H); generalize (slot_is_within_bounds _ H); + generalize (mreg_is_within_bounds _ H); generalize (slot_is_within_bounds _ H); simpl; intros; auto. (* call *) eapply size_arguments_bound; eauto. (* builtin *) split; intros. apply H1. apply in_or_app; auto. - apply H0. rewrite slots_of_locs_charact; auto. + apply H0. rewrite slots_of_locs_charact; auto. Qed. Lemma function_is_within_bounds: -- cgit