From e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:25:18 +0200 Subject: Support for 64-bit architectures: generic support - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly. --- backend/ValueDomain.v | 731 ++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 617 insertions(+), 114 deletions(-) (limited to 'backend/ValueDomain.v') diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index bc09c3dc..6b314904 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -116,21 +116,21 @@ Qed. (** * Abstracting pointers *) Inductive aptr : Type := - | Pbot (**r bottom (empty set of pointers) *) - | Gl (id: ident) (ofs: int) (**r pointer into the block for global variable [id] at offset [ofs] *) - | Glo (id: ident) (**r pointer anywhere into the block for global [id] *) - | Glob (**r pointer into any global variable *) - | Stk (ofs: int) (**r pointer into the current stack frame at offset [ofs] *) - | Stack (**r pointer anywhere into the current stack frame *) - | Nonstack (**r pointer anywhere but into the current stack frame *) - | Ptop. (**r any valid pointer *) + | Pbot (**r bottom (empty set of pointers) *) + | Gl (id: ident) (ofs: ptrofs) (**r pointer into the block for global variable [id] at offset [ofs] *) + | Glo (id: ident) (**r pointer anywhere into the block for global [id] *) + | Glob (**r pointer into any global variable *) + | Stk (ofs: ptrofs) (**r pointer into the current stack frame at offset [ofs] *) + | Stack (**r pointer anywhere into the current stack frame *) + | Nonstack (**r pointer anywhere but into the current stack frame *) + | Ptop. (**r any valid pointer *) Definition eq_aptr: forall (p1 p2: aptr), {p1=p2} + {p1<>p2}. Proof. - intros. generalize ident_eq, Int.eq_dec; intros. decide equality. + intros. generalize ident_eq, Ptrofs.eq_dec; intros. decide equality. Defined. -Inductive pmatch (b: block) (ofs: int): aptr -> Prop := +Inductive pmatch (b: block) (ofs: ptrofs): aptr -> Prop := | pmatch_gl: forall id, bc b = BCglob id -> pmatch b ofs (Gl id ofs) @@ -191,7 +191,7 @@ Definition plub (p q: aptr) : aptr := | Pbot, _ => q | _, Pbot => p | Gl id1 ofs1, Gl id2 ofs2 => - if ident_eq id1 id2 then if Int.eq_dec ofs1 ofs2 then p else Glo id1 else Glob + if ident_eq id1 id2 then if Ptrofs.eq_dec ofs1 ofs2 then p else Glo id1 else Glob | Gl id1 ofs1, Glo id2 => if ident_eq id1 id2 then q else Glob | Glo id1, Gl id2 ofs2 => @@ -205,7 +205,7 @@ Definition plub (p q: aptr) : aptr := | Nonstack, (Gl _ _ | Glo _ | Glob) => Nonstack | Stk ofs1, Stk ofs2 => - if Int.eq_dec ofs1 ofs2 then p else Stack + if Ptrofs.eq_dec ofs1 ofs2 then p else Stack | (Stk _ | Stack), Stack => Stack | Stack, Stk _ => @@ -219,7 +219,7 @@ Proof. intros; unfold plub; destruct p; destruct q; auto. destruct (ident_eq id id0). subst id0. rewrite dec_eq_true. - destruct (Int.eq_dec ofs ofs0). subst ofs0. rewrite dec_eq_true. auto. + destruct (Ptrofs.eq_dec ofs ofs0). subst ofs0. rewrite dec_eq_true. auto. rewrite dec_eq_false by auto. auto. rewrite dec_eq_false by auto. auto. destruct (ident_eq id id0). subst id0. @@ -231,7 +231,7 @@ Proof. destruct (ident_eq id id0). subst id0. rewrite dec_eq_true; auto. rewrite dec_eq_false; auto. - destruct (Int.eq_dec ofs ofs0). subst ofs0. rewrite dec_eq_true; auto. + destruct (Ptrofs.eq_dec ofs ofs0). subst ofs0. rewrite dec_eq_true; auto. rewrite dec_eq_false; auto. Qed. @@ -240,12 +240,12 @@ Lemma pge_lub_l: Proof. unfold plub; destruct p, q; auto with va. - destruct (ident_eq id id0). - destruct (Int.eq_dec ofs ofs0); subst; constructor. + destruct (Ptrofs.eq_dec ofs ofs0); subst; constructor. constructor. - destruct (ident_eq id id0); subst; constructor. - destruct (ident_eq id id0); subst; constructor. - destruct (ident_eq id id0); subst; constructor. -- destruct (Int.eq_dec ofs ofs0); subst; constructor. +- destruct (Ptrofs.eq_dec ofs ofs0); subst; constructor. Qed. Lemma pge_lub_r: @@ -274,27 +274,27 @@ Proof. - unfold plub; destruct q; repeat rewrite dec_eq_true; constructor. - rewrite dec_eq_true; constructor. - rewrite dec_eq_true; constructor. -- rewrite dec_eq_true. destruct (Int.eq_dec ofs ofs0); constructor. -- destruct (ident_eq id id0). destruct (Int.eq_dec ofs ofs0); constructor. constructor. +- rewrite dec_eq_true. destruct (Ptrofs.eq_dec ofs ofs0); constructor. +- destruct (ident_eq id id0). destruct (Ptrofs.eq_dec ofs ofs0); constructor. constructor. - destruct (ident_eq id id0); constructor. - destruct (ident_eq id id0); constructor. - destruct (ident_eq id id0); constructor. -- destruct (ident_eq id id0). destruct (Int.eq_dec ofs ofs0); constructor. constructor. +- destruct (ident_eq id id0). destruct (Ptrofs.eq_dec ofs ofs0); constructor. constructor. - destruct (ident_eq id id0); constructor. - destruct (ident_eq id id0); constructor. - destruct (ident_eq id id0); constructor. -- destruct (Int.eq_dec ofs ofs0); constructor. +- destruct (Ptrofs.eq_dec ofs ofs0); constructor. Qed. Definition pincl (p q: aptr) : bool := match p, q with | Pbot, _ => true - | Gl id1 ofs1, Gl id2 ofs2 => peq id1 id2 && Int.eq_dec ofs1 ofs2 + | Gl id1 ofs1, Gl id2 ofs2 => peq id1 id2 && Ptrofs.eq_dec ofs1 ofs2 | Gl id1 ofs1, Glo id2 => peq id1 id2 | Glo id1, Glo id2 => peq id1 id2 | (Gl _ _ | Glo _ | Glob), Glob => true | (Gl _ _ | Glo _ | Glob | Nonstack), Nonstack => true - | Stk ofs1, Stk ofs2 => Int.eq_dec ofs1 ofs2 + | Stk ofs1, Stk ofs2 => Ptrofs.eq_dec ofs1 ofs2 | Stk ofs1, Stack => true | Stack, Stack => true | _, Ptop => true @@ -322,32 +322,32 @@ Proof. intros. eapply pmatch_ge; eauto. apply pincl_ge; auto. Qed. -Definition padd (p: aptr) (n: int) : aptr := +Definition padd (p: aptr) (n: ptrofs) : aptr := match p with - | Gl id ofs => Gl id (Int.add ofs n) - | Stk ofs => Stk (Int.add ofs n) + | Gl id ofs => Gl id (Ptrofs.add ofs n) + | Stk ofs => Stk (Ptrofs.add ofs n) | _ => p end. Lemma padd_sound: forall b ofs p delta, pmatch b ofs p -> - pmatch b (Int.add ofs delta) (padd p delta). + pmatch b (Ptrofs.add ofs delta) (padd p delta). Proof. intros. inv H; simpl padd; eauto with va. Qed. -Definition psub (p: aptr) (n: int) : aptr := +Definition psub (p: aptr) (n: ptrofs) : aptr := match p with - | Gl id ofs => Gl id (Int.sub ofs n) - | Stk ofs => Stk (Int.sub ofs n) + | Gl id ofs => Gl id (Ptrofs.sub ofs n) + | Stk ofs => Stk (Ptrofs.sub ofs n) | _ => p end. Lemma psub_sound: forall b ofs p delta, pmatch b ofs p -> - pmatch b (Int.sub ofs delta) (psub p delta). + pmatch b (Ptrofs.sub ofs delta) (psub p delta). Proof. intros. inv H; simpl psub; eauto with va. Qed. @@ -367,29 +367,6 @@ Proof. intros. inv H; simpl poffset; eauto with va. Qed. -Definition psub2 (p q: aptr) : option int := - match p, q with - | Gl id1 ofs1, Gl id2 ofs2 => - if peq id1 id2 then Some (Int.sub ofs1 ofs2) else None - | Stk ofs1, Stk ofs2 => - Some (Int.sub ofs1 ofs2) - | _, _ => - None - end. - -Lemma psub2_sound: - forall b1 ofs1 p1 b2 ofs2 p2 delta, - psub2 p1 p2 = Some delta -> - pmatch b1 ofs1 p1 -> - pmatch b2 ofs2 p2 -> - b1 = b2 /\ delta = Int.sub ofs1 ofs2. -Proof. - intros. destruct p1; try discriminate; destruct p2; try discriminate; simpl in H. -- destruct (peq id id0); inv H. inv H0; inv H1. - split. eapply bc_glob; eauto. reflexivity. -- inv H; inv H0; inv H1. split. eapply bc_stack; eauto. reflexivity. -Qed. - Definition cmp_different_blocks (c: comparison) : abool := match c with | Ceq => Maybe false @@ -413,7 +390,7 @@ Definition pcmp (c: comparison) (p1 p2: aptr) : abool := match p1, p2 with | Pbot, _ | _, Pbot => Bnone | Gl id1 ofs1, Gl id2 ofs2 => - if peq id1 id2 then Maybe (Int.cmpu c ofs1 ofs2) + if peq id1 id2 then Maybe (Ptrofs.cmpu c ofs1 ofs2) else cmp_different_blocks c | Gl id1 ofs1, Glo id2 => if peq id1 id2 then Btop else cmp_different_blocks c @@ -421,7 +398,7 @@ Definition pcmp (c: comparison) (p1 p2: aptr) : abool := if peq id1 id2 then Btop else cmp_different_blocks c | Glo id1, Glo id2 => if peq id1 id2 then Btop else cmp_different_blocks c - | Stk ofs1, Stk ofs2 => Maybe (Int.cmpu c ofs1 ofs2) + | Stk ofs1, Stk ofs2 => Maybe (Ptrofs.cmpu c ofs1 ofs2) | (Gl _ _ | Glo _ | Glob | Nonstack), (Stk _ | Stack) => cmp_different_blocks c | (Stk _ | Stack), (Gl _ _ | Glo _ | Glob | Nonstack) => cmp_different_blocks c | _, _ => Btop @@ -438,17 +415,59 @@ Proof. (cmp_different_blocks c)). { intros. simpl. rewrite dec_eq_false by assumption. - destruct (valid b1 (Int.unsigned ofs1) && valid b2 (Int.unsigned ofs2)); simpl. + destruct Archi.ptr64. + apply cmp_different_blocks_none. + destruct (valid b1 (Ptrofs.unsigned ofs1) && valid b2 (Ptrofs.unsigned ofs2)); simpl. apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } assert (SAME: b1 = b2 -> cmatch (Val.cmpu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2)) - (Maybe (Int.cmpu c ofs1 ofs2))). + (Maybe (Ptrofs.cmpu c ofs1 ofs2))). { - intros. subst b2. simpl. rewrite dec_eq_true. - destruct ((valid b1 (Int.unsigned ofs1) || valid b1 (Int.unsigned ofs1 - 1)) && - (valid b1 (Int.unsigned ofs2) || valid b1 (Int.unsigned ofs2 - 1))); simpl. + intros. subst b2. simpl. destruct Archi.ptr64. + constructor. + rewrite dec_eq_true. + destruct ((valid b1 (Ptrofs.unsigned ofs1) || valid b1 (Ptrofs.unsigned ofs1 - 1)) && + (valid b1 (Ptrofs.unsigned ofs2) || valid b1 (Ptrofs.unsigned ofs2 - 1))); simpl. + constructor. + constructor. + } + unfold pcmp; inv H; inv H0; (apply cmatch_top || (apply DIFF; congruence) || idtac). + - destruct (peq id id0). subst id0. apply SAME. eapply bc_glob; eauto. + auto with va. + - destruct (peq id id0); auto with va. + - destruct (peq id id0); auto with va. + - destruct (peq id id0); auto with va. + - apply SAME. eapply bc_stack; eauto. +Qed. + +Lemma pcmp_sound_64: + forall valid c b1 ofs1 p1 b2 ofs2 p2, + pmatch b1 ofs1 p1 -> pmatch b2 ofs2 p2 -> + cmatch (Val.cmplu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2)) (pcmp c p1 p2). +Proof. + intros. + assert (DIFF: b1 <> b2 -> + cmatch (Val.cmplu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2)) + (cmp_different_blocks c)). + { + intros. simpl. rewrite dec_eq_false by assumption. + destruct Archi.ptr64; simpl. + destruct (valid b1 (Ptrofs.unsigned ofs1) && valid b2 (Ptrofs.unsigned ofs2)); simpl. + apply cmp_different_blocks_sound. + apply cmp_different_blocks_none. + apply cmp_different_blocks_none. + } + assert (SAME: b1 = b2 -> + cmatch (Val.cmplu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2)) + (Maybe (Ptrofs.cmpu c ofs1 ofs2))). + { + intros. subst b2. simpl. destruct Archi.ptr64. + rewrite dec_eq_true. + destruct ((valid b1 (Ptrofs.unsigned ofs1) || valid b1 (Ptrofs.unsigned ofs1 - 1)) && + (valid b1 (Ptrofs.unsigned ofs2) || valid b1 (Ptrofs.unsigned ofs2 - 1))); simpl. + constructor. constructor. constructor. } @@ -475,15 +494,15 @@ Definition pdisjoint (p1: aptr) (sz1: Z) (p2: aptr) (sz2: Z) : bool := | _, Pbot => true | Gl id1 ofs1, Gl id2 ofs2 => if peq id1 id2 - then zle (Int.unsigned ofs1 + sz1) (Int.unsigned ofs2) - || zle (Int.unsigned ofs2 + sz2) (Int.unsigned ofs1) + then zle (Ptrofs.unsigned ofs1 + sz1) (Ptrofs.unsigned ofs2) + || zle (Ptrofs.unsigned ofs2 + sz2) (Ptrofs.unsigned ofs1) else true | Gl id1 ofs1, Glo id2 => negb(peq id1 id2) | Glo id1, Gl id2 ofs2 => negb(peq id1 id2) | Glo id1, Glo id2 => negb(peq id1 id2) | Stk ofs1, Stk ofs2 => - zle (Int.unsigned ofs1 + sz1) (Int.unsigned ofs2) - || zle (Int.unsigned ofs2 + sz2) (Int.unsigned ofs1) + zle (Ptrofs.unsigned ofs1 + sz1) (Ptrofs.unsigned ofs2) + || zle (Ptrofs.unsigned ofs2 + sz2) (Ptrofs.unsigned ofs1) | (Gl _ _ | Glo _ | Glob | Nonstack), (Stk _ | Stack) => true | (Stk _ | Stack), (Gl _ _ | Glo _ | Glob | Nonstack) => true | _, _ => false @@ -493,7 +512,7 @@ Lemma pdisjoint_sound: forall sz1 b1 ofs1 p1 sz2 b2 ofs2 p2, pdisjoint p1 sz1 p2 sz2 = true -> pmatch b1 ofs1 p1 -> pmatch b2 ofs2 p2 -> - b1 <> b2 \/ Int.unsigned ofs1 + sz1 <= Int.unsigned ofs2 \/ Int.unsigned ofs2 + sz2 <= Int.unsigned ofs1. + b1 <> b2 \/ Ptrofs.unsigned ofs1 + sz1 <= Ptrofs.unsigned ofs2 \/ Ptrofs.unsigned ofs2 + sz2 <= Ptrofs.unsigned ofs1. Proof. intros. inv H0; inv H1; simpl in H; try discriminate; try (left; congruence). - destruct (peq id id0). subst id0. destruct (orb_true_elim _ _ H); InvBooleans; auto. @@ -1154,6 +1173,28 @@ Proof. intros. unfold binop_int; inv H; auto with va; inv H0; auto with va. Qed. +Definition unop_long (sem: int64 -> int64) (x: aval) := + match x with L n => L (sem n) | _ => ntop1 x end. + +Lemma unop_long_sound: + forall sem v x, + vmatch v x -> + vmatch (match v with Vlong i => Vlong(sem i) | _ => Vundef end) (unop_long sem x). +Proof. + intros. unfold unop_long; inv H; auto with va. +Qed. + +Definition binop_long (sem: int64 -> int64 -> int64) (x y: aval) := + match x, y with L n, L m => L (sem n m) | _, _ => ntop2 x y end. + +Lemma binop_long_sound: + forall sem v x w y, + vmatch v x -> vmatch w y -> + vmatch (match v, w with Vlong i, Vlong j => Vlong(sem i j) | _, _ => Vundef end) (binop_long sem x y). +Proof. + intros. unfold binop_long; inv H; auto with va; inv H0; auto with va. +Qed. + Definition unop_float (sem: float -> float) (x: aval) := match x with F n => F (sem n) | _ => ntop1 x end. @@ -1502,9 +1543,9 @@ Proof (unop_int_sound Int.neg). Definition add (x y: aval) := match x, y with | I i, I j => I (Int.add i j) - | Ptr p, I i | I i, Ptr p => Ptr (padd p i) + | Ptr p, I i | I i, Ptr p => Ptr (if Archi.ptr64 then poffset p else padd p (Ptrofs.of_int i)) | Ptr p, _ | _, Ptr p => Ptr (poffset p) - | Ifptr p, I i | I i, Ifptr p => Ifptr (padd p i) + | Ifptr p, I i | I i, Ifptr p => Ifptr (if Archi.ptr64 then poffset p else padd p (Ptrofs.of_int i)) | Ifptr p, Ifptr q => Ifptr (plub (poffset p) (poffset q)) | Ifptr p, _ | _, Ifptr p => Ifptr (poffset p) | _, _ => ntop2 x y @@ -1513,7 +1554,9 @@ Definition add (x y: aval) := Lemma add_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.add v w) (add x y). Proof. - intros. unfold Val.add, add; inv H; inv H0; constructor; + intros. unfold Val.add, add. destruct Archi.ptr64. +- inv H; inv H0; constructor. +- inv H; inv H0; constructor; ((apply padd_sound; assumption) || (eapply poffset_sound; eassumption) || idtac). apply pmatch_lub_r. eapply poffset_sound; eauto. apply pmatch_lub_l. eapply poffset_sound; eauto. @@ -1522,13 +1565,9 @@ Qed. Definition sub (v w: aval) := match v, w with | I i1, I i2 => I (Int.sub i1 i2) - | Ptr p, I i => Ptr (psub p i) -(* problem with undefs *) -(* - | Ptr p1, Ptr p2 => match psub2 p1 p2 with Some n => I n | _ => itop end -*) + | Ptr p, I i => if Archi.ptr64 then Ifptr (poffset p) else Ptr (psub p (Ptrofs.of_int i)) | Ptr p, _ => Ifptr (poffset p) - | Ifptr p, I i => Ifptr (psub p i) + | Ifptr p, I i => if Archi.ptr64 then Ifptr (plub (poffset p) (provenance w)) else Ifptr (psub p (Ptrofs.of_int i)) | Ifptr p, _ => Ifptr (plub (poffset p) (provenance w)) | _, _ => ntop2 v w end. @@ -1536,9 +1575,9 @@ Definition sub (v w: aval) := Lemma sub_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.sub v w) (sub x y). Proof. - intros. inv H; subst; inv H0; subst; simpl; - try (destruct (eq_block b b0)); - eauto using psub_sound, poffset_sound, pmatch_lub_l with va. + intros. unfold Val.sub, sub. destruct Archi.ptr64. +- inv H; inv H0; eauto with va. +- inv H; inv H0; try (destruct (eq_block b b0)); eauto using psub_sound, poffset_sound, pmatch_lub_l with va. Qed. Definition mul := binop_int Int.mul. @@ -1659,6 +1698,246 @@ Proof. rewrite LTU; auto with va. Qed. +(** 64-bit integer operations *) + +Definition shift_long (sem: int64 -> int -> int64) (v w: aval) := + match w with + | I amount => + if Int.ltu amount Int64.iwordsize' then + match v with + | L i => L (sem i amount) + | _ => ntop1 v + end + else ntop1 v + | _ => ntop1 v + end. + +Lemma shift_long_sound: + forall sem v w x y, + vmatch v x -> vmatch w y -> + vmatch (match v, w with + | Vlong i, Vint j => if Int.ltu j Int64.iwordsize' + then Vlong (sem i j) else Vundef + | _, _ => Vundef end) + (shift_long sem x y). +Proof. + intros. + assert (DEFAULT: + vmatch (match v, w with + | Vlong i, Vint j => if Int.ltu j Int64.iwordsize' + then Vlong (sem i j) else Vundef + | _, _ => Vundef end) + (ntop1 x)). + { destruct v; try constructor; destruct w; try constructor. + destruct (Int.ltu i0 Int64.iwordsize'); constructor. } + unfold shift_long. destruct y; auto. + destruct (Int.ltu n Int64.iwordsize') eqn:LT; auto. + destruct x; auto. + inv H; inv H0. rewrite LT. constructor. +Qed. + +Definition shll := shift_long Int64.shl'. + +Lemma shll_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shll v w) (shll x y). +Proof (shift_long_sound Int64.shl'). + +Definition shrl := shift_long Int64.shr'. + +Lemma shrl_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shrl v w) (shrl x y). +Proof (shift_long_sound Int64.shr'). + +Definition shrlu := shift_long Int64.shru'. + +Lemma shrlu_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shrlu v w) (shrlu x y). +Proof (shift_long_sound Int64.shru'). + +Definition andl := binop_long Int64.and. + +Lemma andl_sound: + forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.andl v w) (andl x y). +Proof (binop_long_sound Int64.and). + +Definition orl := binop_long Int64.or. + +Lemma orl_sound: + forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.orl v w) (orl x y). +Proof (binop_long_sound Int64.or). + +Definition xorl := binop_long Int64.xor. + +Lemma xorl_sound: + forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.xorl v w) (xorl x y). +Proof (binop_long_sound Int64.xor). + +Definition notl := unop_long Int64.not. + +Lemma notl_sound: + forall v x, vmatch v x -> vmatch (Val.notl v) (notl x). +Proof (unop_long_sound Int64.not). + +Definition rotate_long (sem: int64 -> int64 -> int64) (v w: aval) := + match v, w with + | L i, I amount => L (sem i (Int64.repr (Int.unsigned amount))) + | _, _ => ntop1 v + end. + +Lemma rotate_long_sound: + forall sem v w x y, + vmatch v x -> vmatch w y -> + vmatch (match v, w with + | Vlong i, Vint j => Vlong (sem i (Int64.repr (Int.unsigned j))) + | _, _ => Vundef end) + (rotate_long sem x y). +Proof. + intros. + assert (DEFAULT: + vmatch (match v, w with + | Vlong i, Vint j => Vlong (sem i (Int64.repr (Int.unsigned j))) + | _, _ => Vundef end) + (ntop1 x)). + { destruct v; try constructor. destruct w; constructor. } + unfold rotate_long. destruct x; auto. destruct y; auto. inv H; inv H0. constructor. +Qed. + +Definition roll := rotate_long Int64.rol. + +Lemma roll_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.roll v w) (roll x y). +Proof (rotate_long_sound Int64.rol). + +Definition rorl := rotate_long Int64.ror. + +Lemma rorl_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.rorl v w) (rorl x y). +Proof (rotate_long_sound Int64.ror). + +Definition negl := unop_long Int64.neg. + +Lemma negl_sound: + forall v x, vmatch v x -> vmatch (Val.negl v) (negl x). +Proof (unop_long_sound Int64.neg). + +Definition addl (x y: aval) := + match x, y with + | L i, L j => L (Int64.add i j) + | Ptr p, L i | L i, Ptr p => Ptr (if Archi.ptr64 then padd p (Ptrofs.of_int64 i) else poffset p) + | Ptr p, _ | _, Ptr p => Ptr (poffset p) + | Ifptr p, L i | L i, Ifptr p => Ifptr (if Archi.ptr64 then padd p (Ptrofs.of_int64 i) else poffset p) + | Ifptr p, Ifptr q => Ifptr (plub (poffset p) (poffset q)) + | Ifptr p, _ | _, Ifptr p => Ifptr (poffset p) + | _, _ => ntop2 x y + end. + +Lemma addl_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.addl v w) (addl x y). +Proof. + intros. unfold Val.addl, addl. destruct Archi.ptr64. +- inv H; inv H0; constructor; + ((apply padd_sound; assumption) || (eapply poffset_sound; eassumption) || idtac). + apply pmatch_lub_r. eapply poffset_sound; eauto. + apply pmatch_lub_l. eapply poffset_sound; eauto. +- inv H; inv H0; constructor. +Qed. + +Definition subl (v w: aval) := + match v, w with + | L i1, L i2 => L (Int64.sub i1 i2) + | Ptr p, L i => if Archi.ptr64 then Ptr (psub p (Ptrofs.of_int64 i)) else Ifptr (poffset p) + | Ptr p, _ => Ifptr (poffset p) + | Ifptr p, L i => if Archi.ptr64 then Ifptr (psub p (Ptrofs.of_int64 i)) else Ifptr (plub (poffset p) (provenance w)) + | Ifptr p, _ => Ifptr (plub (poffset p) (provenance w)) + | _, _ => ntop2 v w + end. + +Lemma subl_sound: + forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.subl v w) (subl x y). +Proof. + intros. unfold Val.subl, subl. destruct Archi.ptr64. +- inv H; inv H0; try (destruct (eq_block b b0)); eauto using psub_sound, poffset_sound, pmatch_lub_l with va. +- inv H; inv H0; eauto with va. +Qed. + +Definition mull := binop_long Int64.mul. + +Lemma mull_sound: + forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mull v w) (mull x y). +Proof (binop_long_sound Int64.mul). + +Definition divls (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + || Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone + then if va_strict tt then Vbot else ntop + else L (Int64.divs i1 i2) + | _, _ => ntop2 v w + end. + +Lemma divls_sound: + forall v w u x y, vmatch v x -> vmatch w y -> Val.divls v w = Some u -> vmatch u (divls x y). +Proof. + intros. destruct v; destruct w; try discriminate; simpl in H1. + destruct (Int64.eq i0 Int64.zero + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone) eqn:E; inv H1. + inv H; inv H0; auto with va. simpl. rewrite E. constructor. +Qed. + +Definition divlu (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + then if va_strict tt then Vbot else ntop + else L (Int64.divu i1 i2) + | _, _ => ntop2 v w + end. + +Lemma divlu_sound: + forall v w u x y, vmatch v x -> vmatch w y -> Val.divlu v w = Some u -> vmatch u (divlu x y). +Proof. + intros. destruct v; destruct w; try discriminate; simpl in H1. + destruct (Int64.eq i0 Int64.zero) eqn:E; inv H1. + inv H; inv H0; auto with va. simpl. rewrite E. constructor. +Qed. + +Definition modls (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + || Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone + then if va_strict tt then Vbot else ntop + else L (Int64.mods i1 i2) + | _, _ => ntop2 v w + end. + +Lemma modls_sound: + forall v w u x y, vmatch v x -> vmatch w y -> Val.modls v w = Some u -> vmatch u (modls x y). +Proof. + intros. destruct v; destruct w; try discriminate; simpl in H1. + destruct (Int64.eq i0 Int64.zero + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone) eqn:E; inv H1. + inv H; inv H0; auto with va. simpl. rewrite E. constructor. +Qed. + +Definition modlu (v w: aval) := + match w, v with + | L i2, L i1 => + if Int64.eq i2 Int64.zero + then if va_strict tt then Vbot else ntop + else L (Int64.modu i1 i2) + | _, _ => ntop2 v w + end. + +Lemma modlu_sound: + forall v w u x y, vmatch v x -> vmatch w y -> Val.modlu v w = Some u -> vmatch u (modlu x y). +Proof. + intros. destruct v; destruct w; try discriminate; simpl in H1. + destruct (Int64.eq i0 Int64.zero) eqn:E; inv H1. + inv H; inv H0; auto with va. simpl. rewrite E. constructor. +Qed. + (** Floating-point arithmetic operations *) Definition negf := unop_float Float.neg. @@ -1778,6 +2057,30 @@ Proof. apply Z.min_case; auto with va. Qed. +Definition longofint (v: aval) := + match v with + | I i => L (Int64.repr (Int.signed i)) + | _ => ntop1 v + end. + +Lemma longofint_sound: + forall v x, vmatch v x -> vmatch (Val.longofint v) (longofint x). +Proof. + unfold Val.longofint, longofint; intros; inv H; auto with va. +Qed. + +Definition longofintu (v: aval) := + match v with + | I i => L (Int64.repr (Int.unsigned i)) + | _ => ntop1 v + end. + +Lemma longofintu_sound: + forall v x, vmatch v x -> vmatch (Val.longofintu v) (longofintu x). +Proof. + unfold Val.longofintu, longofintu; intros; inv H; auto with va. +Qed. + Definition singleoffloat (v: aval) := match v with | F f => FS (Float.to_single f) @@ -1932,6 +2235,130 @@ Proof. inv H; simpl; auto with va. Qed. +Definition longoffloat (x: aval) := + match x with + | F f => + match Float.to_long f with + | Some i => L i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma longoffloat_sound: + forall v x w, vmatch v x -> Val.longoffloat v = Some w -> vmatch w (longoffloat x). +Proof. + unfold Val.longoffloat; intros. destruct v; try discriminate. + destruct (Float.to_long f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + +Definition longuoffloat (x: aval) := + match x with + | F f => + match Float.to_longu f with + | Some i => L i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma longuoffloat_sound: + forall v x w, vmatch v x -> Val.longuoffloat v = Some w -> vmatch w (longuoffloat x). +Proof. + unfold Val.longuoffloat; intros. destruct v; try discriminate. + destruct (Float.to_longu f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + +Definition floatoflong (x: aval) := + match x with + | L i => F(Float.of_long i) + | _ => ntop1 x + end. + +Lemma floatoflong_sound: + forall v x w, vmatch v x -> Val.floatoflong v = Some w -> vmatch w (floatoflong x). +Proof. + unfold Val.floatoflong; intros. destruct v; inv H0. + inv H; simpl; auto with va. +Qed. + +Definition floatoflongu (x: aval) := + match x with + | L i => F(Float.of_longu i) + | _ => ntop1 x + end. + +Lemma floatoflongu_sound: + forall v x w, vmatch v x -> Val.floatoflongu v = Some w -> vmatch w (floatoflongu x). +Proof. + unfold Val.floatoflongu; intros. destruct v; inv H0. + inv H; simpl; auto with va. +Qed. + +Definition longofsingle (x: aval) := + match x with + | FS f => + match Float32.to_long f with + | Some i => L i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma longofsingle_sound: + forall v x w, vmatch v x -> Val.longofsingle v = Some w -> vmatch w (longofsingle x). +Proof. + unfold Val.longofsingle; intros. destruct v; try discriminate. + destruct (Float32.to_long f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + +Definition longuofsingle (x: aval) := + match x with + | FS f => + match Float32.to_longu f with + | Some i => L i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma longuofsingle_sound: + forall v x w, vmatch v x -> Val.longuofsingle v = Some w -> vmatch w (longuofsingle x). +Proof. + unfold Val.longuofsingle; intros. destruct v; try discriminate. + destruct (Float32.to_longu f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + +Definition singleoflong (x: aval) := + match x with + | L i => FS(Float32.of_long i) + | _ => ntop1 x + end. + +Lemma singleoflong_sound: + forall v x w, vmatch v x -> Val.singleoflong v = Some w -> vmatch w (singleoflong x). +Proof. + unfold Val.singleoflong; intros. destruct v; inv H0. + inv H; simpl; auto with va. +Qed. + +Definition singleoflongu (x: aval) := + match x with + | L i => FS(Float32.of_longu i) + | _ => ntop1 x + end. + +Lemma singleoflongu_sound: + forall v x w, vmatch v x -> Val.singleoflongu v = Some w -> vmatch w (singleoflongu x). +Proof. + unfold Val.singleoflongu; intros. destruct v; inv H0. + inv H; simpl; auto with va. +Qed. + Definition floatofwords (x y: aval) := match x, y with | I i, I j => F(Float.from_words i j) @@ -2166,13 +2593,17 @@ Proof. assert (IP: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vint i) (Vptr b ofs)) (cmp_different_blocks c)). { - intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))). + intros. simpl. destruct Archi.ptr64. + apply cmp_different_blocks_none. + destruct (Int.eq i Int.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } assert (PI: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vptr b ofs) (Vint i)) (cmp_different_blocks c)). { - intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))). + intros. simpl. destruct Archi.ptr64. + apply cmp_different_blocks_none. + destruct (Int.eq i Int.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } unfold cmpu_bool; inversion H; subst; inversion H0; subst; @@ -2199,6 +2630,58 @@ Proof. - constructor. Qed. +Definition cmplu_bool (c: comparison) (v w: aval) : abool := + match v, w with + | L i1, L i2 => Just (Int64.cmpu c i1 i2) + | Ptr _, L _ => cmp_different_blocks c + | L _, Ptr _ => cmp_different_blocks c + | Ptr p1, Ptr p2 => pcmp c p1 p2 + | Ptr p1, Ifptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c) + | Ifptr p1, Ptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c) + | _, _ => Btop + end. + +Lemma cmplu_bool_sound: + forall valid c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmplu_bool valid c v w) (cmplu_bool c x y). +Proof. + intros. + assert (IP: forall i b ofs, + cmatch (Val.cmplu_bool valid c (Vlong i) (Vptr b ofs)) (cmp_different_blocks c)). + { + intros. simpl. destruct Archi.ptr64; simpl. + destruct (Int64.eq i Int64.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))). + apply cmp_different_blocks_sound. apply cmp_different_blocks_none. + apply cmp_different_blocks_none. + } + assert (PI: forall i b ofs, + cmatch (Val.cmplu_bool valid c (Vptr b ofs) (Vlong i)) (cmp_different_blocks c)). + { + intros. simpl. destruct Archi.ptr64; simpl. + destruct (Int64.eq i Int64.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))). + apply cmp_different_blocks_sound. apply cmp_different_blocks_none. + apply cmp_different_blocks_none. + } + unfold cmplu_bool; inversion H; subst; inversion H0; subst; + auto using cmatch_top, cmp_different_blocks_none, pcmp_none, + cmatch_lub_l, cmatch_lub_r, pcmp_sound_64. +- constructor. +Qed. + +Definition cmpl_bool (c: comparison) (v w: aval) : abool := + match v, w with + | L i1, L i2 => Just (Int64.cmp c i1 i2) + | _, _ => Btop + end. + +Lemma cmpl_bool_sound: + forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmpl_bool c v w) (cmpl_bool c x y). +Proof. + intros. + unfold cmpl_bool; inversion H; subst; inversion H0; subst; + auto using cmatch_top. +- constructor. +Qed. + Definition cmpf_bool (c: comparison) (v w: aval) : abool := match v, w with | F f1, F f2 => Just (Float.cmp c f1 f2) @@ -2298,12 +2781,15 @@ Definition vnormalize (chunk: memory_chunk) (v: aval) := | Mint16unsigned, I i => I (Int.zero_ext 16 i) | Mint16unsigned, Uns p n => Uns (provenance v) (Z.min n 16) | Mint16unsigned, _ => Uns (provenance v) 16 - | Mint32, (I _ | Uns _ _ | Sgn _ _ | Ptr _ | Ifptr _) => v - | Mint64, L _ => v - | Mint64, (Ptr p | Ifptr p | Uns p _ | Sgn p _) => Ifptr (if va_strict tt then Pbot else p) + | Mint32, (I _ | Uns _ _ | Sgn _ _ | Ifptr _) => v + | Mint32, Ptr p => if Archi.ptr64 then Ifptr p else v + | Mint64, (L _ | Ifptr _) => v + | Mint64, (Uns p _ | Sgn p _) => Ifptr p + | Mint64, Ptr p => if Archi.ptr64 then v else Ifptr p | Mfloat32, FS f => v | Mfloat64, F f => v - | Many32, (I _ | Uns _ _ | Sgn _ _ | Ptr _ | Ifptr _ | FS _) => v + | Many32, (I _ | Uns _ _ | Sgn _ _ | FS _ | Ifptr _) => v + | Many32, Ptr p => if Archi.ptr64 then Ifptr p else v | Many64, _ => v | _, _ => Ifptr (provenance v) end. @@ -2311,7 +2797,8 @@ Definition vnormalize (chunk: memory_chunk) (v: aval) := Lemma vnormalize_sound: forall chunk v x, vmatch v x -> vmatch (Val.load_result chunk v) (vnormalize chunk x). Proof. - unfold Val.load_result, vnormalize; induction 1; destruct chunk; auto with va. + unfold Val.load_result, vnormalize; generalize Archi.ptr64; intros ptr64; + induction 1; destruct chunk; auto with va. - destruct (zlt n 8); constructor; auto with va. apply is_sign_ext_uns; auto. apply is_sign_ext_sgn; auto with va. @@ -2326,10 +2813,19 @@ Proof. - constructor. omega. apply is_zero_ext_uns; auto with va. - constructor. xomega. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va. - constructor. omega. apply is_zero_ext_uns; auto with va. +- destruct ptr64; auto with va. +- destruct ptr64; auto with va. +- destruct ptr64; auto with va. +- destruct ptr64; auto with va. +- destruct ptr64; auto with va. +- destruct ptr64; auto with va. - constructor. omega. apply is_sign_ext_sgn; auto with va. - constructor. omega. apply is_zero_ext_uns; auto with va. - constructor. omega. apply is_sign_ext_sgn; auto with va. - constructor. omega. apply is_zero_ext_uns; auto with va. +- destruct ptr64; auto with va. +- destruct ptr64; auto with va. +- destruct ptr64; auto with va. Qed. Lemma vnormalize_cast: @@ -2351,13 +2847,13 @@ Proof. - (* int32 *) auto. - (* int64 *) - destruct v; try contradiction; constructor. + auto. - (* float32 *) destruct v; try contradiction; constructor. - (* float64 *) destruct v; try contradiction; constructor. - (* any32 *) - auto. + destruct Archi.ptr64; auto. - (* any64 *) auto. Qed. @@ -2379,7 +2875,7 @@ Lemma vnormalize_monotone: forall chunk x y, vge x y -> vge (vnormalize chunk x) (vnormalize chunk y). Proof with (auto using provenance_monotone with va). - intros chunk x y V; inversion V; subst; destruct chunk; simpl... + intros chunk x y V; unfold vnormalize; generalize Archi.ptr64; intro ptr64; inversion V; subst; destruct chunk eqn:C; simpl... - destruct (zlt n 8); constructor... apply is_sign_ext_uns... apply is_sign_ext_sgn... @@ -2393,19 +2889,19 @@ Proof with (auto using provenance_monotone with va). destruct (zlt n2 8)... - destruct (zlt n1 16). rewrite zlt_true by omega... destruct (zlt n2 16)... -- destruct (va_strict tt)... - constructor... apply is_sign_ext_sgn... apply Z.min_case... - constructor... apply is_zero_ext_uns... - constructor... apply is_sign_ext_sgn... apply Z.min_case... - constructor... apply is_zero_ext_uns... - unfold provenance; destruct (va_strict tt)... -- destruct (va_strict tt)... - destruct (zlt n2 8); constructor... - destruct (zlt n2 16); constructor... -- destruct (va_strict tt)... -- destruct (va_strict tt)... -- destruct (va_strict tt)... -- destruct (va_strict tt)... +- destruct ptr64... +- destruct ptr64... +- destruct ptr64... +- destruct ptr64... +- destruct ptr64... +- destruct ptr64... - constructor... apply is_sign_ext_sgn... - constructor... apply is_zero_ext_uns... - constructor... apply is_sign_ext_sgn... @@ -2420,8 +2916,6 @@ Proof with (auto using provenance_monotone with va). - unfold provenance; destruct (va_strict tt)... - destruct (zlt n 8)... - destruct (zlt n 16)... -- destruct (va_strict tt)... -- destruct (va_strict tt)... Qed. (** Abstracting memory blocks *) @@ -2648,7 +3142,7 @@ Lemma store_provenance: forall chunk m b ofs v m' b' ofs' b'' ofs'' q i, Mem.store chunk m b ofs v = Some m' -> Mem.loadbytes m' b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil) -> - v = Vptr b'' ofs'' /\ (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) + v = Vptr b'' ofs'' /\ (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) \/ Mem.loadbytes m b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil). Proof. intros. exploit storebytes_provenance; eauto. eapply Mem.store_storebytes; eauto. @@ -2704,7 +3198,8 @@ Proof. generalize (decode_val_shape chunk byte1' bytes'). rewrite <- Q. intros DEC; inv DEC; try contradiction. assert (v = Vptr bx ofsx). - { destruct H5 as [E|[E|E]]; rewrite E in H4; destruct v; simpl in H4; congruence. } + { destruct H5 as [E|[E|[E|E]]]; rewrite E in H4; destruct v; simpl in H4; + try congruence; destruct Archi.ptr64; congruence. } exploit In_loadbytes; eauto. eauto with coqlib. intros (ofs' & X & Y). subst v. exploit storebytes_provenance; eauto. intros [Z | Z]. @@ -3177,10 +3672,10 @@ Definition load (chunk: memory_chunk) (rm: romem) (m: amem) (p: aptr) : aval := | Pbot => if va_strict tt then Vbot else Vtop | Gl id ofs => match rm!id with - | Some ab => ablock_load chunk ab (Int.unsigned ofs) + | Some ab => ablock_load chunk ab (Ptrofs.unsigned ofs) | None => match m.(am_glob)!id with - | Some ab => ablock_load chunk ab (Int.unsigned ofs) + | Some ab => ablock_load chunk ab (Ptrofs.unsigned ofs) | None => vnormalize chunk (Ifptr m.(am_nonstack)) end end @@ -3193,7 +3688,7 @@ Definition load (chunk: memory_chunk) (rm: romem) (m: amem) (p: aptr) : aval := | None => vnormalize chunk (Ifptr m.(am_nonstack)) end end - | Stk ofs => ablock_load chunk m.(am_stack) (Int.unsigned ofs) + | Stk ofs => ablock_load chunk m.(am_stack) (Ptrofs.unsigned ofs) | Stack => ablock_load_anywhere chunk m.(am_stack) | Glob | Nonstack => vnormalize chunk (Ifptr m.(am_nonstack)) | Ptop => vnormalize chunk (Ifptr m.(am_top)) @@ -3205,7 +3700,7 @@ Definition loadv (chunk: memory_chunk) (rm: romem) (m: amem) (addr: aval) : aval Definition store (chunk: memory_chunk) (m: amem) (p: aptr) (av: aval) : amem := {| am_stack := match p with - | Stk ofs => ablock_store chunk m.(am_stack) (Int.unsigned ofs) av + | Stk ofs => ablock_store chunk m.(am_stack) (Ptrofs.unsigned ofs) av | Stack | Ptop => ablock_store_anywhere chunk m.(am_stack) av | _ => m.(am_stack) end; @@ -3213,7 +3708,7 @@ Definition store (chunk: memory_chunk) (m: amem) (p: aptr) (av: aval) : amem := match p with | Gl id ofs => let ab := match m.(am_glob)!id with Some ab => ab | None => ablock_init m.(am_nonstack) end in - PTree.set id (ablock_store chunk ab (Int.unsigned ofs) av) m.(am_glob) + PTree.set id (ablock_store chunk ab (Ptrofs.unsigned ofs) av) m.(am_glob) | Glo id => let ab := match m.(am_glob)!id with Some ab => ab | None => ablock_init m.(am_nonstack) end in PTree.set id (ablock_store_anywhere chunk ab av) m.(am_glob) @@ -3251,7 +3746,7 @@ Definition loadbytes (m: amem) (rm: romem) (p: aptr) : aptr := Definition storebytes (m: amem) (dst: aptr) (sz: Z) (p: aptr) : amem := {| am_stack := match dst with - | Stk ofs => ablock_storebytes m.(am_stack) p (Int.unsigned ofs) sz + | Stk ofs => ablock_storebytes m.(am_stack) p (Ptrofs.unsigned ofs) sz | Stack | Ptop => ablock_storebytes_anywhere m.(am_stack) p | _ => m.(am_stack) end; @@ -3259,7 +3754,7 @@ Definition storebytes (m: amem) (dst: aptr) (sz: Z) (p: aptr) : amem := match dst with | Gl id ofs => let ab := match m.(am_glob)!id with Some ab => ab | None => ablock_init m.(am_nonstack) end in - PTree.set id (ablock_storebytes ab p (Int.unsigned ofs) sz) m.(am_glob) + PTree.set id (ablock_storebytes ab p (Ptrofs.unsigned ofs) sz) m.(am_glob) | Glo id => let ab := match m.(am_glob)!id with Some ab => ab | None => ablock_init m.(am_nonstack) end in PTree.set id (ablock_storebytes_anywhere ab p) m.(am_glob) @@ -3276,7 +3771,7 @@ Definition storebytes (m: amem) (dst: aptr) (sz: Z) (p: aptr) : amem := Theorem load_sound: forall chunk m b ofs v rm am p, - Mem.load chunk m b (Int.unsigned ofs) = Some v -> + Mem.load chunk m b (Ptrofs.unsigned ofs) = Some v -> romatch m rm -> mmatch m am -> pmatch b ofs p -> @@ -3321,7 +3816,7 @@ Qed. Theorem store_sound: forall chunk m b ofs v m' am p av, - Mem.store chunk m b (Int.unsigned ofs) v = Some m' -> + Mem.store chunk m b (Ptrofs.unsigned ofs) v = Some m' -> mmatch m am -> pmatch b ofs p -> vmatch v av -> @@ -3399,7 +3894,7 @@ Qed. Theorem loadbytes_sound: forall m b ofs sz bytes am rm p, - Mem.loadbytes m b (Int.unsigned ofs) sz = Some bytes -> + Mem.loadbytes m b (Ptrofs.unsigned ofs) sz = Some bytes -> romatch m rm -> mmatch m am -> pmatch b ofs p -> @@ -3432,7 +3927,7 @@ Qed. Theorem storebytes_sound: forall m b ofs bytes m' am p sz q, - Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' -> + Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' -> mmatch m am -> pmatch b ofs p -> length bytes = nat_of_Z sz -> @@ -3716,8 +4211,8 @@ Lemma vmatch_inj: forall bc v x, vmatch bc v x -> Val.inject (inj_of_bc bc) v v. Proof. induction 1; econstructor. - eapply pmatch_inj; eauto. rewrite Int.add_zero; auto. - eapply pmatch_inj; eauto. rewrite Int.add_zero; auto. + eapply pmatch_inj; eauto. rewrite Ptrofs.add_zero; auto. + eapply pmatch_inj; eauto. rewrite Ptrofs.add_zero; auto. Qed. Lemma vmatch_list_inj: @@ -3752,7 +4247,7 @@ Proof. { exploit mmatch_top; eauto. intros [P Q]. eapply pmatch_top'. eapply Q; eauto. } inv PM; auto. - rewrite Int.add_zero; auto. + rewrite Ptrofs.add_zero; auto. - (* free blocks *) intros. unfold inj_of_bc. erewrite bc_below_invalid; eauto. - (* mapped blocks *) @@ -3765,7 +4260,7 @@ Proof. auto. - (* overflow *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r. split. omega. apply Int.unsigned_range_2. + rewrite Zplus_0_r. split. omega. apply Ptrofs.unsigned_range_2. - (* perm inv *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Zplus_0_r in H2. auto. @@ -4046,13 +4541,21 @@ Hint Resolve cnot_sound symbol_address_sound neg_sound add_sound sub_sound mul_sound mulhs_sound mulhu_sound divs_sound divu_sound mods_sound modu_sound shrx_sound + shll_sound shrl_sound shrlu_sound + andl_sound orl_sound xorl_sound notl_sound roll_sound rorl_sound + negl_sound addl_sound subl_sound mull_sound + divls_sound divlu_sound modls_sound modlu_sound negf_sound absf_sound addf_sound subf_sound mulf_sound divf_sound negfs_sound absfs_sound addfs_sound subfs_sound mulfs_sound divfs_sound - zero_ext_sound sign_ext_sound singleoffloat_sound floatofsingle_sound + zero_ext_sound sign_ext_sound longofint_sound longofintu_sound + singleoffloat_sound floatofsingle_sound intoffloat_sound intuoffloat_sound floatofint_sound floatofintu_sound intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound + longoffloat_sound longuoffloat_sound floatoflong_sound floatoflongu_sound + longofsingle_sound longuofsingle_sound singleoflong_sound singleoflongu_sound longofwords_sound loword_sound hiword_sound - cmpu_bool_sound cmp_bool_sound cmpf_bool_sound cmpfs_bool_sound + cmpu_bool_sound cmp_bool_sound cmplu_bool_sound cmpl_bool_sound + cmpf_bool_sound cmpfs_bool_sound maskzero_sound : va. -- cgit