From 6f3225b0623b9c97eed7d40ddc320b08c79c6518 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 10 Feb 2013 10:08:27 +0000 Subject: lib/Integers.v: revised and extended, faster implementation based on bit-level operations provided by ZArith in Coq 8.4. Other modules: adapted accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Memdata.v | 35 ++++++++++++++++++----------------- common/Values.v | 12 ++++++------ 2 files changed, 24 insertions(+), 23 deletions(-) (limited to 'common') diff --git a/common/Memdata.v b/common/Memdata.v index 5f06d2c..8afe752 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -190,7 +190,7 @@ Opaque Byte.wordsize. replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega. rewrite two_p_is_exp; try omega. rewrite Zmod_recombine. rewrite IHn. rewrite Zplus_comm. - rewrite Byte.Z_mod_two_p_eq. reflexivity. + rewrite Byte.Z_mod_modulus_eq. reflexivity. apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega. Qed. @@ -214,7 +214,7 @@ Lemma decode_encode_int_1: Proof. intros. rewrite decode_encode_int. rewrite <- (Int.repr_unsigned (Int.zero_ext 8 x)). - decEq. symmetry. apply Int.zero_ext_mod. compute; auto. + decEq. symmetry. apply Int.zero_ext_mod. compute. intuition congruence. Qed. Lemma decode_encode_int_2: @@ -222,7 +222,7 @@ Lemma decode_encode_int_2: Proof. intros. rewrite decode_encode_int. rewrite <- (Int.repr_unsigned (Int.zero_ext 16 x)). - decEq. symmetry. apply Int.zero_ext_mod. compute; auto. + decEq. symmetry. apply Int.zero_ext_mod. compute; intuition congruence. Qed. Lemma decode_encode_int_4: @@ -419,14 +419,14 @@ Opaque inj_pointer. destruct v; destruct chunk1; simpl; try (apply decode_val_undef); destruct chunk2; unfold decode_val; auto; try (rewrite proj_inj_bytes). (* int-int *) - rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. compute; auto. - rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. compute; auto. - rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. compute; auto. - rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. compute; auto. - rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. compute; auto. - rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. compute; auto. - rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. compute; auto. - rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. compute; auto. + rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega. + rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega. + rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega. + rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega. + rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. omega. + rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. omega. + rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. omega. + rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. omega. rewrite decode_encode_int_4. auto. rewrite decode_encode_int_4. auto. rewrite decode_encode_int_4. auto. @@ -482,7 +482,8 @@ Qed. Lemma encode_val_int8_zero_ext: forall n, encode_val Mint8unsigned (Vint (Int.zero_ext 8 n)) = encode_val Mint8unsigned (Vint n). Proof. - intros; unfold encode_val. decEq. apply encode_int_8_mod. apply Int.eqmod_zero_ext. compute; auto. + intros; unfold encode_val. decEq. apply encode_int_8_mod. apply Int.eqmod_zero_ext. + compute; intuition congruence. Qed. Lemma encode_val_int8_sign_ext: @@ -494,7 +495,7 @@ Qed. Lemma encode_val_int16_zero_ext: forall n, encode_val Mint16unsigned (Vint (Int.zero_ext 16 n)) = encode_val Mint16unsigned (Vint n). Proof. - intros; unfold encode_val. decEq. apply encode_int_16_mod. apply Int.eqmod_zero_ext. compute; auto. + intros; unfold encode_val. decEq. apply encode_int_16_mod. apply Int.eqmod_zero_ext. compute; intuition congruence. Qed. Lemma encode_val_int16_sign_ext: @@ -516,10 +517,10 @@ Lemma decode_val_cast: end. Proof. unfold decode_val; intros; destruct chunk; auto; destruct (proj_bytes l); auto. - unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. compute; auto. - unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. compute; auto. - unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. compute; auto. - unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. compute; auto. + unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. + unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. + unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. + unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. simpl. rewrite Float.singleoffloat_of_bits. auto. Qed. diff --git a/common/Values.v b/common/Values.v index 177cd93..f02fa70 100644 --- a/common/Values.v +++ b/common/Values.v @@ -428,14 +428,14 @@ Theorem cast8unsigned_and: forall x, zero_ext 8 x = and x (Vint(Int.repr 255)). Proof. destruct x; simpl; auto. decEq. - change 255 with (two_p 8 - 1). apply Int.zero_ext_and. vm_compute; auto. + change 255 with (two_p 8 - 1). apply Int.zero_ext_and. omega. Qed. Theorem cast16unsigned_and: forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)). Proof. destruct x; simpl; auto. decEq. - change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. vm_compute; auto. + change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. omega. Qed. Theorem bool_of_val_of_bool: @@ -600,7 +600,7 @@ Theorem mul_pow2: mul x (Vint n) = shl x (Vint logn). Proof. intros; destruct x; simpl; auto. - change 32 with (Z_of_nat Int.wordsize). + change 32 with Int.zwordsize. rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto. Qed. @@ -929,17 +929,17 @@ Qed. Lemma zero_ext_and: forall n v, - 0 < n < Z_of_nat Int.wordsize -> + 0 < n < Int.zwordsize -> Val.zero_ext n v = Val.and v (Vint (Int.repr (two_p n - 1))). Proof. - intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. + intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. omega. Qed. Lemma rolm_lt_zero: forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero). Proof. intros. unfold cmp, cmp_bool; destruct v; simpl; auto. - transitivity (Vint (Int.shru i (Int.repr (Z_of_nat Int.wordsize - 1)))). + transitivity (Vint (Int.shru i (Int.repr (Int.zwordsize - 1)))). decEq. symmetry. rewrite Int.shru_rolm. auto. auto. rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto. Qed. -- cgit v1.2.3