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. --- cfrontend/C2C.ml | 62 +++-- cfrontend/Cexec.v | 237 +++++++++-------- cfrontend/Clight.v | 32 +-- cfrontend/Cminorgen.v | 6 +- cfrontend/Cminorgenproof.v | 174 ++++++------ cfrontend/Cop.v | 605 +++++++++++++++++++++++------------------- cfrontend/Csem.v | 30 +-- cfrontend/Csharpminor.v | 2 +- cfrontend/Cshmgen.v | 108 +++++--- cfrontend/Cshmgenproof.v | 465 ++++++++++++++++++++++---------- cfrontend/Cstrategy.v | 16 +- cfrontend/Csyntax.v | 2 +- cfrontend/Ctypes.v | 50 ++-- cfrontend/Ctyping.v | 177 +++++++----- cfrontend/Initializers.v | 31 +-- cfrontend/Initializersproof.v | 84 +++--- cfrontend/SimplExprproof.v | 22 +- cfrontend/SimplLocals.v | 2 +- cfrontend/SimplLocalsproof.v | 72 ++--- 19 files changed, 1251 insertions(+), 926 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 14976d01..b68887c5 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -197,7 +197,7 @@ let builtins_generic = { false); "__compcert_va_composite", (TPtr(TVoid [], []), - [TPtr(TVoid [], []); TInt(IUInt, [])], + [TPtr(TVoid [], []); TInt(IULong, [])], false); (* Helper functions for int64 arithmetic *) "__i64_dtos", @@ -390,14 +390,13 @@ let make_builtin_va_arg_by_val helper ty ty_ret arg = let make_builtin_va_arg_by_ref helper ty arg = let ty_fun = - Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), + Tfunction(Tcons(Tpointer(Tvoid, noattr), Tcons(Ctyping.size_t, Tnil)), Tpointer(Tvoid, noattr), cc_default) in let ty_ptr = Tpointer(ty, noattr) in let call = Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), - Econs(va_list_ptr arg, - Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)), + Econs(va_list_ptr arg, Econs(Esizeof(ty, Ctyping.size_t), Enil)), Tpointer(Tvoid, noattr)) in Evalof(Ederef(Ecast(call, ty_ptr), ty), ty) @@ -442,27 +441,31 @@ let convertCallconv va unproto attr = (** Types *) -let convertIkind = function - | C.IBool -> (Unsigned, Ctypes.IBool) - | C.IChar -> ((if (!Machine.config).Machine.char_signed - then Signed else Unsigned), I8) - | C.ISChar -> (Signed, I8) - | C.IUChar -> (Unsigned, I8) - | C.IInt -> (Signed, I32) - | C.IUInt -> (Unsigned, I32) - | C.IShort -> (Signed, I16) - | C.IUShort -> (Unsigned, I16) - | C.ILong -> (Signed, I32) - | C.IULong -> (Unsigned, I32) - (* Special-cased in convertTyp below *) - | C.ILongLong | C.IULongLong -> assert false - -let convertFkind = function - | C.FFloat -> F32 - | C.FDouble -> F64 +let convertIkind k a : coq_type = + match k with + | C.IBool -> Tint (IBool, Unsigned, a) + | C.IChar -> Tint (I8, (if Machine.((!config).char_signed) + then Signed else Unsigned), a) + | C.ISChar -> Tint (I8, Signed, a) + | C.IUChar -> Tint (I8, Unsigned, a) + | C.IInt -> Tint (I32, Signed, a) + | C.IUInt -> Tint (I32, Unsigned, a) + | C.IShort -> Tint (I16, Signed, a) + | C.IUShort -> Tint (I16, Unsigned, a) + | C.ILong -> if Machine.((!config).sizeof_long) = 8 + then Tlong (Signed, a) else Tint (I32, Signed, a) + | C.IULong -> if Machine.((!config).sizeof_long) = 8 + then Tlong (Unsigned, a) else Tint (I32, Unsigned, a) + | C.ILongLong -> Tlong (Signed, a) + | C.IULongLong -> Tlong (Unsigned, a) + +let convertFkind k a : coq_type = + match k with + | C.FFloat -> Tfloat (F32, a) + | C.FDouble -> Tfloat (F64, a) | C.FLongDouble -> if not !Clflags.option_flongdouble then unsupported "'long double' type"; - F64 + Tfloat (F64, a) let checkFunctionType env tres targs = if not !Clflags.option_fstruct_passing then begin @@ -482,14 +485,10 @@ let checkFunctionType env tres targs = let rec convertTyp env t = match t with | C.TVoid a -> Tvoid - | C.TInt(C.ILongLong, a) -> - Tlong(Signed, convertAttr a) - | C.TInt(C.IULongLong, a) -> - Tlong(Unsigned, convertAttr a) | C.TInt(ik, a) -> - let (sg, sz) = convertIkind ik in Tint(sz, sg, convertAttr a) + convertIkind ik (convertAttr a) | C.TFloat(fk, a) -> - Tfloat(convertFkind fk, convertAttr a) + convertFkind fk (convertAttr a) | C.TPtr(ty, a) -> Tpointer(convertTyp env ty, convertAttr a) | C.TArray(ty, None, a) -> @@ -514,8 +513,7 @@ let rec convertTyp env t = | C.TUnion(id, a) -> Tunion(intern_string id.name, convertAttr a) | C.TEnum(id, a) -> - let (sg, sz) = convertIkind Cutil.enum_ikind in - Tint(sz, sg, convertAttr a) + convertIkind Cutil.enum_ikind (convertAttr a) and convertParams env = function | [] -> Tnil @@ -650,7 +648,7 @@ let rec convertExpr env e = | C.EConst(C.CInt(i, k, _)) -> let sg = if Cutil.is_signed_ikind k then Signed else Unsigned in - if k = ILongLong || k = IULongLong + if Cutil.sizeof_ikind k = 8 then Ctyping.econst_long (coqint_of_camlint64 i) sg else Ctyping.econst_int (convertInt i) sg | C.EConst(C.CFloat(f, k)) -> diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index a2bfa6e1..4dcf2a47 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -12,25 +12,11 @@ (** Animating the CompCert C semantics *) -Require Import String. -Require Import Axioms. -Require Import Classical. -Require Import Decidableplus. -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import AST. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Determinism. -Require Import Ctypes. -Require Import Cop. -Require Import Csyntax. -Require Import Csem. +Require Import Axioms Classical. +Require Import String Coqlib Decidableplus. +Require Import Errors Maps Integers Floats. +Require Import AST Values Memory Events Globalenvs Determinism. +Require Import Ctypes Cop Csyntax Csem. Require Cstrategy. Local Open Scope string_scope. @@ -74,7 +60,7 @@ Proof. intros until ty. destruct a; simpl; congruence. Qed. -Definition is_loc (a: expr) : option (block * int * type) := +Definition is_loc (a: expr) : option (block * ptrofs * type) := match a with | Eloc b ofs ty => Some(b, ofs, ty) | _ => None @@ -106,16 +92,17 @@ Section EXEC. Variable ge: genv. Definition eventval_of_val (v: val) (t: typ) : option eventval := - match v, t with - | Vint i, AST.Tint => Some (EVint i) - | Vfloat f, AST.Tfloat => Some (EVfloat f) - | Vsingle f, AST.Tsingle => Some (EVsingle f) - | Vlong n, AST.Tlong => Some (EVlong n) - | Vptr b ofs, AST.Tint => + match v with + | Vint i => check (typ_eq t AST.Tint); Some (EVint i) + | Vfloat f => check (typ_eq t AST.Tfloat); Some (EVfloat f) + | Vsingle f => check (typ_eq t AST.Tsingle); Some (EVsingle f) + | Vlong n => check (typ_eq t AST.Tlong); Some (EVlong n) + | Vptr b ofs => do id <- Genv.invert_symbol ge b; check (Genv.public_symbol ge id); + check (typ_eq t AST.Tptr); Some (EVptr_global id ofs) - | _, _ => None + | _ => None end. Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list eventval) := @@ -129,32 +116,45 @@ Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list event end. Definition val_of_eventval (ev: eventval) (t: typ) : option val := - match ev, t with - | EVint i, AST.Tint => Some (Vint i) - | EVfloat f, AST.Tfloat => Some (Vfloat f) - | EVsingle f, AST.Tsingle => Some (Vsingle f) - | EVlong n, AST.Tlong => Some (Vlong n) - | EVptr_global id ofs, AST.Tint => + match ev with + | EVint i => check (typ_eq t AST.Tint); Some (Vint i) + | EVfloat f => check (typ_eq t AST.Tfloat); Some (Vfloat f) + | EVsingle f => check (typ_eq t AST.Tsingle); Some (Vsingle f) + | EVlong n => check (typ_eq t AST.Tlong); Some (Vlong n) + | EVptr_global id ofs => check (Genv.public_symbol ge id); + check (typ_eq t AST.Tptr); do b <- Genv.find_symbol ge id; Some (Vptr b ofs) - | _, _ => None + end. + +Ltac mydestr := + match goal with + | [ |- None = Some _ -> _ ] => intro X; discriminate + | [ |- Some _ = Some _ -> _ ] => intro X; inv X + | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr + | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr + | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr + | _ => idtac end. Lemma eventval_of_val_sound: forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v. Proof. - intros. destruct v; destruct t; simpl in H; inv H; try constructor. - destruct (Genv.invert_symbol ge b) as [id|] eqn:?; try discriminate. - destruct (Genv.public_symbol ge id) eqn:?; inv H1. - constructor. auto. apply Genv.invert_find_symbol; auto. + intros until ev. destruct v; simpl; mydestr; constructor. + auto. apply Genv.invert_find_symbol; auto. Qed. Lemma eventval_of_val_complete: forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev. Proof. - induction 1; simpl; auto. - rewrite (Genv.find_invert_symbol _ _ H0). simpl in H; rewrite H. auto. + induction 1; simpl. +- auto. +- auto. +- auto. +- auto. +- rewrite (Genv.find_invert_symbol _ _ H0). simpl in H; rewrite H. + rewrite dec_eq_true. auto. Qed. Lemma list_eventval_of_val_sound: @@ -177,21 +177,23 @@ Qed. Lemma val_of_eventval_sound: forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v. Proof. - intros. destruct ev; destruct t; simpl in H; inv H; try constructor. - destruct (Genv.public_symbol ge i) eqn:?; try discriminate. - destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1. - constructor; auto. + intros until v. destruct ev; simpl; mydestr; constructor; auto. Qed. Lemma val_of_eventval_complete: forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v. Proof. - induction 1; simpl; auto. simpl in *. rewrite H, H0; auto. + induction 1; simpl. +- auto. +- auto. +- auto. +- auto. +- simpl in *. rewrite H, H0. rewrite dec_eq_true. auto. Qed. (** Volatile memory accesses. *) -Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) +Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: ptrofs) : option (world * trace * val) := if Genv.block_is_volatile ge b then do id <- Genv.invert_symbol ge b; @@ -202,10 +204,10 @@ Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) Some(w', Event_vload chunk id ofs res :: nil, Val.load_result chunk vres) end else - do v <- Mem.load chunk m b (Int.unsigned ofs); + do v <- Mem.load chunk m b (Ptrofs.unsigned ofs); Some(w, E0, v). -Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) (v: val) +Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: ptrofs) (v: val) : option (world * trace * mem) := if Genv.block_is_volatile ge b then do id <- Genv.invert_symbol ge b; @@ -213,19 +215,9 @@ Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block do w' <- nextworld_vstore w chunk id ofs ev; Some(w', Event_vstore chunk id ofs ev :: nil, m) else - do m' <- Mem.store chunk m b (Int.unsigned ofs) v; + do m' <- Mem.store chunk m b (Ptrofs.unsigned ofs) v; Some(w, E0, m'). -Ltac mydestr := - match goal with - | [ |- None = Some _ -> _ ] => let X := fresh "X" in intro X; discriminate - | [ |- Some _ = Some _ -> _ ] => let X := fresh "X" in intro X; inv X - | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr - | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr - | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr - | _ => idtac - end. - Lemma do_volatile_load_sound: forall w chunk m b ofs w' t v, do_volatile_load w chunk m b ofs = Some(w', t, v) -> @@ -276,7 +268,7 @@ Qed. (** Accessing locations *) -Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : option (world * trace * val) := +Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: ptrofs) : option (world * trace * val) := match access_mode ty with | By_value chunk => match type_is_volatile ty with @@ -288,37 +280,37 @@ Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : o | _ => None end. -Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop := - (alignof_blockcopy ge ty | Int.unsigned ofs') /\ (alignof_blockcopy ge ty | Int.unsigned ofs) /\ - (b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs - \/ Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs - \/ Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs'). +Definition assign_copy_ok (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': ptrofs) : Prop := + (alignof_blockcopy ge ty | Ptrofs.unsigned ofs') /\ (alignof_blockcopy ge ty | Ptrofs.unsigned ofs) /\ + (b' <> b \/ Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs + \/ Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs + \/ Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs'). Remark check_assign_copy: - forall (ty: type) (b: block) (ofs: int) (b': block) (ofs': int), + forall (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': ptrofs), { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }. Proof with try (right; intuition omega). intros. unfold assign_copy_ok. assert (alignof_blockcopy ge ty > 0) by apply alignof_blockcopy_pos. - destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs')); auto... - destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs)); auto... + destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs')); auto... + destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs)); auto... assert (Y: {b' <> b \/ - Int.unsigned ofs' = Int.unsigned ofs \/ - Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs \/ - Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs'} + + Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs \/ + Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs \/ + Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs'} + {~(b' <> b \/ - Int.unsigned ofs' = Int.unsigned ofs \/ - Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs \/ - Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs')}). + Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs \/ + Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs \/ + Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs')}). destruct (eq_block b' b); auto. - destruct (zeq (Int.unsigned ofs') (Int.unsigned ofs)); auto. - destruct (zle (Int.unsigned ofs' + sizeof ge ty) (Int.unsigned ofs)); auto. - destruct (zle (Int.unsigned ofs + sizeof ge ty) (Int.unsigned ofs')); auto. + destruct (zeq (Ptrofs.unsigned ofs') (Ptrofs.unsigned ofs)); auto. + destruct (zle (Ptrofs.unsigned ofs' + sizeof ge ty) (Ptrofs.unsigned ofs)); auto. + destruct (zle (Ptrofs.unsigned ofs + sizeof ge ty) (Ptrofs.unsigned ofs')); auto. right; intuition omega. destruct Y... left; intuition omega. Defined. -Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v: val): option (world * trace * mem) := +Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: ptrofs) (v: val): option (world * trace * mem) := match access_mode ty with | By_value chunk => match type_is_volatile ty with @@ -329,8 +321,8 @@ Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v match v with | Vptr b' ofs' => if check_assign_copy ty b ofs b' ofs' then - do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ge ty); - do m' <- Mem.storebytes m b (Int.unsigned ofs) bytes; + do bytes <- Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ge ty); + do m' <- Mem.storebytes m b (Ptrofs.unsigned ofs) bytes; Some(w, E0, m') else None | _ => None @@ -433,21 +425,29 @@ Definition do_ef_volatile_store (chunk: memory_chunk) | _ => None end. -Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: int) +Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: ptrofs) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := do b <- Genv.find_symbol ge id; do_ef_volatile_load chunk w (Vptr b ofs :: vargs) m. -Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: int) +Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: ptrofs) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := do b <- Genv.find_symbol ge id; do_ef_volatile_store chunk w (Vptr b ofs :: vargs) m. +Definition do_alloc_size (v: val) : option ptrofs := + match v with + | Vint n => if Archi.ptr64 then None else Some (Ptrofs.of_int n) + | Vlong n => if Archi.ptr64 then Some (Ptrofs.of_int64 n) else None + | _ => None + end. + Definition do_ef_malloc (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match vargs with - | Vint n :: nil => - let (m', b) := Mem.alloc m (-4) (Int.unsigned n) in - do m'' <- Mem.store Mint32 m' b (-4) (Vint n); - Some(w, E0, Vptr b Int.zero, m'') + | v :: nil => + do sz <- do_alloc_size v; + let (m', b) := Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned sz) in + do m'' <- Mem.store Mptr m' b (- size_chunk Mptr) v; + Some(w, E0, Vptr b Ptrofs.zero, m'') | _ => None end. @@ -455,14 +455,11 @@ Definition do_ef_free (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match vargs with | Vptr b lo :: nil => - do vsz <- Mem.load Mint32 m b (Int.unsigned lo - 4); - match vsz with - | Vint sz => - check (zlt 0 (Int.unsigned sz)); - do m' <- Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz); - Some(w, E0, Vundef, m') - | _ => None - end + do vsz <- Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr); + do sz <- do_alloc_size vsz; + check (zlt 0 (Ptrofs.unsigned sz)); + do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz); + Some(w, E0, Vundef, m') | _ => None end. @@ -478,9 +475,9 @@ Definition do_ef_memcpy (sz al: Z) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match vargs with | Vptr bdst odst :: Vptr bsrc osrc :: nil => - if decide (memcpy_args_ok sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc)) then - do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz; - do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes; + if decide (memcpy_args_ok sz al bdst (Ptrofs.unsigned odst) bsrc (Ptrofs.unsigned osrc)) then + do bytes <- Mem.loadbytes m bsrc (Ptrofs.unsigned osrc) sz; + do m' <- Mem.storebytes m bdst (Ptrofs.unsigned odst) bytes; Some(w, E0, Vundef, m') else None | _ => None @@ -526,6 +523,9 @@ Lemma do_ef_external_sound: do_external ef w vargs m = Some(w', t, vres, m') -> external_call ef ge vargs m t vres m' /\ possible_trace w t w'. Proof with try congruence. + assert (SIZE: forall v sz, do_alloc_size v = Some sz -> v = Vptrofs sz). + { intros until sz; unfold Vptrofs; destruct v; simpl; destruct Archi.ptr64 eqn:SF; + intros EQ; inv EQ; f_equal; symmetry; eauto with ptrofs. } intros until m'. destruct ef; simpl. (* EF_external *) @@ -545,16 +545,16 @@ Proof with try congruence. exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto. auto. (* EF_malloc *) - unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs... - destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b] eqn:?. mydestr. - split. econstructor; eauto. constructor. + unfold do_ef_malloc. destruct vargs... destruct vargs... mydestr. + destruct (Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned i)) as [m1 b] eqn:?. mydestr. + split. apply SIZE in Heqo. subst v. econstructor; eauto. constructor. (* EF_free *) unfold do_ef_free. destruct vargs... destruct v... destruct vargs... - mydestr. destruct v... mydestr. - split. econstructor; eauto. omega. constructor. + mydestr. split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. constructor. (* EF_memcpy *) unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... - destruct v... destruct vargs... mydestr. apply Decidable_sound in Heqb1. red in Heqb1. + destruct v... destruct vargs... mydestr. + apply Decidable_sound in Heqb1. red in Heqb1. split. econstructor; eauto; tauto. constructor. (* EF_annot *) unfold do_ef_annot. mydestr. @@ -575,6 +575,10 @@ Lemma do_ef_external_complete: external_call ef ge vargs m t vres m' -> possible_trace w t w' -> do_external ef w vargs m = Some(w', t, vres, m'). Proof. + assert (SIZE: forall n, do_alloc_size (Vptrofs n) = Some n). + { unfold Vptrofs, do_alloc_size; intros; destruct Archi.ptr64 eqn:SF. + rewrite Ptrofs.of_int64_to_int64; auto. + rewrite Ptrofs.of_int_to_int; auto. } intros. destruct ef; simpl in *. (* EF_external *) eapply do_external_function_complete; eauto. @@ -590,13 +594,13 @@ Proof. exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto. (* EF_malloc *) inv H; unfold do_ef_malloc. - inv H0. rewrite H1. rewrite H2. auto. + inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto. (* EF_free *) inv H; unfold do_ef_free. - inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega. + inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega. (* EF_memcpy *) inv H; unfold do_ef_memcpy. - inv H0. rewrite Decidable_complete, H7, H8. auto. + inv H0. rewrite Decidable_complete. rewrite H7; rewrite H8; auto. red. tauto. (* EF_annot *) inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. @@ -680,10 +684,10 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match e!x with | Some(b, ty') => check type_eq ty ty'; - topred (Lred "red_var_local" (Eloc b Int.zero ty) m) + topred (Lred "red_var_local" (Eloc b Ptrofs.zero ty) m) | None => do b <- Genv.find_symbol ge x; - topred (Lred "red_var_global" (Eloc b Int.zero ty) m) + topred (Lred "red_var_global" (Eloc b Ptrofs.zero ty) m) end | LV, Ederef r ty => match is_val r with @@ -702,7 +706,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := do co <- ge.(genv_cenv)!id; match field_offset ge f (co_members co) with | Error _ => stuck - | OK delta => topred (Lred "red_field_struct" (Eloc b (Int.add ofs (Int.repr delta)) ty) m) + | OK delta => topred (Lred "red_field_struct" (Eloc b (Ptrofs.add ofs (Ptrofs.repr delta)) ty) m) end | Tunion id _ => do co <- ge.(genv_cenv)!id; @@ -782,9 +786,9 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) end | RV, Esizeof ty' ty => - topred (Rred "red_sizeof" (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0) + topred (Rred "red_sizeof" (Eval (Vptrofs (Ptrofs.repr (sizeof ge ty'))) ty) m E0) | RV, Ealignof ty' ty => - topred (Rred "red_alignof" (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0) + topred (Rred "red_alignof" (Eval (Vptrofs (Ptrofs.repr (alignof ge ty'))) ty) m E0) | RV, Eassign l1 r2 ty => match is_loc l1, is_val r2 with | Some(b, ofs, ty1), Some(v2, ty2) => @@ -1870,7 +1874,7 @@ Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type match PTree.get id e with | Some (b, ty') => check (type_eq ty ty'); - do w', t, m1 <- do_assign_loc w ty m b Int.zero v1; + do w', t, m1 <- do_assign_loc w ty m b Ptrofs.zero v1; match t with nil => sem_bind_parameters w e m1 params lv | _ => None end | None => None end @@ -2034,15 +2038,12 @@ Definition do_step (w: world) (s: state) : list transition := Ltac myinv := match goal with - | [ |- In _ nil -> _ ] => let X := fresh "X" in intro X; elim X + | [ |- In _ nil -> _ ] => intro X; elim X | [ |- In _ (ret _ _) -> _ ] => - let X := fresh "X" in intro X; elim X; clear X; - [let EQ := fresh "EQ" in intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] + [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] | [ |- In _ (_ :: nil) -> _ ] => - let X := fresh "X" in - intro X; elim X; clear X; - [let EQ := fresh "EQ" in intro EQ; inv EQ; myinv | myinv] + intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv] | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index e6426fb8..7a4c49a2 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -202,7 +202,7 @@ Definition temp_env := PTree.t val. memory load is performed. If the type [ty] indicates an access by reference or by copy, the pointer [Vptr b ofs] is returned. *) -Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : val -> Prop := +Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs) : val -> Prop := | deref_loc_value: forall chunk v, access_mode ty = By_value chunk -> Mem.loadv chunk m (Vptr b ofs) = Some v -> @@ -220,7 +220,7 @@ Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : val -> Prop := This is allowed only if [ty] indicates an access by value or by copy. [m'] is the updated memory state. *) -Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: int): +Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: ptrofs): val -> mem -> Prop := | assign_loc_value: forall v chunk m', access_mode ty = By_value chunk -> @@ -228,13 +228,13 @@ Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: in assign_loc ce ty m b ofs v m' | assign_loc_copy: forall b' ofs' bytes m', access_mode ty = By_copy -> - (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Int.unsigned ofs')) -> - (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Int.unsigned ofs)) -> - b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs - \/ Int.unsigned ofs' + sizeof ce ty <= Int.unsigned ofs - \/ Int.unsigned ofs + sizeof ce ty <= Int.unsigned ofs' -> - Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ce ty) = Some bytes -> - Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' -> + (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Ptrofs.unsigned ofs')) -> + (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Ptrofs.unsigned ofs)) -> + b' <> b \/ Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs + \/ Ptrofs.unsigned ofs' + sizeof ce ty <= Ptrofs.unsigned ofs + \/ Ptrofs.unsigned ofs + sizeof ce ty <= Ptrofs.unsigned ofs' -> + Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ce ty) = Some bytes -> + Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' -> assign_loc ce ty m b ofs (Vptr b' ofs') m'. Section SEMANTICS. @@ -274,7 +274,7 @@ Inductive bind_parameters (e: env): | bind_parameters_cons: forall m id ty params v1 vl b m1 m2, PTree.get id e = Some(b, ty) -> - assign_loc ge ty m b Int.zero v1 m1 -> + assign_loc ge ty m b Ptrofs.zero v1 m1 -> bind_parameters e m1 params vl m2 -> bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. @@ -384,9 +384,9 @@ Inductive eval_expr: expr -> val -> Prop := sem_cast v1 (typeof a) ty m = Some v -> eval_expr (Ecast a ty) v | eval_Esizeof: forall ty1 ty, - eval_expr (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) + eval_expr (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1))) | eval_Ealignof: forall ty1 ty, - eval_expr (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))) + eval_expr (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1))) | eval_Elvalue: forall a loc ofs v, eval_lvalue a loc ofs -> deref_loc (typeof a) m loc ofs v -> @@ -396,14 +396,14 @@ Inductive eval_expr: expr -> val -> Prop := in l-value position. The result is the memory location [b, ofs] that contains the value of the expression [a]. *) -with eval_lvalue: expr -> block -> int -> Prop := +with eval_lvalue: expr -> block -> ptrofs -> Prop := | eval_Evar_local: forall id l ty, e!id = Some(l, ty) -> - eval_lvalue (Evar id ty) l Int.zero + eval_lvalue (Evar id ty) l Ptrofs.zero | eval_Evar_global: forall id l ty, e!id = None -> Genv.find_symbol ge id = Some l -> - eval_lvalue (Evar id ty) l Int.zero + eval_lvalue (Evar id ty) l Ptrofs.zero | eval_Ederef: forall a ty l ofs, eval_expr a (Vptr l ofs) -> eval_lvalue (Ederef a ty) l ofs @@ -412,7 +412,7 @@ with eval_lvalue: expr -> block -> int -> Prop := typeof a = Tstruct id att -> ge.(genv_cenv)!id = Some co -> field_offset ge i (co_members co) = OK delta -> - eval_lvalue (Efield a i ty) l (Int.add ofs (Int.repr delta)) + eval_lvalue (Efield a i ty) l (Ptrofs.add ofs (Ptrofs.repr delta)) | eval_Efield_union: forall a i ty l ofs id co att, eval_expr a (Vptr l ofs) -> typeof a = Tunion id att -> diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index b9a28ee1..5017fc8e 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -47,8 +47,8 @@ Definition compilenv := PTree.t Z. Definition var_addr (cenv: compilenv) (id: ident): expr := match PTree.get id cenv with - | Some ofs => Econst (Oaddrstack (Int.repr ofs)) - | None => Econst (Oaddrsymbol id Int.zero) + | Some ofs => Econst (Oaddrstack (Ptrofs.repr ofs)) + | None => Econst (Oaddrsymbol id Ptrofs.zero) end. (** * Translation of expressions and statements. *) @@ -269,7 +269,7 @@ Definition transl_funbody Definition transl_function (f: Csharpminor.function): res function := let (cenv, stacksize) := build_compilenv f in - if zle stacksize Int.max_unsigned + if zle stacksize Ptrofs.max_unsigned then transl_funbody cenv stacksize f else Error(msg "Cminorgen: too many local variables, stack size exceeded"). diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 2f551d68..ea1bc89c 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -76,7 +76,7 @@ Lemma sig_preserved: Proof. intros until tf; destruct f; simpl. unfold transl_function. destruct (build_compilenv f). - case (zle z Int.max_unsigned); simpl bind; try congruence. + case (zle z Ptrofs.max_unsigned); simpl bind; try congruence. intros. monadInv H. simpl. eapply sig_preserved_body; eauto. intro. inv H. reflexivity. Qed. @@ -190,7 +190,7 @@ Qed. Inductive match_var (f: meminj) (sp: block): option (block * Z) -> option Z -> Prop := | match_var_local: forall b sz ofs, - Val.inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> + Val.inject f (Vptr b Ptrofs.zero) (Vptr sp (Ptrofs.repr ofs)) -> match_var f sp (Some(b, sz)) (Some ofs) | match_var_global: match_var f sp None None. @@ -311,7 +311,7 @@ Proof. intros. rewrite PTree.gsspec. destruct (peq id0 id). (* the new var *) subst id0. rewrite CENV. constructor. econstructor. eauto. - rewrite Int.add_commut; rewrite Int.add_zero; auto. + rewrite Ptrofs.add_commut; rewrite Ptrofs.add_zero; auto. (* old vars *) generalize (me_vars0 id0). rewrite PTree.gro; auto. intros M; inv M. constructor; eauto. @@ -794,7 +794,7 @@ Definition cenv_mem_separated (cenv: compilenv) (vars: list (ident * Z)) (f: mem Lemma match_callstack_alloc_variables_rec: forall tm sp tf cenv le te lo cs, Mem.valid_block tm sp -> - fn_stackspace tf <= Int.max_unsigned -> + fn_stackspace tf <= Ptrofs.max_unsigned -> (forall ofs k p, Mem.perm tm sp ofs k p -> 0 <= ofs < fn_stackspace tf) -> (forall ofs k p, 0 <= ofs < fn_stackspace tf -> Mem.perm tm sp ofs k p) -> forall e1 m1 vars e2 m2, @@ -854,7 +854,7 @@ Qed. Lemma match_callstack_alloc_variables: forall tm1 sp tm2 m1 vars e m2 cenv f1 cs fn le te, Mem.alloc tm1 0 (fn_stackspace fn) = (tm2, sp) -> - fn_stackspace fn <= Int.max_unsigned -> + fn_stackspace fn <= Ptrofs.max_unsigned -> alloc_variables empty_env m1 vars e m2 -> list_norepet (map fst vars) -> cenv_compat cenv vars (fn_stackspace fn) -> @@ -1225,7 +1225,7 @@ Qed. Theorem match_callstack_function_entry: forall fn cenv tf m e m' tm tm' sp f cs args targs le, build_compilenv fn = (cenv, tf.(fn_stackspace)) -> - tf.(fn_stackspace) <= Int.max_unsigned -> + tf.(fn_stackspace) <= Ptrofs.max_unsigned -> list_norepet (map fst (Csharpminor.fn_vars fn)) -> list_norepet (Csharpminor.fn_params fn) -> list_disjoint (Csharpminor.fn_params fn) (Csharpminor.fn_temps fn) -> @@ -1334,82 +1334,91 @@ Lemma eval_binop_compat: eval_binop op tv1 tv2 tm = Some tv /\ Val.inject f v tv. Proof. - destruct op; simpl; intros. - inv H; inv H0; inv H1; TrivialExists. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - inv H; inv H0; inv H1; TrivialExists. - apply Int.sub_add_l. - simpl. destruct (eq_block b1 b0); auto. - subst b1. rewrite H in H0; inv H0. - rewrite dec_eq_true. rewrite Int.sub_shifted. auto. - inv H; inv H0; inv H1; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct op; simpl; intros; inv H. +- TrivialExists. apply Val.add_inject; auto. +- TrivialExists. apply Val.sub_inject; auto. +- TrivialExists. inv H0; inv H1; constructor. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. destruct (Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. - destruct (Int.eq i0 Int.zero); inv H. TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. + || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H4; TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int.eq i0 Int.zero); inv H4. TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. destruct (Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. - destruct (Int.eq i0 Int.zero); inv H. TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. + || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H4; TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int.eq i0 Int.zero); inv H4. TrivialExists. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int.iwordsize); constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int.iwordsize); constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int.iwordsize); constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists. apply Val.addl_inject; auto. +- TrivialExists. apply Val.subl_inject; auto. +- TrivialExists. inv H0; inv H1; constructor. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. destruct (Int64.eq i0 Int64.zero - || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. - destruct (Int64.eq i0 Int64.zero); inv H. TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H4; TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int64.eq i0 Int64.zero); inv H4. TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. destruct (Int64.eq i0 Int64.zero - || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. - destruct (Int64.eq i0 Int64.zero); inv H. TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. -(* cmpu *) - inv H. econstructor; split; eauto. - unfold Val.cmpu. + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H4; TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int64.eq i0 Int64.zero); inv H4. TrivialExists. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int64.iwordsize'); constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int64.iwordsize'); constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int64.iwordsize'); constructor. +- (* cmp *) + TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool. +- (* cmpu *) + TrivialExists. unfold Val.cmpu. destruct (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E. replace (Val.cmpu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b). - destruct b; simpl; constructor. + apply val_inject_val_of_optbool. symmetry. eapply Val.cmpu_bool_inject; eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. simpl; auto. -(* cmpf *) - inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. -(* cmpfs *) - inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. -(* cmpl *) - unfold Val.cmpl in *. inv H0; inv H1; simpl in H; inv H. +- (* cmpf *) + TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool. +- (* cmpfs *) + TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool. +- (* cmpl *) + unfold Val.cmpl in *. inv H0; inv H1; simpl in H4; inv H4. econstructor; split. simpl; eauto. apply val_inject_val_of_bool. -(* cmplu *) - unfold Val.cmplu in *. inv H0; inv H1; simpl in H; inv H. +- (* cmplu *) + unfold Val.cmplu in *. + destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E. + simpl in H4; inv H4. + replace (Val.cmplu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b). econstructor; split. simpl; eauto. apply val_inject_val_of_bool. + symmetry. eapply Val.cmplu_bool_inject; eauto. + intros; eapply Mem.valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. + intros; eapply Mem.different_pointers_inject; eauto. + discriminate. Qed. (** * Correctness of Cminor construction functions *) @@ -1421,21 +1430,22 @@ Lemma var_addr_correct: match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) -> eval_var_addr ge e id b -> exists tv, - eval_expr tge (Vptr sp Int.zero) te tm (var_addr cenv id) tv - /\ Val.inject f (Vptr b Int.zero) tv. + eval_expr tge (Vptr sp Ptrofs.zero) te tm (var_addr cenv id) tv + /\ Val.inject f (Vptr b Ptrofs.zero) tv. Proof. unfold var_addr; intros. assert (match_var f sp e!id cenv!id). inv H. inv MENV. auto. inv H1; inv H0; try congruence. (* local *) - exists (Vptr sp (Int.repr ofs)); split. - constructor. simpl. rewrite Int.add_zero_l; auto. + exists (Vptr sp (Ptrofs.repr ofs)); split. + constructor. simpl. rewrite Ptrofs.add_zero_l; auto. congruence. (* global *) exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG. - exists (Vptr b Int.zero); split. - constructor. simpl. rewrite symbols_preserved. rewrite H2. auto. + exists (Vptr b Ptrofs.zero); split. + constructor. simpl. unfold Genv.symbol_address. + rewrite symbols_preserved. rewrite H2. auto. econstructor; eauto. Qed. @@ -1497,7 +1507,7 @@ Lemma transl_expr_correct: forall ta (TR: transl_expr cenv a = OK ta), exists tv, - eval_expr tge (Vptr sp Int.zero) te tm ta tv + eval_expr tge (Vptr sp Ptrofs.zero) te tm ta tv /\ Val.inject f v tv. Proof. induction 3; intros; simpl in TR; try (monadInv TR). @@ -1535,7 +1545,7 @@ Lemma transl_exprlist_correct: forall ta (TR: transl_exprlist cenv a = OK ta), exists tv, - eval_exprlist tge (Vptr sp Int.zero) te tm ta tv + eval_exprlist tge (Vptr sp Ptrofs.zero) te tm ta tv /\ Val.inject_list f v tv. Proof. induction 3; intros; monadInv TR. @@ -1569,7 +1579,7 @@ Inductive match_cont: Csharpminor.cont -> Cminor.cont -> compilenv -> exit_env - transl_funbody cenv sz fn = OK tfn -> match_cont k tk cenv xenv cs -> match_cont (Csharpminor.Kcall optid fn e le k) - (Kcall optid tfn (Vptr sp Int.zero) te tk) + (Kcall optid tfn (Vptr sp Ptrofs.zero) te tk) cenv' nil (Frame cenv tfn e le te sp lo hi :: cs). @@ -1584,7 +1594,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := (Mem.nextblock m) (Mem.nextblock tm)) (MK: match_cont k tk cenv xenv cs), match_states (Csharpminor.State fn s k e le m) - (State tfn ts tk (Vptr sp Int.zero) te tm) + (State tfn ts tk (Vptr sp Ptrofs.zero) te tm) | match_state_seq: forall fn s1 s2 k e le m tfn ts1 tk sp te tm cenv xenv f lo hi cs sz (TRF: transl_funbody cenv sz fn = OK tfn) @@ -1595,7 +1605,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := (Mem.nextblock m) (Mem.nextblock tm)) (MK: match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs), match_states (Csharpminor.State fn (Csharpminor.Sseq s1 s2) k e le m) - (State tfn ts1 tk (Vptr sp Int.zero) te tm) + (State tfn ts1 tk (Vptr sp Ptrofs.zero) te tm) | match_callstate: forall fd args k m tfd targs tk tm f cs cenv (TR: transl_fundef fd = OK tfd) @@ -1789,7 +1799,7 @@ Lemma switch_match_states: (MK: match_cont k tk cenv xenv cs) (TK: transl_lblstmt_cont cenv xenv ls tk tk'), exists S, - plus step tge (State tfn (Sexit O) tk' (Vptr sp Int.zero) te tm) E0 S + plus step tge (State tfn (Sexit O) tk' (Vptr sp Ptrofs.zero) te tm) E0 S /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e le m) S. Proof. intros. inv TK. @@ -2050,7 +2060,7 @@ Opaque PTree.set. (* ifthenelse *) monadInv TR. exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. - left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Int.zero) te tm); split. + left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Ptrofs.zero) te tm); split. apply plus_one. eapply step_ifthenelse; eauto. eapply bool_of_val_inject; eauto. econstructor; eauto. destruct b; auto. @@ -2152,7 +2162,7 @@ Opaque PTree.set. (* internal call *) monadInv TR. generalize EQ; clear EQ; unfold transl_function. caseEq (build_compilenv f). intros ce sz BC. - destruct (zle sz Int.max_unsigned); try congruence. + destruct (zle sz Ptrofs.max_unsigned); try congruence. intro TRBODY. generalize TRBODY; intro TMP. monadInv TMP. set (tf := mkfunction (Csharpminor.fn_sig f) diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 4ac56b04..8defd9d9 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -22,6 +22,7 @@ Require Import Floats. Require Import Values. Require Import Memory. Require Import Ctypes. +Require Archi. (** * Syntax of operators. *) @@ -72,7 +73,7 @@ Inductive incr_or_decr : Type := Incr | Decr. (** ** Casts and truth values *) Inductive classify_cast_cases : Type := - | cast_case_neutral (**r int|pointer -> int32|pointer *) + | cast_case_pointer (**r between pointer types or intptr_t types *) | cast_case_i2i (sz2:intsize) (si2:signedness) (**r int -> int *) | cast_case_f2f (**r double -> double *) | cast_case_s2s (**r single -> single *) @@ -89,10 +90,10 @@ Inductive classify_cast_cases : Type := | cast_case_l2s (si1: signedness) (**r long -> single *) | cast_case_f2l (si2:signedness) (**r double -> long *) | cast_case_s2l (si2:signedness) (**r single -> long *) + | cast_case_i2bool (**r int -> bool *) + | cast_case_l2bool (**r long -> bool *) | cast_case_f2bool (**r double -> bool *) | cast_case_s2bool (**r single -> bool *) - | cast_case_l2bool (**r long -> bool *) - | cast_case_p2bool (**r pointer -> bool *) | cast_case_struct (id1 id2: ident) (**r struct -> struct *) | cast_case_union (id1 id2: ident) (**r union -> union *) | cast_case_void (**r any -> void *) @@ -100,33 +101,54 @@ Inductive classify_cast_cases : Type := Definition classify_cast (tfrom tto: type) : classify_cast_cases := match tto, tfrom with - | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral + (* To [void] *) + | Tvoid, _ => cast_case_void + (* To [_Bool] *) + | Tint IBool _ _, Tint _ _ _ => cast_case_i2bool + | Tint IBool _ _, Tlong _ _ => cast_case_l2bool | Tint IBool _ _, Tfloat F64 _ => cast_case_f2bool | Tint IBool _ _, Tfloat F32 _ => cast_case_s2bool - | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool - | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2 + | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => + if Archi.ptr64 then cast_case_l2bool else cast_case_i2bool + (* To [int] other than [_Bool] *) + | Tint sz2 si2 _, Tint _ _ _ => + if Archi.ptr64 then cast_case_i2i sz2 si2 + else if intsize_eq sz2 I32 then cast_case_pointer + else cast_case_i2i sz2 si2 + | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2 | Tint sz2 si2 _, Tfloat F64 _ => cast_case_f2i sz2 si2 | Tint sz2 si2 _, Tfloat F32 _ => cast_case_s2i sz2 si2 - | Tfloat F64 _, Tfloat F64 _ => cast_case_f2f - | Tfloat F32 _, Tfloat F32 _ => cast_case_s2s - | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f - | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s - | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1 - | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1 - | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral - | Tlong _ _, Tlong _ _ => cast_case_l2l + | Tint sz2 si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => + if Archi.ptr64 then cast_case_l2i sz2 si2 + else if intsize_eq sz2 I32 then cast_case_pointer + else cast_case_i2i sz2 si2 + (* To [long] *) + | Tlong _ _, Tlong _ _ => + if Archi.ptr64 then cast_case_pointer else cast_case_l2l | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1 - | Tint IBool _ _, Tlong _ _ => cast_case_l2bool - | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2 | Tlong si2 _, Tfloat F64 _ => cast_case_f2l si2 | Tlong si2 _, Tfloat F32 _ => cast_case_s2l si2 + | Tlong si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => + if Archi.ptr64 then cast_case_pointer else cast_case_i2l si2 + (* To [float] *) + | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1 + | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1 | Tfloat F64 _, Tlong si1 _ => cast_case_l2f si1 | Tfloat F32 _, Tlong si1 _ => cast_case_l2s si1 - | Tpointer _ _, Tlong _ _ => cast_case_l2i I32 Unsigned - | Tlong si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2 + | Tfloat F64 _, Tfloat F64 _ => cast_case_f2f + | Tfloat F32 _, Tfloat F32 _ => cast_case_s2s + | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f + | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s + (* To pointer types *) + | Tpointer _ _, Tint _ _ _ => + if Archi.ptr64 then cast_case_i2l Unsigned else cast_case_pointer + | Tpointer _ _, Tlong _ _ => + if Archi.ptr64 then cast_case_pointer else cast_case_l2i I32 Unsigned + | Tpointer _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_pointer + (* To struct or union types *) | Tstruct id2 _, Tstruct id1 _ => cast_case_struct id1 id2 | Tunion id2 _, Tunion id1 _ => cast_case_union id1 id2 - | Tvoid, _ => cast_case_void + (* Catch-all *) | _, _ => cast_case_default end. @@ -200,9 +222,11 @@ Definition cast_single_long (si : signedness) (f: float32) : option int64 := Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := match classify_cast t1 t2 with - | cast_case_neutral => + | cast_case_pointer => match v with - | Vint _ | Vptr _ _ => Some v + | Vptr _ _ => Some v + | Vint _ => if Archi.ptr64 then None else Some v + | Vlong _ => if Archi.ptr64 then Some v else None | _ => None end | cast_case_i2i sz2 si2 => @@ -258,6 +282,25 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := end | _ => None end + | cast_case_i2bool => + match v with + | Vint n => + Some(Vint(if Int.eq n Int.zero then Int.zero else Int.one)) + | Vptr b ofs => + if Archi.ptr64 then None else + if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some Vone else None + | _ => None + end + | cast_case_l2bool => + match v with + | Vlong n => + Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one)) + | Vptr b ofs => + if negb Archi.ptr64 then None else + if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some Vone else None + + | _ => None + end | cast_case_f2bool => match v with | Vfloat f => @@ -270,12 +313,6 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := Some(Vint(if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one)) | _ => None end - | cast_case_p2bool => - match v with - | Vint i => Some (Vint (cast_int_int IBool Signed i)) - | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vone else None - | _ => None - end | cast_case_l2l => match v with | Vlong n => Some (Vlong n) @@ -291,12 +328,6 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := | Vlong n => Some(Vint (cast_int_int sz si (Int.repr (Int64.unsigned n)))) | _ => None end - | cast_case_l2bool => - match v with - | Vlong n => - Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one)) - | _ => None - end | cast_case_l2f si1 => match v with | Vlong i => Some (Vfloat (cast_long_float si1 i)) @@ -350,16 +381,15 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := Inductive classify_bool_cases : Type := | bool_case_i (**r integer *) + | bool_case_l (**r long *) | bool_case_f (**r double float *) | bool_case_s (**r single float *) - | bool_case_p (**r pointer *) - | bool_case_l (**r long *) | bool_default. Definition classify_bool (ty: type) : classify_bool_cases := match typeconv ty with | Tint _ _ _ => bool_case_i - | Tpointer _ _ => bool_case_p + | Tpointer _ _ => if Archi.ptr64 then bool_case_l else bool_case_i | Tfloat F64 _ => bool_case_f | Tfloat F32 _ => bool_case_s | Tlong _ _ => bool_case_l @@ -376,6 +406,17 @@ Definition bool_val (v: val) (t: type) (m: mem) : option bool := | bool_case_i => match v with | Vint n => Some (negb (Int.eq n Int.zero)) + | Vptr b ofs => + if Archi.ptr64 then None else + if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some true else None + | _ => None + end + | bool_case_l => + match v with + | Vlong n => Some (negb (Int64.eq n Int64.zero)) + | Vptr b ofs => + if negb Archi.ptr64 then None else + if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some true else None | _ => None end | bool_case_f => @@ -388,17 +429,6 @@ Definition bool_val (v: val) (t: type) (m: mem) : option bool := | Vsingle f => Some (negb (Float32.cmp Ceq f Float32.zero)) | _ => None end - | bool_case_p => - match v with - | Vint n => Some (negb (Int.eq n Int.zero)) - | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some true else None - | _ => None - end - | bool_case_l => - match v with - | Vlong n => Some (negb (Int64.eq n Int64.zero)) - | _ => None - end | bool_default => None end. @@ -407,35 +437,7 @@ Definition bool_val (v: val) (t: type) (m: mem) : option bool := (** *** Boolean negation *) Definition sem_notbool (v: val) (ty: type) (m: mem): option val := - match classify_bool ty with - | bool_case_i => - match v with - | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) - | _ => None - end - | bool_case_f => - match v with - | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero)) - | _ => None - end - | bool_case_s => - match v with - | Vsingle f => Some (Val.of_bool (Float32.cmp Ceq f Float32.zero)) - | _ => None - end - | bool_case_p => - match v with - | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) - | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vfalse else None - | _ => None - end - | bool_case_l => - match v with - | Vlong n => Some (Val.of_bool (Int64.eq n Int64.zero)) - | _ => None - end - | bool_default => None - end. + option_map (fun b => Val.of_bool (negb b)) (bool_val v ty m). (** *** Opposite and absolute value *) @@ -623,57 +625,55 @@ Definition sem_binarith (** *** Addition *) Inductive classify_add_cases : Type := - | add_case_pi(ty: type) (**r pointer, int *) - | add_case_ip(ty: type) (**r int, pointer *) - | add_case_pl(ty: type) (**r pointer, long *) - | add_case_lp(ty: type) (**r long, pointer *) - | add_default. (**r numerical type, numerical type *) + | add_case_pi (ty: type) (si: signedness) (**r pointer, int *) + | add_case_pl (ty: type) (**r pointer, long *) +(* + | add_case_ip (si: signedness) (ty: type) (**r int, pointer *) + | add_case_lp (ty: type) (**r long, pointer *) +*) + | add_default. (**r numerical type, numerical type *) Definition classify_add (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tpointer ty _, Tint _ _ _ => add_case_pi ty - | Tint _ _ _, Tpointer ty _ => add_case_ip ty + | Tpointer ty _, Tint _ si _ => add_case_pi ty si | Tpointer ty _, Tlong _ _ => add_case_pl ty +(* + | Tint _ si _, Tpointer ty _ => add_case_ip si ty | Tlong _ _, Tpointer ty _ => add_case_lp ty +*) | _, _ => add_default end. +Definition ptrofs_of_int (si: signedness) (n: int) : ptrofs := + match si with + | Signed => Ptrofs.of_ints n + | Unsigned => Ptrofs.of_intu n + end. + Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m: mem): option val := match classify_add t1 t2 with - | add_case_pi ty => (**r pointer plus integer *) - match v1,v2 with + | add_case_pi ty si => (**r pointer plus integer *) + match v1, v2 with | Vptr b1 ofs1, Vint n2 => - Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) - | Vint n1, Vint n2 => - Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) - | _, _ => None - end - | add_case_ip ty => (**r integer plus pointer *) - match v1,v2 with - | Vint n1, Vptr b2 ofs2 => - Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) + let n2 := ptrofs_of_int si n2 in + Some (Vptr b1 (Ptrofs.add ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) | Vint n1, Vint n2 => - Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) + if Archi.ptr64 then None else Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vlong n1, Vint n2 => + let n2 := cast_int_long si n2 in + if Archi.ptr64 then Some (Vlong (Int64.add n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None | _, _ => None end | add_case_pl ty => (**r pointer plus long *) - match v1,v2 with + match v1, v2 with | Vptr b1 ofs1, Vlong n2 => - let n2 := Int.repr (Int64.unsigned n2) in - Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + let n2 := Ptrofs.of_int64 n2 in + Some (Vptr b1 (Ptrofs.add ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) | Vint n1, Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in - Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) - | _, _ => None - end - | add_case_lp ty => (**r long plus pointer *) - match v1,v2 with - | Vlong n1, Vptr b2 ofs2 => - let n1 := Int.repr (Int64.unsigned n1) in - Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) - | Vlong n1, Vint n2 => - let n1 := Int.repr (Int64.unsigned n1) in - Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) + if Archi.ptr64 then None else Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vlong n1, Vlong n2 => + if Archi.ptr64 then Some (Vlong (Int64.add n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None | _, _ => None end | add_default => @@ -688,14 +688,14 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (** *** Subtraction *) Inductive classify_sub_cases : Type := - | sub_case_pi(ty: type) (**r pointer, int *) - | sub_case_pp(ty: type) (**r pointer, pointer *) - | sub_case_pl(ty: type) (**r pointer, long *) - | sub_default. (**r numerical type, numerical type *) + | sub_case_pi (ty: type) (si: signedness) (**r pointer, int *) + | sub_case_pp (ty: type) (**r pointer, pointer *) + | sub_case_pl (ty: type) (**r pointer, long *) + | sub_default. (**r numerical type, numerical type *) Definition classify_sub (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tpointer ty _, Tint _ _ _ => sub_case_pi ty + | Tpointer ty _, Tint _ si _ => sub_case_pi ty si | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty | Tpointer ty _, Tlong _ _ => sub_case_pl ty | _, _ => sub_default @@ -703,22 +703,28 @@ Definition classify_sub (ty1: type) (ty2: type) := Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m:mem): option val := match classify_sub t1 t2 with - | sub_case_pi ty => (**r pointer minus integer *) - match v1,v2 with + | sub_case_pi ty si => (**r pointer minus integer *) + match v1, v2 with | Vptr b1 ofs1, Vint n2 => - Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + let n2 := ptrofs_of_int si n2 in + Some (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) | Vint n1, Vint n2 => - Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + if Archi.ptr64 then None else Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vlong n1, Vint n2 => + let n2 := cast_int_long si n2 in + if Archi.ptr64 then Some (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None | _, _ => None end | sub_case_pl ty => (**r pointer minus long *) - match v1,v2 with + match v1, v2 with | Vptr b1 ofs1, Vlong n2 => - let n2 := Int.repr (Int64.unsigned n2) in - Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + let n2 := Ptrofs.of_int64 n2 in + Some (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) | Vint n1, Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in - Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + if Archi.ptr64 then None else Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vlong n1, Vlong n2 => + if Archi.ptr64 then Some (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None | _, _ => None end | sub_case_pp ty => (**r pointer minus pointer *) @@ -726,8 +732,8 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) | Vptr b1 ofs1, Vptr b2 ofs2 => if eq_block b1 b2 then let sz := sizeof cenv ty in - if zlt 0 sz && zle sz Int.max_signed - then Some (Vint (Int.divs (Int.sub ofs1 ofs2) (Int.repr sz))) + if zlt 0 sz && zle sz Ptrofs.max_signed + then Some (Vptrofs (Ptrofs.divs (Ptrofs.sub ofs1 ofs2) (Ptrofs.repr sz))) else None else None | _, _ => None @@ -903,6 +909,8 @@ Definition sem_shr (v1:val) (t1:type) (v2: val) (t2:type) : option val := Inductive classify_cmp_cases : Type := | cmp_case_pp (**r pointer, pointer *) + | cmp_case_pi (si: signedness) (**r pointer, int *) + | cmp_case_ip (si: signedness) (**r int, pointer *) | cmp_case_pl (**r pointer, long *) | cmp_case_lp (**r long, pointer *) | cmp_default. (**r numerical, numerical *) @@ -910,32 +918,64 @@ Inductive classify_cmp_cases : Type := Definition classify_cmp (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with | Tpointer _ _ , Tpointer _ _ => cmp_case_pp - | Tpointer _ _ , Tint _ _ _ => cmp_case_pp - | Tint _ _ _, Tpointer _ _ => cmp_case_pp + | Tpointer _ _ , Tint _ si _ => cmp_case_pi si + | Tint _ si _, Tpointer _ _ => cmp_case_ip si | Tpointer _ _ , Tlong _ _ => cmp_case_pl | Tlong _ _ , Tpointer _ _ => cmp_case_lp | _, _ => cmp_default end. +Definition cmp_ptr (m: mem) (c: comparison) (v1 v2: val): option val := + option_map Val.of_bool + (if Archi.ptr64 + then Val.cmplu_bool (Mem.valid_pointer m) c v1 v2 + else Val.cmpu_bool (Mem.valid_pointer m) c v1 v2). + Definition sem_cmp (c:comparison) (v1: val) (t1: type) (v2: val) (t2: type) (m: mem): option val := match classify_cmp t1 t2 with | cmp_case_pp => - option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) + cmp_ptr m c v1 v2 + | cmp_case_pi si => + match v2 with + | Vint n2 => + let v2' := Vptrofs (ptrofs_of_int si n2) in + cmp_ptr m c v1 v2' + | Vptr b ofs => + if Archi.ptr64 then None else cmp_ptr m c v1 v2 + | _ => + None + end + | cmp_case_ip si => + match v1 with + | Vint n1 => + let v1' := Vptrofs (ptrofs_of_int si n1) in + cmp_ptr m c v1' v2 + | Vptr b ofs => + if Archi.ptr64 then None else cmp_ptr m c v1 v2 + | _ => + None + end | cmp_case_pl => match v2 with | Vlong n2 => - let n2 := Int.repr (Int64.unsigned n2) in - option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n2)) - | _ => None + let v2' := Vptrofs (Ptrofs.of_int64 n2) in + cmp_ptr m c v1 v2' + | Vptr b ofs => + if Archi.ptr64 then cmp_ptr m c v1 v2 else None + | _ => + None end | cmp_case_lp => match v1 with | Vlong n1 => - let n1 := Int.repr (Int64.unsigned n1) in - option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c (Vint n1) v2) - | _ => None + let v1' := Vptrofs (Ptrofs.of_int64 n1) in + cmp_ptr m c v1' v2 + | Vptr b ofs => + if Archi.ptr64 then cmp_ptr m c v1 v2 else None + | _ => + None end | cmp_default => sem_binarith @@ -1047,30 +1087,30 @@ Variables m m': mem. Hypothesis valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.valid_pointer m b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m' b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m b1 (Int.unsigned ofs) = true -> - Mem.weak_valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m' b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_pointer_no_overflow: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Hypothesis valid_different_pointers_inj: forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - Mem.valid_pointer m b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m b2 (Ptrofs.unsigned ofs2) = true -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). Remark val_inject_vtrue: forall f, Val.inject f Vtrue Vtrue. Proof. unfold Vtrue; auto. Qed. @@ -1082,11 +1122,18 @@ Remark val_inject_of_bool: forall f b, Val.inject f (Val.of_bool b) (Val.of_bool Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. Qed. -Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool. +Remark val_inject_vptrofs: forall n, Val.inject f (Vptrofs n) (Vptrofs n). +Proof. intros. unfold Vptrofs. destruct Archi.ptr64; auto. Qed. + +Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool val_inject_vptrofs. Ltac TrivialInject := match goal with - | |- exists v', Some ?v = Some v' /\ _ => exists v; split; auto + | [ H: None = Some _ |- _ ] => discriminate + | [ H: Some _ = Some _ |- _ ] => inv H; TrivialInject + | [ H: match ?x with Some _ => _ | None => _ end = Some _ |- _ ] => destruct x; TrivialInject + | [ H: match ?x with true => _ | false => _ end = Some _ |- _ ] => destruct x eqn:?; TrivialInject + | [ |- exists v', Some ?v = Some v' /\ _ ] => exists v; split; auto | _ => idtac end. @@ -1096,20 +1143,31 @@ Lemma sem_cast_inj: Val.inject f v1 tv1 -> exists tv, sem_cast tv1 ty1 ty m'= Some tv /\ Val.inject f v tv. Proof. - unfold sem_cast; intros; destruct (classify_cast ty1 ty); - inv H0; inv H; TrivialInject. + unfold sem_cast; intros; destruct (classify_cast ty1 ty); inv H0; TrivialInject. - econstructor; eauto. -- destruct (cast_float_int si2 f0); inv H1; TrivialInject. -- destruct (cast_single_int si2 f0); inv H1; TrivialInject. -- destruct (cast_float_long si2 f0); inv H1; TrivialInject. -- destruct (cast_single_long si2 f0); inv H1; TrivialInject. -- destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VALID; inv H2. - erewrite weak_valid_pointer_inj by eauto. TrivialInject. -- destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto. -- destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto. +- erewrite weak_valid_pointer_inj by eauto. TrivialInject. +- erewrite weak_valid_pointer_inj by eauto. TrivialInject. +- destruct (ident_eq id1 id2); TrivialInject. econstructor; eauto. +- destruct (ident_eq id1 id2); TrivialInject. econstructor; eauto. - econstructor; eauto. Qed. +Lemma bool_val_inj: + forall v ty b tv, + bool_val v ty m = Some b -> + Val.inject f v tv -> + bool_val tv ty m' = Some b. +Proof. + unfold bool_val; intros. + destruct (classify_bool ty); inv H0; try congruence. + destruct Archi.ptr64; try discriminate. + destruct (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs1)) eqn:VP; inv H. + erewrite weak_valid_pointer_inj by eauto. auto. + destruct Archi.ptr64; try discriminate. + destruct (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs1)) eqn:VP; inv H. + erewrite weak_valid_pointer_inj by eauto. auto. +Qed. + Lemma sem_unary_operation_inj: forall op v1 ty v tv1, sem_unary_operation op v1 ty m = Some v -> @@ -1117,15 +1175,14 @@ Lemma sem_unary_operation_inj: exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ Val.inject f v tv. Proof. unfold sem_unary_operation; intros. destruct op. - (* notbool *) - unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject. - destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H2. - erewrite weak_valid_pointer_inj by eauto. TrivialInject. - (* notint *) +- (* notbool *) + unfold sem_notbool in *. destruct (bool_val v1 ty m) as [b|] eqn:BV; simpl in H; inv H. + erewrite bool_val_inj by eauto. simpl. TrivialInject. +- (* notint *) unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject. - (* neg *) +- (* neg *) unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject. - (* absfloat *) +- (* absfloat *) unfold sem_absfloat in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject. Qed. @@ -1175,6 +1232,24 @@ Proof. destruct (Int.ltu i0 Int64.iwordsize'); inv H; auto. Qed. +Remark sem_cmp_ptr_inj: + forall c v1 v2 v tv1 tv2, + cmp_ptr m c v1 v2 = Some v -> + Val.inject f v1 tv1 -> + Val.inject f v2 tv2 -> + exists tv, cmp_ptr m' c tv1 tv2 = Some tv /\ Val.inject f v tv. +Proof. + unfold cmp_ptr; intros. + remember (if Archi.ptr64 + then Val.cmplu_bool (Mem.valid_pointer m) c v1 v2 + else Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as ob. + destruct ob as [b|]; simpl in H; inv H. + exists (Val.of_bool b); split; auto. + destruct Archi.ptr64. + erewrite Val.cmplu_bool_inject by eauto. auto. + erewrite Val.cmpu_bool_inject by eauto. auto. +Qed. + Remark sem_cmp_inj: forall cmp v1 tv1 ty1 v2 tv2 ty2 v, sem_cmp cmp v1 ty1 v2 ty2 m = Some v -> @@ -1185,24 +1260,15 @@ Proof. intros. unfold sem_cmp in *; destruct (classify_cmp ty1 ty2). - (* pointer - pointer *) - destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. - replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b). - simpl. TrivialInject. - symmetry. eapply Val.cmpu_bool_inject; eauto. + eapply sem_cmp_ptr_inj; eauto. +- (* pointer - int *) + inversion H1; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto. +- (* int - pointer *) + inversion H0; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto. - (* pointer - long *) - destruct v2; try discriminate. inv H1. - set (v2 := Vint (Int.repr (Int64.unsigned i))) in *. - destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. - replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 v2) with (Some b). - simpl. TrivialInject. - symmetry. eapply Val.cmpu_bool_inject with (v2 := v2); eauto. constructor. + inversion H1; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto. - (* long - pointer *) - destruct v1; try discriminate. inv H0. - set (v1 := Vint (Int.repr (Int64.unsigned i))) in *. - destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. - replace (Val.cmpu_bool (Mem.valid_pointer m') cmp v1 tv2) with (Some b). - simpl. TrivialInject. - symmetry. eapply Val.cmpu_bool_inject with (v1 := v1); eauto. constructor. + inversion H0; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto. - (* numerical - numerical *) assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))). { @@ -1220,26 +1286,22 @@ Proof. unfold sem_binary_operation; intros; destruct op. - (* add *) unfold sem_add in *; destruct (classify_add ty1 ty2). - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + + inv H0; inv H1; TrivialInject. + econstructor. eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. + + inv H0; inv H1; TrivialInject. + econstructor. eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. + eapply sem_binarith_inject; eauto; intros; exact I. - (* sub *) unfold sem_sub in *; destruct (classify_sub ty1 ty2). - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. rewrite Int.sub_add_l. auto. - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; TrivialInject. + econstructor. eauto. rewrite Ptrofs.sub_add_l. auto. + + inv H0; inv H1; TrivialInject. destruct (eq_block b1 b0); try discriminate. subst b1. rewrite H0 in H2; inv H2. rewrite dec_eq_true. - destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3. - rewrite Int.sub_shifted. TrivialInject. - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. rewrite Int.sub_add_l. auto. + destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Ptrofs.max_signed); inv H. + rewrite Ptrofs.sub_shifted. TrivialInject. + + inv H0; inv H1; TrivialInject. + econstructor. eauto. rewrite Ptrofs.sub_add_l. auto. + eapply sem_binarith_inject; eauto; intros; exact I. - (* mul *) eapply sem_binarith_inject; eauto; intros; exact I. @@ -1286,18 +1348,6 @@ Proof. - eapply sem_cmp_inj; eauto. Qed. -Lemma bool_val_inj: - forall v ty b tv, - bool_val v ty m = Some b -> - Val.inject f v tv -> - bool_val tv ty m' = Some b. -Proof. - unfold bool_val; intros. - destruct (classify_bool ty); inv H0; try congruence. - destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H. - erewrite weak_valid_pointer_inj by eauto. auto. -Qed. - End GENERIC_INJECTION. Lemma sem_cast_inject: @@ -1364,7 +1414,7 @@ Lemma cast_bool_bool_val: assert (A: classify_bool t = match t with | Tint _ _ _ => bool_case_i - | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p + | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ => if Archi.ptr64 then bool_case_l else bool_case_i | Tfloat F64 _ => bool_case_f | Tfloat F32 _ => bool_case_s | Tlong _ _ => bool_case_l @@ -1373,9 +1423,12 @@ Lemma cast_bool_bool_val: { unfold classify_bool; destruct t; simpl; auto. destruct i; auto. } - unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto. + unfold bool_val. rewrite A. + unfold sem_cast, classify_cast; remember Archi.ptr64 as ptr64; destruct t; simpl; auto; destruct v; auto. destruct (Int.eq i0 Int.zero); auto. + destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i0)); auto. destruct (Int64.eq i Int64.zero); auto. + destruct (negb ptr64); auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. destruct f; auto. destruct f; auto. destruct f; auto. @@ -1383,13 +1436,30 @@ Lemma cast_bool_bool_val: destruct (Float.cmp Ceq f0 Float.zero); auto. destruct f; auto. destruct (Float32.cmp Ceq f0 Float32.zero); auto. - destruct f; auto. + destruct f; auto. + destruct ptr64; auto. destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. - destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. - destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. + destruct ptr64; auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto. + destruct ptr64; auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. + destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Int.eq i Int.zero); auto. + destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto. + destruct ptr64; auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. + destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Int.eq i Int.zero); auto. + destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto. + destruct ptr64; auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. + destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. Qed. (** Relation between Boolean value and Boolean negation. *) @@ -1399,13 +1469,13 @@ Lemma notbool_bool_val: sem_notbool v t m = match bool_val v t m with None => None | Some b => Some(Val.of_bool (negb b)) end. Proof. - intros. unfold sem_notbool, bool_val. - destruct (classify_bool t); auto; destruct v; auto; rewrite ? negb_involutive; auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. + intros. unfold sem_notbool. destruct (bool_val v t m) as [[] | ]; reflexivity. Qed. (** Properties of values obtained by casting to a given type. *) +Section VAL_CASTED. + Inductive val_casted: val -> type -> Prop := | val_casted_int: forall sz si attr n, cast_int_int sz si n = n -> @@ -1419,9 +1489,13 @@ Inductive val_casted: val -> type -> Prop := | val_casted_ptr_ptr: forall b ofs ty attr, val_casted (Vptr b ofs) (Tpointer ty attr) | val_casted_int_ptr: forall n ty attr, - val_casted (Vint n) (Tpointer ty attr) + Archi.ptr64 = false -> val_casted (Vint n) (Tpointer ty attr) | val_casted_ptr_int: forall b ofs si attr, - val_casted (Vptr b ofs) (Tint I32 si attr) + Archi.ptr64 = false -> val_casted (Vptr b ofs) (Tint I32 si attr) + | val_casted_long_ptr: forall n ty attr, + Archi.ptr64 = true -> val_casted (Vlong n) (Tpointer ty attr) + | val_casted_ptr_long: forall b ofs si attr, + Archi.ptr64 = true -> val_casted (Vptr b ofs) (Tlong si attr) | val_casted_struct: forall id attr b ofs, val_casted (Vptr b ofs) (Tstruct id attr) | val_casted_union: forall id attr b ofs, @@ -1429,6 +1503,8 @@ Inductive val_casted: val -> type -> Prop := | val_casted_void: forall v, val_casted v Tvoid. +Hint Constructors val_casted. + Remark cast_int_int_idem: forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i. Proof. @@ -1438,77 +1514,50 @@ Proof. destruct (Int.eq i Int.zero); auto. Qed. +Ltac DestructCases := + match goal with + | [H: match match ?x with _ => _ end with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases + | [H: match ?x with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases + | [H: Some _ = Some _ |- _ ] => inv H; DestructCases + | [H: None = Some _ |- _ ] => discriminate H + | [H: @eq intsize _ _ |- _ ] => discriminate H || (clear H; DestructCases) + | [ |- val_casted (Vint (if ?x then Int.zero else Int.one)) _ ] => + try (constructor; destruct x; reflexivity) + | [ |- val_casted (Vint _) (Tint ?sz ?sg _) ] => + try (constructor; apply (cast_int_int_idem sz sg)) + | _ => idtac + end. + Lemma cast_val_is_casted: forall v ty ty' v' m, sem_cast v ty ty' m = Some v' -> val_casted v' ty'. Proof. - unfold sem_cast; intros. destruct ty'; simpl in *. -- (* void *) - constructor. -- (* int *) - destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H. - constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I8 s). - destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). - destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I16 s). - constructor. apply (cast_int_int_idem I16 s). - destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). - destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). - constructor. auto. - constructor. - constructor. auto. - destruct (cast_single_int s f); inv H1. constructor. auto. - destruct (cast_float_int s f); inv H1. constructor; auto. - constructor; auto. - constructor. - constructor; auto. - constructor. - constructor; auto. - constructor. - constructor. simpl. destruct (Int.eq i0 Int.zero); auto. - constructor. simpl. destruct (Int64.eq i Int64.zero); auto. - constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. - constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. -- (* long *) - destruct ty; try (destruct f); try discriminate. - destruct v; inv H. constructor. - destruct v; inv H. constructor. - destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor. - destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor. - destruct v; inv H. constructor. - destruct v; inv H. constructor. - destruct v; inv H. constructor. -- (* float *) - destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor. -- (* pointer *) - destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor. -- (* array (impossible case) *) - discriminate. -- (* function (impossible case) *) - discriminate. -- (* structs *) - destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i); inv H; constructor. -- (* unions *) - destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i); inv H; constructor. + unfold sem_cast; intros. + destruct ty, ty'; simpl in H; DestructCases; constructor; auto. Qed. +End VAL_CASTED. + (** As a consequence, casting twice is equivalent to casting once. *) Lemma cast_val_casted: forall v ty m, val_casted v ty -> sem_cast v ty ty m = Some v. Proof. - intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto. - destruct sz; congruence. - unfold proj_sumbool; repeat rewrite dec_eq_true; auto. - unfold proj_sumbool; repeat rewrite dec_eq_true; auto. + intros. unfold sem_cast; inversion H; clear H; subst v ty; simpl. +- destruct Archi.ptr64; [ | destruct (intsize_eq sz I32)]. ++ destruct sz; f_equal; f_equal; assumption. ++ subst sz; auto. ++ destruct sz; f_equal; f_equal; assumption. +- auto. +- auto. +- destruct Archi.ptr64; auto. +- auto. +- rewrite H0; auto. +- rewrite H0; auto. +- rewrite H0; auto. +- rewrite H0; auto. +- rewrite dec_eq_true; auto. +- rewrite dec_eq_true; auto. +- auto. Qed. Lemma cast_idempotent: diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 30e6200d..0c3e00de 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -63,7 +63,7 @@ Variable ge: genv. returned, and [t] the trace of observables (nonempty if this is a volatile access). *) -Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : trace -> val -> Prop := +Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs) : trace -> val -> Prop := | deref_loc_value: forall chunk v, access_mode ty = By_value chunk -> type_is_volatile ty = false -> @@ -87,7 +87,7 @@ Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : trace -> val -> [m'] is the updated memory state and [t] the trace of observables (nonempty if this is a volatile store). *) -Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int): +Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs): val -> trace -> mem -> Prop := | assign_loc_value: forall v chunk m', access_mode ty = By_value chunk -> @@ -100,13 +100,13 @@ Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int): assign_loc ty m b ofs v t m' | assign_loc_copy: forall b' ofs' bytes m', access_mode ty = By_copy -> - (alignof_blockcopy ge ty | Int.unsigned ofs') -> - (alignof_blockcopy ge ty | Int.unsigned ofs) -> - b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs - \/ Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs - \/ Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs' -> - Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ge ty) = Some bytes -> - Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' -> + (alignof_blockcopy ge ty | Ptrofs.unsigned ofs') -> + (alignof_blockcopy ge ty | Ptrofs.unsigned ofs) -> + b' <> b \/ Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs + \/ Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs + \/ Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs' -> + Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ge ty) = Some bytes -> + Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' -> assign_loc ty m b ofs (Vptr b' ofs') E0 m'. (** Allocation of function-local variables. @@ -142,7 +142,7 @@ Inductive bind_parameters (e: env): | bind_parameters_cons: forall m id ty params v1 vl b m1 m2, PTree.get id e = Some(b, ty) -> - assign_loc ty m b Int.zero v1 E0 m1 -> + assign_loc ty m b Ptrofs.zero v1 E0 m1 -> bind_parameters e m1 params vl m2 -> bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. @@ -211,12 +211,12 @@ Inductive lred: expr -> mem -> expr -> mem -> Prop := | red_var_local: forall x ty m b, e!x = Some(b, ty) -> lred (Evar x ty) m - (Eloc b Int.zero ty) m + (Eloc b Ptrofs.zero ty) m | red_var_global: forall x ty m b, e!x = None -> Genv.find_symbol ge x = Some b -> lred (Evar x ty) m - (Eloc b Int.zero ty) m + (Eloc b Ptrofs.zero ty) m | red_deref: forall b ofs ty1 ty m, lred (Ederef (Eval (Vptr b ofs) ty1) ty) m (Eloc b ofs ty) m @@ -224,7 +224,7 @@ Inductive lred: expr -> mem -> expr -> mem -> Prop := ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta -> lred (Efield (Eval (Vptr b ofs) (Tstruct id a)) f ty) m - (Eloc b (Int.add ofs (Int.repr delta)) ty) m + (Eloc b (Ptrofs.add ofs (Ptrofs.repr delta)) ty) m | red_field_union: forall b ofs id co a f ty m, ge.(genv_cenv)!id = Some co -> lred (Efield (Eval (Vptr b ofs) (Tunion id a)) f ty) m @@ -274,10 +274,10 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := E0 (Eparen (if b then r1 else r2) ty ty) m | red_sizeof: forall ty1 ty m, rred (Esizeof ty1 ty) m - E0 (Eval (Vint (Int.repr (sizeof ge ty1))) ty) m + E0 (Eval (Vptrofs (Ptrofs.repr (sizeof ge ty1))) ty) m | red_alignof: forall ty1 ty m, rred (Ealignof ty1 ty) m - E0 (Eval (Vint (Int.repr (alignof ge ty1))) ty) m + E0 (Eval (Vptrofs (Ptrofs.repr (alignof ge ty1))) ty) m | red_assign: forall b ofs ty1 v2 ty2 m v t m', sem_cast v2 ty2 ty1 m = Some v -> assign_loc ty1 m b ofs v t m' -> diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index e42091af..4393640c 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -321,7 +321,7 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr (Evar id) v | eval_Eaddrof: forall id b, eval_var_addr e id b -> - eval_expr (Eaddrof id) (Vptr b Int.zero) + eval_expr (Eaddrof id) (Vptr b Ptrofs.zero) | eval_Econst: forall cst v, eval_constant cst = Some v -> eval_expr (Econst cst) v diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 40b51bd3..4e7aca8a 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -49,6 +49,9 @@ Definition make_floatconst (f: float) := Econst (Ofloatconst f). Definition make_singleconst (f: float32) := Econst (Osingleconst f). +Definition make_ptrofsconst (n: Z) := + if Archi.ptr64 then make_longconst (Int64.repr n) else make_intconst (Int.repr n). + Definition make_singleoffloat (e: expr) := Eunop Osingleoffloat e. Definition make_floatofsingle (e: expr) := Eunop Ofloatofsingle e. @@ -106,7 +109,7 @@ Definition make_longofsingle (e: expr) (sg: signedness) := | Unsigned => Eunop Olonguofsingle e end. -Definition make_cmp_ne_zero (e: expr) := +Definition make_cmpu_ne_zero (e: expr) := match e with | Ebinop (Ocmp c) e1 e2 => e | Ebinop (Ocmpu c) e1 e2 => e @@ -114,7 +117,7 @@ Definition make_cmp_ne_zero (e: expr) := | Ebinop (Ocmpfs c) e1 e2 => e | Ebinop (Ocmpl c) e1 e2 => e | Ebinop (Ocmplu c) e1 e2 => e - | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero) + | _ => Ebinop (Ocmpu Cne) e (make_intconst Int.zero) end. (** Variants of [sizeof] and [alignof] that check that the given type is complete. *) @@ -139,12 +142,12 @@ Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) := | I16, Signed => Eunop Ocast16signed e | I16, Unsigned => Eunop Ocast16unsigned e | I32, _ => e - | IBool, _ => make_cmp_ne_zero e + | IBool, _ => make_cmpu_ne_zero e end. Definition make_cast (from to: type) (e: expr) := match classify_cast from to with - | cast_case_neutral => OK e + | cast_case_pointer => OK e | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2) | cast_case_f2f => OK e | cast_case_s2s => OK e @@ -161,10 +164,10 @@ Definition make_cast (from to: type) (e: expr) := | cast_case_l2s si1 => OK (make_singleoflong e si1) | cast_case_f2l si2 => OK (make_longoffloat e si2) | cast_case_s2l si2 => OK (make_longofsingle e si2) + | cast_case_i2bool => OK (make_cmpu_ne_zero e) | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)) | cast_case_s2bool => OK (Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero)) - | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero)) - | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero)) + | cast_case_l2bool => OK (Ebinop (Ocmplu Cne) e (make_longconst Int64.zero)) | cast_case_struct id1 id2 => OK e | cast_case_union id1 id2 => OK e | cast_case_void => OK e @@ -176,11 +179,10 @@ Definition make_cast (from to: type) (e: expr) := Definition make_boolean (e: expr) (ty: type) := match classify_bool ty with - | bool_case_i => make_cmp_ne_zero e + | bool_case_i => make_cmpu_ne_zero e | bool_case_f => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero) | bool_case_s => Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero) - | bool_case_p => Ebinop (Ocmpu Cne) e (make_intconst Int.zero) - | bool_case_l => Ebinop (Ocmpl Cne) e (make_longconst Int64.zero) + | bool_case_l => Ebinop (Ocmplu Cne) e (make_longconst Int64.zero) | bool_default => e (**r should not happen *) end. @@ -188,12 +190,11 @@ Definition make_boolean (e: expr) (ty: type) := Definition make_notbool (e: expr) (ty: type) := match classify_bool ty with - | bool_case_i => OK (Ebinop (Ocmp Ceq) e (make_intconst Int.zero)) + | bool_case_i => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero)) | bool_case_f => OK (Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero)) | bool_case_s => OK (Ebinop (Ocmpfs Ceq) e (make_singleconst Float32.zero)) - | bool_case_p => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero)) - | bool_case_l => OK (Ebinop (Ocmpl Ceq) e (make_longconst Int64.zero)) - | _ => Error (msg "Cshmgen.make_notbool") + | bool_case_l => OK (Ebinop (Ocmplu Ceq) e (make_longconst Int64.zero)) + | bool_default => Error (msg "Cshmgen.make_notbool") end. Definition make_neg (e: expr) (ty: type) := @@ -202,7 +203,7 @@ Definition make_neg (e: expr) (ty: type) := | neg_case_f => OK (Eunop Onegf e) | neg_case_s => OK (Eunop Onegfs e) | neg_case_l _ => OK (Eunop Onegl e) - | _ => Error (msg "Cshmgen.make_neg") + | neg_default => Error (msg "Cshmgen.make_neg") end. Definition make_absfloat (e: expr) (ty: type) := @@ -211,14 +212,14 @@ Definition make_absfloat (e: expr) (ty: type) := | neg_case_f => OK (Eunop Oabsf e) | neg_case_s => OK (Eunop Oabsf (make_floatofsingle e)) | neg_case_l sg => OK (Eunop Oabsf (make_floatoflong e sg)) - | _ => Error (msg "Cshmgen.make_absfloat") + | neg_default => Error (msg "Cshmgen.make_absfloat") end. Definition make_notint (e: expr) (ty: type) := match classify_notint ty with | notint_case_i _ => OK (Eunop Onotint e) | notint_case_l _ => OK (Eunop Onotl e) - | _ => Error (msg "Cshmgen.make_notint") + | notint_default => Error (msg "Cshmgen.make_notint") end. (** Binary operators *) @@ -241,40 +242,52 @@ Definition make_binarith (iop iopu fop sop lop lopu: binary_operation) Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with - | add_case_pi ty => - do sz <- sizeof ce ty; - let n := make_intconst (Int.repr sz) in - OK (Ebinop Oadd e1 (Ebinop Omul n e2)) - | add_case_ip ty => + | add_case_pi ty si => do sz <- sizeof ce ty; - let n := make_intconst (Int.repr sz) in - OK (Ebinop Oadd e2 (Ebinop Omul n e1)) + if Archi.ptr64 then + let n := make_longconst (Int64.repr sz) in + OK (Ebinop Oaddl e1 (Ebinop Omull n (make_longofint e2 si))) + else + let n := make_intconst (Int.repr sz) in + OK (Ebinop Oadd e1 (Ebinop Omul n e2)) | add_case_pl ty => do sz <- sizeof ce ty; - let n := make_intconst (Int.repr sz) in - OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))) - | add_case_lp ty => - do sz <- sizeof ce ty; - let n := make_intconst (Int.repr sz) in - OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1))) + if Archi.ptr64 then + let n := make_longconst (Int64.repr sz) in + OK (Ebinop Oaddl e1 (Ebinop Omull n e2)) + else + let n := make_intconst (Int.repr sz) in + OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))) | add_default => make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2 end. Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_sub ty1 ty2 with - | sub_case_pi ty => + | sub_case_pi ty si => do sz <- sizeof ce ty; - let n := make_intconst (Int.repr sz) in - OK (Ebinop Osub e1 (Ebinop Omul n e2)) + if Archi.ptr64 then + let n := make_longconst (Int64.repr sz) in + OK (Ebinop Osubl e1 (Ebinop Omull n (make_longofint e2 si))) + else + let n := make_intconst (Int.repr sz) in + OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => do sz <- sizeof ce ty; - let n := make_intconst (Int.repr sz) in - OK (Ebinop Odiv (Ebinop Osub e1 e2) n) + if Archi.ptr64 then + let n := make_longconst (Int64.repr sz) in + OK (Ebinop Odivl (Ebinop Osubl e1 e2) n) + else + let n := make_intconst (Int.repr sz) in + OK (Ebinop Odiv (Ebinop Osub e1 e2) n) | sub_case_pl ty => do sz <- sizeof ce ty; - let n := make_intconst (Int.repr sz) in - OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2))) + if Archi.ptr64 then + let n := make_longconst (Int64.repr sz) in + OK (Ebinop Osubl e1 (Ebinop Omull n e2)) + else + let n := make_intconst (Int.repr sz) in + OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2))) | sub_default => make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2 end. @@ -333,11 +346,20 @@ Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) := | shift_default => Error (msg "Cshmgen.make_shr") end. +Definition make_cmp_ptr (c: comparison) (e1 e2: expr) := + Ebinop (if Archi.ptr64 then Ocmplu c else Ocmpu c) e1 e2. + Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_cmp ty1 ty2 with - | cmp_case_pp => OK (Ebinop (Ocmpu c) e1 e2) - | cmp_case_pl => OK (Ebinop (Ocmpu c) e1 (Eunop Ointoflong e2)) - | cmp_case_lp => OK (Ebinop (Ocmpu c) (Eunop Ointoflong e1) e2) + | cmp_case_pp => OK (make_cmp_ptr c e1 e2) + | cmp_case_pi si => + OK (make_cmp_ptr c e1 (if Archi.ptr64 then make_longofint e2 si else e2)) + | cmp_case_ip si => + OK (make_cmp_ptr c (if Archi.ptr64 then make_longofint e1 si else e1) e2) + | cmp_case_pl => + OK (make_cmp_ptr c e1 (if Archi.ptr64 then e2 else Eunop Ointoflong e2)) + | cmp_case_lp => + OK (make_cmp_ptr c (if Archi.ptr64 then e1 else Eunop Ointoflong e1) e2) | cmp_default => make_binarith (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpfs c) (Ocmpl c) (Ocmplu c) @@ -421,7 +443,9 @@ Definition make_field_access (ce: composite_env) (ty: type) (f: ident) (a: expr) Error (MSG "Undefined struct " :: CTX id :: nil) | Some co => do ofs <- field_offset ce f (co_members co); - OK (Ebinop Oadd a (make_intconst (Int.repr ofs))) + OK (if Archi.ptr64 + then Ebinop Oaddl a (make_longconst (Int64.repr ofs)) + else Ebinop Oadd a (make_intconst (Int.repr ofs))) end | Tunion id _ => OK a @@ -469,9 +493,9 @@ Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr do addr <- make_field_access ce (typeof b) i tb; make_load addr ty | Clight.Esizeof ty' ty => - do sz <- sizeof ce ty'; OK(make_intconst (Int.repr sz)) + do sz <- sizeof ce ty'; OK(make_ptrofsconst sz) | Clight.Ealignof ty' ty => - do al <- alignof ce ty'; OK(make_intconst (Int.repr al)) + do al <- alignof ce ty'; OK(make_ptrofsconst al) end (** [transl_lvalue a] returns the Csharpminor code that evaluates diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 8bc97b99..3a35b87e 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -245,6 +245,19 @@ Proof. intros. unfold make_floatconst. econstructor. reflexivity. Qed. +Lemma make_ptrofsconst_correct: + forall n e le m, + eval_expr ge e le m (make_ptrofsconst n) (Vptrofs (Ptrofs.repr n)). +Proof. + intros. unfold Vptrofs, make_ptrofsconst. destruct Archi.ptr64 eqn:SF. +- replace (Ptrofs.to_int64 (Ptrofs.repr n)) with (Int64.repr n). + apply make_longconst_correct. + symmetry; auto with ptrofs. +- replace (Ptrofs.to_int (Ptrofs.repr n)) with (Int.repr n). + apply make_intconst_correct. + symmetry; auto with ptrofs. +Qed. + Lemma make_singleoffloat_correct: forall a n e le m, eval_expr ge e le m a (Vfloat n) -> @@ -276,38 +289,62 @@ Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correc Hint Constructors eval_expr eval_exprlist: cshm. Hint Extern 2 (@eq trace _ _) => traceEq: cshm. -Lemma make_cmp_ne_zero_correct: +Lemma make_cmpu_ne_zero_correct: forall e le m a n, eval_expr ge e le m a (Vint n) -> - eval_expr ge e le m (make_cmp_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)). + eval_expr ge e le m (make_cmpu_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)). Proof. intros. - assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmp Cne) a (make_intconst Int.zero)) + assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) (Vint (if Int.eq n Int.zero then Int.zero else Int.one))). - econstructor; eauto with cshm. simpl. unfold Val.cmp, Val.cmp_bool. - unfold Int.cmp. destruct (Int.eq n Int.zero); auto. + { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + unfold Int.cmpu. destruct (Int.eq n Int.zero); auto. } assert (CMP: forall ob, Val.of_optbool ob = Vint n -> n = (if Int.eq n Int.zero then Int.zero else Int.one)). - intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2. + { intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2. rewrite Int.eq_false. auto. apply Int.one_not_zero. - rewrite Int.eq_true. auto. + rewrite Int.eq_true. auto. } destruct a; simpl; auto. destruct b; auto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. - simpl in H6. inv H6. unfold Val.cmp in H0. eauto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. - simpl in H6. inv H6. unfold Val.cmp in H0. eauto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. - simpl in H6. inv H6. unfold Val.cmp in H0. eauto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. - simpl in H6. unfold Val.cmpfs in H6. - destruct (Val.cmpfs_bool c v1 v2) as [[]|]; inv H6; reflexivity. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. eauto. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. eauto. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. eauto. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. eauto. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmpl in H6. destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmplu in H6. - destruct (Val.cmplu_bool c v1 v2) as [[]|]; inv H6; reflexivity. + destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [[]|]; inv H6; reflexivity. +Qed. + +Lemma make_cmpu_ne_zero_correct_ptr: + forall e le m a b i, + eval_expr ge e le m a (Vptr b i) -> + Archi.ptr64 = false -> + Mem.weak_valid_pointer m b (Ptrofs.unsigned i) = true -> + eval_expr ge e le m (make_cmpu_ne_zero a) Vone. +Proof. + intros. + assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) Vone). + { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + unfold Mem.weak_valid_pointer in H1. rewrite H0, H1. + rewrite Int.eq_true; auto. } + assert (OF_OPTBOOL: forall ob, Some (Val.of_optbool ob) <> Some (Vptr b i)). + { intros. destruct ob as [[]|]; discriminate. } + assert (OF_BOOL: forall ob, option_map Val.of_bool ob <> Some (Vptr b i)). + { intros. destruct ob as [[]|]; discriminate. } + destruct a; simpl; auto. destruct b0; auto. +- inv H; eelim OF_OPTBOOL; eauto. +- inv H; eelim OF_OPTBOOL; eauto. +- inv H; eelim OF_OPTBOOL; eauto. +- inv H; eelim OF_OPTBOOL; eauto. +- inv H; eelim OF_BOOL; eauto. +- inv H; eelim OF_BOOL; eauto. Qed. Lemma make_cast_int_correct: @@ -320,10 +357,27 @@ Proof. destruct si; eauto with cshm. destruct si; eauto with cshm. auto. - apply make_cmp_ne_zero_correct; auto. + apply make_cmpu_ne_zero_correct; auto. Qed. -Hint Resolve make_cast_int_correct: cshm. +Lemma make_longofint_correct: + forall e le m a n si, + eval_expr ge e le m a (Vint n) -> + eval_expr ge e le m (make_longofint a si) (Vlong (cast_int_long si n)). +Proof. + intros. unfold make_longofint, cast_int_long. destruct si; eauto with cshm. +Qed. + +Hint Resolve make_cast_int_correct make_longofint_correct: cshm. + +Ltac InvEval := + match goal with + | [ H: None = Some _ |- _ ] => discriminate + | [ H: Some _ = Some _ |- _ ] => inv H; InvEval + | [ H: match ?x with Some _ => _ | None => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval + | [ H: match ?x with true => _ | false => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval + | _ => idtac + end. Lemma make_cast_correct: forall e le m a b v ty1 ty2 v', @@ -333,59 +387,51 @@ Lemma make_cast_correct: eval_expr ge e le m b v'. Proof. intros. unfold make_cast, sem_cast in *; - destruct (classify_cast ty1 ty2); inv H; destruct v; inv H1; eauto with cshm. - (* single -> int *) + destruct (classify_cast ty1 ty2); inv H; destruct v; InvEval; eauto with cshm. +- (* single -> int *) unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm. - (* float -> int *) - destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2. +- (* float -> int *) apply make_cast_int_correct. - unfold cast_float_int in E. unfold make_intoffloat. - destruct si2; econstructor; eauto; simpl; rewrite E; auto. - (* single -> int *) - destruct (cast_single_int si2 f) as [i|] eqn:E; inv H2. + unfold cast_float_int in Heqo. unfold make_intoffloat. + destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto. +- (* single -> int *) apply make_cast_int_correct. - unfold cast_single_int in E. unfold make_intofsingle. - destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto. - (* long -> int *) - unfold make_longofint, cast_int_long. destruct si1; eauto with cshm. - (* long -> float *) + unfold cast_single_int in Heqo. unfold make_intofsingle. + destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto. +- (* long -> float *) unfold make_floatoflong, cast_long_float. destruct si1; eauto with cshm. - (* long -> single *) +- (* long -> single *) unfold make_singleoflong, cast_long_single. destruct si1; eauto with cshm. - (* float -> long *) - destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2. - unfold cast_float_long in E. unfold make_longoffloat. - destruct si2; econstructor; eauto; simpl; rewrite E; auto. - (* single -> long *) - destruct (cast_single_long si2 f) as [i|] eqn:E; inv H2. - unfold cast_single_long in E. unfold make_longofsingle. - destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto. - (* float -> bool *) +- (* float -> long *) + unfold cast_float_long in Heqo. unfold make_longoffloat. + destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto. +- (* single -> long *) + unfold cast_single_long in Heqo. unfold make_longofsingle. + destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto. +- (* int -> bool *) + apply make_cmpu_ne_zero_correct; auto. +- (* pointer (32 bits) -> bool *) + eapply make_cmpu_ne_zero_correct_ptr; eauto. +- (* long -> bool *) + econstructor; eauto with cshm. + simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu. + destruct (Int64.eq i Int64.zero); auto. +- (* pointer (64 bits) -> bool *) + econstructor; eauto with cshm. + simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in Heqb1. + rewrite Heqb0, Heqb1. rewrite Int64.eq_true. reflexivity. +- (* float -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f Float.zero); auto. - (* single -> bool *) +- (* single -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f Float32.zero); auto. - (* long -> bool *) - econstructor; eauto with cshm. - simpl. unfold Val.cmpl, Val.cmpl_bool, Int64.cmp. - destruct (Int64.eq i Int64.zero); auto. - (* int -> bool *) - econstructor; eauto with cshm. - simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. - destruct (Int.eq i Int.zero); auto. - (* pointer -> bool *) - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:VALID; inv H2. - econstructor; eauto with cshm. - simpl. unfold Val.cmpu. simpl. rewrite Int.eq_true. - unfold Mem.weak_valid_pointer in VALID; rewrite VALID. - auto. - (* struct *) - destruct (ident_eq id1 id2); inv H2; auto. - (* union *) - destruct (ident_eq id1 id2); inv H2; auto. +- (* struct *) + destruct (ident_eq id1 id2); inv H1; auto. +- (* union *) + destruct (ident_eq id1 id2); inv H1; auto. Qed. Lemma make_boolean_correct: @@ -397,29 +443,28 @@ Lemma make_boolean_correct: /\ Val.bool_of_val vb b. Proof. intros. unfold make_boolean. unfold bool_val in H0. - destruct (classify_bool ty); destruct v; inv H0. -(* int *) - econstructor; split. apply make_cmp_ne_zero_correct with (n := i); auto. + destruct (classify_bool ty); destruct v; InvEval. +- (* int *) + econstructor; split. apply make_cmpu_ne_zero_correct with (n := i); auto. destruct (Int.eq i Int.zero); simpl; constructor. -(* float *) +- (* ptr 32 bits *) + exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor. +- (* long *) + econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmplu. simpl. eauto. + destruct (Int64.eq i Int64.zero); simpl; constructor. +- (* ptr 64 bits *) + exists Vone; split. + econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. + unfold Mem.weak_valid_pointer in Heqb0. rewrite Heqb0, Heqb1, Int64.eq_true. reflexivity. + constructor. +- (* float *) econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq. destruct (Float.cmp Cne f Float.zero); constructor. -(* single *) +- (* single *) econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq. destruct (Float32.cmp Cne f Float32.zero); constructor. -(* pointer *) - econstructor; split. econstructor; eauto with cshm. simpl. eauto. - unfold Val.cmpu, Val.cmpu_bool. simpl. - destruct (Int.eq i Int.zero); simpl; constructor. - econstructor; split. econstructor; eauto with cshm. simpl. eauto. - destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i)) eqn:V; inv H2. - unfold Val.cmpu, Val.cmpu_bool. simpl. - unfold Mem.weak_valid_pointer in V; rewrite V. constructor. -(* long *) - econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. - destruct (Int64.eq i Int64.zero); simpl; constructor. Qed. Lemma make_neg_correct: @@ -454,11 +499,24 @@ Lemma make_notbool_correct: eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. - unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1; - destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:V; inv H0. - econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. - unfold Mem.weak_valid_pointer in V; rewrite V. auto. + unfold sem_notbool, bool_val, make_notbool; intros until m; intros SEM MAKE EV1. + destruct (classify_bool tya); inv MAKE; destruct va; simpl in SEM; InvEval. +- econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. + destruct (Int.eq i Int.zero); auto. +- destruct Archi.ptr64 eqn:SF; inv SEM. + destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0. + econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int.eq_true. auto. +- econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu. + destruct (Int64.eq i Int64.zero); auto. +- destruct Archi.ptr64 eqn:SF; inv SEM. + destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0. + econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. + unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int64.eq_true. auto. +- econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. + destruct (Float.cmp Ceq f Float.zero); auto. +- econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. + destruct (Float32.cmp Ceq f Float32.zero); auto. Qed. Lemma make_notint_correct: @@ -561,19 +619,66 @@ End MAKE_BIN. Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm. +(* +Lemma eqm_ptrofs_of_int: + forall si i, + Ptrofs.eqm (Ptrofs.unsigned (ptrofs_of_int si i)) + (match si with Signed => Int.signed i | Unsigned => Int.unsigned i end). +Proof. + intros. unfold ptrofs_of_int. destruct si; apply Ptrofs.eqm_sym; apply Ptrofs.eqm_unsigned_repr. +Qed. + +Lemma ptrofs_mul_32: + forall si n i, + Archi.ptr64 = false -> + Ptrofs.of_int (Int.mul (Int.repr n) i) = Ptrofs.mul (Ptrofs.repr n) (ptrofs_of_int si i). +Proof. + intros. apply Ptrofs.eqm_samerepr. + eapply Ptrofs.eqm_trans; [ | apply Ptrofs.eqm_mult ]. + apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + apply Ptrofs.eqm_unsigned_repr_r. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + apply Ptrofs.eqm_sym. eapply Ptrofs.eqm_trans. apply eqm_ptrofs_of_int. + apply -> Val.ptrofs_eqm_32; auto. destruct si. apply Int.eqm_signed_unsigned. apply Int.eqm_refl. +Qed. + +Lemma ptrofs_mul_32_64: + forall n i, + Archi.ptr64 = false -> + Ptrofs.of_int (Int.mul (Int.repr n) (Int64.loword i)) = Ptrofs.mul (Ptrofs.repr n) (Ptrofs.of_int64 i). +Proof. + intros. apply Ptrofs.eqm_samerepr. + eapply Ptrofs.eqm_trans; [ | apply Ptrofs.eqm_mult ]. + apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + apply Ptrofs.eqm_unsigned_repr_r. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + unfold Ptrofs.of_int64. apply Ptrofs.eqm_unsigned_repr_r. + unfold Int64.loword. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. +Qed. +*) + Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)). Proof. red; unfold make_add, sem_add; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_add tya tyb); try (monadInv MAKE). -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. + simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)). + { destruct si; simpl; apply Ptrofs.agree64_repr; auto. } + auto with ptrofs. ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs). + auto with ptrofs. +- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. + simpl. rewrite SF. do 3 f_equal. auto with ptrofs. ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto). + auto with ptrofs. - eapply make_binarith_correct; eauto; intros; auto. Qed. @@ -582,25 +687,61 @@ Proof. red; unfold make_sub, sem_sub; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_sub tya tyb); try (monadInv MAKE). -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM. - destruct (eq_block b0 b1); try discriminate. +- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. + simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)). + { destruct si; simpl; apply Ptrofs.agree64_repr; auto. } + auto with ptrofs. ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs). + auto with ptrofs. +- rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ. set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *. + destruct va; InvEval; destruct vb; InvEval. + destruct (eq_block b0 b1); try discriminate. destruct (zlt 0 sz); try discriminate. - destruct (zle sz Int.max_signed); simpl in H0; inv H0. + destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM. + assert (E1: Ptrofs.signed (Ptrofs.repr sz) = sz). + { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; omega. } + destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c. ++ assert (E: Int64.signed (Int64.repr sz) = sz). + { apply Int64.signed_repr. + replace Int64.max_signed with Ptrofs.max_signed. + generalize Int64.min_signed_neg; omega. + unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. } econstructor; eauto with cshm. - rewrite dec_eq_true; simpl. - assert (E: Int.signed (Int.repr sz) = sz). - { apply Int.signed_repr. generalize Int.min_signed_neg; omega. } + rewrite SF, dec_eq_true. simpl. + predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero. + rewrite H in E; rewrite Int64.signed_zero in E; omegaContradiction. + predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone. + rewrite H0 in E; rewrite Int64.signed_mone in E; omegaContradiction. + rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. do 2 f_equal. + symmetry. auto with ptrofs. ++ assert (E: Int.signed (Int.repr sz) = sz). + { apply Int.signed_repr. + replace Int.max_signed with Ptrofs.max_signed. + generalize Int.min_signed_neg; omega. + unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity. + } + econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl. predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero. rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction. predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone. rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction. - rewrite andb_false_r; auto. -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. + rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. do 2 f_equal. + symmetry. auto with ptrofs. +- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. + simpl. rewrite SF. do 3 f_equal. + auto with ptrofs. ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto). + auto with ptrofs. - eapply make_binarith_correct; eauto; intros; auto. Qed. @@ -716,25 +857,61 @@ Proof. unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto. Qed. +Lemma make_cmp_ptr_correct: + forall cmp e le m a va b vb v, + cmp_ptr m cmp va vb = Some v -> + eval_expr ge e le m a va -> + eval_expr ge e le m b vb -> + eval_expr ge e le m (make_cmp_ptr cmp a b) v. +Proof. + unfold cmp_ptr, make_cmp_ptr; intros. + destruct Archi.ptr64. +- econstructor; eauto. +- econstructor; eauto. simpl. unfold Val.cmpu. + destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bo|]; inv H. auto. +Qed. + +Remark make_ptrofs_of_int_correct: + forall e le m a i si, + eval_expr ge e le m a (Vint i) -> + eval_expr ge e le m (if Archi.ptr64 then make_longofint a si else a) (Vptrofs (ptrofs_of_int si i)). +Proof. + intros. unfold Vptrofs, ptrofs_of_int. destruct Archi.ptr64 eqn:SF. +- unfold make_longofint. destruct si. ++ replace (Ptrofs.to_int64 (Ptrofs.of_ints i)) with (Int64.repr (Int.signed i)). + eauto with cshm. + apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. ++ replace (Ptrofs.to_int64 (Ptrofs.of_intu i)) with (Int64.repr (Int.unsigned i)). + eauto with cshm. + apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. +- destruct si. ++ replace (Ptrofs.to_int (Ptrofs.of_ints i)) with i. auto. + symmetry. auto with ptrofs. ++ replace (Ptrofs.to_int (Ptrofs.of_intu i)) with i. auto. + symmetry. auto with ptrofs. +Qed. + +Remark make_ptrofs_of_int64_correct: + forall e le m a i, + eval_expr ge e le m a (Vlong i) -> + eval_expr ge e le m (if Archi.ptr64 then a else Eunop Ointoflong a) (Vptrofs (Ptrofs.of_int64 i)). +Proof. + intros. unfold Vptrofs. destruct Archi.ptr64 eqn:SF. +- replace (Ptrofs.to_int64 (Ptrofs.of_int64 i)) with i. auto. + symmetry. auto with ptrofs. +- econstructor; eauto. simpl. do 2 f_equal. + apply Int.eqm_samerepr. rewrite Ptrofs.eqm32 by auto. apply Ptrofs.eqm_unsigned_repr. +Qed. + Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp). Proof. red; unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_cmp tya tyb). -- inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; - simpl in SEM; inv SEM. - econstructor; eauto. simpl. unfold Val.cmpu. rewrite E. auto. -- inv MAKE. destruct vb; try discriminate. - set (vb := Vint (Int.repr (Int64.unsigned i))) in *. - destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; - simpl in SEM; inv SEM. - econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with vb. - unfold Val.cmpu. rewrite E. auto. -- inv MAKE. destruct va; try discriminate. - set (va := Vint (Int.repr (Int64.unsigned i))) in *. - destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; - simpl in SEM; inv SEM. - econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with va. - unfold Val.cmpu. rewrite E. auto. +- inv MAKE. eapply make_cmp_ptr_correct; eauto. +- inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct. +- inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct. +- inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct. +- inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct. - eapply make_binarith_correct; eauto; intros; auto. Qed. @@ -1042,49 +1219,53 @@ Lemma transl_expr_lvalue_correct: Csharpminor.eval_expr tge te le m ta (Vptr b ofs)). Proof. apply eval_expr_lvalue_ind; intros; try (monadInv TR). -(* const int *) +- (* const int *) apply make_intconst_correct. -(* const float *) +- (* const float *) apply make_floatconst_correct. -(* const single *) +- (* const single *) apply make_singleconst_correct. -(* const long *) +- (* const long *) apply make_longconst_correct. -(* temp var *) +- (* temp var *) constructor; auto. -(* addrof *) +- (* addrof *) simpl in TR. auto. -(* unop *) +- (* unop *) eapply transl_unop_correct; eauto. -(* binop *) +- (* binop *) eapply transl_binop_correct; eauto. -(* cast *) +- (* cast *) eapply make_cast_correct; eauto. -(* sizeof *) - rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_intconst_correct. -(* alignof *) - rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_intconst_correct. -(* rvalue out of lvalue *) +- (* sizeof *) + rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct. +- (* alignof *) + rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct. +- (* rvalue out of lvalue *) exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]]. eapply make_load_correct; eauto. -(* var local *) +- (* var local *) exploit (me_local _ _ MENV); eauto. intros EQ. econstructor. eapply eval_var_addr_local. eauto. -(* var global *) +- (* var global *) econstructor. eapply eval_var_addr_global. eapply match_env_globals; eauto. rewrite symbols_preserved. auto. -(* deref *) +- (* deref *) simpl in TR. eauto. -(* field struct *) +- (* field struct *) unfold make_field_access in EQ0. rewrite H1 in EQ0. destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; monadInv EQ0. exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B]. - rewrite <- B in EQ1. - eapply eval_Ebinop; eauto. - apply make_intconst_correct. - simpl. unfold ge in *; simpl in *. congruence. -(* field union *) + rewrite <- B in EQ1. + assert (x0 = delta) by (unfold ge in *; simpl in *; congruence). + subst x0. + destruct Archi.ptr64 eqn:SF. ++ eapply eval_Ebinop; eauto using make_longconst_correct. + simpl. rewrite SF. do 3 f_equal. auto with ptrofs. ++ eapply eval_Ebinop; eauto using make_intconst_correct. + simpl. rewrite SF. do 3 f_equal. auto with ptrofs. +- (* field union *) unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0. auto. Qed. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 6b2924e4..2f731068 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -84,16 +84,16 @@ Section SIMPLE_EXPRS. Variable e: env. Variable m: mem. -Inductive eval_simple_lvalue: expr -> block -> int -> Prop := +Inductive eval_simple_lvalue: expr -> block -> ptrofs -> Prop := | esl_loc: forall b ofs ty, eval_simple_lvalue (Eloc b ofs ty) b ofs | esl_var_local: forall x ty b, e!x = Some(b, ty) -> - eval_simple_lvalue (Evar x ty) b Int.zero + eval_simple_lvalue (Evar x ty) b Ptrofs.zero | esl_var_global: forall x ty b, e!x = None -> Genv.find_symbol ge x = Some b -> - eval_simple_lvalue (Evar x ty) b Int.zero + eval_simple_lvalue (Evar x ty) b Ptrofs.zero | esl_deref: forall r ty b ofs, eval_simple_rvalue r (Vptr b ofs) -> eval_simple_lvalue (Ederef r ty) b ofs @@ -102,7 +102,7 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop := typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta -> - eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta)) + eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta)) | esl_field_union: forall r f ty b ofs id co a, eval_simple_rvalue r (Vptr b ofs) -> typeof r = Tunion id a -> @@ -133,9 +133,9 @@ with eval_simple_rvalue: expr -> val -> Prop := sem_cast v1 (typeof r1) ty m = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, - eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) + eval_simple_rvalue (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1))) | esr_alignof: forall ty1 ty, - eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))). + eval_simple_rvalue (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1))). Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop := | esrl_nil: @@ -813,13 +813,13 @@ Ltac StepR REC C' a := exists v; constructor. (* var *) exploit safe_inv; eauto; simpl. intros [b A]. - exists b; exists Int.zero. + exists b; exists Ptrofs.zero. intuition. apply esl_var_local; auto. apply esl_var_global; auto. (* field *) StepR IHa (fun x => C(Efield x f0 ty)) a. exploit safe_inv. eexact SAFE0. eauto. simpl. intros [b [ofs [EQ TY]]]. subst v. destruct (typeof a) eqn:?; try contradiction. - destruct TY as (co & delta & CE & OFS). exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto. + destruct TY as (co & delta & CE & OFS). exists b; exists (Ptrofs.add ofs (Ptrofs.repr delta)); econstructor; eauto. destruct TY as (co & CE). exists b; exists ofs; econstructor; eauto. (* valof *) destruct (andb_prop _ _ S) as [S1 S2]. clear S. rewrite negb_true_iff in S2. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index fd7a6b96..914328be 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -55,7 +55,7 @@ Inductive expr : Type := (**r function call [r1(rargs)] *) | Ebuiltin (ef: external_function) (tyargs: typelist) (rargs: exprlist) (ty: type) (**r builtin function call *) - | Eloc (b: block) (ofs: int) (ty: type) + | Eloc (b: block) (ofs: ptrofs) (ty: type) (**r memory location, result of evaluating a l-value *) | Eparen (r: expr) (tycast: type) (ty: type) (**r marked subexpression *) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 9faa6d40..0794743d 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -78,15 +78,19 @@ with typelist : Type := | Tnil: typelist | Tcons: type -> typelist -> typelist. +Lemma intsize_eq: forall (s1 s2: intsize), {s1=s2} + {s1<>s2}. +Proof. + decide equality. +Defined. + Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2} with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}. Proof. - assert (forall (x y: intsize), {x=y} + {x<>y}) by decide equality. assert (forall (x y: signedness), {x=y} + {x<>y}) by decide equality. assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality. assert (forall (x y: attr), {x=y} + {x<>y}). { decide equality. decide equality. apply N.eq_dec. apply bool_dec. } - generalize ident_eq zeq bool_dec ident_eq; intros. + generalize ident_eq zeq bool_dec ident_eq intsize_eq; intros. decide equality. decide equality. decide equality. @@ -272,7 +276,7 @@ Fixpoint alignof (env: composite_env) (t: type) : Z := | Tlong _ _ => Archi.align_int64 | Tfloat F32 _ => 4 | Tfloat F64 _ => Archi.align_float64 - | Tpointer _ _ => 4 + | Tpointer _ _ => if Archi.ptr64 then 8 else 4 | Tarray t' _ _ => alignof env t' | Tfunction _ _ _ => 1 | Tstruct id _ | Tunion id _ => @@ -299,11 +303,11 @@ Proof. exists 1%nat; auto. exists 2%nat; auto. exists 0%nat; auto. - (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity). + unfold Archi.align_int64. destruct Archi.ptr64; ((exists 2%nat; reflexivity) || (exists 3%nat; reflexivity)). destruct f. exists 2%nat; auto. - (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity). - exists 2%nat; auto. + unfold Archi.align_float64. destruct Archi.ptr64; ((exists 2%nat; reflexivity) || (exists 3%nat; reflexivity)). + exists (if Archi.ptr64 then 3%nat else 2%nat); destruct Archi.ptr64; auto. apply IHt. exists 0%nat; auto. destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto. @@ -335,7 +339,7 @@ Fixpoint sizeof (env: composite_env) (t: type) : Z := | Tlong _ _ => 8 | Tfloat F32 _ => 4 | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 + | Tpointer _ _ => if Archi.ptr64 then 8 else 4 | Tarray t' n _ => sizeof env t' * Z.max 0 n | Tfunction _ _ _ => 1 | Tstruct id _ | Tunion id _ => @@ -348,6 +352,7 @@ Proof. induction t; simpl; try omega. destruct i; omega. destruct f; omega. + destruct Archi.ptr64; omega. change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega. destruct (env!i). apply co_sizeof_pos. omega. destruct (env!i). apply co_sizeof_pos. omega. @@ -370,8 +375,8 @@ Proof. induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. - apply Zdivide_refl. - destruct i; apply Zdivide_refl. -- exists (8 / Archi.align_int64); reflexivity. -- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. +- exists (8 / Archi.align_int64). unfold Archi.align_int64; destruct Archi.ptr64; reflexivity. +- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity. - apply Zdivide_refl. - apply Z.divide_mul_l; auto. - apply Zdivide_refl. @@ -576,7 +581,7 @@ Definition access_mode (ty: type) : mode := | Tfloat F32 _ => By_value Mfloat32 | Tfloat F64 _ => By_value Mfloat64 | Tvoid => By_nothing - | Tpointer _ _ => By_value Mint32 + | Tpointer _ _ => By_value Mptr | Tarray _ _ _ => By_reference | Tfunction _ _ _ => By_reference | Tstruct _ _ => By_copy @@ -609,7 +614,7 @@ Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z := | Tlong _ _ => 8 | Tfloat F32 _ => 4 | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 + | Tpointer _ _ => if Archi.ptr64 then 8 else 4 | Tarray t' _ _ => alignof_blockcopy env t' | Tfunction _ _ _ => 1 | Tstruct id _ | Tunion id _ => @@ -633,9 +638,14 @@ Proof. rewrite two_power_nat_two_p. rewrite ! inj_S. change 8 with (two_p 3). apply two_p_monotone. omega. } - induction ty; simpl; auto. + induction ty; simpl. + auto. destruct i; auto. + auto. destruct f; auto. + destruct Archi.ptr64; auto. + apply IHty. + auto. destruct (env!i); auto. destruct (env!i); auto. Qed. @@ -714,20 +724,16 @@ Fixpoint type_of_params (params: list (ident * type)) : typelist := Definition typ_of_type (t: type) : AST.typ := match t with - | Tfloat F32 _ => AST.Tsingle - | Tfloat _ _ => AST.Tfloat + | Tvoid => AST.Tint + | Tint _ _ _ => AST.Tint | Tlong _ _ => AST.Tlong - | _ => AST.Tint + | Tfloat F32 _ => AST.Tsingle + | Tfloat F64 _ => AST.Tfloat + | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr end. Definition opttyp_of_type (t: type) : option AST.typ := - match t with - | Tvoid => None - | Tfloat F32 _ => Some AST.Tsingle - | Tfloat _ _ => Some AST.Tfloat - | Tlong _ _ => Some AST.Tlong - | _ => Some AST.Tint - end. + if type_eq t Tvoid then None else Some (typ_of_type t). Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := match tl with diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 440e4e84..521ae519 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -26,6 +26,12 @@ Local Open Scope error_monad_scope. Definition strict := false. Opaque strict. +Definition size_t : type := + if Archi.ptr64 then Tlong Unsigned noattr else Tint I32 Unsigned noattr. + +Definition ptrdiff_t : type := + if Archi.ptr64 then Tlong Signed noattr else Tint I32 Signed noattr. + (** * Operations over types *) (** The type of a member of a composite (struct or union). @@ -107,20 +113,20 @@ Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type := match op with | Oadd => match classify_add ty1 ty2 with - | add_case_pi ty | add_case_ip ty - | add_case_pl ty | add_case_lp ty => OK (Tpointer ty noattr) + | add_case_pi ty _ (*| add_case_ip ty*) + | add_case_pl ty (*| add_case_lp ty*) => OK (Tpointer ty noattr) | add_default => binarith_type ty1 ty2 "operator +" end | Osub => match classify_sub ty1 ty2 with - | sub_case_pi ty | sub_case_pl ty => OK (Tpointer ty noattr) + | sub_case_pi ty _ | sub_case_pl ty => OK (Tpointer ty noattr) (* | sub_case_pp ty1 ty2 => if type_eq (remove_attributes ty1) (remove_attributes ty2) then OK (Tint I32 Signed noattr) else Error (msg "operator - : incompatible pointer types") *) - | sub_case_pp ty => OK (Tint I32 Signed noattr) + | sub_case_pp ty => OK ptrdiff_t | sub_default => binarith_type ty1 ty2 "operator infix -" end | Omul => binarith_type ty1 ty2 "operator infix *" @@ -281,9 +287,13 @@ Inductive wt_val : val -> type -> Prop := wt_int n sz sg -> wt_val (Vint n) (Tint sz sg a) | wt_val_ptr_int: forall b ofs sg a, + Archi.ptr64 = false -> wt_val (Vptr b ofs) (Tint I32 sg a) | wt_val_long: forall n sg a, wt_val (Vlong n) (Tlong sg a) + | wt_val_ptr_long: forall b ofs sg a, + Archi.ptr64 = true -> + wt_val (Vptr b ofs) (Tlong sg a) | wt_val_float: forall f a, wt_val (Vfloat f) (Tfloat F64 a) | wt_val_single: forall f a, @@ -291,7 +301,11 @@ Inductive wt_val : val -> type -> Prop := | wt_val_pointer: forall b ofs ty a, wt_val (Vptr b ofs) (Tpointer ty a) | wt_val_int_pointer: forall n ty a, + Archi.ptr64 = false -> wt_val (Vint n) (Tpointer ty a) + | wt_val_long_pointer: forall n ty a, + Archi.ptr64 = true -> + wt_val (Vlong n) (Tpointer ty a) | wt_val_array: forall b ofs ty sz a, wt_val (Vptr b ofs) (Tarray ty sz a) | wt_val_function: forall b ofs tyargs tyres cc, @@ -359,9 +373,9 @@ Inductive wt_rvalue : expr -> Prop := wt_cast (typeof r2) ty -> wt_cast (typeof r3) ty -> wt_rvalue (Econdition r1 r2 r3 ty) | wt_Esizeof: forall ty, - wt_rvalue (Esizeof ty (Tint I32 Unsigned noattr)) + wt_rvalue (Esizeof ty size_t) | wt_Ealignof: forall ty, - wt_rvalue (Ealignof ty (Tint I32 Unsigned noattr)) + wt_rvalue (Ealignof ty size_t) | wt_Eassign: forall l r, wt_lvalue l -> wt_rvalue r -> wt_cast (typeof r) (typeof l) -> wt_rvalue (Eassign l r (typeof l)) @@ -522,11 +536,10 @@ Hint Extern 1 (wt_int _ _ _) => reflexivity: ty. Ltac DestructCases := match goal with - | [H: match match ?x with _ => _ end with _ => _ end = Some _ |- _ ] => destruct x; DestructCases - | [H: match match ?x with _ => _ end with _ => _ end = OK _ |- _ ] => destruct x; DestructCases - | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x; DestructCases - | [H: match ?x with _ => _ end = Some _ |- _ ] => destruct x; DestructCases - | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x; DestructCases + | [H: match match ?x with _ => _ end with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases + | [H: match match ?x with _ => _ end with _ => _ end = OK _ |- _ ] => destruct x eqn:?; DestructCases + | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x eqn:?; DestructCases + | [H: match ?x with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases | [H: Some _ = Some _ |- _ ] => inv H; DestructCases | [H: None = Some _ |- _ ] => discriminate | [H: OK _ = OK _ |- _ ] => inv H; DestructCases @@ -628,11 +641,14 @@ Definition econst_int (n: int) (sg: signedness) : expr := (Eval (Vint n) (Tint I32 sg noattr)). Definition econst_ptr_int (n: int) (ty: type) : expr := - (Eval (Vint n) (Tpointer ty noattr)). + (Eval (if Archi.ptr64 then Vlong (Int64.repr (Int.unsigned n)) else Vint n) (Tpointer ty noattr)). Definition econst_long (n: int64) (sg: signedness) : expr := (Eval (Vlong n) (Tlong sg noattr)). +Definition econst_ptr_long (n: int64) (ty: type) : expr := + (Eval (if Archi.ptr64 then Vlong n else Vint (Int64.loword n)) (Tpointer ty noattr)). + Definition econst_float (n: float) : expr := (Eval (Vfloat n) (Tfloat F64 noattr)). @@ -684,10 +700,10 @@ Definition econdition' (r1 r2 r3: expr) (ty: type) : res expr := OK (Econdition r1 r2 r3 ty). Definition esizeof (ty: type) : expr := - Esizeof ty (Tint I32 Unsigned noattr). + Esizeof ty size_t. Definition ealignof (ty: type) : expr := - Ealignof ty (Tint I32 Unsigned noattr). + Ealignof ty size_t. Definition eassign (l r: expr) : res expr := do x1 <- check_lval l; do x2 <- check_rval r; @@ -954,7 +970,9 @@ Lemma binarith_type_cast: binarith_type t1 t2 m = OK t -> wt_cast t1 t /\ wt_cast t2 t. Proof. unfold wt_cast, binarith_type, classify_binarith; intros; DestructCases; - simpl; split; try congruence. destruct f; congruence. + simpl; split; try congruence; + try (destruct Archi.ptr64; congruence). + destruct f0; congruence. Qed. Lemma typeconv_cast: @@ -969,6 +987,16 @@ Proof. destruct i; auto. Qed. +Lemma wt_cast_int: + forall i1 s1 a1 i2 s2 a2, wt_cast (Tint i1 s1 a1) (Tint i2 s2 a2). +Proof. + intros; red; simpl. + destruct Archi.ptr64; [ | destruct (Ctypes.intsize_eq i2 I32)]. +- destruct i2; congruence. +- subst i2; congruence. +- destruct i2; congruence. +Qed. + Lemma type_combine_cast: forall t1 t2 t, type_combine t1 t2 = OK t -> @@ -980,9 +1008,9 @@ Proof. unfold wt_cast; destruct t1; try discriminate; destruct t2; simpl in H; inv H. - simpl; split; congruence. - destruct (intsize_eq i i0 && signedness_eq s s0); inv H3. - simpl; destruct i; split; congruence. + split; apply wt_cast_int. - destruct (signedness_eq s s0); inv H3. - simpl; split; congruence. + simpl; split; try congruence; destruct Archi.ptr64; congruence. - destruct (floatsize_eq f f0); inv H3. simpl; destruct f0; split; congruence. - monadInv H3. simpl; split; congruence. @@ -1006,11 +1034,14 @@ Proof. destruct (typeconv t1) eqn:T1; try discriminate; destruct (typeconv t2) eqn:T2; inv H; eauto using D, binarith_type_cast. - split; apply typeconv_cast; unfold wt_cast. - rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. + rewrite T1; simpl; try congruence; destruct Archi.ptr64; congruence. + rewrite T2; simpl; try congruence; destruct Archi.ptr64; congruence. - split; apply typeconv_cast; unfold wt_cast. - rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. + rewrite T1; simpl; try congruence; destruct Archi.ptr64; congruence. + rewrite T2; simpl; try congruence; destruct Archi.ptr64; congruence. - split; apply typeconv_cast; unfold wt_cast. - rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. + rewrite T1; simpl; try congruence; destruct Archi.ptr64; congruence. + rewrite T2; simpl; try congruence; destruct Archi.ptr64; congruence. Qed. Section SOUNDNESS_CONSTRUCTORS. @@ -1063,7 +1094,7 @@ Qed. Lemma econst_ptr_int_sound: forall n ty, wt_expr ce e (econst_ptr_int n ty). Proof. - unfold econst_ptr_int; auto with ty. + unfold econst_ptr_int; intros. destruct Archi.ptr64 eqn:SF; auto with ty. Qed. Lemma econst_long_sound: @@ -1072,6 +1103,12 @@ Proof. unfold econst_long; auto with ty. Qed. +Lemma econst_ptr_long_sound: + forall n ty, wt_expr ce e (econst_ptr_long n ty). +Proof. + unfold econst_ptr_long; intros. destruct Archi.ptr64 eqn:SF; auto with ty. +Qed. + Lemma econst_float_sound: forall n, wt_expr ce e (econst_float n). Proof. @@ -1354,28 +1391,17 @@ Proof. - destruct (Int.eq n Int.zero); auto. Qed. -Hint Resolve pres_cast_int_int: ty. +Lemma wt_val_casted: + forall v ty, val_casted v ty -> wt_val v ty. +Proof. + induction 1; constructor; auto. +- rewrite <- H; apply pres_cast_int_int. +Qed. Lemma pres_sem_cast: forall m v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 m = Some v2 -> wt_val v2 ty2. Proof. - unfold sem_cast, classify_cast; induction 1; simpl; intros; DestructCases; auto with ty. -- constructor. apply (pres_cast_int_int I8 s). -- constructor. apply (pres_cast_int_int I16 s). -- destruct (Int.eq n Int.zero); auto with ty. -- constructor. apply (pres_cast_int_int I8 s). -- constructor. apply (pres_cast_int_int I16 s). -- destruct (Int64.eq n Int64.zero); auto with ty. -- constructor. apply (pres_cast_int_int I8 s). -- constructor. apply (pres_cast_int_int I16 s). -- destruct (Float.cmp Ceq f Float.zero); auto with ty. -- constructor. apply (pres_cast_int_int I8 s). -- constructor. apply (pres_cast_int_int I16 s). -- destruct (Float32.cmp Ceq f Float32.zero); auto with ty. -- constructor. reflexivity. -- destruct (Int.eq n Int.zero); auto with ty. -- constructor. reflexivity. -- constructor. reflexivity. + intros. apply wt_val_casted. eapply cast_val_is_casted; eauto. Qed. Lemma pres_sem_binarith: @@ -1459,6 +1485,8 @@ Proof with (try discriminate). - inv H; eauto. - DestructCases; eauto. - DestructCases; eauto. +- DestructCases; eauto. +- DestructCases; eauto. - unfold sem_binarith in H0. set (ty' := Cop.binarith_type (classify_binarith ty1 ty2)) in *. destruct (sem_cast v1 ty1 ty') as [v1'|]... @@ -1480,6 +1508,7 @@ Proof. eapply pres_sem_binarith; eauto; intros; exact I. - (* sub *) unfold sem_sub in SEM; DestructCases; auto with ty. + unfold ptrdiff_t, Vptrofs. destruct Archi.ptr64; auto with ty. eapply pres_sem_binarith; eauto; intros; exact I. - (* mul *) unfold sem_mul in SEM. eapply pres_sem_binarith; eauto; intros; exact I. @@ -1522,13 +1551,12 @@ Proof. intros until v; intros TY SEM WT1. destruct op; simpl in TY; simpl in SEM. - (* notbool *) - unfold sem_notbool in SEM; DestructCases. - destruct (Int.eq i Int.zero); constructor; auto with ty. - destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty. - destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty. - destruct (Int.eq i Int.zero); constructor; auto with ty. - constructor. constructor. - destruct (Int64.eq i Int64.zero); constructor; auto with ty. + unfold sem_notbool in SEM. + assert (A: ty = Tint I32 Signed noattr) by (destruct (classify_bool ty1); inv TY; auto). + assert (B: exists b, v = Val.of_bool b). + { destruct (bool_val v1 ty1 m); inv SEM. exists (negb b); auto. } + destruct B as [b B]. + rewrite A, B. destruct b; constructor; auto with ty. - (* notint *) unfold sem_notint in SEM; DestructCases; auto with ty. - (* neg *) @@ -1542,16 +1570,18 @@ Lemma wt_load_result: access_mode ty = By_value chunk -> wt_val (Val.load_result chunk v) ty. Proof. - intros until v; intros AC. destruct ty; simpl in AC; try discriminate. - destruct i; [destruct s|destruct s|idtac|idtac]; inv AC; simpl; destruct v; auto with ty. - constructor; red. apply Int.sign_ext_idem; omega. - constructor; red. apply Int.zero_ext_idem; omega. - constructor; red. apply Int.sign_ext_idem; omega. - constructor; red. apply Int.zero_ext_idem; omega. - constructor; red. apply Int.zero_ext_idem; omega. - inv AC; simpl; destruct v; auto with ty. - destruct f; inv AC; simpl; destruct v; auto with ty. - inv AC; simpl; destruct v; auto with ty. + unfold access_mode, Val.load_result. remember Archi.ptr64 as ptr64. + intros until v; intros AC. destruct ty; simpl in AC; try discriminate AC. +- destruct i; [destruct s|destruct s|idtac|idtac]; inv AC; simpl. + destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; omega. + destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega. + destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; omega. + destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega. + destruct Archi.ptr64 eqn:SF; destruct v; auto with ty. + destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega. +- inv AC. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty. +- destruct f; inv AC; destruct v; auto with ty. +- inv AC. unfold Mptr. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty. Qed. Lemma wt_decode_val: @@ -1560,19 +1590,26 @@ Lemma wt_decode_val: wt_val (decode_val chunk vl) ty. Proof. intros until vl; intros ACC. - destruct ty; simpl in ACC; try discriminate. -- destruct i; [destruct s|destruct s|idtac|idtac]; inv ACC; unfold decode_val; + assert (LR: forall v, wt_val (Val.load_result chunk v) ty) by (eauto using wt_load_result). + destruct ty; simpl in ACC; try discriminate. +- destruct i; [destruct s|destruct s|idtac|idtac]; inv ACC; unfold decode_val. destruct (proj_bytes vl); auto with ty. constructor; red. apply Int.sign_ext_idem; omega. + destruct (proj_bytes vl); auto with ty. constructor; red. apply Int.zero_ext_idem; omega. + destruct (proj_bytes vl); auto with ty. constructor; red. apply Int.sign_ext_idem; omega. + destruct (proj_bytes vl); auto with ty. constructor; red. apply Int.zero_ext_idem; omega. - apply wt_load_result. auto. + destruct (proj_bytes vl). auto with ty. destruct Archi.ptr64 eqn:SF; auto with ty. + destruct (proj_bytes vl); auto with ty. constructor; red. apply Int.zero_ext_idem; omega. -- inv ACC. unfold decode_val. destruct (proj_bytes vl); auto with ty. +- inv ACC. unfold decode_val. destruct (proj_bytes vl). auto with ty. + destruct Archi.ptr64 eqn:SF; auto with ty. - destruct f; inv ACC; unfold decode_val; destruct (proj_bytes vl); auto with ty. -- inv ACC. unfold decode_val. destruct (proj_bytes vl); auto with ty. - apply wt_load_result. auto. +- inv ACC. unfold decode_val. destruct (proj_bytes vl). + unfold Mptr in *. destruct Archi.ptr64 eqn:SF; auto with ty. + unfold Mptr in *. destruct Archi.ptr64 eqn:SF; auto with ty. Qed. Lemma wt_deref_loc: @@ -1604,15 +1641,19 @@ Qed. Lemma wt_bool_cast: forall ty, wt_bool ty -> wt_cast ty type_bool. Proof. - unfold wt_bool, wt_cast; unfold classify_bool; intros. destruct ty; simpl in *; try congruence. destruct f; congruence. + unfold wt_bool, wt_cast; unfold classify_bool; intros. + destruct ty; simpl in *; try congruence; + try (destruct Archi.ptr64; congruence). + destruct f; congruence. Qed. Lemma wt_cast_self: forall t1 t2, wt_cast t1 t2 -> wt_cast t2 t2. Proof. unfold wt_cast; intros. destruct t2; simpl in *; try congruence. - destruct i; congruence. - destruct f; congruence. +- apply (wt_cast_int i s a i s a). +- destruct Archi.ptr64; congruence. +- destruct f; congruence. Qed. Lemma binarith_type_int32s: @@ -1672,8 +1713,8 @@ Proof. - (* seqor false *) subst. constructor. auto. apply wt_bool_cast; auto. red; intros. inv H0; auto with ty. - (* condition *) constructor. destruct b; auto. destruct b; auto. red; auto. -- (* sizeof *) constructor; auto with ty. -- (* alignof *) constructor; auto with ty. +- (* sizeof *) unfold size_t, Vptrofs; destruct Archi.ptr64; constructor; auto with ty. +- (* alignof *) unfold size_t, Vptrofs; destruct Archi.ptr64; constructor; auto with ty. - (* assign *) inversion H5. constructor. eapply pres_sem_cast; eauto. - (* assignop *) subst tyres l r. constructor. auto. constructor. constructor. eapply wt_deref_loc; eauto. @@ -2105,7 +2146,7 @@ Proof. intros. inv H. econstructor. constructor. apply Genv.find_funct_ptr_prop with (p := prog) (b := b); auto. intros. inv WTPROG. destruct f0; simpl; auto. apply H4 with id; auto. - instantiate (1 := (Vptr b Int.zero)). rewrite Genv.find_funct_find_funct_ptr. auto. + instantiate (1 := (Vptr b Ptrofs.zero)). rewrite Genv.find_funct_find_funct_ptr. auto. Qed. End PRESERVATION. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 7228cd75..5b7e52c8 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -12,18 +12,9 @@ (** Compile-time evaluation of initializers for global C variables. *) -Require Import Coqlib. -Require Import Maps. -Require Import Errors. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import AST. -Require Import Memory. -Require Import Globalenvs. -Require Import Ctypes. -Require Import Cop. -Require Import Csyntax. +Require Import Coqlib Maps Errors. +Require Import Integers Floats Values AST Memory Globalenvs. +Require Import Ctypes Cop Csyntax. Open Scope error_monad_scope. @@ -38,7 +29,7 @@ Open Scope error_monad_scope. (** [constval a] evaluates the constant expression [a]. If [a] is a r-value, the returned value denotes: -- [Vint n], [Vfloat f]: the corresponding number +- [Vint n], [Vlong n], [Vfloat f], [Vsingle f]: the corresponding number - [Vptr id ofs]: address of global variable [id] plus byte offset [ofs] - [Vundef]: erroneous expression @@ -88,9 +79,9 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := | Ecast r ty => do v1 <- constval ce r; do_cast v1 (typeof r) ty | Esizeof ty1 ty => - OK (Vint (Int.repr (sizeof ce ty1))) + OK (Vptrofs (Ptrofs.repr (sizeof ce ty1))) | Ealignof ty1 ty => - OK (Vint (Int.repr (alignof ce ty1))) + OK (Vptrofs (Ptrofs.repr (alignof ce ty1))) | Eseqand r1 r2 ty => do v1 <- constval ce r1; do v2 <- constval ce r2; @@ -119,7 +110,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := | Ecomma r1 r2 ty => do v1 <- constval ce r1; constval ce r2 | Evar x ty => - OK(Vptr x Int.zero) + OK(Vptr x Ptrofs.zero) | Ederef r ty => constval ce r | Efield l f ty => @@ -128,7 +119,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := do co <- lookup_composite ce id; do delta <- field_offset ce f (co_members co); do v <- constval ce l; - OK (Val.add v (Vint (Int.repr delta))) + OK (Val.offset_ptr v (Ptrofs.repr delta)) | Tunion id _ => constval ce l | _ => @@ -161,11 +152,13 @@ Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res ini | Vint n, Tint (I8|IBool) sg _ => OK(Init_int8 n) | Vint n, Tint I16 sg _ => OK(Init_int16 n) | Vint n, Tint I32 sg _ => OK(Init_int32 n) - | Vint n, Tpointer _ _ => OK(Init_int32 n) + | Vint n, Tpointer _ _ => assertion (negb Archi.ptr64); OK(Init_int32 n) | Vlong n, Tlong _ _ => OK(Init_int64 n) + | Vlong n, Tpointer _ _ => assertion (Archi.ptr64); OK(Init_int64 n) | Vsingle f, Tfloat F32 _ => OK(Init_float32 f) | Vfloat f, Tfloat F64 _ => OK(Init_float64 f) - | Vptr id ofs, Tint I32 sg _ => OK(Init_addrof id ofs) + | Vptr id ofs, Tint I32 sg _ => assertion (negb Archi.ptr64); OK(Init_addrof id ofs) + | Vptr id ofs, Tlong _ _ => assertion (Archi.ptr64); OK(Init_addrof id ofs) | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs) | Vundef, _ => Error(msg "undefined operation in initializer") | _, _ => Error (msg "type mismatch in initializer") diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index d5f39d7d..49ac858e 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -12,21 +12,9 @@ (** Compile-time evaluation of initializers for global C variables. *) -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import AST. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Ctypes. -Require Import Cop. -Require Import Csyntax. -Require Import Csem. +Require Import Coqlib Maps. +Require Import Errors Integers Floats Values AST Memory Globalenvs Events Smallstep. +Require Import Ctypes Cop Csyntax Csem. Require Import Initializers. Open Scope error_monad_scope. @@ -77,23 +65,23 @@ Section SIMPLE_EXPRS. Variable e: env. Variable m: mem. -Inductive eval_simple_lvalue: expr -> block -> int -> Prop := +Inductive eval_simple_lvalue: expr -> block -> ptrofs -> Prop := | esl_loc: forall b ofs ty, eval_simple_lvalue (Eloc b ofs ty) b ofs | esl_var_local: forall x ty b, e!x = Some(b, ty) -> - eval_simple_lvalue (Evar x ty) b Int.zero + eval_simple_lvalue (Evar x ty) b Ptrofs.zero | esl_var_global: forall x ty b, e!x = None -> Genv.find_symbol ge x = Some b -> - eval_simple_lvalue (Evar x ty) b Int.zero + eval_simple_lvalue (Evar x ty) b Ptrofs.zero | esl_deref: forall r ty b ofs, eval_simple_rvalue r (Vptr b ofs) -> eval_simple_lvalue (Ederef r ty) b ofs | esl_field_struct: forall r f ty b ofs id co a delta, eval_simple_rvalue r (Vptr b ofs) -> typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta -> - eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta)) + eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta)) | esl_field_union: forall r f ty b ofs id a, eval_simple_rvalue r (Vptr b ofs) -> typeof r = Tunion id a -> @@ -123,9 +111,9 @@ with eval_simple_rvalue: expr -> val -> Prop := sem_cast v1 (typeof r1) ty m = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, - eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) + eval_simple_rvalue (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1))) | esr_alignof: forall ty1 ty, - eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))) + eval_simple_rvalue (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1))) | esr_seqand_true: forall r1 r2 ty v1 v2 v3, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue r2 v2 -> @@ -418,9 +406,9 @@ Proof. (* cast *) eapply sem_cast_match; eauto. (* sizeof *) - constructor. + auto. (* alignof *) - constructor. + auto. (* seqand *) destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. @@ -459,7 +447,7 @@ Proof. rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ. exploit constval_rvalue; eauto. intro MV. inv MV. simpl. replace x0 with delta by congruence. econstructor; eauto. - rewrite ! Int.add_assoc. f_equal. apply Int.add_commut. + rewrite ! Ptrofs.add_assoc. f_equal. apply Ptrofs.add_commut. simpl. auto. (* field union *) rewrite H0 in CV. eauto. @@ -617,30 +605,36 @@ Proof. exploit sem_cast_match; eauto. intros D. unfold Genv.store_init_data. inv D. - (* int *) - destruct ty; try discriminate. - destruct i0; inv EQ2. +- (* int *) + remember Archi.ptr64 as ptr64. destruct ty; try discriminate EQ2. ++ destruct i0; inv EQ2. destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto. simpl in H2; inv H2. assumption. simpl in H2; inv H2. assumption. - inv EQ2. simpl in H2; inv H2. assumption. - (* long *) - destruct ty; inv EQ2. simpl in H2; inv H2. assumption. - (* float *) ++ destruct ptr64; inv EQ2. simpl in H2; unfold Mptr in H2; rewrite <- Heqptr64 in H2; inv H2. assumption. +- (* Long *) + remember Archi.ptr64 as ptr64. destruct ty; inv EQ2. ++ simpl in H2; inv H2. assumption. ++ simpl in H2; unfold Mptr in H2; destruct Archi.ptr64; inv H4. + inv H2; assumption. +- (* float *) destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. - (* single *) +- (* single *) destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. - (* pointer *) +- (* pointer *) unfold inj in H. - assert (data = Init_addrof b1 ofs1 /\ chunk = Mint32). - destruct ty; inv EQ2; inv H2. - destruct i; inv H5. intuition congruence. auto. + assert (data = Init_addrof b1 ofs1 /\ chunk = Mptr). + { remember Archi.ptr64 as ptr64. + destruct ty; inversion EQ2. + destruct i; inv H5. unfold Mptr. destruct Archi.ptr64; inv H6; inv H2; auto. + subst ptr64. unfold Mptr. destruct Archi.ptr64; inv H5; inv H2; auto. + inv H2. auto. } destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H. - rewrite Int.add_zero in H3. auto. - (* undef *) + rewrite Ptrofs.add_zero in H3. auto. +- (* undef *) discriminate. Qed. @@ -651,19 +645,24 @@ Lemma transl_init_single_size: transl_init_single ge ty a = OK data -> init_data_size data = sizeof ge ty. Proof. - intros. monadInv H. destruct x0. + intros. monadInv H. remember Archi.ptr64 as ptr64. destruct x0. - monadInv EQ2. - destruct ty; try discriminate. destruct i0; inv EQ2; auto. - inv EQ2; auto. -- destruct ty; inv EQ2; auto. + destruct ptr64; inv EQ2. +Local Transparent sizeof. + unfold sizeof. rewrite <- Heqptr64; auto. +- destruct ty; inv EQ2; auto. + unfold sizeof. destruct Archi.ptr64; inv H0; auto. - destruct ty; try discriminate. destruct f0; inv EQ2; auto. - destruct ty; try discriminate. destruct f0; inv EQ2; auto. - destruct ty; try discriminate. destruct i0; inv EQ2; auto. - inv EQ2; auto. + destruct Archi.ptr64 eqn:SF; inv H0. simpl. rewrite SF; auto. + destruct ptr64; inv EQ2. simpl. rewrite <- Heqptr64; auto. + inv EQ2. unfold init_data_size, sizeof. auto. Qed. Notation idlsize := init_data_list_size. @@ -710,6 +709,7 @@ with tr_init_struct_size: sizeof_struct ge pos fl <= sizeof ge ty -> idlsize data + pos = sizeof ge ty. Proof. +Local Opaque sizeof. - destruct 1; simpl. + erewrite transl_init_single_size by eauto. omega. + Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 64e52df8..ad7b296a 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -736,9 +736,15 @@ Remark sem_cast_deterministic: v1 = v2. Proof. unfold sem_cast; intros. destruct (classify_cast ty ty'); try congruence. - destruct v; try congruence. - destruct (Mem.weak_valid_pointer m1 b (Int.unsigned i)); inv H. - destruct (Mem.weak_valid_pointer m2 b (Int.unsigned i)); inv H0. +- destruct v; try congruence. + destruct Archi.ptr64; try discriminate. + destruct (Mem.weak_valid_pointer m1 b (Ptrofs.unsigned i)); inv H. + destruct (Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i)); inv H0. + auto. +- destruct v; try congruence. + destruct (negb Archi.ptr64); try discriminate. + destruct (Mem.weak_valid_pointer m1 b (Ptrofs.unsigned i)); inv H. + destruct (Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i)); inv H0. auto. Qed. @@ -756,9 +762,13 @@ Qed. Lemma static_bool_val_sound: forall v t m b, bool_val v t Mem.empty = Some b -> bool_val v t m = Some b. Proof. - intros until b; unfold bool_val. destruct (classify_bool t); destruct v; auto. - intros E. unfold Mem.weak_valid_pointer, Mem.valid_pointer, proj_sumbool in E. - rewrite ! pred_dec_false in E by (apply Mem.perm_empty). discriminate. + assert (A: forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false). + { unfold Mem.weak_valid_pointer, Mem.valid_pointer, proj_sumbool; intros. + rewrite ! pred_dec_false by (apply Mem.perm_empty). auto. } + intros until b; unfold bool_val. + destruct (classify_bool t); destruct v; destruct Archi.ptr64 eqn:SF; auto. +- rewrite A; congruence. +- simpl; rewrite A; congruence. Qed. Lemma step_makeif: diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index 580f02c2..c0086a38 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -40,7 +40,7 @@ Definition is_liftable_var (cenv: compilenv) (a: expr) : option ident := Definition make_cast (a: expr) (tto: type) : expr := match classify_cast (typeof a) tto with - | cast_case_neutral => a + | cast_case_pointer => a | cast_case_i2i I32 _ => a | cast_case_f2f => a | cast_case_s2s => a diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 48a7a773..8ed924e5 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -187,21 +187,23 @@ Lemma val_casted_load_result: Val.load_result chunk v = v. Proof. intros. inversion H; clear H; subst v ty; simpl in H0. - destruct sz. +- destruct sz. destruct si; inversion H0; clear H0; subst chunk; simpl in *; congruence. destruct si; inversion H0; clear H0; subst chunk; simpl in *; congruence. clear H1. inv H0. auto. inversion H0; clear H0; subst chunk. simpl in *. destruct (Int.eq n Int.zero); subst n; reflexivity. - inv H0; auto. - inv H0; auto. - inv H0; auto. - inv H0; auto. - inv H0; auto. - inv H0; auto. - discriminate. - discriminate. - discriminate. +- inv H0; auto. +- inv H0; auto. +- inv H0; auto. +- inv H0. unfold Mptr, Val.load_result; destruct Archi.ptr64; auto. +- inv H0. unfold Mptr, Val.load_result; rewrite H1; auto. +- inv H0. unfold Val.load_result; rewrite H1; auto. +- inv H0. unfold Mptr, Val.load_result; rewrite H1; auto. +- inv H0. unfold Val.load_result; rewrite H1; auto. +- discriminate. +- discriminate. +- discriminate. Qed. Lemma val_casted_inject: @@ -209,7 +211,7 @@ Lemma val_casted_inject: Val.inject f v v' -> val_casted v ty -> val_casted v' ty. Proof. intros. inv H; auto. - inv H0; constructor. + inv H0; constructor; auto. inv H0; constructor. Qed. @@ -250,7 +252,7 @@ Proof. econstructor; eauto. unfold sem_cast, make_cast in *. destruct (classify_cast (typeof a) tto); auto. - destruct v1; inv H0; auto. + destruct v1; destruct Archi.ptr64; inv H0; auto. destruct sz2; auto. destruct v1; inv H0; auto. destruct v1; inv H0; auto. destruct v1; inv H0; auto. @@ -269,10 +271,19 @@ Lemma cast_typeconv: val_casted v ty -> sem_cast v ty (typeconv ty) m = Some v. Proof. - induction 1; simpl; auto. -- destruct sz; auto. -- unfold sem_cast. simpl. rewrite dec_eq_true; auto. + induction 1; simpl. +- unfold sem_cast, classify_cast; destruct sz, Archi.ptr64; auto. +- auto. +- auto. +- unfold sem_cast, classify_cast; destruct Archi.ptr64; auto. +- auto. +- unfold sem_cast; simpl; rewrite H; auto. +- unfold sem_cast; simpl; rewrite H; auto. +- unfold sem_cast; simpl; rewrite H; auto. +- unfold sem_cast; simpl; rewrite H; auto. +- unfold sem_cast; simpl. rewrite dec_eq_true; auto. - unfold sem_cast. simpl. rewrite dec_eq_true; auto. +- auto. Qed. Lemma step_Sdebug_temp: @@ -380,13 +391,13 @@ Lemma match_envs_assign_lifted: e!id = Some(b, ty) -> val_casted v ty -> Val.inject f v tv -> - assign_loc ge ty m b Int.zero v m' -> + assign_loc ge ty m b Ptrofs.zero v m' -> VSet.mem id cenv = true -> match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi. Proof. intros. destruct H. generalize (me_vars0 id); intros MV; inv MV; try congruence. rewrite ENV in H0; inv H0. inv H3; try congruence. - unfold Mem.storev in H0. rewrite Int.unsigned_zero in H0. + unfold Mem.storev in H0. rewrite Ptrofs.unsigned_zero in H0. constructor; eauto; intros. (* vars *) destruct (peq id0 id). subst id0. @@ -746,7 +757,8 @@ Proof. unfold access_mode; intros. assert (size_chunk chunk = sizeof ge ty). { - destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto. + destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto; + unfold Mptr; simpl; destruct Archi.ptr64; auto. } omega. Qed. @@ -1019,10 +1031,10 @@ Proof. destruct (zeq (sizeof tge ty) 0). + (* special case size = 0 *) assert (bytes = nil). - { exploit (Mem.loadbytes_empty m bsrc (Int.unsigned osrc) (sizeof tge ty)). + { exploit (Mem.loadbytes_empty m bsrc (Ptrofs.unsigned osrc) (sizeof tge ty)). omega. congruence. } subst. - destruct (Mem.range_perm_storebytes tm bdst' (Int.unsigned (Int.add odst (Int.repr delta))) nil) + destruct (Mem.range_perm_storebytes tm bdst' (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta))) nil) as [tm' SB]. simpl. red; intros; omegaContradiction. exists tm'. @@ -1038,15 +1050,15 @@ Proof. exploit Mem.loadbytes_length; eauto. intros LEN. assert (SZPOS: sizeof tge ty > 0). { generalize (sizeof_pos tge ty); omega. } - assert (RPSRC: Mem.range_perm m bsrc (Int.unsigned osrc) (Int.unsigned osrc + sizeof tge ty) Cur Nonempty). + assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. - assert (RPDST: Mem.range_perm m bdst (Int.unsigned odst) (Int.unsigned odst + sizeof tge ty) Cur Nonempty). + assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty). replace (sizeof tge ty) with (Z_of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. rewrite LEN. apply nat_of_Z_eq. omega. - assert (PSRC: Mem.perm m bsrc (Int.unsigned osrc) Cur Nonempty). + assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty). apply RPSRC. omega. - assert (PDST: Mem.perm m bdst (Int.unsigned odst) Cur Nonempty). + assert (PDST: Mem.perm m bdst (Ptrofs.unsigned odst) Cur Nonempty). apply RPDST. omega. exploit Mem.address_inject. eauto. eexact PSRC. eauto. intros EQ1. exploit Mem.address_inject. eauto. eexact PDST. eauto. intros EQ2. @@ -1449,7 +1461,7 @@ Proof. rewrite ENV in H6; inv H6. inv H0; try congruence. assert (chunk0 = chunk). simpl in H. congruence. subst chunk0. - assert (v0 = v). unfold Mem.loadv in H2. rewrite Int.unsigned_zero in H2. congruence. subst v0. + assert (v0 = v). unfold Mem.loadv in H2. rewrite Ptrofs.unsigned_zero in H2. congruence. subst v0. exists tv; split; auto. constructor; auto. simpl in H; congruence. simpl in H; congruence. @@ -1464,13 +1476,13 @@ Proof. rewrite H1. exploit me_vars; eauto. instantiate (1 := id). intros MV. inv MV; try congruence. rewrite ENV in H; inv H. - exists b'; exists Int.zero; split. + exists b'; exists Ptrofs.zero; split. apply eval_Evar_local; auto. econstructor; eauto. (* global var *) rewrite H2. exploit me_vars; eauto. instantiate (1 := id). intros MV. inv MV; try congruence. - exists l; exists Int.zero; split. + exists l; exists Ptrofs.zero; split. apply eval_Evar_global. auto. rewrite <- H0. apply symbols_preserved. destruct GLOB as [bound GLOB1]. inv GLOB1. econstructor; eauto. @@ -1484,7 +1496,7 @@ Proof. inversion B. subst. econstructor; econstructor; split. eapply eval_Efield_struct; eauto. rewrite typeof_simpl_expr; eauto. - econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + econstructor; eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. (* field union *) rewrite <- comp_env_preserved in *. exploit eval_simpl_expr; eauto. intros [tv [A B]]. @@ -1721,12 +1733,12 @@ Lemma match_cont_find_funct: exists tfd, Genv.find_funct tge tvf = Some tfd /\ transf_fundef fd = OK tfd. Proof. intros. exploit match_cont_globalenv; eauto. intros [bound1 MG]. destruct MG. - inv H1; simpl in H0; try discriminate. destruct (Int.eq_dec ofs1 Int.zero); try discriminate. + inv H1; simpl in H0; try discriminate. destruct (Ptrofs.eq_dec ofs1 Ptrofs.zero); try discriminate. subst ofs1. assert (f b1 = Some(b1, 0)). apply DOMAIN. eapply FUNCTIONS; eauto. rewrite H1 in H2; inv H2. - rewrite Int.add_zero. simpl. rewrite dec_eq_true. apply function_ptr_translated; auto. + rewrite Ptrofs.add_zero. simpl. rewrite dec_eq_true. apply function_ptr_translated; auto. Qed. (** Relating execution states *) -- cgit