diff options
Diffstat (limited to 'ia32/Op.v')
| -rw-r--r-- | ia32/Op.v | 64 |
1 files changed, 32 insertions, 32 deletions
@@ -17,7 +17,7 @@ - [operation]: arithmetic and logical operations; - [addressing]: addressing modes for load and store operations. - These types are IA32-specific and correspond roughly to what the + These types are IA32-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 @@ -49,7 +49,7 @@ Inductive condition : Type := | Cmaskzero: int -> condition (**r test [(arg & constant) == 0] *) | Cmasknotzero: int -> condition. (**r test [(arg & constant) != 0] *) -(** Addressing modes. [r1], [r2], etc, are the arguments to the +(** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) Inductive addressing: Type := @@ -475,7 +475,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. @@ -499,7 +499,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. @@ -529,9 +529,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) as [[]|]; auto. - repeat (destruct vl; auto). + repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. destruct vl; auto. destruct vl; auto. destruct vl; auto. destruct vl; auto. destruct (Val.maskzero_bool v i) as [[]|]; auto. @@ -554,13 +554,13 @@ 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: forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. Proof. - intros. destruct op; auto. simpl. decEq. apply type_shift_stack_addressing. + intros. destruct op; auto. simpl. decEq. apply type_shift_stack_addressing. Qed. Lemma eval_shift_stack_addressing: @@ -578,7 +578,7 @@ Lemma eval_shift_stack_operation: eval_operation ge (Val.add sp (Vint delta)) op vl m. Proof. intros. destruct op; simpl; auto. - apply eval_shift_stack_addressing. + apply eval_shift_stack_addressing. Qed. (** Offset an addressing mode [addr] by a quantity [delta], so that @@ -613,12 +613,12 @@ Proof. rewrite !Val.add_assoc; auto. rewrite !Val.add_assoc; auto. 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. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. + rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. unfold Genv.symbol_address. destruct (Genv.find_symbol ge i0); auto. - rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. - rewrite Val.add_assoc. auto. + rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. + rewrite Val.add_assoc. auto. Qed. Lemma eval_offset_addressing: @@ -627,7 +627,7 @@ Lemma eval_offset_addressing: eval_addressing ge sp addr args = Some v -> eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)). Proof. - intros. unfold offset_addressing in H; inv H. + intros. unfold offset_addressing in H; inv H. eapply eval_offset_addressing_total; eauto. Qed. @@ -832,9 +832,9 @@ Proof. inv H4; simpl; auto. inv H4; simpl; auto. inv H4; 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; inv H2; simpl; auto. inv H4; simpl; auto. @@ -842,11 +842,11 @@ Proof. inv H4; inv H2; simpl; auto. 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 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. @@ -859,14 +859,14 @@ Proof. inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. - inv H4; simpl in H1; try discriminate. simpl. + inv H4; simpl in H1; try discriminate. simpl. destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. inv H2; simpl; auto. destruct (Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize); auto. - eapply eval_addressing_inj; eauto. + eapply eval_addressing_inj; eauto. inv H4; simpl; auto. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. @@ -912,7 +912,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: @@ -922,7 +922,7 @@ Remark weak_valid_pointer_extends: Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. Proof. - intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. + intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. Qed. Remark weak_valid_pointer_no_overflow_extends: @@ -978,11 +978,11 @@ Proof. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends. apply valid_different_pointers_extends; auto. - intros. apply val_inject_lessdef. auto. + intros. apply val_inject_lessdef. auto. apply val_inject_lessdef; auto. - eauto. + eauto. auto. - destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. + destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. Lemma eval_addressing_lessdef: @@ -998,8 +998,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. @@ -1021,7 +1021,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. @@ -1043,11 +1043,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. @@ -1062,14 +1062,14 @@ 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. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. - intros. apply symbol_address_inject. + intros. apply symbol_address_inject. Qed. End EVAL_INJECT. |