Merge of the newmem and newextcalls branches:

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


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

4 files changed, 534 insertions, 4 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 5375c04..380ac73 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -554,6 +554,27 @@ Proof.
   omega.
 Qed.
 
+Lemma Zmod_recombine:
+  forall x a b,
+  a > 0 -> b > 0 ->
+  x mod (a * b) = ((x/b) mod a) * b + (x mod b).
+Proof.
+  intros. 
+  set (xb := x/b). 
+  apply Zmod_unique with (xb/a).
+  generalize (Z_div_mod_eq x b H0); fold xb; intro EQ1.
+  generalize (Z_div_mod_eq xb a H); intro EQ2.
+  rewrite EQ2 in EQ1. 
+  eapply trans_eq. eexact EQ1. ring.
+  generalize (Z_mod_lt x b H0). intro. 
+  generalize (Z_mod_lt xb a H). intro.
+  assert (0 <= xb mod a * b <= a * b - b).
+    split. apply Zmult_le_0_compat; omega.
+    replace (a * b - b) with ((a - 1) * b) by ring.
+    apply Zmult_le_compat; omega. 
+  omega.
+Qed.
+
 (** Properties of divisibility. *)
 
 Lemma Zdivides_trans:
@@ -573,6 +594,45 @@ Proof.
   inv H0. rewrite Z_div_mult; auto. ring.
 Qed.
 
+(** Conversion from [Z] to [nat]. *)
+
+Definition nat_of_Z (z: Z) : nat :=
+  match z with
+  | Z0 => O
+  | Zpos p => nat_of_P p
+  | Zneg p => O
+  end.
+
+Lemma nat_of_Z_max:
+  forall z, Z_of_nat (nat_of_Z z) = Zmax z 0.
+Proof.
+  intros. unfold Zmax. destruct z; simpl; auto.
+  symmetry. apply Zpos_eq_Z_of_nat_o_nat_of_P.
+Qed.
+
+Lemma nat_of_Z_eq:
+  forall z, z >= 0 -> Z_of_nat (nat_of_Z z) = z.
+Proof.
+  intros. rewrite nat_of_Z_max. apply Zmax_left. auto.
+Qed.
+
+Lemma nat_of_Z_neg:
+  forall n, n <= 0 -> nat_of_Z n = O.
+Proof.
+  destruct n; unfold Zle; simpl; auto. congruence.
+Qed.
+
+Lemma nat_of_Z_plus:
+  forall p q,
+  p >= 0 -> q >= 0 ->
+  nat_of_Z (p + q) = (nat_of_Z p + nat_of_Z q)%nat.
+Proof.
+  intros. 
+  apply inj_eq_rev. rewrite inj_plus.
+  repeat rewrite nat_of_Z_eq; auto. omega.
+Qed.
+
+
 (** Alignment: [align n amount] returns the smallest multiple of [amount]
   greater than or equal to [n]. *)
 
@@ -817,6 +877,18 @@ Proof.
   auto. rewrite IHl1. auto.
 Qed.
 
+Lemma list_append_map_inv:
+  forall (A B: Type) (f: A -> B) (m1 m2: list B) (l: list A),
+  List.map f l = m1 ++ m2 ->
+  exists l1, exists l2, List.map f l1 = m1 /\ List.map f l2 = m2 /\ l = l1 ++ l2.
+Proof.
+  induction m1; simpl; intros.
+  exists (@nil A); exists l; auto.
+  destruct l; simpl in H; inv H. 
+  exploit IHm1; eauto. intros [l1 [l2 [P [Q R]]]]. subst l. 
+  exists (a0 :: l1); exists l2; intuition. simpl; congruence.
+Qed.
+
 (** Properties of list membership. *)
 
 Lemma in_cns:
@@ -1050,6 +1122,14 @@ Inductive list_forall2: list A -> list B -> Prop :=
       list_forall2 al bl ->
       list_forall2 (a1 :: al) (b1 :: bl).
 
+Lemma list_forall2_app:
+  forall a2 b2 a1 b1,
+  list_forall2 a1 b1 -> list_forall2 a2 b2 -> 
+  list_forall2 (a1 ++ a2) (b1 ++ b2).
+Proof.
+  induction 1; intros; simpl. auto. constructor; auto. 
+Qed.
+
 End FORALL2.
 
 Lemma list_forall2_imply:
@@ -1095,6 +1175,26 @@ Proof.
   destruct l; simpl; auto.
 Qed.
 
