From f5bb397acd12292f6b41438778f2df7391d6f2fe Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:26:56 +0200 Subject: bug 17392: remove trailing whitespace in source files --- powerpc/Op.v | 58 +++++++++++++++++++++++++++++----------------------------- 1 file changed, 29 insertions(+), 29 deletions(-) (limited to 'powerpc/Op.v') diff --git a/powerpc/Op.v b/powerpc/Op.v index 6866b086..c8028557 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -17,7 +17,7 @@ - [operation]: arithmetic and logical operations; - [addressing]: addressing modes for load and store operations. - These types are PowerPC-specific and correspond roughly to what the + These types are PowerPC-specific and correspond roughly to what the processor can compute in one instruction. In other terms, these types reflect the state of the program after instruction selection. For a processor-independent set of operations, see the abstract @@ -118,7 +118,7 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp: condition -> operation. (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) -(** Addressing modes. [r1], [r2], etc, are the arguments to the +(** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) Inductive addressing: Type := @@ -184,7 +184,7 @@ Definition eval_operation | Ointconst n, nil => Some (Vint n) | Ofloatconst n, nil => Some (Vfloat n) | Osingleconst n, nil => Some (Vsingle n) - | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) + | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs)) | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1) | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1) @@ -436,7 +436,7 @@ Proof with (try exact I). destruct v0; destruct v1... destruct v0... destruct v0... - destruct (eval_condition c vl m); simpl... destruct b... + destruct (eval_condition c vl m); simpl... destruct b... Qed. End SOUNDNESS. @@ -460,7 +460,7 @@ Proof. intros until a. unfold is_move_operation; destruct op; try (intros; discriminate). destruct args. intros; discriminate. - destruct args. intros. intuition congruence. + destruct args. intros. intuition congruence. intros; discriminate. Qed. @@ -488,9 +488,9 @@ Proof. repeat (destruct vl; auto). apply Val.negate_cmpu_bool. repeat (destruct vl; auto). apply Val.negate_cmp_bool. repeat (destruct vl; auto). apply Val.negate_cmpu_bool. - repeat (destruct vl; auto). + repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto. - repeat (destruct vl; auto). + repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.maskzero_bool v i) as [[]|]; auto. Qed. @@ -511,7 +511,7 @@ Definition shift_stack_operation (delta: int) (op: operation) := Lemma type_shift_stack_addressing: forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr. Proof. - intros. destruct addr; auto. + intros. destruct addr; auto. Qed. Lemma type_shift_stack_operation: @@ -559,10 +559,10 @@ Lemma eval_offset_addressing: Proof. intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst. rewrite Val.add_assoc; auto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. - rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. - rewrite Val.add_assoc. auto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. + rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. + rewrite Val.add_assoc. auto. Qed. (** Operations that are so cheap to recompute that CSE should not factor them out. *) @@ -591,7 +591,7 @@ Lemma op_depends_on_memory_correct: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence. unfold eval_condition. - destruct c; simpl; auto; try discriminate. + destruct c; simpl; auto; try discriminate. Qed. (** Global variables mentioned in an operation or addressing mode *) @@ -630,7 +630,7 @@ Remark symbol_address_preserved: Proof. unfold Genv.symbol_address; intros. rewrite agree_on_symbols; auto. Qed. - + Lemma eval_operation_preserved: forall sp op vl m, eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m. @@ -740,25 +740,25 @@ Lemma eval_operation_inj: Proof. intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. apply GL; simpl; auto. - apply Values.Val.add_inject; auto. + apply Values.Val.add_inject; auto. inv H4; simpl; auto. inv H4; simpl; auto. apply Values.Val.add_inject; auto. apply Values.Val.add_inject; auto. apply Values.Val.add_inject; auto. apply GL; simpl; auto. - inv H4; inv H2; simpl; auto. econstructor; eauto. + inv H4; inv H2; simpl; auto. econstructor; eauto. rewrite Int.sub_add_l. auto. - destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. + destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. rewrite Int.sub_shifted. auto. - inv H4; auto. + inv H4; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. - inv H4; inv H3; simpl in H1; inv H1. simpl. + inv H4; inv H3; simpl in H1; inv H1. simpl. destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists. - inv H4; inv H3; simpl in H1; inv H1. simpl. + inv H4; inv H3; simpl in H1; inv H1. simpl. destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. @@ -841,7 +841,7 @@ Remark valid_pointer_extends: Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. Proof. - intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. + intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. Qed. Remark weak_valid_pointer_extends: @@ -909,8 +909,8 @@ Proof. apply valid_different_pointers_extends; auto. intros. rewrite <- val_inject_lessdef; auto. rewrite <- val_inject_lessdef; auto. - eauto. auto. - destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. + eauto. auto. + destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. Lemma eval_addressing_lessdef: @@ -926,8 +926,8 @@ Proof. eapply eval_addressing_inj with (sp1 := sp). intros. rewrite <- val_inject_lessdef; auto. rewrite <- val_inject_lessdef; auto. - eauto. auto. - destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. + eauto. auto. + destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. End EVAL_LESSDEF. @@ -949,7 +949,7 @@ Remark symbol_address_inject: forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. - exploit (proj1 globals); eauto. intros. + exploit (proj1 globals); eauto. intros. econstructor; eauto. rewrite Int.add_zero; auto. Qed. @@ -971,11 +971,11 @@ Lemma eval_addressing_inject: forall addr vl1 vl2 v1, Val.inject_list f vl1 vl2 -> eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> - exists v2, + exists v2, eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 /\ Val.inject f v1 v2. Proof. - intros. + intros. rewrite eval_shift_stack_addressing. simpl. eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. intros. apply symbol_address_inject. @@ -990,7 +990,7 @@ Lemma eval_operation_inject: eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. - intros. + intros. rewrite eval_shift_stack_operation. simpl. eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. @@ -1015,7 +1015,7 @@ End EVAL_INJECT. / \ / \ / \ \ / \ / \ / -0--> [1] --1--> [2] --0--> [3] - / + / [0] \ -1--> [4] --0--> [5] --1--> [6] -- cgit