From e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:25:18 +0200 Subject: Support for 64-bit architectures: generic support - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly. --- lib/Integers.v | 457 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 454 insertions(+), 3 deletions(-) (limited to 'lib/Integers.v') diff --git a/lib/Integers.v b/lib/Integers.v index 16c95e01..593f0ccc 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -15,10 +15,9 @@ (** Formalizations of machine integers modulo $2^N$ #2N#. *) -Require Import Eqdep_dec. -Require Import Zquot. -Require Import Zwf. +Require Import Eqdep_dec Zquot Zwf. Require Import Coqlib. +Require Archi. (** * Comparisons *) @@ -3652,6 +3651,53 @@ Proof. unfold min_signed, max_signed; omega. Qed. +Lemma signed_eq: + forall x y, eq x y = zeq (signed x) (signed y). +Proof. + intros. unfold eq. unfold proj_sumbool. + destruct (zeq (unsigned x) (unsigned y)); + destruct (zeq (signed x) (signed y)); auto. + elim n. unfold signed. rewrite e; auto. + elim n. apply eqm_small_eq; auto with ints. + eapply eqm_trans. apply eqm_sym. apply eqm_signed_unsigned. + rewrite e. apply eqm_signed_unsigned. +Qed. + +Lemma not_lt: + forall x y, negb (lt y x) = (lt x y || eq x y). +Proof. + intros. unfold lt. rewrite signed_eq. unfold proj_sumbool. + destruct (zlt (signed y) (signed x)). + rewrite zlt_false. rewrite zeq_false. auto. omega. omega. + destruct (zeq (signed x) (signed y)). + rewrite zlt_false. auto. omega. + rewrite zlt_true. auto. omega. +Qed. + +Lemma lt_not: + forall x y, lt y x = negb (lt x y) && negb (eq x y). +Proof. + intros. rewrite <- negb_orb. rewrite <- not_lt. rewrite negb_involutive. auto. +Qed. + +Lemma not_ltu: + forall x y, negb (ltu y x) = (ltu x y || eq x y). +Proof. + intros. unfold ltu, eq. + destruct (zlt (unsigned y) (unsigned x)). + rewrite zlt_false. rewrite zeq_false. auto. omega. omega. + destruct (zeq (unsigned x) (unsigned y)). + rewrite zlt_false. auto. omega. + rewrite zlt_true. auto. omega. +Qed. + +Lemma ltu_not: + forall x y, ltu y x = negb (ltu x y) && negb (eq x y). +Proof. + intros. rewrite <- negb_orb. rewrite <- not_ltu. rewrite negb_involutive. auto. +Qed. + + (** Non-overlapping test *) Definition no_overlap (ofs1: int) (sz1: Z) (ofs2: int) (sz2: Z) : bool := @@ -4007,6 +4053,130 @@ Proof. omega. Qed. +Lemma shl'_mul_two_p: + forall x y, + shl' x y = mul x (repr (two_p (Int.unsigned y))). +Proof. + intros. unfold shl', mul. apply eqm_samerepr. + rewrite Zshiftl_mul_two_p. apply eqm_mult. apply eqm_refl. apply eqm_unsigned_repr. + generalize (Int.unsigned_range y); omega. +Qed. + +Lemma shl'_one_two_p: + forall y, shl' one y = repr (two_p (Int.unsigned y)). +Proof. + intros. rewrite shl'_mul_two_p. rewrite mul_commut. rewrite mul_one. auto. +Qed. + +Theorem shl'_mul: + forall x y, + shl' x y = mul x (shl' one y). +Proof. + intros. rewrite shl'_one_two_p. apply shl'_mul_two_p. +Qed. + +(** Powers of two with exponents given as 32-bit ints *) + +Definition one_bits' (x: int) : list Int.int := + List.map Int.repr (Z_one_bits wordsize (unsigned x) 0). + +Definition is_power2' (x: int) : option Int.int := + match Z_one_bits wordsize (unsigned x) 0 with + | i :: nil => Some (Int.repr i) + | _ => None + end. + +Theorem one_bits'_range: + forall x i, In i (one_bits' x) -> Int.ltu i iwordsize' = true. +Proof. + intros. + destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]]. + exploit Z_one_bits_range; eauto. intros R. + unfold Int.ltu. rewrite EQ. rewrite Int.unsigned_repr. + change (Int.unsigned iwordsize') with zwordsize. apply zlt_true. omega. + assert (zwordsize < Int.max_unsigned) by reflexivity. omega. +Qed. + +Fixpoint int_of_one_bits' (l: list Int.int) : int := + match l with + | nil => zero + | a :: b => add (shl' one a) (int_of_one_bits' b) + end. + +Theorem one_bits'_decomp: + forall x, x = int_of_one_bits' (one_bits' x). +Proof. + assert (REC: forall l, + (forall i, In i l -> 0 <= i < zwordsize) -> + int_of_one_bits' (List.map Int.repr l) = repr (powerserie l)). + { induction l; simpl; intros. + - auto. + - rewrite IHl by eauto. apply eqm_samerepr; apply eqm_add. + + rewrite shl'_one_two_p. rewrite Int.unsigned_repr. apply eqm_sym; apply eqm_unsigned_repr. + exploit (H a). auto. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. + + apply eqm_sym; apply eqm_unsigned_repr. + } + intros. rewrite <- (repr_unsigned x) at 1. unfold one_bits'. rewrite REC. + rewrite <- Z_one_bits_powerserie. auto. apply unsigned_range. + apply Z_one_bits_range. +Qed. + +Lemma is_power2'_rng: + forall n logn, + is_power2' n = Some logn -> + 0 <= Int.unsigned logn < zwordsize. +Proof. + unfold is_power2'; intros n logn P2. + destruct (Z_one_bits wordsize (unsigned n) 0) as [ | i [ | ? ?]] eqn:B; inv P2. + assert (0 <= i < zwordsize). + { apply Z_one_bits_range with (unsigned n). rewrite B; auto with coqlib. } + rewrite Int.unsigned_repr. auto. + assert (zwordsize < Int.max_unsigned) by reflexivity. + omega. +Qed. + +Theorem is_power2'_range: + forall n logn, + is_power2' n = Some logn -> Int.ltu logn iwordsize' = true. +Proof. + intros. unfold Int.ltu. change (Int.unsigned iwordsize') with zwordsize. + apply zlt_true. generalize (is_power2'_rng _ _ H). tauto. +Qed. + +Lemma is_power2'_correct: + forall n logn, + is_power2' n = Some logn -> + unsigned n = two_p (Int.unsigned logn). +Proof. + unfold is_power2'; intros. + destruct (Z_one_bits wordsize (unsigned n) 0) as [ | i [ | ? ?]] eqn:B; inv H. + rewrite (Z_one_bits_powerserie (unsigned n)) by (apply unsigned_range). + rewrite Int.unsigned_repr. rewrite B; simpl. omega. + assert (0 <= i < zwordsize). + { apply Z_one_bits_range with (unsigned n). rewrite B; auto with coqlib. } + assert (zwordsize < Int.max_unsigned) by reflexivity. + omega. +Qed. + +Theorem mul_pow2': + forall x n logn, + is_power2' n = Some logn -> + mul x n = shl' x logn. +Proof. + intros. rewrite shl'_mul. f_equal. rewrite shl'_one_two_p. + rewrite <- (repr_unsigned n). f_equal. apply is_power2'_correct; auto. +Qed. + +Theorem divu_pow2': + forall x n logn, + is_power2' n = Some logn -> + divu x n = shru' x logn. +Proof. + intros. generalize (is_power2'_correct n logn H). intro. + symmetry. unfold divu. rewrite H0. unfold shru'. rewrite Zshiftr_div_two_p. auto. + eapply is_power2'_rng; eauto. +Qed. + (** Decomposing 64-bit ints as pairs of 32-bit ints *) Definition loword (n: int) : Int.int := Int.repr (unsigned n). @@ -4528,3 +4698,284 @@ Strategy 0 [Wordsize_64.wordsize]. Notation int64 := Int64.int. Global Opaque Int.repr Int64.repr Byte.repr. + +(** * Specialization to offsets in pointer values *) + +Module Wordsize_Ptrofs. + Definition wordsize := if Archi.ptr64 then 64%nat else 32%nat. + Remark wordsize_not_zero: wordsize <> 0%nat. + Proof. unfold wordsize; destruct Archi.ptr64; congruence. Qed. +End Wordsize_Ptrofs. + +Strategy opaque [Wordsize_Ptrofs.wordsize]. + +Module Ptrofs. + +Include Make(Wordsize_Ptrofs). + +Definition to_int (x: int): Int.int := Int.repr (unsigned x). + +Definition to_int64 (x: int): Int64.int := Int64.repr (unsigned x). + +Definition of_int (x: Int.int) : int := repr (Int.unsigned x). + +Definition of_intu := of_int. + +Definition of_ints (x: Int.int) : int := repr (Int.signed x). + +Definition of_int64 (x: Int64.int) : int := repr (Int64.unsigned x). + +Definition of_int64u := of_int64. + +Definition of_int64s (x: Int64.int) : int := repr (Int64.signed x). + +Section AGREE32. + +Hypothesis _32: Archi.ptr64 = false. + +Lemma modulus_eq32: modulus = Int.modulus. +Proof. + unfold modulus, wordsize. + change Wordsize_Ptrofs.wordsize with (if Archi.ptr64 then 64%nat else 32%nat). + rewrite _32. reflexivity. +Qed. + +Lemma eqm32: + forall x y, Int.eqm x y <-> eqm x y. +Proof. + intros. unfold Int.eqm, eqm. rewrite modulus_eq32; tauto. +Qed. + +Definition agree32 (a: Ptrofs.int) (b: Int.int) : Prop := + Ptrofs.unsigned a = Int.unsigned b. + +Lemma agree32_repr: + forall i, agree32 (Ptrofs.repr i) (Int.repr i). +Proof. + intros; red. rewrite Ptrofs.unsigned_repr_eq, Int.unsigned_repr_eq. + apply f_equal2. auto. apply modulus_eq32. +Qed. + +Lemma agree32_signed: + forall a b, agree32 a b -> Ptrofs.signed a = Int.signed b. +Proof. + unfold agree32; intros. unfold signed, Int.signed, half_modulus, Int.half_modulus. + rewrite modulus_eq32. rewrite H. auto. +Qed. + +Lemma agree32_of_int: + forall b, agree32 (of_int b) b. +Proof. + unfold of_int; intros. rewrite <- (Int.repr_unsigned b) at 2. apply agree32_repr. +Qed. + +Lemma agree32_of_ints: + forall b, agree32 (of_ints b) b. +Proof. + unfold of_int; intros. rewrite <- (Int.repr_signed b) at 2. apply agree32_repr. +Qed. + +Lemma agree32_of_int_eq: + forall a b, agree32 a b -> of_int b = a. +Proof. + unfold agree32, of_int; intros. rewrite <- H. apply repr_unsigned. +Qed. + +Lemma agree32_of_ints_eq: + forall a b, agree32 a b -> of_ints b = a. +Proof. + unfold of_ints; intros. erewrite <- agree32_signed by eauto. apply repr_signed. +Qed. + +Lemma agree32_to_int: + forall a, agree32 a (to_int a). +Proof. + unfold agree32, to_int; intros. rewrite <- (agree32_repr (unsigned a)). + rewrite repr_unsigned; auto. +Qed. + +Lemma agree32_to_int_eq: + forall a b, agree32 a b -> to_int a = b. +Proof. + unfold agree32, to_int; intros. rewrite H. apply Int.repr_unsigned. +Qed. + +Lemma agree32_neg: + forall a1 b1, agree32 a1 b1 -> agree32 (Ptrofs.neg a1) (Int.neg b1). +Proof. + unfold agree32, Ptrofs.neg, Int.neg; intros. rewrite H. apply agree32_repr. +Qed. + +Lemma agree32_add: + forall a1 b1 a2 b2, + agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.add a1 a2) (Int.add b1 b2). +Proof. + unfold agree32, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree32_repr. +Qed. + +Lemma agree32_sub: + forall a1 b1 a2 b2, + agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.sub a1 a2) (Int.sub b1 b2). +Proof. + unfold agree32, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree32_repr. +Qed. + +Lemma agree32_mul: + forall a1 b1 a2 b2, + agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.mul a1 a2) (Int.mul b1 b2). +Proof. + unfold agree32, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree32_repr. +Qed. + +Lemma agree32_divs: + forall a1 b1 a2 b2, + agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.divs a1 a2) (Int.divs b1 b2). +Proof. + intros; unfold agree32, Ptrofs.divs, Int.divs. + erewrite ! agree32_signed by eauto. apply agree32_repr. +Qed. + +Lemma of_int_to_int: + forall n, of_int (to_int n) = n. +Proof. + intros; unfold of_int, to_int. apply eqm_repr_eq. rewrite <- eqm32. + apply Int.eqm_sym; apply Int.eqm_unsigned_repr. +Qed. + +End AGREE32. + +Section AGREE64. + +Hypothesis _64: Archi.ptr64 = true. + +Lemma modulus_eq64: modulus = Int64.modulus. +Proof. + unfold modulus, wordsize. + change Wordsize_Ptrofs.wordsize with (if Archi.ptr64 then 64%nat else 32%nat). + rewrite _64. reflexivity. +Qed. + +Lemma eqm64: + forall x y, Int64.eqm x y <-> eqm x y. +Proof. + intros. unfold Int64.eqm, eqm. rewrite modulus_eq64; tauto. +Qed. + +Definition agree64 (a: Ptrofs.int) (b: Int64.int) : Prop := + Ptrofs.unsigned a = Int64.unsigned b. + +Lemma agree64_repr: + forall i, agree64 (Ptrofs.repr i) (Int64.repr i). +Proof. + intros; red. rewrite Ptrofs.unsigned_repr_eq, Int64.unsigned_repr_eq. + apply f_equal2. auto. apply modulus_eq64. +Qed. + +Lemma agree64_signed: + forall a b, agree64 a b -> Ptrofs.signed a = Int64.signed b. +Proof. + unfold agree64; intros. unfold signed, Int64.signed, half_modulus, Int64.half_modulus. + rewrite modulus_eq64. rewrite H. auto. +Qed. + +Lemma agree64_of_int: + forall b, agree64 (of_int64 b) b. +Proof. + unfold of_int64; intros. rewrite <- (Int64.repr_unsigned b) at 2. apply agree64_repr. +Qed. + +Lemma agree64_of_int_eq: + forall a b, agree64 a b -> of_int64 b = a. +Proof. + unfold agree64, of_int64; intros. rewrite <- H. apply repr_unsigned. +Qed. + +Lemma agree64_to_int: + forall a, agree64 a (to_int64 a). +Proof. + unfold agree64, to_int64; intros. rewrite <- (agree64_repr (unsigned a)). + rewrite repr_unsigned; auto. +Qed. + +Lemma agree64_to_int_eq: + forall a b, agree64 a b -> to_int64 a = b. +Proof. + unfold agree64, to_int64; intros. rewrite H. apply Int64.repr_unsigned. +Qed. + +Lemma agree64_neg: + forall a1 b1, agree64 a1 b1 -> agree64 (Ptrofs.neg a1) (Int64.neg b1). +Proof. + unfold agree64, Ptrofs.neg, Int64.neg; intros. rewrite H. apply agree64_repr. +Qed. + +Lemma agree64_add: + forall a1 b1 a2 b2, + agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.add a1 a2) (Int64.add b1 b2). +Proof. + unfold agree64, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree64_repr. +Qed. + +Lemma agree64_sub: + forall a1 b1 a2 b2, + agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.sub a1 a2) (Int64.sub b1 b2). +Proof. + unfold agree64, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree64_repr. +Qed. + +Lemma agree64_mul: + forall a1 b1 a2 b2, + agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.mul a1 a2) (Int64.mul b1 b2). +Proof. + unfold agree64, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree64_repr. +Qed. + +Lemma agree64_divs: + forall a1 b1 a2 b2, + agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.divs a1 a2) (Int64.divs b1 b2). +Proof. + intros; unfold agree64, Ptrofs.divs, Int64.divs. + erewrite ! agree64_signed by eauto. apply agree64_repr. +Qed. + +Lemma of_int64_to_int64: + forall n, of_int64 (to_int64 n) = n. +Proof. + intros; unfold of_int64, to_int64. apply eqm_repr_eq. rewrite <- eqm64. + apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr. +Qed. + +End AGREE64. + +Hint Resolve + agree32_repr agree32_of_int agree32_of_ints agree32_of_int_eq agree32_of_ints_eq + agree32_to_int agree32_to_int_eq agree32_neg agree32_add agree32_sub agree32_mul agree32_divs + agree64_repr agree64_of_int agree64_of_int_eq + agree64_to_int agree64_to_int_eq agree64_neg agree64_add agree64_sub agree64_mul agree64_divs : ptrofs. + +End Ptrofs. + +Strategy 0 [Wordsize_Ptrofs.wordsize]. + +Notation ptrofs := Ptrofs.int. + +Global Opaque Ptrofs.repr. + +Hint Resolve Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans + Int.eqm_small_eq Int.eqm_add Int.eqm_neg Int.eqm_sub Int.eqm_mult + Int.eqm_unsigned_repr Int.eqm_unsigned_repr_l Int.eqm_unsigned_repr_r + Int.unsigned_range Int.unsigned_range_2 + Int.repr_unsigned Int.repr_signed Int.unsigned_repr : ints. + +Hint Resolve Int64.modulus_pos Int64.eqm_refl Int64.eqm_refl2 Int64.eqm_sym Int64.eqm_trans + Int64.eqm_small_eq Int64.eqm_add Int64.eqm_neg Int64.eqm_sub Int64.eqm_mult + Int64.eqm_unsigned_repr Int64.eqm_unsigned_repr_l Int64.eqm_unsigned_repr_r + Int64.unsigned_range Int64.unsigned_range_2 + Int64.repr_unsigned Int64.repr_signed Int64.unsigned_repr : ints. + +Hint Resolve Ptrofs.modulus_pos Ptrofs.eqm_refl Ptrofs.eqm_refl2 Ptrofs.eqm_sym Ptrofs.eqm_trans + Ptrofs.eqm_small_eq Ptrofs.eqm_add Ptrofs.eqm_neg Ptrofs.eqm_sub Ptrofs.eqm_mult + Ptrofs.eqm_unsigned_repr Ptrofs.eqm_unsigned_repr_l Ptrofs.eqm_unsigned_repr_r + Ptrofs.unsigned_range Ptrofs.unsigned_range_2 + Ptrofs.repr_unsigned Ptrofs.repr_signed Ptrofs.unsigned_repr : ints. + -- cgit