From a74f6b45d72834b5b8417297017bd81424123d98 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 7 Mar 2010 15:52:58 +0000 Subject: 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 --- lib/Coqlib.v | 127 +++++++++++++++++++++++ lib/Integers.v | 15 ++- lib/Intv.v | 319 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/Maps.v | 77 ++++++++++++++ 4 files changed, 534 insertions(+), 4 deletions(-) create mode 100644 lib/Intv.v (limited to 'lib') 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. -- cgit v1.2.3