- Added alignment constraints to memory loads and stores.

- In Cminor and below, removed pointer validity check in semantics of 
  comparisons, so that evaluation of expressions is independent of
  memory state.
- In Cminor and below, removed "alloc" instruction.
- Cleaned up commented-away parts.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 25 insertions, 53 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index ff6e9ae..a79ea29 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -18,6 +18,7 @@
     library. *)
 
 Require Export ZArith.
+Require Export Znumtheory.
 Require Export List.
 Require Export Bool.
 Require Import Wf_nat.
@@ -526,6 +527,25 @@ Proof.
   omega.
 Qed.
 
+(** Properties of divisibility. *)
+
+Lemma Zdivides_trans:
+  forall x y z, (x | y) -> (y | z) -> (x | z).
+Proof.
+  intros. inv H. inv H0. exists (q0 * q). ring.
+Qed.
+
+Definition Zdivide_dec:
+  forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }.
+Proof.
+  intros. destruct (zeq (Zmod q p) 0).
+  left. exists (q / p). 
+  transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto.
+  transitivity (p * (q / p)). omega. ring.
+  right; red; intros. elim n. apply Z_div_exact_1; auto. 
+  inv H0. rewrite Z_div_mult; auto. ring.
+Qed.
+
 (** Alignment: [align n amount] returns the smallest multiple of [amount]
   greater than or equal to [n]. *)
 
@@ -542,6 +562,11 @@ Proof.
   rewrite Zmult_comm. omega.
 Qed.
 
+Lemma align_divides: forall x y, y > 0 -> (y | align x y).
+Proof.
+  intros. unfold align. apply Zdivide_factor_l. 
+Qed.
+
 (** * Definitions and theorems on the data types [option], [sum] and [list] *)
 
 Set Implicit Arguments.
diff --git a/lib/Integers.v b/lib/Integers.v
index a9644bc..ff29d2a 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -2252,59 +2252,6 @@ Proof.
   rewrite <- two_p_is_exp. unfold modulus. rewrite two_power_nat_two_p.
   decEq. omega. omega. omega.
 Qed.
-(*
-Lemma zero_ext_charact:
-  forall x y,
-  zero_ext n x = y <->
-  0 <= unsigned y < two_p n /\ eqmod (two_p n) (unsigned x) (unsigned y).
-Proof.
-  intros. unfold zero_ext. set (x' := unsigned x). split; intros.
-  subst y.
-  assert (0 <= x' mod two_p n < two_p n). apply Z_mod_lt. apply two_p_n_pos.
-  rewrite unsigned_repr. split. auto. 
-  apply eqmod_mod. apply two_p_n_pos.
-  generalize two_p_n_range. omega.
-  destruct H. destruct H0 as [k EQ].  
-  assert (x' mod two_p n = unsigned y).
-  apply Zmod_unique with k; auto.
-  rewrite H0. apply repr_unsigned.
-Qed.
-
-Lemma sign_ext_charact:
-  forall x y,
-  sign_ext n x = y <->
-  -(two_p (n-1)) <= signed y < two_p (n-1)
-  /\ eqmod (two_p n) (unsigned x) (signed y).
-Proof.
-  intros. unfold sign_ext. set (x' := unsigned x). split; intros.
-  assert (0 <= x' mod two_p n < two_p n). apply Z_mod_lt. apply two_p_n_pos.
-  destruct (zlt (x' mod two_p n) (two_p (n - 1))); subst y.
-  rewrite signed_repr. split. omega. 
-  apply eqmod_mod. apply two_p_n_pos.
-  assert (min_signed < 0). vm_compute; auto. 
-  generalize two_p_n_range'. omega.
-  rewrite signed_repr. split. 
-  assert (two_p n = 2 * two_p (n-1)). rewrite <- two_p_S. decEq. omega. omega. 
-  omega. 
-  apply eqmod_trans with (x' - 0). apply eqmod_refl2. omega.
-  apply eqmod_sub. apply eqmod_mod. apply two_p_n_pos. 
-  exists (-1). ring. 
-  split. generalize two_p_n_range'. 
-  change (max_signed + 1) with (- min_signed). omega. 
-  generalize two_p_n_range'. omega.
-
-  destruct H. destruct H0 as [k EQ].
-  assert (two_p n = 2 * two_p (n - 1)). rewrite <- two_p_S. decEq. omega. omega.
-  assert (signed y >= 0 \/ signed y < 0) by omega. destruct H1.
-  assert (x' mod two_p n = signed y).
-  apply Zmod_unique with k; auto. omega.
-  rewrite zlt_true. rewrite H2. apply repr_signed. omega.
-  assert (x' mod two_p n = signed y + two_p n).
-  apply Zmod_unique with (k-1). rewrite EQ. ring. omega. 
-  rewrite zlt_false. replace (x' mod two_p n - two_p n) with (signed y) by omega. apply repr_signed.
-  omega.
-Qed.
-*)
 
 Lemma sign_ext_charact:
   forall x y,