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/Memory.v | 67 +++++++++++++++++++++++++++++---------------------------- 1 file changed, 34 insertions(+), 33 deletions(-) (limited to 'common/Memory.v') 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. -- cgit v1.2.3