From a6c369cbd63996c1571ae601b7d92070f024b22c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 5 Oct 2013 08:11:34 +0000 Subject: Merge of the "alignas" branch. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 30 ++++-- cfrontend/Cexec.v | 9 +- cfrontend/Clight.v | 3 +- cfrontend/Csem.v | 3 +- cfrontend/Cshmgen.v | 2 +- cfrontend/Cshmgenproof.v | 4 +- cfrontend/Ctypes.v | 231 ++++++++++++++++++++++++++---------------- cfrontend/Initializers.v | 13 ++- cfrontend/Initializersproof.v | 52 ++++++---- cfrontend/PrintCsyntax.ml | 6 +- cfrontend/SimplLocalsproof.v | 18 ++-- 11 files changed, 234 insertions(+), 137 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 20e00c8c..dd9cfbf4 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -206,9 +206,21 @@ let convertInt n = coqint_of_camlint(Int64.to_int32 n) (** Attributes *) -let convertAttr a = List.mem AVolatile a - -let mergeAttr a1 a2 = a1 || a2 +let rec log2 n = if n = 1 then 0 else 1 + log2 (n lsr 1) + +let convertAttr a = + { attr_volatile = List.mem AVolatile a; + attr_alignas = + let n = Cutil.alignas_attribute a in + if n > 0 then Some (N.of_int (log2 n)) else None } + +let mergeAttr a1 a2 = + { attr_volatile = a1.attr_volatile || a2.attr_volatile; + attr_alignas = + match a1.attr_alignas, a2.attr_alignas with + | None, aa -> aa + | aa, None -> aa + | Some n1, Some n2 -> Some (if N.le n1 n2 then n1 else n2) } let mergeTypAttr ty a2 = match ty with @@ -340,9 +352,10 @@ let rec convertTypList env = function | t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl) let cacheCompositeDef env su id attr flds = - (* we currently ignore attributes on structs and unions *) let ty = - match su with C.Struct -> C.TStruct(id, []) | C.Union -> C.TUnion(id, []) in + match su with + | C.Struct -> C.TStruct(id, attr) + | C.Union -> C.TUnion(id, attr) in Hashtbl.add compositeCache id (convertTyp env ty) let rec projFunType env ty = @@ -821,6 +834,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in let ty' = convertTyp env ty in let sz = Ctypes.sizeof ty' in + let al = Ctypes.alignof ty' in let attr = Cutil.attributes_of_type env ty in let init' = match optinit with @@ -828,10 +842,6 @@ let convertGlobvar loc env (sto, id, ty, optinit) = if sto = C.Storage_extern then [] else [Init_space sz] | Some i -> convertInitializer env ty i in - let align = - match Cutil.find_custom_attributes ["aligned"; "__aligned__"] attr with - | [[C.AInt n]] -> Some(Int64.to_int n) - | _ -> Cutil.alignof env ty in let (section, near_access) = Sections.for_variable env id' ty (optinit <> None) in if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then @@ -839,7 +849,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = id.name (Z.to_string sz)); Hashtbl.add decl_atom id' { a_storage = sto; - a_alignment = align; + a_alignment = Some (Z.to_int al); a_sections = [section]; a_small_data = near_access; a_inline = false; diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 70a02c19..f83c7009 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -285,7 +285,7 @@ Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : o end. Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop := - (alignof ty | Int.unsigned ofs') /\ (alignof ty | Int.unsigned ofs) /\ + (alignof_blockcopy ty | Int.unsigned ofs') /\ (alignof_blockcopy ty | Int.unsigned ofs) /\ (b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs'). @@ -295,9 +295,10 @@ Remark check_assign_copy: { 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 ty > 0). apply alignof_pos; auto. - destruct (Zdivide_dec (alignof ty) (Int.unsigned ofs')); auto... - destruct (Zdivide_dec (alignof ty) (Int.unsigned ofs)); auto... + assert (alignof_blockcopy ty > 0). + { unfold alignof_blockcopy. apply Z.min_case. omega. apply alignof_pos. } + destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs')); auto... + destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs)); auto... assert (Y: {b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/ diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 3bd06dff..6a579993 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -218,7 +218,8 @@ Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int): assign_loc ty m b ofs v m' | assign_loc_copy: forall b' ofs' bytes m', access_mode ty = By_copy -> - (alignof ty | Int.unsigned ofs') -> (alignof ty | Int.unsigned ofs) -> + (alignof_blockcopy ty | Int.unsigned ofs') -> + (alignof_blockcopy ty | Int.unsigned ofs) -> b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs' -> diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 0f9b3f8a..5d94c537 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -91,7 +91,8 @@ Inductive assign_loc {F V: Type} (ge: Genv.t F V) (ty: type) (m: mem) (b: block) assign_loc ge ty m b ofs v t m' | assign_loc_copy: forall b' ofs' bytes m', access_mode ty = By_copy -> - (alignof ty | Int.unsigned ofs') -> (alignof ty | Int.unsigned ofs) -> + (alignof_blockcopy ty | Int.unsigned ofs') -> + (alignof_blockcopy ty | Int.unsigned ofs) -> b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs' -> diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index a303a7fd..fd349856 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -307,7 +307,7 @@ Definition make_load (addr: expr) (ty_res: type) := by-copy assignment of a value of Clight type [ty]. *) Definition make_memcpy (dst src: expr) (ty: type) := - Sbuiltin None (EF_memcpy (Ctypes.sizeof ty) (Ctypes.alignof ty)) + Sbuiltin None (EF_memcpy (Ctypes.sizeof ty) (Ctypes.alignof_blockcopy ty)) (dst :: src :: nil). (** [make_store addr ty rhs] stores the value of the diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 24576fc6..79069449 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -657,9 +657,9 @@ Proof. econstructor. econstructor. eauto. econstructor. eauto. constructor. econstructor; eauto. - apply alignof_1248. + apply alignof_blockcopy_1248. apply sizeof_pos. - apply sizeof_alignof_compat. + eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat. Qed. Lemma make_store_correct: diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 8d00b955..abd015c8 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -45,14 +45,15 @@ Inductive floatsize : Type := | F32: floatsize | F64: floatsize. -(** Every type carries a set of attributes. Currently, only one - attribute is modeled: [volatile]. *) +(** Every type carries a set of attributes. Currently, only two + attributes are modeled: [volatile] and [_Alignas(n)] (from ISO C 2011). *) Record attr : Type := mk_attr { - attr_volatile: bool + attr_volatile: bool; + attr_alignas: option N (**r log2 of required alignment *) }. -Definition noattr := {| attr_volatile := false |}. +Definition noattr := {| attr_volatile := false; attr_alignas := None |}. (** The syntax of type expressions. Some points to note: - Array types [Tarray n] carry the size [n] of the array. @@ -113,10 +114,11 @@ Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2} with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2} with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}. Proof. - assert (forall (x y: intsize), {x=y} + {x<>y}). decide equality. - assert (forall (x y: signedness), {x=y} + {x<>y}). decide equality. - assert (forall (x y: floatsize), {x=y} + {x<>y}). decide equality. - assert (forall (x y: attr), {x=y} + {x<>y}). decide equality. apply bool_dec. + 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. intros E1 E2. decide equality. decide equality. @@ -161,21 +163,25 @@ Definition typeconv (ty: type) : type := (** Natural alignment of a type, in bytes. *) Fixpoint alignof (t: type) : Z := - match t with - | Tvoid => 1 - | Tint I8 _ _ => 1 - | Tint I16 _ _ => 2 - | Tint I32 _ _ => 4 - | Tint IBool _ _ => 1 - | Tlong _ _ => 8 - | Tfloat F32 _ => 4 - | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 - | Tarray t' _ _ => alignof t' - | Tfunction _ _ => 1 - | Tstruct _ fld _ => alignof_fields fld - | Tunion _ fld _ => alignof_fields fld - | Tcomp_ptr _ _ => 4 + match attr_alignas (attr_of_type t) with + | Some l => two_p (Z.of_N l) + | None => + match t with + | Tvoid => 1 + | Tint I8 _ _ => 1 + | Tint I16 _ _ => 2 + | Tint I32 _ _ => 4 + | Tint IBool _ _ => 1 + | Tlong _ _ => 8 + | Tfloat F32 _ => 4 + | Tfloat F64 _ => 8 + | Tpointer _ _ => 4 + | Tarray t' _ _ => alignof t' + | Tfunction _ _ => 1 + | Tstruct _ fld _ => alignof_fields fld + | Tunion _ fld _ => alignof_fields fld + | Tcomp_ptr _ _ => 4 + end end with alignof_fields (f: fieldlist) : Z := @@ -187,49 +193,72 @@ with alignof_fields (f: fieldlist) : Z := Scheme type_ind2 := Induction for type Sort Prop with fieldlist_ind2 := Induction for fieldlist Sort Prop. -Lemma alignof_1248: - forall t, alignof t = 1 \/ alignof t = 2 \/ alignof t = 4 \/ alignof t = 8 -with alignof_fields_1248: - forall f, alignof_fields f = 1 \/ alignof_fields f = 2 \/ alignof_fields f = 4 \/ alignof_fields f = 8. +Lemma alignof_two_p: + forall t, exists n, alignof t = two_power_nat n +with alignof_fields_two_p: + forall f, exists n, alignof_fields f = two_power_nat n. Proof. - induction t; simpl; auto. - destruct i; auto. - destruct f; auto. - induction f; simpl; auto. - rewrite Zmax_spec. destruct (zlt (alignof_fields f) (alignof t)); auto. + assert (X: forall t a, + (exists n, a = two_power_nat n) -> + exists n, + match attr_alignas (attr_of_type t) with + | Some l => two_p (Z.of_N l) + | None => a + end = two_power_nat n). + { + intros. + destruct (attr_alignas (attr_of_type t)). + exists (N.to_nat n). rewrite two_power_nat_two_p. rewrite N_nat_Z. auto. + auto. + } + induction t; apply X; simpl; auto. + exists 0%nat; auto. + destruct i. + exists 0%nat; auto. exists 1%nat; auto. exists 2%nat; auto. + exists 0%nat; auto. exists 3%nat; auto. + destruct f. + exists 2%nat; auto. exists 3%nat; auto. + exists 2%nat; auto. + exists 0%nat; auto. + exists 2%nat; auto. + induction f; simpl. + exists 0%nat; auto. + apply Z.max_case; auto. Qed. Lemma alignof_pos: forall t, alignof t > 0. Proof. - intros. generalize (alignof_1248 t). omega. + intros. destruct (alignof_two_p t) as [n EQ]. rewrite EQ. apply two_power_nat_pos. Qed. Lemma alignof_fields_pos: forall f, alignof_fields f > 0. Proof. - intros. generalize (alignof_fields_1248 f). omega. + intros. destruct (alignof_fields_two_p f) as [n EQ]. rewrite EQ. apply two_power_nat_pos. Qed. (** Size of a type, in bytes. *) Fixpoint sizeof (t: type) : Z := - match t with - | Tvoid => 1 - | Tint I8 _ _ => 1 - | Tint I16 _ _ => 2 - | Tint I32 _ _ => 4 - | Tint IBool _ _ => 1 - | Tlong _ _ => 8 - | Tfloat F32 _ => 4 - | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 - | Tarray t' n _ => sizeof t' * Zmax 1 n - | Tfunction _ _ => 1 - | Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t) - | Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t) - | Tcomp_ptr _ _ => 4 - end + let sz := + match t with + | Tvoid => 1 + | Tint I8 _ _ => 1 + | Tint I16 _ _ => 2 + | Tint I32 _ _ => 4 + | Tint IBool _ _ => 1 + | Tlong _ _ => 8 + | Tfloat F32 _ => 4 + | Tfloat F64 _ => 8 + | Tpointer _ _ => 4 + | Tarray t' n _ => sizeof t' * Zmax 1 n + | Tfunction _ _ => 1 + | Tstruct _ fld _ => Zmax 1 (sizeof_struct fld 0) + | Tunion _ fld _ => Zmax 1 (sizeof_union fld) + | Tcomp_ptr _ _ => 4 + end + in align sz (alignof t) with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z := match fld with @@ -246,23 +275,15 @@ with sizeof_union (fld: fieldlist) : Z := Lemma sizeof_pos: forall t, sizeof t > 0. Proof. - intro t0. - apply (type_ind2 (fun t => sizeof t > 0) - (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0)); - intros; simpl; auto; try omega. + assert (X: forall t sz, sz > 0 -> align sz (alignof t) > 0). + { + intros. generalize (align_le sz (alignof t) (alignof_pos t)). omega. + } +Local Opaque alignof. + induction t; simpl; apply X; try xomega. destruct i; omega. destruct f; omega. - apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega. - destruct H. - generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). - generalize (Zmax1 1 (sizeof_struct f 0)). omega. - generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). - generalize (Zmax1 1 (sizeof_union f)). omega. - split. omega. auto. - destruct H0. split; intros. - generalize (Zmax2 (sizeof t) (sizeof_union f)). omega. - apply H1. - generalize (align_le pos (alignof t) (alignof_pos t)). omega. + apply Zmult_gt_0_compat. auto. xomega. Qed. Lemma sizeof_struct_incr: @@ -271,17 +292,14 @@ Proof. induction fld; intros; simpl. omega. eapply Zle_trans. 2: apply IHfld. apply Zle_trans with (align pos (alignof t)). - apply align_le. apply alignof_pos. - assert (sizeof t > 0) by apply sizeof_pos. omega. + apply align_le. apply alignof_pos. + generalize (sizeof_pos t); omega. Qed. Lemma sizeof_alignof_compat: forall t, (alignof t | sizeof t). Proof. - induction t; simpl; try (apply Zdivide_refl). - apply Zdivide_mult_l. auto. - apply align_divides. apply alignof_fields_pos. - apply align_divides. apply alignof_fields_pos. + intros. destruct t; apply align_divides; apply alignof_pos. Qed. (** Byte offset for a field in a struct or union. @@ -333,7 +351,7 @@ Lemma field_offset_in_range: Proof. intros. exploit field_offset_rec_in_range; eauto. intros [A B]. split. auto. simpl. eapply Zle_trans. eauto. - eapply Zle_trans. eapply Zle_max_r. apply align_le. apply alignof_fields_pos. + eapply Zle_trans. eapply Zle_max_r. apply align_le. apply alignof_pos. Qed. (** Second, two distinct fields do not overlap *) @@ -484,40 +502,83 @@ with unroll_composite_fields (fld: fieldlist) : fieldlist := | Fcons id ty fld' => Fcons id (unroll_composite ty) (unroll_composite_fields fld') end. +Lemma attr_of_type_unroll_composite: + forall ty, attr_of_type (unroll_composite ty) = attr_of_type ty. +Proof. + intros. destruct ty; simpl; auto; destruct (ident_eq i cid); auto. +Qed. + Lemma alignof_unroll_composite: forall ty, alignof (unroll_composite ty) = alignof ty. Proof. +Local Transparent alignof. apply (type_ind2 (fun ty => alignof (unroll_composite ty) = alignof ty) (fun fld => alignof_fields (unroll_composite_fields fld) = alignof_fields fld)); simpl; intros; auto. - destruct (ident_eq i cid); auto. - destruct (ident_eq i cid); auto. - destruct (ident_eq i cid); auto. - decEq; auto. + rewrite H; auto. + destruct (ident_eq i cid); auto. simpl. rewrite H; auto. + destruct (ident_eq i cid); auto. simpl. rewrite H; auto. + destruct (ident_eq i cid); auto. congruence. Qed. Lemma sizeof_unroll_composite: forall ty, sizeof (unroll_composite ty) = sizeof ty. Proof. -Opaque alignof. +Local Opaque alignof. apply (type_ind2 (fun ty => sizeof (unroll_composite ty) = sizeof ty) (fun fld => sizeof_union (unroll_composite_fields fld) = sizeof_union fld /\ forall pos, sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos)); simpl; intros; auto. - congruence. - destruct H. rewrite <- (alignof_unroll_composite (Tstruct i f a)). - simpl. destruct (ident_eq i cid); simpl. auto. rewrite H0; auto. - destruct H. rewrite <- (alignof_unroll_composite (Tunion i f a)). - simpl. destruct (ident_eq i cid); simpl. auto. rewrite H; auto. - destruct (ident_eq i cid); auto. - destruct H0. split. congruence. - intros. rewrite alignof_unroll_composite. rewrite H1. rewrite H. auto. +- rewrite H. rewrite <- (alignof_unroll_composite (Tarray t z a)). auto. +- rewrite <- (alignof_unroll_composite (Tstruct i f a)). simpl. + destruct H. destruct (ident_eq i cid). auto. simpl. rewrite H0. auto. +- rewrite <- (alignof_unroll_composite (Tunion i f a)). simpl. + destruct H. destruct (ident_eq i cid). auto. simpl. rewrite H. auto. +- destruct (ident_eq i cid); auto. +- destruct H0. split. + + congruence. + + intros. rewrite H1. rewrite H. rewrite alignof_unroll_composite. auto. Qed. End UNROLL_COMPOSITE. +(** A variatn of [alignof] for use in block copy operations + (which do not support alignments greater than 8). *) + +Definition alignof_blockcopy (ty: type) := Zmin 8 (alignof ty). + +Lemma alignof_blockcopy_1248: + forall ty, let a := alignof_blockcopy ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8. +Proof. + intros. unfold a, alignof_blockcopy. + destruct (alignof_two_p ty) as [n EQ]. rewrite EQ. + destruct n; auto. + destruct n; auto. + destruct n; auto. + right; right; right. apply Z.min_l. + rewrite two_power_nat_two_p. rewrite ! inj_S. + change 8 with (two_p 3). + apply two_p_monotone. omega. +Qed. + +Lemma alignof_blockcopy_divides: + forall ty, (alignof_blockcopy ty | alignof ty). +Proof. + intros. unfold alignof_blockcopy. + destruct (alignof_two_p ty) as [n EQ]. rewrite EQ. + destruct n. apply Zdivide_refl. + destruct n. apply Zdivide_refl. + destruct n. apply Zdivide_refl. + replace (two_power_nat (S(S(S n)))) with (two_p (3 + Z.of_nat n)). + rewrite two_p_is_exp by omega. change (two_p 3) with 8. + apply Z.min_case. + exists (two_p (Z.of_nat n)). ring. + apply Zdivide_refl. + rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega. +Qed. + (** Extracting a type list from a function parameter declaration. *) Fixpoint type_of_params (params: list (ident * type)) : typelist := diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index e7debfcb..ec06cfdb 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -19,6 +19,7 @@ Require Import Floats. Require Import Values. Require Import AST. Require Import Memory. +Require Import Globalenvs. Require Import Ctypes. Require Import Cop. Require Import Csyntax. @@ -173,11 +174,15 @@ Fixpoint transl_init (ty: type) (i: initializer) {struct i} : res (list init_data) := match i, ty with | Init_single a, _ => - do d <- transl_init_single ty a; OK (d :: nil) + do d <- transl_init_single ty a; + OK (d :: padding (Genv.init_data_size d) (sizeof ty)) | Init_compound il, Tarray tyelt sz _ => - if zle sz 0 - then OK (Init_space(sizeof tyelt) :: nil) - else transl_init_array tyelt il sz + if zle sz 0 then + OK (Init_space(sizeof ty) :: nil) + else + do dl <- transl_init_array tyelt il sz; + OK(let n := sizeof ty - sizeof tyelt * sz in + if zle n 0 then dl else dl ++ Init_space n :: nil) | Init_compound il, Tstruct _ Fnil _ => OK (Init_space (sizeof ty) :: nil) | Init_compound il, Tstruct id fl _ => diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index f3de05c1..ef9ec6ca 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -523,21 +523,22 @@ Qed. Lemma transl_init_single_size: forall ty a data, transl_init_single ty a = OK data -> - Genv.init_data_size data = sizeof ty. -Proof. + Genv.init_data_size data <= sizeof ty. +Proof with (simpl; apply align_le; apply alignof_pos). +Local Opaque alignof. intros. monadInv H. destruct x0. monadInv EQ2. destruct ty; try discriminate. - destruct i0; inv EQ2; reflexivity. - inv EQ2; reflexivity. - inv EQ2; reflexivity. - destruct ty; inv EQ2; reflexivity. + destruct i0; inv EQ2... + inv EQ2... + inv EQ2... + destruct ty; inv EQ2... destruct ty; try discriminate. - destruct f0; inv EQ2; reflexivity. + destruct f0; inv EQ2... destruct ty; try discriminate. - destruct i0; inv EQ2; reflexivity. - inv EQ2; reflexivity. - inv EQ2; reflexivity. + destruct i0; inv EQ2... + inv EQ2... + inv EQ2... Qed. Notation idlsize := Genv.init_data_list_size. @@ -616,25 +617,31 @@ with transl_init_list_size: Proof. induction i; intros. (* single *) - monadInv H. simpl. rewrite (transl_init_single_size _ _ _ EQ). omega. + monadInv H. simpl. rewrite padding_size. omega. eapply transl_init_single_size; eauto. (* compound *) simpl in H. destruct ty; try discriminate. (* compound array *) - destruct (zle z 0). - monadInv H. simpl. repeat rewrite Zmax_spec. rewrite zlt_true. rewrite zlt_true. ring. - omega. generalize (sizeof_pos ty); omega. - simpl. rewrite Zmax_spec. rewrite zlt_false. - eapply (proj1 (transl_init_list_size il)). auto. omega. + set (sz := sizeof (Tarray ty z a)) in *. + destruct (zle z 0). inv H. simpl. rewrite Z.max_l. omega. + generalize (sizeof_pos (Tarray ty z a)). unfold sz; omega. + monadInv H. exploit (proj1 (transl_init_list_size il)); eauto. intros SX. + assert (sizeof ty * z <= sz). + { unfold sz. simpl. rewrite Z.max_r. apply align_le; apply alignof_pos. omega. } + destruct (zle (sz - sizeof ty * z)). + omega. + rewrite idlsize_app. simpl. rewrite Z.max_l by omega. omega. (* compound struct *) - destruct f. - inv H. reflexivity. + set (sz := sizeof (Tstruct i f a)) in *. + destruct f. + inv H. simpl. rewrite Z.max_l. omega. generalize (sizeof_pos (Tstruct i Fnil a)); unfold sz; omega. replace (idlsize data) with (idlsize data + 0) by omega. eapply (proj1 (proj2 (transl_init_list_size il))). eauto. rewrite sizeof_struct_eq. 2: congruence. apply align_le. apply alignof_pos. (* compound union *) + set (sz := sizeof (Tunion i f a)) in *. destruct f. - inv H. reflexivity. + inv H. simpl. rewrite Z.max_l. omega. generalize (sizeof_pos (Tunion i Fnil a)); unfold sz; omega. eapply (proj2 (proj2 (transl_init_list_size il))). eauto. rewrite sizeof_union_eq. 2: congruence. eapply Zle_trans. 2: apply align_le. simpl. apply Zmax_bound_l. omega. @@ -767,12 +774,17 @@ Proof. (* single *) monadInv H3. exploit transl_init_single_steps; eauto. intros. - simpl. rewrite H3. auto. + simpl. rewrite H3. apply store_init_data_list_padding. (* array *) destruct (zle sz 0). exploit exec_init_array_length; eauto. destruct il; intros. subst. inv H. inv H1. auto. omegaContradiction. + monadInv H1. + change (align (sizeof ty * Z.max 1 sz) (alignof (Tarray ty sz a))) + with (sizeof (Tarray ty sz a)). + destruct (zle (sizeof (Tarray ty sz a) - sizeof ty * sz) 0). eauto. + eapply store_init_data_list_app; eauto. (* struct *) destruct fl. inv H. inv H1. auto. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 897a2ee5..ec82869f 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -78,7 +78,11 @@ let struct_unions = ref StructUnion.empty (* Declarator (identifier + type) *) let attributes a = - if attr_volatile a then " volatile" else "" + let s1 = if a.attr_volatile then " volatile" else "" in + match a.attr_alignas with + | None -> s1 + | Some l -> + sprintf " _Alignas(%Ld)%s" (Int64.shift_left 1L (N.to_int l)) s1 let name_optid id = if id = "" then "" else " " ^ id diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 83e73753..62bbd67d 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -761,10 +761,12 @@ Qed. Lemma sizeof_by_value: forall ty chunk, - access_mode ty = By_value chunk -> sizeof ty = size_chunk chunk. + access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ty. Proof. - unfold access_mode; intros. - destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto. + unfold access_mode; intros. +Local Opaque alignof. + destruct ty; try destruct i; try destruct s; try destruct f; inv H; + apply align_le; apply alignof_pos. Qed. Definition env_initial_value (e: env) (m: mem) := @@ -782,7 +784,7 @@ Proof. apply IHalloc_variables. red; intros. rewrite PTree.gsspec in H2. destruct (peq id0 id). inv H2. eapply Mem.load_alloc_same'; eauto. - omega. erewrite sizeof_by_value; eauto. omega. + omega. rewrite Zplus_0_l. eapply sizeof_by_value; eauto. apply Zdivide_0. eapply Mem.load_alloc_other; eauto. Qed. @@ -1044,10 +1046,10 @@ Proof. exploit Mem.storebytes_mapped_inject; eauto. intros [tm' [C D]]. exists tm'. split. eapply assign_loc_copy; try rewrite EQ1; try rewrite EQ2; eauto. - eapply Mem.aligned_area_inject with (m := m); eauto. apply alignof_1248. - apply sizeof_alignof_compat. - eapply Mem.aligned_area_inject with (m := m); eauto. apply alignof_1248. - apply sizeof_alignof_compat. + eapply Mem.aligned_area_inject with (m := m); eauto. apply alignof_blockcopy_1248. + eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat. + eapply Mem.aligned_area_inject with (m := m); eauto. apply alignof_blockcopy_1248. + eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat. eapply Mem.disjoint_or_equal_inject with (m := m); eauto. apply Mem.range_perm_max with Cur; auto. apply Mem.range_perm_max with Cur; auto. -- cgit