From 1f004665758e26e6e48d13f5702fe55af8944448 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 25 Oct 2016 15:11:30 +0200 Subject: Update ARM port. Not tested yet. --- arm/Op.v | 189 ++++++++++++++++++++++++++++----------------------------------- 1 file changed, 84 insertions(+), 105 deletions(-) (limited to 'arm/Op.v') diff --git a/arm/Op.v b/arm/Op.v index bc717d7b..0d31c2ac 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -35,6 +35,7 @@ Require Import Globalenvs. Require Import Events. Set Implicit Arguments. +Local Transparent Archi.ptr64. Record shift_amount: Type := { s_amount: int; @@ -74,8 +75,8 @@ Inductive operation : Type := | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) | Ofloatconst: float -> operation (**r [rd] is set to the given 64-bit float constant *) | Osingleconst: float32 -> operation (**r [rd] is set to the given 32-bit float constant *) - | Oaddrsymbol: ident -> int -> operation (**r [rd] is set to the the address of the symbol plus the offset *) - | Oaddrstack: int -> operation (**r [rd] is set to the stack pointer plus the given offset *) + | Oaddrsymbol: ident -> ptrofs -> operation (**r [rd] is set to the the address of the symbol plus the offset *) + | Oaddrstack: ptrofs -> operation (**r [rd] is set to the stack pointer plus the given offset *) (*c Integer arithmetic: *) | Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *) | Ocast16signed: operation (**r [rd] is 16-bit sign extension of [r1] *) @@ -148,7 +149,7 @@ Inductive addressing: Type := | Aindexed: int -> addressing (**r Address is [r1 + offset] *) | Aindexed2: addressing (**r Address is [r1 + r2] *) | Aindexed2shift: shift -> addressing (**r Address is [r1 + shifted r2] *) - | Ainstack: int -> addressing. (**r Address is [stack_pointer + offset] *) + | Ainstack: ptrofs -> addressing. (**r Address is [stack_pointer + offset] *) (** Comparison functions (used in module [CSE]). *) @@ -173,10 +174,8 @@ Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. - generalize Int.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. + generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intros. + generalize Float.eq_dec Float32.eq_dec; intros. generalize eq_shift; intro. generalize eq_condition; intro. decide equality. @@ -184,7 +183,7 @@ Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec; intro. + generalize Int.eq_dec Ptrofs.eq_dec; intro. generalize eq_shift; intro. decide equality. Defined. @@ -235,7 +234,7 @@ Definition eval_operation | Ofloatconst n, nil => Some (Vfloat n) | Osingleconst n, nil => Some (Vsingle n) | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) - | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs)) + | Oaddrstack ofs, nil => Some (Val.offset_ptr sp ofs) | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1) | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1) | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2) @@ -305,10 +304,24 @@ Definition eval_addressing | Aindexed n, v1 :: nil => Some (Val.add v1 (Vint n)) | Aindexed2, v1 :: v2 :: nil => Some (Val.add v1 v2) | Aindexed2shift s, v1 :: v2 :: nil => Some (Val.add v1 (eval_shift s v2)) - | Ainstack ofs, nil => Some (Val.add sp (Vint ofs)) + | Ainstack ofs, nil => Some (Val.offset_ptr sp ofs) | _, _ => None end. +Remark eval_addressing_Ainstack: + forall (F V: Type) (genv: Genv.t F V) sp ofs, + eval_addressing genv sp (Ainstack ofs) nil = Some (Val.offset_ptr sp ofs). +Proof. + intros. reflexivity. +Qed. + +Remark eval_addressing_Ainstack_inv: + forall (F V: Type) (genv: Genv.t F V) sp ofs vl v, + eval_addressing genv sp (Ainstack ofs) vl = Some v -> vl = nil /\ v = Val.offset_ptr sp ofs. +Proof. + unfold eval_addressing; intros; destruct vl; inv H; auto. +Qed. + Ltac FuncInv := match goal with | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => @@ -430,7 +443,7 @@ Lemma type_of_operation_sound: op <> Omove -> eval_operation genv sp op vl m = Some v -> Val.has_type v (snd (type_of_operation op)). -Proof with (try exact I). +Proof with (try exact I; try reflexivity). assert (S: forall s v, Val.has_type (eval_shift s v) Tint). intros. unfold eval_shift. destruct s; destruct v; simpl; auto; rewrite s_range; exact I. intros. @@ -588,15 +601,15 @@ Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) -Definition shift_stack_addressing (delta: int) (addr: addressing) := +Definition shift_stack_addressing (delta: Z) (addr: addressing) := match addr with - | Ainstack ofs => Ainstack (Int.add delta ofs) + | Ainstack ofs => Ainstack (Ptrofs.add (Ptrofs.repr delta) ofs) | _ => addr end. -Definition shift_stack_operation (delta: int) (op: operation) := +Definition shift_stack_operation (delta: Z) (op: operation) := match op with - | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) + | Oaddrstack ofs => Oaddrstack (Ptrofs.add (Ptrofs.repr delta) ofs) | _ => op end. @@ -614,79 +627,43 @@ Qed. Lemma eval_shift_stack_addressing: forall F V (ge: Genv.t F V) sp addr vl delta, - eval_addressing ge sp (shift_stack_addressing delta addr) vl = - eval_addressing ge (Val.add sp (Vint delta)) addr vl. + eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = + eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. intros. destruct addr; simpl; auto. - rewrite Val.add_assoc. simpl. auto. + rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_shift_stack_operation: forall F V (ge: Genv.t F V) sp op vl m delta, - eval_operation ge sp (shift_stack_operation delta op) vl m = - eval_operation ge (Val.add sp (Vint delta)) op vl m. + eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m = + eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m. Proof. intros. destruct op; simpl; auto. - rewrite Val.add_assoc. simpl. auto. + rewrite Ptrofs.add_zero_l; auto. Qed. (** Offset an addressing mode [addr] by a quantity [delta], so that it designates the pointer [delta] bytes past the pointer designated by [addr]. May be undefined, in which case [None] is returned. *) -Definition offset_addressing (addr: addressing) (delta: int) : option addressing := +Definition offset_addressing (addr: addressing) (delta: Z) : option addressing := match addr with - | Aindexed n => Some(Aindexed (Int.add n delta)) + | Aindexed n => Some(Aindexed (Int.add n (Int.repr delta))) | Aindexed2 => None | Aindexed2shift s => None - | Ainstack n => Some(Ainstack (Int.add n delta)) + | Ainstack n => Some(Ainstack (Ptrofs.add n (Ptrofs.repr delta))) end. Lemma eval_offset_addressing: forall (F V: Type) (ge: Genv.t F V) sp addr args delta addr' v, offset_addressing addr delta = Some addr' -> eval_addressing ge sp addr args = Some v -> - eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)). + eval_addressing ge sp addr' args = Some(Val.add v (Vint (Int.repr delta))). Proof. intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst. rewrite Val.add_assoc; auto. - rewrite Val.add_assoc. auto. -Qed. - -(** Transformation of addressing modes with two operands or more - into an equivalent arithmetic operation. This is used in the [Reload] - pass when a store instruction cannot be reloaded directly because - it runs out of temporary registers. *) - -(** For the ARM, there are only two binary addressing mode: [Aindexed2] - and [Aindexed2shift]. The corresponding operations are [Oadd] - and [Oaddshift]. *) - -Definition op_for_binary_addressing (addr: addressing) : operation := - match addr with - | Aindexed2 => Oadd - | Aindexed2shift s => Oaddshift s - | _ => Ointconst Int.zero (* never happens *) - end. - -Lemma eval_op_for_binary_addressing: - forall (F V: Type) (ge: Genv.t F V) sp addr args v m, - (length args >= 2)%nat -> - eval_addressing ge sp addr args = Some v -> - eval_operation ge sp (op_for_binary_addressing addr) args m = Some v. -Proof. - intros. - unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; simpl. - congruence. - congruence. -Qed. - -Lemma type_op_for_binary_addressing: - forall addr, - (length (type_of_addressing addr) >= 2)%nat -> - type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint). -Proof. - intros. destruct addr; simpl in H; reflexivity || omegaContradiction. + destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. do 4 f_equal. symmetry; auto with ptrofs. Qed. (** Two-address operations. There are none in the ARM architecture. *) @@ -781,30 +758,30 @@ Variable m2: mem. Hypothesis valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - 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. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_pointer_no_overflow: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Hypothesis valid_different_pointers_inj: forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). Ltac InvInject := match goal with @@ -871,20 +848,20 @@ 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 Val.offset_ptr_inject; auto. inv H4; simpl; auto. inv H4; simpl; auto. - apply Values.Val.add_inject; auto. - apply Values.Val.add_inject; auto. apply eval_shift_inj; auto. - apply Values.Val.add_inject; auto. + apply Val.add_inject; auto. + apply Val.add_inject; auto. apply eval_shift_inj; auto. + apply Val.add_inject; auto. - apply Values.Val.sub_inject; auto. - apply Values.Val.sub_inject; auto. apply eval_shift_inj; auto. - apply Values.Val.sub_inject; auto. apply eval_shift_inj; auto. - apply (@Values.Val.sub_inject f (Vint i) (Vint i) v v'); auto. + apply Val.sub_inject; auto. + apply Val.sub_inject; auto. apply eval_shift_inj; auto. + apply Val.sub_inject; auto. apply eval_shift_inj; auto. + apply (@Val.sub_inject f (Vint i) (Vint i) v v'); auto. inv H4; inv H2; simpl; auto. - apply Values.Val.add_inject; auto. inv H4; inv H2; simpl; auto. + apply Val.add_inject; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H3; simpl in H1; inv H1. simpl. @@ -965,10 +942,10 @@ Lemma eval_addressing_inj: exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. - apply Values.Val.add_inject; auto. - apply Values.Val.add_inject; auto. - apply Values.Val.add_inject; auto. apply eval_shift_inj; auto. - apply Values.Val.add_inject; auto. + apply Val.add_inject; auto. + apply Val.add_inject; auto. + apply Val.add_inject; auto. apply eval_shift_inj; auto. + apply Val.offset_ptr_inject; auto. Qed. End EVAL_COMPAT. @@ -984,40 +961,40 @@ Remark valid_pointer_extends: forall m1 m2, Mem.extends m1 m2 -> forall b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Proof. - intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. + intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.valid_pointer_extends; eauto. Qed. Remark weak_valid_pointer_extends: forall m1 m2, Mem.extends m1 m2 -> forall b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - 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. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Proof. - intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. + intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. Qed. Remark weak_valid_pointer_no_overflow_extends: forall m1 b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2. + intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: forall m1 b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> Some(b1, 0) = Some (b1', delta1) -> Some(b2, 0) = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned(Int.add ofs1 (Int.repr delta1)) <> Int.unsigned(Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned(Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned(Ptrofs.add ofs2 (Ptrofs.repr delta2)). Proof. intros. inv H2; inv H3. auto. Qed. @@ -1096,7 +1073,7 @@ Remark symbol_address_inject: Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. - econstructor; eauto. rewrite Int.add_zero; auto. + econstructor; eauto. rewrite Ptrofs.add_zero; auto. Qed. Lemma eval_condition_inject: @@ -1116,34 +1093,36 @@ Qed. 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 -> + eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = Some v1 -> exists v2, - eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 + eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. - rewrite eval_shift_stack_addressing. simpl. - eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. - intros; apply symbol_address_inject. + rewrite eval_shift_stack_addressing. + eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto. + intros. apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> - eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> + eval_operation genv (Vptr sp1 Ptrofs.zero) op vl1 m1 = Some v1 -> exists v2, - eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 + eval_operation genv (Vptr sp2 Ptrofs.zero) (shift_stack_operation delta op) vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_operation. simpl. - eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. + eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.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. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. End EVAL_INJECT. -- cgit