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

3 files changed, 139 insertions, 1 deletions

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.