+(** A list of [n] elements, all equal to [x]. *)
+
+Fixpoint list_repeat {A: Type} (n: nat) (x: A) {struct n} :=
+  match n with
+  | O => nil
+  | S m => x :: list_repeat m x
+  end.
+
+Lemma length_list_repeat:
+  forall (A: Type) n (x: A), length (list_repeat n x) = n.
+Proof.
+  induction n; simpl; intros. auto. decEq; auto.
+Qed.
+
+Lemma in_list_repeat:
+  forall (A: Type) n (x: A) y, In y (list_repeat n x) -> y = x.
+Proof.
+  induction n; simpl; intros. elim H. destruct H; auto.
+Qed.
+
 (** * Definitions and theorems over boolean types *)
 
 Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool :=
@@ -1110,6 +1210,12 @@ Proof.
   intros P Q a. destruct a; simpl. auto. congruence.
 Qed.
 
+Lemma proj_sumbool_is_true:
+  forall (P: Prop) (a: {P}+{~P}), P -> proj_sumbool a = true.
+Proof.
+  intros. unfold proj_sumbool. destruct a. auto. contradiction. 
+Qed.
+
 Section DECIDABLE_EQUALITY.
 
 Variable A: Type.
@@ -1141,3 +1247,24 @@ Proof.
 Qed.
 
 End DECIDABLE_EQUALITY.
+
+Section DECIDABLE_PREDICATE.
+
+Variable P: Prop.
+Variable dec: {P} + {~P}.
+Variable A: Type.
+
+Lemma pred_dec_true:
+  forall (a b: A), P -> (if dec then a else b) = a.
+Proof.
+  intros. destruct dec. auto. contradiction.
+Qed.
+
+Lemma pred_dec_false:
+  forall (a b: A), ~P -> (if dec then a else b) = b.
+Proof.
+  intros. destruct dec. contradiction. auto.
+Qed.
+
+End DECIDABLE_PREDICATE.
+
diff --git a/lib/Integers.v b/lib/Integers.v
index fb6eee2..b443d54 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -2670,15 +2670,15 @@ Qed.
 
 End Make.
 
-(** * Specialization to 32-bit integers. *)
+(** * Specialization to 32-bit integers and to bytes. *)
 
-Module IntWordsize.
+Module Wordsize_32.
   Definition wordsize := 32%nat.
   Remark wordsize_not_zero: wordsize <> 0%nat.
   Proof. unfold wordsize; congruence. Qed.
-End IntWordsize.
+End Wordsize_32.
 
-Module Int := Make(IntWordsize).
+Module Int := Make(Wordsize_32).
 
 Notation int := Int.int.
 
@@ -2688,5 +2688,12 @@ Proof.
   exists (two_p (32-5)); reflexivity. 
 Qed.
 
+Module Wordsize_8.
+  Definition wordsize := 8%nat.
+  Remark wordsize_not_zero: wordsize <> 0%nat.
+  Proof. unfold wordsize; congruence. Qed.
+End Wordsize_8.
 
+Module Byte := Integers.Make(Wordsize_8).
 
