Revised treatment of _Alignas, for better compatibility with GCC and Clang, and to avoid wasting global variable space by inflating their sizeof needlessly.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2362 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

6 files changed, 196 insertions, 136 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index f83c700..03cab54 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -295,8 +295,7 @@ 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_blockcopy ty > 0).
-  { unfold alignof_blockcopy. apply Z.min_case. omega. apply alignof_pos. }
+  assert (alignof_blockcopy ty > 0) by apply alignof_blockcopy_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 \/
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 7906944..1eb5830 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -658,8 +658,8 @@ Proof.
   econstructor. eauto. econstructor. eauto. constructor. 
   econstructor; eauto. 
   apply alignof_blockcopy_1248.
-  apply sizeof_pos. 
-  eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat.
+  apply sizeof_pos.
+  apply sizeof_alignof_blockcopy_compat.
 Qed.
  
 Lemma make_store_correct:
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index abd015c..c9ef996 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -160,7 +160,7 @@ Definition typeconv (ty: type) : type :=
 
 (** * Operations over types *)
 
-(** Natural alignment of a type, in bytes. *)
+(** Alignment of a type, in bytes. *)
 
 Fixpoint alignof (t: type) : Z :=
   match attr_alignas (attr_of_type t) with
@@ -241,24 +241,22 @@ Qed.
 (** Size of a type, in bytes. *)
 
 Fixpoint sizeof (t: type) : Z :=
-  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)
+  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
 
 with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z :=
   match fld with
@@ -275,15 +273,17 @@ with sizeof_union (fld: fieldlist) : Z :=
 Lemma sizeof_pos:
   forall t, sizeof t > 0.
 Proof.
-  assert (X: forall t sz, sz > 0 -> align sz (alignof t) > 0).
+Local Opaque alignof.
+  assert (X: forall n t, n > 0 -> align n (alignof t) > 0).
   {
-    intros. generalize (align_le sz (alignof t) (alignof_pos t)). omega. 
+    intros. generalize (align_le n (alignof t) (alignof_pos t)). omega.
   }
-Local Opaque alignof.
-  induction t; simpl; apply X; try xomega.
+  induction t; simpl; try xomega.
   destruct i; omega.
   destruct f; omega.
   apply Zmult_gt_0_compat. auto. xomega.
+  apply X. xomega. 
+  apply X. xomega.
 Qed.
 
 Lemma sizeof_struct_incr:
@@ -296,10 +296,33 @@ Proof.
   generalize (sizeof_pos t); omega.
 Qed.
 
+Fixpoint naturally_aligned (t: type) : Prop :=
+  match t with
+  | Tint _ _ a | Tlong _ a | Tfloat _ a | Tpointer _ a | Tcomp_ptr _ a =>
+      attr_alignas a = None
+  | Tarray t' _ a =>
+      attr_alignas a = None /\ naturally_aligned t'
+  | Tvoid | Tfunction _ _ | Tstruct _ _ _ | Tunion _ _ _ =>
+      True
+  end.
+
 Lemma sizeof_alignof_compat:
-  forall t, (alignof t | sizeof t).
+  forall t, naturally_aligned t -> (alignof t | sizeof t).
 Proof.
-  intros. destruct t; apply align_divides; apply alignof_pos.
+Local Transparent alignof.
+  induction t; simpl; intros.
+- apply Zdivide_refl.
+- rewrite H. destruct i; apply Zdivide_refl.
+- rewrite H; apply Zdivide_refl.
+- rewrite H. destruct f; apply Zdivide_refl.
+- rewrite H; apply Zdivide_refl.
+- destruct H. rewrite H. apply Z.divide_mul_l; auto. 
+- apply Zdivide_refl.
+- change (alignof (Tstruct i f a) | align (Z.max 1 (sizeof_struct f 0)) (alignof (Tstruct i f a))).
+  apply align_divides. apply alignof_pos.
+- change (alignof (Tunion i f a) | align (Z.max 1 (sizeof_union f)) (alignof (Tunion i f a))).
+  apply align_divides. apply alignof_pos.
+- rewrite H; apply Zdivide_refl.
 Qed.
 
 (** Byte offset for a field in a struct or union.
@@ -350,8 +373,11 @@ Lemma field_offset_in_range:
   0 <= ofs /\ ofs + sizeof ty <= sizeof (Tstruct sid fld a).
 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_pos.
+  split. auto.
+Local Opaque alignof. 
+  simpl. eapply Zle_trans; eauto. 
+  apply Zle_trans with (Z.max 1 (sizeof_struct fld 0)). xomega. 
+  apply align_le. apply alignof_pos. 
 Qed.
 
 (** Second, two distinct fields do not overlap *)
@@ -531,7 +557,7 @@ Local Opaque alignof.
                    /\ forall pos,
                       sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos));
   simpl; intros; auto.
