From e29b0c71f446ea6267711c7cc19294fd93fb81ad Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Mar 2013 17:28:10 +0000 Subject: Assorted cleanups, esp. to avoid generating _rec and _rect recursors in submodules. (Extraction does not remove them, then.) common/Switch: replaced use of FMaps by our own Maps. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Globalenvs.v | 29 +++++++++------- common/Memory.v | 4 +++ common/Switch.v | 97 ++++++++++++++++++++++++++++++++--------------------- 3 files changed, 79 insertions(+), 51 deletions(-) (limited to 'common') diff --git a/common/Globalenvs.v b/common/Globalenvs.v index d426440..3d9f499 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -53,6 +53,23 @@ Local Open Scope error_monad_scope. Set Implicit Arguments. +(** Auxiliary function for initialization of global variables. *) + +Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem := + if zle n 0 then Some m else + match Mem.store Mint8unsigned m b p Vzero with + | Some m' => store_zeros m' b (p + 1) (n - 1) + | None => None + end. +Proof. + intros. red. omega. + apply Zwf_well_founded. +Qed. + +(* To avoid useless definitions of inductors in extracted code. *) +Local Unset Elimination Schemes. +Local Unset Case Analysis Schemes. + Module Genv. (** * Global environments *) @@ -486,18 +503,6 @@ Proof. destruct i; simpl; try omega. generalize (Zle_max_r z 0). omega. Qed. -Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem := - if zle n 0 then Some m else - let n' := n - 1 in - match Mem.store Mint8unsigned m b p Vzero with - | Some m' => store_zeros m' b (p + 1) n' - | None => None - end. -Proof. - intros. red. omega. - apply Zwf_well_founded. -Qed. - Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option mem := match id with | Init_int8 n => Mem.store Mint8unsigned m b p (Vint n) diff --git a/common/Memory.v b/common/Memory.v index 04a3dda..bfaf67d 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -36,6 +36,10 @@ Require Import Values. Require Export Memdata. Require Export Memtype. +(* To avoid useless definitions of inductors in extracted code. *) +Local Unset Elimination Schemes. +Local Unset Case Analysis Schemes. + Local Notation "a # b" := (ZMap.get b a) (at level 1). Module Mem <: MEM. diff --git a/common/Switch.v b/common/Switch.v index 0ba6186..3e25851 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -17,14 +17,34 @@ to comparison trees. *) Require Import EqNat. -Require Import FMaps. -Require FMapAVL. Require Import Coqlib. +Require Import Maps. Require Import Integers. -Require Import Ordered. -Module IntMap := FMapAVL.Make(OrderedInt). -Module IntMapF := FMapFacts.Facts(IntMap). +Module IntIndexed <: INDEXED_TYPE. + + Definition t := int. + + Definition index (n: int) : positive := + match Int.unsigned n with + | Z0 => xH + | Zpos p => xO p + | Zneg p => xI p (**r never happens *) + end. + + Lemma index_inj: forall n m, index n = index m -> n = m. + Proof. + unfold index; intros. + rewrite <- (Int.repr_unsigned n). rewrite <- (Int.repr_unsigned m). + f_equal. + destruct (Int.unsigned n); destruct (Int.unsigned m); congruence. + Qed. + + Definition eq := Int.eq_dec. + +End IntIndexed. + +Module IntMap := IMap(IntIndexed). (** A multi-way branch is composed of a list of (key, action) pairs, plus a default action. *) @@ -93,14 +113,14 @@ Fixpoint split_eq (pivot: int) (cases: table) else (same, (key, act) :: others) end. -Fixpoint split_between (ofs sz: int) (cases: table) +Fixpoint split_between (dfl: nat) (ofs sz: int) (cases: table) {struct cases} : IntMap.t nat * table := match cases with - | nil => (IntMap.empty nat, nil) + | nil => (IntMap.init dfl, nil) | (key, act) :: rem => - let (inside, outside) := split_between ofs sz rem in + let (inside, outside) := split_between dfl ofs sz rem in if Int.ltu (Int.sub key ofs) sz - then (IntMap.add key act inside, outside) + then (IntMap.set key act inside, outside) else (inside, (key, act) :: outside) end. @@ -110,13 +130,13 @@ Definition refine_low_bound (v lo: Z) := Definition refine_high_bound (v hi: Z) := if zeq v hi then hi - 1 else hi. -Fixpoint validate_jumptable (cases: IntMap.t nat) (default: nat) +Fixpoint validate_jumptable (cases: IntMap.t nat) (tbl: list nat) (n: int) {struct tbl} : bool := match tbl with | nil => true | act :: rem => - beq_nat act (match IntMap.find n cases with Some a => a | None => default end) - && validate_jumptable cases default rem (Int.add n Int.one) + beq_nat act (IntMap.get n cases) + && validate_jumptable cases rem (Int.add n Int.one) end. Fixpoint validate (default: nat) (cases: table) (t: comptree) @@ -147,11 +167,11 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree) end | CTjumptable ofs sz tbl t' => let tbl_len := list_length_z tbl in - match split_between ofs sz cases with + match split_between default ofs sz cases with | (inside, outside) => zle (Int.unsigned sz) tbl_len && zle tbl_len Int.max_signed - && validate_jumptable inside default tbl ofs + && validate_jumptable inside tbl ofs && validate default outside t' lo hi end end. @@ -207,33 +227,33 @@ Qed. Lemma split_between_prop: forall v default ofs sz cases inside outside, - split_between ofs sz cases = (inside, outside) -> + split_between default ofs sz cases = (inside, outside) -> switch_target v default cases = (if Int.ltu (Int.sub v ofs) sz - then match IntMap.find v inside with Some a => a | None => default end + then IntMap.get v inside else switch_target v default outside). Proof. - induction cases; intros until outside; simpl. - intros. inv H. simpl. destruct (Int.ltu (Int.sub v ofs) sz); auto. - destruct a as [key act]. case_eq (split_between ofs sz cases). intros ins outs SEQ. - rewrite (IHcases _ _ SEQ). - case_eq (Int.ltu (Int.sub key ofs) sz); intros; inv H0; simpl. - rewrite IntMapF.add_o. - predSpec Int.eq Int.eq_spec v key. - subst v. rewrite H. rewrite dec_eq_true. auto. - rewrite dec_eq_false; auto. - case_eq (Int.ltu (Int.sub v ofs) sz); intros; auto. - predSpec Int.eq Int.eq_spec v key. - subst v. congruence. - auto. + induction cases; intros until outside; simpl; intros SEQ. +- inv SEQ. destruct (Int.ltu (Int.sub v ofs) sz); auto. rewrite IntMap.gi. auto. +- destruct a as [key act]. + destruct (split_between default ofs sz cases) as [ins outs]. + erewrite IHcases; eauto. + destruct (Int.ltu (Int.sub key ofs) sz) eqn:LT; inv SEQ. + + predSpec Int.eq Int.eq_spec v key. + subst v. rewrite LT. rewrite IntMap.gss. auto. + destruct (Int.ltu (Int.sub v ofs) sz). + rewrite IntMap.gso; auto. + auto. + + simpl. destruct (Int.ltu (Int.sub v ofs) sz) eqn:LT'. + rewrite Int.eq_false. auto. congruence. + auto. Qed. Lemma validate_jumptable_correct_rec: - forall cases default tbl base v, - validate_jumptable cases default tbl base = true -> + forall cases tbl base v, + validate_jumptable cases tbl base = true -> 0 <= Int.unsigned v < list_length_z tbl -> - list_nth_z tbl (Int.unsigned v) = - Some(match IntMap.find (Int.add base v) cases with Some a => a | None => default end). + list_nth_z tbl (Int.unsigned v) = Some(IntMap.get (Int.add base v) cases). Proof. induction tbl; intros until v; simpl. unfold list_length_z; simpl. intros. omegaContradiction. @@ -254,16 +274,15 @@ Proof. Qed. Lemma validate_jumptable_correct: - forall cases default tbl ofs v sz, - validate_jumptable cases default tbl ofs = true -> + forall cases tbl ofs v sz, + validate_jumptable cases tbl ofs = true -> Int.ltu (Int.sub v ofs) sz = true -> Int.unsigned sz <= list_length_z tbl -> - list_nth_z tbl (Int.unsigned (Int.sub v ofs)) = - Some(match IntMap.find v cases with Some a => a | None => default end). + list_nth_z tbl (Int.unsigned (Int.sub v ofs)) = Some(IntMap.get v cases). Proof. intros. exploit Int.ltu_inv; eauto. intros. - rewrite (validate_jumptable_correct_rec cases default tbl ofs). + rewrite (validate_jumptable_correct_rec cases tbl ofs). rewrite Int.sub_add_opp. rewrite Int.add_permut. rewrite <- Int.sub_add_opp. rewrite Int.sub_idem. rewrite Int.add_zero. auto. auto. @@ -312,7 +331,7 @@ Opaque Int.sub. eapply IHt1. eauto. omega. eapply IHt2. eauto. omega. (* jumptable node *) - case_eq (split_between i i0 cases). intros ins outs EQ V RANGE. + case_eq (split_between default i i0 cases). intros ins outs EQ V RANGE. destruct (andb_prop _ _ V). clear V. destruct (andb_prop _ _ H). clear H. destruct (andb_prop _ _ H1). clear H1. -- cgit v1.2.3