+Notation byte := Byte.int.
diff --git a/lib/Intv.v b/lib/Intv.v
new file mode 100644
index 0000000..834f83d
--- /dev/null
+++ b/lib/Intv.v
@@ -0,0 +1,319 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Definitions and theorems about semi-open integer intervals *)
+
+Require Import Coqlib.
+Require Import Zwf.
+Require Coq.Program.Wf.
+Require Recdef.
+
+Definition interv : Type := (Z * Z)%type.
+
+(** * Membership *)
+
+Definition In (x: Z) (i: interv) : Prop := fst i <= x < snd i.
+
+Lemma In_dec:
+  forall x i, {In x i} + {~In x i}.
+Proof.
+  unfold In; intros.
+  case (zle (fst i) x); intros. 
+  case (zlt x (snd i)); intros.
+  left; auto.
+  right; intuition. 
+  right; intuition.
+Qed.
+
+Lemma notin_range: 
+  forall x i,
+  x < fst i \/ x >= snd i -> ~In x i.
+Proof.
+  unfold In; intros; omega. 
+Qed.
+
+Lemma range_notin:
+  forall x i,
+  ~In x i -> fst i < snd i -> x < fst i \/ x >= snd i.
+Proof.
+  unfold In; intros; omega.
+Qed.
+
+(** * Emptyness *)
+
+Definition empty (i: interv) : Prop := fst i >= snd i.
+
+Lemma empty_dec:
+  forall i, {empty i} + {~empty i}.
+Proof.
+  unfold empty; intros. 
+  case (zle (snd i) (fst i)); intros.
+  left; omega.
+  right; omega.
+Qed.
+
+Lemma is_notempty:
+  forall i, fst i < snd i -> ~empty i.
+Proof.
+  unfold empty; intros; omega.
+Qed.
+
+Lemma empty_notin:
+  forall x i, empty i -> ~In x i.
+Proof.
+  unfold empty, In; intros. omega.
+Qed.
+
+Lemma in_notempty:
+  forall x i, In x i -> ~empty i.
+Proof.
+  unfold empty, In; intros. omega.
+Qed.
+
+(** * Disjointness *)
+
+Definition disjoint (i j: interv) : Prop :=
+  forall x, In x i -> ~In x j.
+
+Lemma disjoint_sym:
+  forall i j, disjoint i j -> disjoint j i.
+Proof.
+  unfold disjoint; intros; red; intros. elim (H x); auto. 
+Qed.
+
+Lemma empty_disjoint_r:
+  forall i j, empty j -> disjoint i j.
+Proof.
+  unfold disjoint; intros. apply empty_notin; auto.
+Qed.
+
+Lemma empty_disjoint_l:
+  forall i j, empty i -> disjoint i j.
+Proof.
+  intros. apply disjoint_sym. apply empty_disjoint_r; auto. 
+Qed.
+
+Lemma disjoint_range:
+  forall i j,
+  snd i <= fst j \/ snd j <= fst i -> disjoint i j.
+Proof.
+  unfold disjoint, In; intros. omega.
+Qed.
+
+Lemma range_disjoint:
+  forall i j,
+  disjoint i j ->
+  empty i \/ empty j \/ snd i <= fst j \/ snd j <= fst i.
+Proof.
+  unfold disjoint, empty; intros.
+  destruct (zlt (fst i) (snd i)); auto.
+  destruct (zlt (fst j) (snd j)); auto.
+  right; right.
+  destruct (zlt (fst i) (fst j)).
+(* Case 1: i starts to the left of j. *)
+  destruct (zle (snd i) (fst j)).
+(* Case 1.1: i ends to the left of j, OK *)
+  auto.
+(* Case 1.2: i ends to the right of j's start, not disjoint. *)
+  elim (H (fst j)). red; omega. red; omega.
+(* Case 2: j starts to the left of i *)
+  destruct (zle (snd j) (fst i)).
+(* Case 2.1: j ends to the left of i, OK *)
+  auto.
+(* Case 2.2: j ends to the right of i's start, not disjoint. *)
+  elim (H (fst i)). red; omega. red; omega.
+Qed.
+
+Lemma range_disjoint':
+  forall i j,
+  disjoint i j -> fst i < snd i -> fst j < snd j ->
+  snd i <= fst j \/ snd j <= fst i.
+Proof.
+  intros. exploit range_disjoint; eauto. unfold empty; intuition omega.
+Qed.
+
+Lemma disjoint_dec:
+  forall i j, {disjoint i j} + {~disjoint i j}.
+Proof.
+  intros. 
+  destruct (empty_dec i). left; apply empty_disjoint_l; auto.
+  destruct (empty_dec j). left; apply empty_disjoint_r; auto.
+  destruct (zle (snd i) (fst j)). left; apply disjoint_range; auto.
+  destruct (zle (snd j) (fst i)). left; apply disjoint_range; auto.
+  right; red; intro. exploit range_disjoint; eauto. intuition. 
+Qed.
+
+(** * Shifting an interval by some amount *)
+
+Definition shift (i: interv) (delta: Z) : interv := (fst i + delta, snd i + delta).
+
+Lemma in_shift:
+  forall x i delta,
+  In x i -> In (x + delta) (shift i delta).
+Proof.
+  unfold shift, In; intros. simpl. omega.
+Qed.
+
+Lemma in_shift_inv:
+  forall x i delta,
+  In x (shift i delta) -> In (x - delta) i.
+Proof.
+  unfold shift, In; simpl; intros. omega. 
+Qed.
+
+(** * Enumerating the elements of an interval *)
+
+Section ELEMENTS.
+
+Variable lo: Z.
+
+Function elements_rec (hi: Z) {wf (Zwf lo) hi} : list Z :=
+  if zlt lo hi then (hi-1) :: elements_rec (hi-1) else nil.
+Proof.
+  intros. red. omega. 
+  apply Zwf_well_founded.
+Qed.
+
+Lemma In_elements_rec:
+  forall hi x,
+  List.In x (elements_rec hi) <-> lo <= x < hi.
+Proof.
+  intros. functional induction (elements_rec hi). 
+  simpl; split; intros.
+  destruct H. clear IHl. omega. rewrite IHl in H. clear IHl. omega.
+  destruct (zeq (hi - 1) x); auto. right. rewrite IHl. clear IHl. omega.
+  simpl; intuition. 
+Qed.
+
+End ELEMENTS.
+
+Definition elements (i: interv) : list Z :=
+  elements_rec (fst i) (snd i).
+
+Lemma in_elements:
+  forall x i,
+  In x i -> List.In x (elements i).
+Proof.
+  intros. unfold elements. rewrite In_elements_rec. auto.
+Qed.
+
+Lemma elements_in:
+  forall x i,
+  List.In x (elements i) -> In x i.
+Proof.
+  unfold elements; intros. 
+  rewrite In_elements_rec in H. auto. 
+Qed.
+
+(** * Checking properties on all elements of an interval *)
+
+Section FORALL.
+
+Variables P Q: Z -> Prop.
+Variable f: forall (x: Z), {P x} + {Q x}.
+Variable lo: Z.
+
+Program Fixpoint forall_rec (hi: Z) {wf (Zwf lo) hi}:
+                 {forall x, lo <= x < hi -> P x}
+                 + {exists x, lo <= x < hi /\ Q x} :=
+  if zlt lo hi then
+    match f (hi - 1) with
+    | left _ =>
+        match forall_rec (hi - 1) with
+        | left _ => left _ _
+        | right _ => right _ _
+        end
+    | right _ => right _ _
+    end
+  else
+    left _ _
+.
+Next Obligation.
+  red. omega. 
+Qed.
+Next Obligation.
+  assert (x = hi - 1 \/ x < hi - 1) by omega.
+  destruct H2. congruence. auto. 
+Qed.
+Next Obligation.
+  elim wildcard'0. intros y [A B]. exists y; split; auto. omega.
+Qed.
+Next Obligation.
+  exists (hi - 1); split; auto. omega.
+Qed.
+Next Obligation.
+  omegaContradiction.
+Qed.
+Next Obligation.
+  apply Zwf_well_founded.
+Defined.
+
+End FORALL.
+
+Definition forall_dec
+       (P Q: Z -> Prop) (f: forall (x: Z), {P x} + {Q x}) (i: interv) :
+       {forall x, In x i -> P x} + {exists x, In x i /\ Q x} :=
+ forall_rec P Q f (fst i) (snd i).
+
+(** * Folding a function over all elements of an interval *)
+
+Section FOLD.
+
+Variable A: Type.
+Variable f: Z -> A -> A.
+Variable lo: Z.
+Variable a: A.
+
+Function fold_rec (hi: Z) {wf (Zwf lo) hi} : A :=
+  if zlt lo hi then f (hi - 1) (fold_rec (hi - 1)) else a.
+Proof.
+  intros. red. omega. 
+  apply Zwf_well_founded.
+Qed.
+
+Lemma fold_rec_elements:
+  forall hi, fold_rec hi = List.fold_right f a (elements_rec lo hi).
+Proof.
+  intros. functional induction (fold_rec hi).
+  rewrite elements_rec_equation. rewrite zlt_true; auto. 
+  simpl. congruence. 
+  rewrite elements_rec_equation. rewrite zlt_false; auto. 
+Qed.
+
+End FOLD.
+
+Definition fold {A: Type} (f: Z -> A -> A) (a: A) (i: interv) : A :=
+  fold_rec A f (fst i) a (snd i).
+
+Lemma fold_elements:
+  forall (A: Type) (f: Z -> A -> A) a i,
+  fold f a i = List.fold_right f a (elements i).
+Proof.
+  intros. unfold fold, elements. apply fold_rec_elements. 
+Qed.
+
+(** Hints *)
+
+Hint Resolve
+  notin_range range_notin
+  is_notempty empty_notin in_notempty
+  disjoint_sym empty_disjoint_r empty_disjoint_l
+  disjoint_range
+  in_shift in_shift_inv
+  in_elements elements_in : intv.
+
+
+
+    
diff --git a/lib/Maps.v b/lib/Maps.v
index 4c0bd50..cdee00c 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -124,6 +124,17 @@ Module Type TREE.
   Hypothesis elements_keys_norepet:
     forall (A: Type) (m: t A), 
     list_norepet (List.map (@fst elt A) (elements m)).
+  Hypothesis elements_canonical_order:
+    forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B),
+    (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) ->
+    (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) ->
+    list_forall2
+      (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
+      (elements m) (elements n).
+  Hypothesis elements_extensional:
+    forall (A: Type) (m n: t A),
+    (forall i, get i m = get i n) ->
+    elements m = elements n.
 
   (** Folding a function over all bindings of a tree. *)
   Variable fold:
@@ -901,6 +912,72 @@ Module PTree <: TREE.
     intros. change (list_norepet (xkeys m 1)). apply xelements_keys_norepet.
   Qed.
 
+  Theorem elements_canonical_order:
+    forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B),
+    (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) ->
+    (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) ->
+    list_forall2
+      (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
+      (elements m) (elements n).
+  Proof.
+    intros until R.
+    assert (forall m n j,
+    (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) ->
+    (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) ->
+    list_forall2
+      (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
+      (xelements m j) (xelements n j)).
+    induction m; induction n; intros; simpl.
+    constructor.
+    destruct o. exploit (H0 xH). simpl. reflexivity. simpl. intros [x [P Q]]. congruence.
+    change (@nil (positive*A)) with ((@nil (positive * A))++nil).
+    apply list_forall2_app.
+    apply IHn1.
+    intros. rewrite gleaf in H1. congruence.
+    intros. exploit (H0 (xO i)). simpl; eauto. rewrite gleaf. intros [x [P Q]]. congruence.
+    apply IHn2.
+    intros. rewrite gleaf in H1. congruence.
+    intros. exploit (H0 (xI i)). simpl; eauto. rewrite gleaf. intros [x [P Q]]. congruence.
+    destruct o. exploit (H xH). simpl. reflexivity. simpl. intros [x [P Q]]. congruence.
+    change (@nil (positive*B)) with (xelements (@Leaf B) (append j 2) ++ (xelements (@Leaf B) (append j 3))).
+    apply list_forall2_app.
+    apply IHm1.
+    intros. exploit (H (xO i)). simpl; eauto. rewrite gleaf. intros [y [P Q]]. congruence.
+    intros. rewrite gleaf in H1. congruence.
+    apply IHm2.
+    intros. exploit (H (xI i)). simpl; eauto. rewrite gleaf. intros [y [P Q]]. congruence.
+    intros. rewrite gleaf in H1. congruence.
+    exploit (IHm1 n1 (append j 2)). 
+    intros. exploit (H (xO i)). simpl; eauto. simpl. auto.
+    intros. exploit (H0 (xO i)). simpl; eauto. simpl; auto.
+    intro REC1.
+    exploit (IHm2 n2 (append j 3)). 
+    intros. exploit (H (xI i)). simpl; eauto. simpl. auto.
+    intros. exploit (H0 (xI i)). simpl; eauto. simpl; auto.
+    intro REC2.
+    destruct o; destruct o0.
+    apply list_forall2_app; auto. constructor; auto. 
+    simpl; split; auto. exploit (H xH). simpl; eauto. simpl. intros [y [P Q]]. congruence.
+    exploit (H xH). simpl; eauto. simpl. intros [y [P Q]]; congruence.
+    exploit (H0 xH). simpl; eauto. simpl. intros [x [P Q]]; congruence.
+    apply list_forall2_app; auto.
+
+    unfold elements; auto.
+  Qed.
+
+  Theorem elements_extensional:
+    forall (A: Type) (m n: t A),
+    (forall i, get i m = get i n) ->
+    elements m = elements n.
+  Proof.
+    intros. 
+    exploit (elements_canonical_order (fun (x y: A) => x = y) m n). 
+    intros. rewrite H in H0. exists x; auto.
+    intros. rewrite <- H in H0. exists y; auto.
+    induction 1. auto. destruct a1 as [a2 a3]; destruct b1 as [b2 b3]; simpl in *.
+    destruct H0. congruence.
+  Qed.
+
 (*
   Definition fold (A B : Type) (f: B -> positive -> A -> B) (tr: t A) (v: B) :=
      List.fold_left (fun a p => f a (fst p) (snd p)) (elements tr) v.