-- rewrite H. rewrite <- (alignof_unroll_composite (Tarray t z a)). auto.
+- rewrite H. 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.
@@ -544,39 +570,82 @@ Qed.
 
 End UNROLL_COMPOSITE.
 
-(** A variatn of [alignof] for use in block copy operations
-  (which do not support alignments greater than 8). *)
+(** A variant of [alignof] for use in block copy operations.
+  Block copy operations do not support alignments greater than 8,
+  and require the size to be an integral multiple of the alignment. *)
 
-Definition alignof_blockcopy (ty: type) := Zmin 8 (alignof ty).
+Fixpoint alignof_blockcopy (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_blockcopy t'
+  | Tfunction _ _ => 1
+  | Tstruct _ fld _ => Zmin 8 (alignof t)
+  | Tunion _ fld _ => Zmin 8 (alignof t)
+  | Tcomp_ptr _ _ => 4
+  end.
 
 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.
+  assert (X: forall ty, let a := Zmin 8 (alignof ty) in
+             a = 1 \/ a = 2 \/ a = 4 \/ a = 8).
+  {
+    intros. destruct (alignof_two_p ty) as [n EQ]. unfold a; 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.
+  }
+  induction ty; simpl; auto.
+  destruct i; auto.
+  destruct f; auto.
 Qed.
 
-Lemma alignof_blockcopy_divides:
-  forall ty, (alignof_blockcopy ty | alignof ty).
+Lemma alignof_blockcopy_pos:
+  forall ty, alignof_blockcopy ty > 0.
 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.
+  intros. generalize (alignof_blockcopy_1248 ty). simpl. intuition omega.
+Qed.
+
+Lemma sizeof_alignof_blockcopy_compat:
+  forall ty, (alignof_blockcopy ty | sizeof ty).
+Proof.
+  assert (X: forall ty sz, (alignof ty | sz) -> (Zmin 8 (alignof ty) | sz)).
+  {
+    intros. destruct (alignof_two_p ty) as [n EQ]. rewrite EQ in *.
+    destruct n; auto.
+    destruct n; auto.
+    destruct n; auto.
+    eapply Zdivide_trans; eauto. 
+    apply Z.min_case. 
+    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.
+    exists (two_p (Z.of_nat n)). ring.
+    rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega.
+    apply Zdivide_refl.
+  }
+  Local Opaque alignof.
+  induction ty; simpl.
+  apply Zdivide_refl.
+  destruct i; apply Zdivide_refl.
+  apply Zdivide_refl.
+  destruct f; apply Zdivide_refl.
+  apply Zdivide_refl.
+  apply Z.divide_mul_l. auto.
+  apply Zdivide_refl.
+  apply X. apply align_divides. apply alignof_pos.
+  apply X. apply align_divides. apply alignof_pos.
   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. *)
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index ec06cfd..fa54627 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -167,22 +167,18 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data :=
   Return the corresponding list of initialization data. *)
 
 Definition padding (frm to: Z) : list init_data :=
-  let n := to - frm in
-  if zle n 0 then nil else Init_space n :: nil.
+  if zlt frm to then Init_space (to - frm) :: nil else nil.
 
 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 :: padding (Genv.init_data_size d) (sizeof ty))
