Merge of branch "unsigned-offsets":

- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int.
  (Fixes issue with wrong comparison of pointers across 0x8000_0000)
- Revised Stacking pass to not use negative SP offsets.
- Add pointer validity checks to Cminor ... Mach
  to support the use of memory injections in Stacking.
- Cleaned up Stacklayout modules.
- IA32: improved code generation for Mgetparam.
- ARM: improved code generation for op-immediate instructions.


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

4 files changed, 93 insertions, 80 deletions

diff --git a/common/Events.v b/common/Events.v
index f590573..b369d46 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -582,7 +582,7 @@ Inductive volatile_load_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V):
           (Val.load_result chunk v) m
   | volatile_load_sem_nonvol: forall b ofs m v,
       block_is_volatile ge b = false ->
-      Mem.load chunk m b (Int.signed ofs) = Some v ->
+      Mem.load chunk m b (Int.unsigned ofs) = Some v ->
       volatile_load_sem chunk ge
           (Vptr b ofs :: nil) m
           E0
@@ -675,7 +675,7 @@ Inductive volatile_store_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V):
           Vundef m
   | volatile_store_sem_nonvol: forall b ofs m v m',
       block_is_volatile ge b = false ->
-      Mem.store chunk m b (Int.signed ofs) v = Some m' ->
+      Mem.store chunk m b (Int.unsigned ofs) v = Some m' ->
       volatile_store_sem chunk ge
           (Vptr b ofs :: v :: nil) m
           E0
@@ -719,7 +719,7 @@ Proof.
   generalize (size_chunk_pos chunk0). intro E.
   generalize (size_chunk_pos chunk). intro G.
   apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
-                              (Int.signed ofs, Int.signed ofs + size_chunk chunk)).
+                              (Int.unsigned ofs, Int.unsigned ofs + size_chunk chunk)).
   red; intros. generalize (H x H5). unfold loc_out_of_bounds, Intv.In; simpl. omega.
   simpl; omega. simpl; omega.
 
@@ -746,16 +746,16 @@ Proof.
   split; intros. eapply Mem.perm_store_1; eauto.
   rewrite <- H4. eapply Mem.load_store_other; eauto.
   destruct (eq_block b0 b2); auto. subst b0; right.
-  assert (EQ: Int.signed (Int.add ofs (Int.repr delta)) = Int.signed ofs + delta).
+  assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta).
     eapply Mem.address_inject; eauto with mem.
-  simpl in A. rewrite EQ in A. rewrite EQ.
+  unfold Mem.storev in A. rewrite EQ in A. rewrite EQ.
   exploit Mem.valid_access_in_bounds. 
   eapply Mem.store_valid_access_3. eexact H0.
   intros [C D].
   generalize (size_chunk_pos chunk0). intro E.
   generalize (size_chunk_pos chunk). intro G.
   apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
-                              (Int.signed ofs + delta, Int.signed ofs + delta + size_chunk chunk)).
+                              (Int.unsigned ofs + delta, Int.unsigned ofs + delta + size_chunk chunk)).
   red; intros. exploit (H2 x H8). eauto. unfold Intv.In; simpl. omega.
   simpl; omega. simpl; omega.
   red; intros; congruence.
@@ -772,7 +772,7 @@ Qed.
 Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V):
               list val -> mem -> trace -> val -> mem -> Prop :=
   | extcall_malloc_sem_intro: forall n m m' b m'',
