From 74487f079dd56663f97f9731cea328931857495c Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 10 Nov 2009 12:50:57 +0000 Subject: Added support for jump tables in back end. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Coqlib.v | 74 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/Integers.v | 25 ++++++++++++++++++++ lib/Ordered.v | 41 +++++++++++++++++++++++++++++++- 3 files changed, 139 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 416afa9..7bc4f8b 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -612,6 +612,80 @@ Proof. Qed. Hint Resolve nth_error_nil: coqlib. +(** Compute the length of a list, with result in [Z]. *) + +Fixpoint list_length_z_aux (A: Type) (l: list A) (acc: Z) {struct l}: Z := + match l with + | nil => acc + | hd :: tl => list_length_z_aux tl (Zsucc acc) + end. + +Remark list_length_z_aux_shift: + forall (A: Type) (l: list A) n m, + list_length_z_aux l n = list_length_z_aux l m + (n - m). +Proof. + induction l; intros; simpl. + omega. + replace (n - m) with (Zsucc n - Zsucc m) by omega. auto. +Qed. + +Definition list_length_z (A: Type) (l: list A) : Z := + list_length_z_aux l 0. + +Lemma list_length_z_cons: + forall (A: Type) (hd: A) (tl: list A), + list_length_z (hd :: tl) = list_length_z tl + 1. +Proof. + intros. unfold list_length_z. simpl. + rewrite (list_length_z_aux_shift tl 1 0). omega. +Qed. + +Lemma list_length_z_pos: + forall (A: Type) (l: list A), + list_length_z l >= 0. +Proof. + induction l; simpl. unfold list_length_z; simpl. omega. + rewrite list_length_z_cons. omega. +Qed. + +(** Extract the n-th element of a list, as [List.nth_error] does, + but the index [n] is of type [Z]. *) + +Fixpoint list_nth_z (A: Type) (l: list A) (n: Z) {struct l}: option A := + match l with + | nil => None + | hd :: tl => if zeq n 0 then Some hd else list_nth_z tl (Zpred n) + end. + +Lemma list_nth_z_in: + forall (A: Type) (l: list A) n x, + list_nth_z l n = Some x -> In x l. +Proof. + induction l; simpl; intros. + congruence. + destruct (zeq n 0). left; congruence. right; eauto. +Qed. + +Lemma list_nth_z_map: + forall (A B: Type) (f: A -> B) (l: list A) n, + list_nth_z (List.map f l) n = option_map f (list_nth_z l n). +Proof. + induction l; simpl; intros. + auto. + destruct (zeq n 0). auto. eauto. +Qed. + +Lemma list_nth_z_range: + forall (A: Type) (l: list A) n x, + list_nth_z l n = Some x -> 0 <= n < list_length_z l. +Proof. + induction l; simpl; intros. + discriminate. + rewrite list_length_z_cons. destruct (zeq n 0). + generalize (list_length_z_pos l); omega. + exploit IHl; eauto. unfold Zpred. omega. +Qed. + (** Properties of [List.incl] (list inclusion). *) Lemma incl_cons_inv: diff --git a/lib/Integers.v b/lib/Integers.v index 1eb59c5..c54b6fe 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -657,6 +657,13 @@ Proof. apply eqm_samerepr. unfold z'; red. exists 1. omega. Qed. +Theorem signed_eq_unsigned: + forall x, unsigned x <= max_signed -> signed x = unsigned x. +Proof. + intros. unfold signed. destruct (zlt (unsigned x) half_modulus). + auto. unfold max_signed in H. omegaContradiction. +Qed. + (** ** Properties of addition *) Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y). @@ -786,6 +793,13 @@ Proof. symmetry. apply sub_add_opp. Qed. +Theorem sub_signed: + forall x y, sub x y = repr (signed x - signed y). +Proof. + intros. unfold sub. apply eqm_samerepr. + apply eqm_sub; apply eqm_sym; apply eqm_signed_unsigned. +Qed. + (** ** Properties of multiplication *) Theorem mul_commut: forall x y, mul x y = mul y x. @@ -2565,4 +2579,15 @@ Proof. omega. Qed. +Theorem ltu_range_test: + forall x y, + ltu x y = true -> unsigned y <= max_signed -> + 0 <= signed x < unsigned y. +Proof. + intros. + unfold Int.ltu in H. destruct (zlt (unsigned x) (unsigned y)); try discriminate. + rewrite signed_eq_unsigned. + generalize (unsigned_range x). omega. omega. +Qed. + End Int. diff --git a/lib/Ordered.v b/lib/Ordered.v index eddc372..1c7c7f4 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -11,11 +11,12 @@ (* *********************************************************************) (** Constructions of ordered types, for use with the [FSet] functors - for finite sets. *) + for finite sets and the [FMap] functors for finite maps. *) Require Import FSets. Require Import Coqlib. Require Import Maps. +Require Import Integers. (** The ordered type of positive numbers *) @@ -49,6 +50,44 @@ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq. End OrderedPositive. +(** The ordered type of machine integers *) + +Module OrderedInt <: OrderedType. + +Definition t := int. +Definition eq (x y: t) := x = y. +Definition lt (x y: t) := Int.unsigned x < Int.unsigned y. + +Lemma eq_refl : forall x : t, eq x x. +Proof (@refl_equal t). +Lemma eq_sym : forall x y : t, eq x y -> eq y x. +Proof (@sym_equal t). +Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. +Proof (@trans_equal t). +Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. +Proof. + unfold lt; intros. omega. +Qed. +Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. +Proof. + unfold lt,eq; intros; red; intros. subst. omega. +Qed. +Lemma compare : forall x y : t, Compare lt eq x y. +Proof. + intros. destruct (zlt (Int.unsigned x) (Int.unsigned y)). + apply LT. auto. + destruct (Int.eq_dec x y). + apply EQ. auto. + apply GT. + assert (Int.unsigned x <> Int.unsigned y). + red; intros. rewrite <- (Int.repr_unsigned x) in n. rewrite <- (Int.repr_unsigned y) in n. congruence. + red. omega. +Qed. + +Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := Int.eq_dec. + +End OrderedInt. + (** Indexed types (those that inject into [positive]) are ordered. *) Module OrderedIndexed(A: INDEXED_TYPE) <: OrderedType. -- cgit v1.2.3