From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: 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 --- common/Events.v | 45 +++++++++++++++++++++++-------------- common/Memory.v | 67 ++++++++++++++++++++++++++++---------------------------- common/Memtype.v | 28 +++++++++++------------ common/Switch.v | 33 ++++++++++++++-------------- 4 files changed, 93 insertions(+), 80 deletions(-) (limited to 'common') 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. -- cgit v1.2.3