-  | Init_compound il, Tarray tyelt sz _ =>
-      if zle sz 0 then
+      do d <- transl_init_single ty a; OK (d :: nil)
+  | Init_compound il, Tarray tyelt nelt _ =>
+      if zle nelt 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)
+        transl_init_array tyelt il nelt
   | 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 ef9ec6c..5db4718 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -523,35 +523,36 @@ 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 with (simpl; apply align_le; apply alignof_pos).
-Local Opaque alignof.
+  Genv.init_data_size data = sizeof ty.
+Proof.
   intros. monadInv H. destruct x0. 
   monadInv EQ2.
   destruct ty; try discriminate. 
-  destruct i0; inv EQ2...
-  inv EQ2...
-  inv EQ2...
-  destruct ty; inv EQ2...
+  destruct i0; inv EQ2; auto.
+  inv EQ2; auto.
+  inv EQ2; auto.
+  destruct ty; inv EQ2; auto.
   destruct ty; try discriminate.
-  destruct f0; inv EQ2...
+  destruct f0; inv EQ2; auto.
   destruct ty; try discriminate.
-  destruct i0; inv EQ2...
-  inv EQ2...
-  inv EQ2...
+  destruct i0; auto.
+  inv EQ2.
+  inv EQ2.
+  inv EQ2; auto.
+  inv EQ2.
+  inv EQ2; auto.
+  inv EQ2; auto.
 Qed.
 
 Notation idlsize := Genv.init_data_list_size.
 
 Remark padding_size:
-  forall frm to,
-  frm <= to -> idlsize (padding frm to) = to - frm.
+  forall frm to, frm <= to -> idlsize (padding frm to) = to - frm.
 Proof.
-  intros. unfold padding. 
-  destruct (zle (to - frm) 0). 
+  unfold padding; intros. destruct (zlt frm to). 
+  simpl. xomega. 
   simpl. omega.
-  simpl. rewrite Zmax_spec. rewrite zlt_true. omega. omega.
-Qed. 
+Qed.
 
 Remark idlsize_app:
   forall d1 d2, idlsize (d1 ++ d2) = idlsize d1 + idlsize d2.
@@ -615,22 +616,19 @@ with transl_init_list_size:
    idlsize data = sizeof ty).
 
 Proof.
-  induction i; intros. 
-  (* single *)
-  monadInv H. simpl. rewrite padding_size. omega. eapply transl_init_single_size; eauto.
-  (* compound *)
+- induction i; intros. 
++ (* single *)
+  monadInv H. simpl. erewrite transl_init_single_size by eauto. omega. 
++ (* compound *)
   simpl in H. destruct ty; try discriminate.
-  (* compound array *)
+* (* compound array *)
   set (sz := sizeof (Tarray ty z a)) in *.
-  destruct (zle z 0). inv H. simpl. rewrite Z.max_l. omega. 
+  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 *)
+  unfold sz; simpl. rewrite Z.max_r by omega. 
+  eapply (proj1 (transl_init_list_size il)); eauto.
+* (* compound struct *)
   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. 
@@ -638,7 +636,7 @@ Proof.
   eapply (proj1 (proj2 (transl_init_list_size il))). eauto.
   rewrite sizeof_struct_eq. 2: congruence. 
   apply align_le. apply alignof_pos.
-  (* compound union *)
+* (* compound union *)
   set (sz := sizeof (Tunion i f a)) in *.
   destruct f.
   inv H. simpl. rewrite Z.max_l. omega. generalize (sizeof_pos (Tunion i Fnil a)); unfold sz; omega. 
@@ -647,33 +645,33 @@ Proof.
   eapply Zle_trans. 2: apply align_le. simpl. apply Zmax_bound_l. omega. 
   apply alignof_pos.
 
-  induction il.
-  (* base cases *)
+- induction il.
++ (* base cases *)
   simpl. intuition. 
-  (* arrays *)
+* (* arrays *)
   destruct (zeq sz 0); inv H. simpl. ring. 
-  (* structs *)
+* (* structs *)
   destruct fl; inv H.
-  simpl in H0. generalize (padding_size pos (sizeof ty) H0). omega.
-  (* unions *)
+  simpl in H0. rewrite padding_size by omega. omega. 
+* (* unions *)
   inv H.