-      Mem.alloc m (-4) (Int.signed n) = (m', b) ->
+      Mem.alloc m (-4) (Int.unsigned n) = (m', b) ->
       Mem.store Mint32 m' b (-4) (Vint n) = Some m'' ->
       extcall_malloc_sem ge (Vint n :: nil) m E0 (Vptr b Int.zero) m''.
 
@@ -782,7 +782,7 @@ Lemma extcall_malloc_ok:
 Proof.
   assert (UNCHANGED:
     forall (P: block -> Z -> Prop) m n m' b m'',
-    Mem.alloc m (-4) (Int.signed n) = (m', b) ->
+    Mem.alloc m (-4) (Int.unsigned n) = (m', b) ->
     Mem.store Mint32 m' b (-4) (Vint n) = Some m'' ->
     mem_unchanged_on P m m'').
   intros; split; intros.
@@ -840,9 +840,9 @@ Qed.
 Inductive extcall_free_sem  (F V: Type) (ge: Genv.t F V):
               list val -> mem -> trace -> val -> mem -> Prop :=
   | extcall_free_sem_intro: forall b lo sz m m',
-      Mem.load Mint32 m b (Int.signed lo - 4) = Some (Vint sz) ->
-      Int.signed sz > 0 ->
-      Mem.free m b (Int.signed lo - 4) (Int.signed lo + Int.signed sz) = Some m' ->
+      Mem.load Mint32 m b (Int.unsigned lo - 4) = Some (Vint sz) ->
+      Int.unsigned sz > 0 ->
+      Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) = Some m' ->
       extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'.
 
 Lemma extcall_free_ok:
@@ -889,13 +889,13 @@ Proof.
 
   inv H0. inv H2. inv H7. inv H9.
   exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. 
-  assert (Mem.range_perm m1 b (Int.signed lo - 4) (Int.signed lo + Int.signed sz) Freeable).
+  assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Freeable).
     eapply Mem.free_range_perm; eauto.
   exploit Mem.address_inject; eauto. 
     apply Mem.perm_implies with Freeable; auto with mem.
     apply H0. instantiate (1 := lo). omega. 
   intro EQ.
-  assert (Mem.range_perm m1' b2 (Int.signed lo + delta - 4) (Int.signed lo + delta + Int.signed sz) Freeable).
+  assert (Mem.range_perm m1' b2 (Int.unsigned lo + delta - 4) (Int.unsigned lo + delta + Int.unsigned sz) Freeable).
     red; intros. 
     replace ofs with ((ofs - delta) + delta) by omega.
     eapply Mem.perm_inject; eauto. apply H0. omega. 
@@ -903,16 +903,16 @@ Proof.
   exists f; exists Vundef; exists m2'; intuition.
 
   econstructor.
-  rewrite EQ. replace (Int.signed lo + delta - 4) with (Int.signed lo - 4 + delta) by omega.
+  rewrite EQ. replace (Int.unsigned lo + delta - 4) with (Int.unsigned lo - 4 + delta) by omega.
   eauto. auto. 
   rewrite EQ. auto.
   
-  assert (Mem.free_list m1 ((b, Int.signed lo - 4, Int.signed lo + Int.signed sz) :: nil) = Some m2).
+  assert (Mem.free_list m1 ((b, Int.unsigned lo - 4, Int.unsigned lo + Int.unsigned sz) :: nil) = Some m2).
     simpl. rewrite H5. auto.
   eapply Mem.free_inject; eauto. 
   intros. destruct (eq_block b b1).
   subst b. assert (delta0 = delta) by congruence. subst delta0. 
-  exists (Int.signed lo - 4); exists (Int.signed lo + Int.signed sz); split.
+  exists (Int.unsigned lo - 4); exists (Int.unsigned lo + Int.unsigned sz); split.
   simpl; auto. omega.
   elimtype False.
   exploit Mem.inject_no_overlap. eauto. eauto. eauto. eauto. 
@@ -1111,3 +1111,16 @@ Proof.
   exploit H2; eauto. intros [g1 [A B]]. congruence.
   auto.
 Qed.
+
+(** Corollary of [external_call_valid_block]. *)
+
+Lemma external_call_nextblock:
+  forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2,
+  external_call ef ge vargs m1 t vres m2 ->
+  Mem.nextblock m1 <= Mem.nextblock m2.
+Proof.
+  intros. 
+  exploit external_call_valid_block; eauto. 
+  instantiate (1 := Mem.nextblock m1 - 1). red; omega.
+  unfold Mem.valid_block. omega.
+Qed.
diff --git a/common/Memory.v b/common/Memory.v
index a6594e4..d7d1d7b 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -488,7 +488,7 @@ Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z): option val :
 
 Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
   match addr with
-  | Vptr b ofs => load chunk m b (Int.signed ofs)
+  | Vptr b ofs => load chunk m b (Int.unsigned ofs)
   | _ => None
   end.
 
@@ -608,7 +608,7 @@ Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val): op
 
 Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   match addr with
-  | Vptr b ofs => store chunk m b (Int.signed ofs) v
+  | Vptr b ofs => store chunk m b (Int.unsigned ofs) v
   | _ => None
   end.
 
@@ -2658,12 +2658,12 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop :=
     mi_range_offset:
       forall b b' delta,
       f b = Some(b', delta) ->
-      Int.min_signed <= delta <= Int.max_signed;
+      0 <= delta <= Int.max_unsigned;
     mi_range_block:
       forall b b' delta,
       f b = Some(b', delta) ->
       delta = 0 \/ 
-      (Int.min_signed <= low_bound m2 b' /\ high_bound m2 b' <= Int.max_signed)
+      (0 <= low_bound m2 b' /\ high_bound m2 b' <= Int.max_unsigned)
   }.
 
 Definition inject := inject'.
@@ -2731,17 +2731,17 @@ Qed.
 Lemma address_inject:
   forall f m1 m2 b1 ofs1 b2 delta,
   inject f m1 m2 ->
-  perm m1 b1 (Int.signed ofs1) Nonempty ->
+  perm m1 b1 (Int.unsigned ofs1) Nonempty ->
   f b1 = Some (b2, delta) ->
-  Int.signed (Int.add ofs1 (Int.repr delta)) = Int.signed ofs1 + delta.
+  Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 Proof.
   intros.
   exploit perm_inject; eauto. intro A.
   exploit perm_in_bounds. eexact A. intros [B C]. 
   exploit mi_range_block; eauto. intros [D | [E F]].
   subst delta. rewrite Int.add_zero. omega.
-  rewrite Int.add_signed.
-  repeat rewrite Int.signed_repr. auto.
+  unfold Int.add.
+  repeat rewrite Int.unsigned_repr. auto.
   eapply mi_range_offset; eauto.
   omega. 
   eapply mi_range_offset; eauto.
@@ -2750,9 +2750,9 @@ Qed.
 Lemma address_inject':
   forall f m1 m2 chunk b1 ofs1 b2 delta,
   inject f m1 m2 ->
-  valid_access m1 chunk b1 (Int.signed ofs1) Nonempty ->
+  valid_access m1 chunk b1 (Int.unsigned ofs1) Nonempty ->
   f b1 = Some (b2, delta) ->
-  Int.signed (Int.add ofs1 (Int.repr delta)) = Int.signed ofs1 + delta.
+  Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 Proof.
   intros. destruct H0. eapply address_inject; eauto. 
   apply H0. generalize (size_chunk_pos chunk). omega. 
@@ -2761,28 +2761,28 @@ Qed.
 Theorem valid_pointer_inject_no_overflow:
   forall f m1 m2 b ofs b' x,
   inject f m1 m2 ->
-  valid_pointer m1 b (Int.signed ofs) = true ->
+  valid_pointer m1 b (Int.unsigned ofs) = true ->
   f b = Some(b', x) ->
-  Int.min_signed <= Int.signed ofs + Int.signed (Int.repr x) <= Int.max_signed.
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr x) <= Int.max_unsigned.
 Proof.
   intros. rewrite valid_pointer_valid_access in H0.
   exploit address_inject'; eauto. intros.
-  rewrite Int.signed_repr; eauto.
-  rewrite <- H2. apply Int.signed_range. 
+  rewrite Int.unsigned_repr; eauto.
+  rewrite <- H2. apply Int.unsigned_range_2. 
   eapply mi_range_offset; eauto.
 Qed.
 
 Theorem valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
   inject f m1 m2 ->
-  valid_pointer m1 b (Int.signed ofs) = true ->
+  valid_pointer m1 b (Int.unsigned ofs) = true ->
   val_inject f (Vptr b ofs) (Vptr b' ofs') ->
-  valid_pointer m2 b' (Int.signed ofs') = true.
+  valid_pointer m2 b' (Int.unsigned ofs') = true.
 Proof.
   intros. inv H1.
   exploit valid_pointer_inject_no_overflow; eauto. intro NOOV.
-  rewrite Int.add_signed. rewrite Int.signed_repr; auto.
-  rewrite Int.signed_repr.
+  unfold Int.add. rewrite Int.unsigned_repr; auto.
+  rewrite Int.unsigned_repr.
   eapply valid_pointer_inject; eauto.
   eapply mi_range_offset; eauto.
 Qed.
@@ -2804,13 +2804,13 @@ Theorem different_pointers_inject:
   forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
   inject f m m' ->
   b1 <> b2 ->
-  valid_pointer m b1 (Int.signed ofs1) = true ->
-  valid_pointer m b2 (Int.signed ofs2) = true ->
+  valid_pointer m b1 (Int.unsigned ofs1) = true ->
+  valid_pointer m b2 (Int.unsigned ofs2) = true ->
   f b1 = Some (b1', delta1) ->
   f b2 = Some (b2', delta2) ->
   b1' <> b2' \/
-  Int.signed (Int.add ofs1 (Int.repr delta1)) <>
-  Int.signed (Int.add ofs2 (Int.repr delta2)).
+  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <>
+  Int.unsigned (Int.add ofs2 (Int.repr delta2)).
 Proof.
   intros. 
   rewrite valid_pointer_valid_access in H1. 
@@ -2820,8 +2820,8 @@ Proof.
   inv H1. simpl in H5. inv H2. simpl in H1.
   eapply meminj_no_overlap_perm. 
   eapply mi_no_overlap; eauto. eauto. eauto. eauto. 
-  apply (H5 (Int.signed ofs1)). omega.
-  apply (H1 (Int.signed ofs2)). omega.
+  apply (H5 (Int.unsigned ofs1)). omega.
+  apply (H1 (Int.unsigned ofs2)). omega.
 Qed.
 
 (** Preservation of loads *)
@@ -2845,9 +2845,9 @@ Theorem loadv_inject:
 Proof.
   intros. inv H1; simpl in H0; try discriminate.
   exploit load_inject; eauto. intros [v2 [LOAD INJ]].
-  exists v2; split; auto. simpl.
-  replace (Int.signed (Int.add ofs1 (Int.repr delta)))
-     with (Int.signed ofs1 + delta).
+  exists v2; split; auto. unfold loadv. 
+  replace (Int.unsigned (Int.add ofs1 (Int.repr delta)))
+     with (Int.unsigned ofs1 + delta).
   auto. symmetry. eapply address_inject'; eauto with mem.
 Qed.
 
@@ -2944,8 +2944,9 @@ Theorem storev_mapped_inject:
     storev chunk m2 a2 v2 = Some n2 /\ inject f n1 n2.
 Proof.
   intros. inv H1; simpl in H0; try discriminate.
-  simpl. replace (Int.signed (Int.add ofs1 (Int.repr delta)))
-            with (Int.signed ofs1 + delta).
+  unfold storev.
+  replace (Int.unsigned (Int.add ofs1 (Int.repr delta)))
+    with (Int.unsigned ofs1 + delta).
   eapply store_mapped_inject; eauto.
   symmetry. eapply address_inject'; eauto with mem.
 Qed.
@@ -3026,8 +3027,8 @@ Theorem alloc_left_mapped_inject:
   inject f m1 m2 ->
   alloc m1 lo hi = (m1', b1) ->
   valid_block m2 b2 ->
-  Int.min_signed <= delta <= Int.max_signed ->
-  delta = 0 \/ Int.min_signed <= low_bound m2 b2 /\ high_bound m2 b2 <= Int.max_signed ->
+  0 <= delta <= Int.max_unsigned ->
+  delta = 0 \/ 0 <= low_bound m2 b2 /\ high_bound m2 b2 <= Int.max_unsigned ->
   (forall ofs p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) p) ->
   inj_offset_aligned delta (hi-lo) ->
   (forall b ofs, 
@@ -3103,7 +3104,7 @@ Proof.
   eapply alloc_right_inject; eauto.
   eauto.
   instantiate (1 := b2). eauto with mem.
-  instantiate (1 := 0). generalize Int.min_signed_neg Int.max_signed_pos; omega.
+  instantiate (1 := 0). unfold Int.max_unsigned. generalize Int.modulus_pos; omega.
   auto.
   intros.
   apply perm_implies with Freeable; auto with mem.
@@ -3260,7 +3261,7 @@ Proof.
 (* range *)
   unfold flat_inj; intros.
   destruct (zlt b (nextblock m)); inv H0.
-  generalize Int.min_signed_neg Int.max_signed_pos; omega.
+  unfold Int.max_unsigned. generalize Int.modulus_pos; omega.
 (* range *)
   unfold flat_inj; intros.
   destruct (zlt b (nextblock m)); inv H0. auto.
diff --git a/common/Memtype.v b/common/Memtype.v
index 050cc84..0973643 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -110,13 +110,13 @@ Parameter store: forall (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: v
 
 Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
   match addr with
-  | Vptr b ofs => load chunk m b (Int.signed ofs)
+  | Vptr b ofs => load chunk m b (Int.unsigned ofs)
   | _ => None
   end.
 
 Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   match addr with
-  | Vptr b ofs => store chunk m b (Int.signed ofs) v
+  | Vptr b ofs => store chunk m b (Int.unsigned ofs) v
   | _ => None
   end.
 
@@ -837,23 +837,23 @@ Axiom valid_pointer_inject:
 Axiom address_inject:
   forall f m1 m2 b1 ofs1 b2 delta,
   inject f m1 m2 ->
-  perm m1 b1 (Int.signed ofs1) Nonempty ->
+  perm m1 b1 (Int.unsigned ofs1) Nonempty ->
   f b1 = Some (b2, delta) ->
-  Int.signed (Int.add ofs1 (Int.repr delta)) = Int.signed ofs1 + delta.
+  Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 
 Axiom valid_pointer_inject_no_overflow:
   forall f m1 m2 b ofs b' x,
   inject f m1 m2 ->
-  valid_pointer m1 b (Int.signed ofs) = true ->
+  valid_pointer m1 b (Int.unsigned ofs) = true ->
   f b = Some(b', x) ->
-  Int.min_signed <= Int.signed ofs + Int.signed (Int.repr x) <= Int.max_signed.
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr x) <= Int.max_unsigned.
 
 Axiom valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
   inject f m1 m2 ->
-  valid_pointer m1 b (Int.signed ofs) = true ->
+  valid_pointer m1 b (Int.unsigned ofs) = true ->
   val_inject f (Vptr b ofs) (Vptr b' ofs') ->
-  valid_pointer m2 b' (Int.signed ofs') = true.
+  valid_pointer m2 b' (Int.unsigned ofs') = true.
 
 Axiom inject_no_overlap:
   forall f m1 m2 b1 b2 b1' b2' delta1 delta2 ofs1 ofs2,
@@ -869,13 +869,13 @@ Axiom different_pointers_inject:
   forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
   inject f m m' ->
   b1 <> b2 ->
-  valid_pointer m b1 (Int.signed ofs1) = true ->
-  valid_pointer m b2 (Int.signed ofs2) = true ->
+  valid_pointer m b1 (Int.unsigned ofs1) = true ->
+  valid_pointer m b2 (Int.unsigned ofs2) = true ->
   f b1 = Some (b1', delta1) ->
   f b2 = Some (b2', delta2) ->
   b1' <> b2' \/
-  Int.signed (Int.add ofs1 (Int.repr delta1)) <>
-  Int.signed (Int.add ofs2 (Int.repr delta2)).
+  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <>
+  Int.unsigned (Int.add ofs2 (Int.repr delta2)).
 
 Axiom load_inject:
   forall f m1 m2 chunk b1 ofs b2 delta v1,
@@ -951,8 +951,8 @@ Axiom alloc_left_mapped_inject:
   inject f m1 m2 ->
   alloc m1 lo hi = (m1', b1) ->
   valid_block m2 b2 ->
-  Int.min_signed <= delta <= Int.max_signed ->
-  delta = 0 \/ Int.min_signed <= low_bound m2 b2 /\ high_bound m2 b2 <= Int.max_signed ->
+  0 <= delta <= Int.max_unsigned ->
+  delta = 0 \/ 0 <= low_bound m2 b2 /\ high_bound m2 b2 <= Int.max_unsigned ->
   (forall ofs p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) p) ->
   inj_offset_aligned delta (hi-lo) ->
   (forall b ofs, 
diff --git a/common/Switch.v b/common/Switch.v
index ee8f6aa..1b3ca9b 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -60,7 +60,7 @@ Fixpoint comptree_match (n: int) (t: comptree) {struct t}: option nat :=
       if Int.ltu n key then comptree_match n t1 else comptree_match n t2
   | CTjumptable ofs sz tbl t' =>
       if Int.ltu (Int.sub n ofs) sz
-      then list_nth_z tbl (Int.signed (Int.sub n ofs))
+      then list_nth_z tbl (Int.unsigned (Int.sub n ofs))
       else comptree_match n t'
   end.
 
@@ -231,23 +231,22 @@ Qed.
 Lemma validate_jumptable_correct_rec:
   forall cases default tbl base v,
   validate_jumptable cases default tbl base = true ->
-  0 <= Int.signed v < list_length_z tbl -> Int.signed v <= Int.max_signed ->
-  list_nth_z tbl (Int.signed v) =
+  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).
 Proof.
   induction tbl; intros until v; simpl.
   unfold list_length_z; simpl. intros. omegaContradiction.
   rewrite list_length_z_cons. intros. destruct (andb_prop _ _ H). clear H.
-  generalize (beq_nat_eq _ _ (sym_equal H2)). clear H2. intro. subst a.
-  destruct (zeq (Int.signed v) 0).
-  rewrite Int.add_signed. rewrite e. rewrite Zplus_0_r. rewrite Int.repr_signed. auto.
-  assert (Int.signed (Int.sub v Int.one) = Int.signed v - 1).
-    rewrite Int.sub_signed. change (Int.signed Int.one) with 1. 
-    apply Int.signed_repr. split. apply Zle_trans with 0. 
-    vm_compute; congruence. omega. omega.
-    replace (Int.add base v) with (Int.add (Int.add base Int.one) (Int.sub v Int.one)).
+  generalize (beq_nat_eq _ _ (sym_equal H1)). clear H1. intro. subst a.
+  destruct (zeq (Int.unsigned v) 0).
+  unfold Int.add. rewrite e. rewrite Zplus_0_r. rewrite Int.repr_unsigned. auto.
+  assert (Int.unsigned (Int.sub v Int.one) = Int.unsigned v - 1).
+    unfold Int.sub. change (Int.unsigned Int.one) with 1. 
+    apply Int.unsigned_repr. split. omega.
+    generalize (Int.unsigned_range_2 v). omega.
+  replace (Int.add base v) with (Int.add (Int.add base Int.one) (Int.sub v Int.one)).
   rewrite <- IHtbl. rewrite H. auto. auto. rewrite H. omega. 
-  rewrite H. omega. 
   rewrite Int.sub_add_opp. rewrite Int.add_permut. rewrite Int.add_assoc. 
   replace (Int.add Int.one (Int.neg Int.one)) with Int.zero.
   rewrite Int.add_zero. apply Int.add_commut.
@@ -258,18 +257,17 @@ Lemma validate_jumptable_correct:
   forall cases default tbl ofs v sz,
   validate_jumptable cases default tbl ofs = true ->
   Int.ltu (Int.sub v ofs) sz = true ->
-  Int.unsigned sz <= list_length_z tbl <= Int.max_signed ->
-  list_nth_z tbl (Int.signed (Int.sub v ofs)) =
+  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).
 Proof.
   intros.
-  exploit Int.ltu_range_test; eauto. omega. intros. 
+  exploit Int.ltu_inv; eauto. intros. 
   rewrite (validate_jumptable_correct_rec cases default 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.
   omega. 
-  omega.
 Qed.
 
 Lemma validate_correct_rec:
@@ -278,6 +276,7 @@ Lemma validate_correct_rec:
   lo <= Int.unsigned v <= hi ->
   comptree_match v t = Some (switch_target v default cases).
 Proof.
+Opaque Int.sub.
   induction t; simpl; intros until hi.
   (* base case *)
   destruct cases as [ | [key1 act1] cases1]; intros.
@@ -320,7 +319,7 @@ Proof.
   rewrite (split_between_prop v _ _ _ _ _ _ EQ).
   case_eq (Int.ltu (Int.sub v i) i0); intros.
   eapply validate_jumptable_correct; eauto. 
-  split; eapply proj_sumbool_true; eauto.
+  eapply proj_sumbool_true; eauto.
   eapply IHt; eauto. 
 Qed.