-  (* inductive cases *)
-  destruct IHil as [A [B C]]. split.
-  (* arrays *)
++ (* inductive cases *)
+  destruct IHil as [A [B C]]. split; [idtac|split].
+* (* arrays *)
   intros. monadInv H.
-  rewrite idlsize_app. 
+  rewrite idlsize_app.
   rewrite (transl_init_size _ _ _ EQ). 
   rewrite (A _ _ _ EQ1).
   ring.
-  (* structs *)
-  split. intros. simpl in H. destruct fl; monadInv H.
-  repeat rewrite idlsize_app. 
+* (* structs *)
+  intros. simpl in H. destruct fl; monadInv H.
+  rewrite ! idlsize_app. 
   simpl in H0. 
   rewrite padding_size.
   rewrite (transl_init_size _ _ _ EQ). 
   rewrite <- (B _ _ _ _ _ EQ1). omega.
   auto. apply align_le. apply alignof_pos. 
-  (* unions *)
+* (* unions *)
   intros. simpl in H. monadInv H. 
   rewrite idlsize_app.
   rewrite (transl_init_size _ _ _ EQ). 
@@ -754,7 +752,7 @@ Remark store_init_data_list_padding:
   forall frm to b ofs m,
   Genv.store_init_data_list ge m b ofs (padding frm to) = Some m.
 Proof.
-  intros. unfold padding. destruct (zle (to - frm) 0); auto.
+  intros. unfold padding. destruct (zlt frm to); auto. 
 Qed.
 
 Lemma transl_init_sound_gen:
@@ -770,40 +768,34 @@ Lemma transl_init_sound_gen:
    transl_init_struct id ty fl il pos = OK data ->
    Genv.store_init_data_list ge m b (ofs + pos) data = Some m').
 Proof.
+Local Opaque sizeof.
   apply exec_init_scheme; simpl; intros.
-  (* single *)
-  monadInv H3.
-  exploit transl_init_single_steps; eauto. intros. 
-  simpl. rewrite H3. apply store_init_data_list_padding. 
-  (* array *)
+- (* single *)
+  monadInv H3. simpl. erewrite transl_init_single_steps by eauto. auto.
+- (* 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 *)
+- (* struct *)
   destruct fl.
   inv H. inv H1. auto.
   replace ofs with (ofs + 0) by omega. eauto.
-  (* union *)
-  monadInv H1. eapply store_init_data_list_app. eauto. apply store_init_data_list_padding. 
+- (* union *)
+  monadInv H1. eapply store_init_data_list_app. eauto.
+  apply store_init_data_list_padding. 
 
-  (* array, empty *)
+- (* array, empty *)
   inv H. auto.
-  (* array, nonempty *)
+- (* array, nonempty *)
   monadInv H3. 
   eapply store_init_data_list_app.
   eauto.
   rewrite (transl_init_size _ _ _ EQ). eauto.
-
-  (* struct, empty *)
+- (* struct, empty *)
   destruct fl; simpl in H; inv H. 
   inv H0. apply store_init_data_list_padding.
-  (* struct, nonempty *)
+- (* struct, nonempty *)
   destruct fl; simpl in H3; inv H3.
   monadInv H4. 
   eapply store_init_data_list_app. apply store_init_data_list_padding.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 62bbd67..8a26b08 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -764,9 +764,11 @@ Lemma sizeof_by_value:
   access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ty.
 Proof.
   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.
+  assert (size_chunk chunk = sizeof ty).
+  {
+    destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto.
+  }
+  omega.
 Qed.
 
 Definition env_initial_value (e: env) (m: mem) :=
@@ -1046,10 +1048,12 @@ 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_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.aligned_area_inject with (m := m); eauto.
+  apply alignof_blockcopy_1248.
+  apply sizeof_alignof_blockcopy_compat.
+  eapply Mem.aligned_area_inject with (m := m); eauto.
+  apply alignof_blockcopy_1248.
+  apply sizeof_alignof_blockcopy_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.