Enforce minimal safe alignment on global variables

backend/Inlining.v

@@ -12,7 +12,7 @@
 
 (** RTL function inlining *)
 
-Require Import Coqlib Wfsimpl Maps Errors Integers.
+Require Import Coqlib Wfsimpl Maps Errors Integers Memory.
 Require Import AST Linking.
 Require Import Op Registers RTL.
 
@@ -230,17 +230,12 @@ Definition initcontext (dpc dreg nreg: positive) (sz: Z) :=
 
 (** The context used to inline a call to another function. *)
 
-Definition min_alignment (sz: Z) :=
-  if zle sz 1 then 1
-  else if zle sz 2 then 2
-  else if zle sz 4 then 4 else 8.
-
 Definition callcontext (ctx: context)
                       (dpc dreg nreg: positive) (sz: Z)
                       (retpc: node) (retreg: reg) :=
   {| dpc := dpc;
      dreg := dreg;
-     dstk := align (ctx.(dstk) + ctx.(mstk)) (min_alignment sz);
+     dstk := align (ctx.(dstk) + ctx.(mstk)) (min_safe_alignment sz);
      mreg := nreg;
      mstk := Z.max sz 0;
      retinfo := Some (spc ctx retpc, sreg ctx retreg) |}.
@@ -250,7 +245,7 @@ Definition callcontext (ctx: context)
 Definition tailcontext (ctx: context) (dpc dreg nreg: positive) (sz: Z) :=
   {| dpc := dpc;
      dreg := dreg;
-     dstk := align ctx.(dstk) (min_alignment sz);
+     dstk := align ctx.(dstk) (min_safe_alignment sz);
      mreg := nreg;
      mstk := Z.max sz 0;
      retinfo := ctx.(retinfo) |}.

backend/Inliningproof.v

@@ -748,30 +748,6 @@ Proof.
   intros. eapply Mem.perm_free_3; eauto.
 Qed.
 
-Lemma min_alignment_sound:
-  forall sz n, (min_alignment sz | n) -> Mem.inj_offset_aligned n sz.
-Proof.
-  intros; red; intros. unfold min_alignment in H.
-  assert (2 <= sz -> (2 | n)). intros.
-    destruct (zle sz 1). extlia.
-    destruct (zle sz 2). auto.
-    destruct (zle sz 4). apply Z.divide_trans with 4; auto. exists 2; auto.
-    apply Z.divide_trans with 8; auto. exists 4; auto.
-  assert (4 <= sz -> (4 | n)). intros.
-    destruct (zle sz 1). extlia.
-    destruct (zle sz 2). extlia.
-    destruct (zle sz 4). auto.
-    apply Z.divide_trans with 8; auto. exists 2; auto.
-  assert (8 <= sz -> (8 | n)). intros.
-    destruct (zle sz 1). extlia.
-    destruct (zle sz 2). extlia.
-    destruct (zle sz 4). extlia.
-    auto.
-  destruct chunk; simpl in *; auto using Z.divide_1_l.
-  apply H2; lia.
-  apply H2; lia.
-Qed.
-
 (** Preservation by external calls *)
 
 Section EXTCALL.
@@ -843,9 +819,9 @@ Proof.
   intros. inv H.
   (* base *)
   eapply match_stacks_inside_base; eauto. congruence.
-  rewrite H1. rewrite DSTK. apply align_unchanged. apply min_alignment_pos. apply Z.divide_0_r.
+  rewrite H1. rewrite DSTK. apply align_unchanged. apply min_safe_alignment_pos. apply Z.divide_0_r.
   (* inlined *)
-  assert (dstk ctx <= dstk ctx'). rewrite H1. apply align_le. apply min_alignment_pos.
+  assert (dstk ctx <= dstk ctx'). rewrite H1. apply align_le. apply min_safe_alignment_pos.
   eapply match_stacks_inside_inlined; eauto.
   red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; lia. apply H3. inv H4. extlia.
   congruence.
@@ -1071,7 +1047,7 @@ Proof.
   apply agree_val_regs_gen; auto.
   eapply Mem.free_left_inject; eauto.
   red; intros; apply PRIV'.
-    assert (dstk ctx <= dstk ctx'). red in H14; rewrite H14. apply align_le. apply min_alignment_pos.
+    assert (dstk ctx <= dstk ctx'). red in H14; rewrite H14. apply align_le. apply min_safe_alignment_pos.
     lia.
 
 - (* builtin *)
@@ -1210,7 +1186,7 @@ Proof.
     eapply range_private_perms; eauto. extlia.
     (* offset is aligned *)
     replace (fn_stacksize f - 0) with (fn_stacksize f) by lia.
-    inv FB. apply min_alignment_sound; auto.
+    inv FB. red; intros. eapply Z.divide_trans; eauto. apply min_safe_alignment_sound; auto.
     (* nobody maps to (sp, dstk ctx...) *)
     intros. exploit (PRIV (ofs + delta')); eauto. extlia.
     intros [A B]. eelim B; eauto.

backend/Inliningspec.v

@@ -12,7 +12,7 @@
 
 (** RTL function inlining: relational specification *)
 
-Require Import Coqlib Wfsimpl Maps Errors Integers.
+Require Import Coqlib Wfsimpl Maps Errors Integers Memory.
 Require Import AST Linking.
 Require Import Op Registers RTL.
 Require Import Inlining.
@@ -256,7 +256,7 @@ Definition context_stack_call (ctx1 ctx2: context): Prop :=
   ctx1.(mstk) >= 0 /\ ctx1.(dstk) + ctx1.(mstk) <= ctx2.(dstk).
 
 Definition context_stack_tailcall (ctx1: context) (f: function) (ctx2: context) : Prop :=
-  ctx2.(dstk) = align ctx1.(dstk) (min_alignment f.(fn_stacksize)).
+  ctx2.(dstk) = align ctx1.(dstk) (min_safe_alignment f.(fn_stacksize)).
 
 Section INLINING_BODY_SPEC.
 
@@ -332,7 +332,7 @@ with tr_funbody: context -> function -> code -> Prop :=
       (forall r, In r f.(fn_params) -> Ple r ctx.(mreg)) ->
       (forall pc i, f.(fn_code)!pc = Some i -> tr_instr ctx pc i c) ->
       ctx.(mstk) = Z.max f.(fn_stacksize) 0 ->
-      (min_alignment f.(fn_stacksize) | ctx.(dstk)) ->
+      (min_safe_alignment f.(fn_stacksize) | ctx.(dstk)) ->
       ctx.(dstk) >= 0 -> ctx.(dstk) + ctx.(mstk) <= stacksize ->
       tr_funbody ctx f c.
 
@@ -454,19 +454,12 @@ Hypothesis rec_spec:
   Ple (Pos.add ctx.(dreg) ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 ->
   ctx.(mstk) = Z.max (fn_stacksize f) 0 ->
-  (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
+  (min_safe_alignment (fn_stacksize f) | ctx.(dstk)) ->
   ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
   (forall pc, Ple ctx.(dpc) pc -> Plt pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) ->
   tr_funbody ctx f c.
 
-Remark min_alignment_pos:
-  forall sz, min_alignment sz > 0.
-Proof.
-  intros; unfold min_alignment.
-  destruct (zle sz 1). lia. destruct (zle sz 2). lia. destruct (zle sz 4); lia.
-Qed.
-
 Ltac inv_incr :=
   match goal with
   | [ H: sincr _ _ |- _ ] => destruct H; inv_incr
@@ -508,14 +501,14 @@ Proof.
     simpl. subst s2; simpl in *; extlia.
     simpl. subst s3; simpl in *; extlia.
     simpl. extlia.
-    simpl. apply align_divides. apply min_alignment_pos.
-    assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. lia.
+    simpl. apply align_divides. apply min_safe_alignment_pos.
+    assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_safe_alignment_pos. lia.
     lia.
     intros. simpl in H. rewrite S1.
     transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; extlia.
     eapply add_moves_unchanged; eauto. unfold node in *; extlia. extlia.
   red; simpl. subst s2; simpl in *. extlia.
-  red; simpl. split. auto. apply align_le. apply min_alignment_pos.
+  red; simpl. split. auto. apply align_le. apply min_safe_alignment_pos.
 (* tailcall *)
   destruct (can_inline fe s1) as [|id f P Q].
   (* not inlined *)
@@ -538,8 +531,8 @@ Proof.
     simpl. subst s3; simpl in *. subst s2; simpl in *. extlia.
     simpl. subst s3; simpl in *; extlia.
     simpl. extlia.
-    simpl. apply align_divides. apply min_alignment_pos.
-    assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. lia.
+    simpl. apply align_divides. apply min_safe_alignment_pos.
+    assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_safe_alignment_pos. lia.
     lia.
     intros. simpl in H. rewrite S1.
     transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; extlia.
@@ -612,7 +605,7 @@ Lemma expand_cfg_rec_spec:
   Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 ->
   ctx.(mstk) = Z.max (fn_stacksize f) 0 ->
-  (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
+  (min_safe_alignment (fn_stacksize f) | ctx.(dstk)) ->
   ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
   (forall pc', Ple ctx.(dpc) pc' -> Plt pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
@@ -665,7 +658,7 @@ Lemma expand_cfg_spec:
   Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 ->
   ctx.(mstk) = Z.max (fn_stacksize f) 0 ->
-  (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
+  (min_safe_alignment (fn_stacksize f) | ctx.(dstk)) ->
   ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
   (forall pc', Ple ctx.(dpc) pc' -> Plt pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->

cfrontend/C2C.ml

@@ -1270,7 +1270,8 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
   Debug.atom_global id id';
   let ty' = convertTyp env ty in
   let sz = Ctypes.sizeof !comp_env ty' in
-  let al = Ctypes.alignof !comp_env ty' in
+  let al =
+    Z.max (Ctypes.alignof !comp_env ty') (Memdata.min_safe_alignment sz) in
   let attr = Cutil.attributes_of_type env ty in
   let init' =
     match optinit with

cfrontend/Cminorgen.v

@@ -13,7 +13,7 @@
 (** Translation from Csharpminor to Cminor. *)
 
 From Coq Require Import FSets FSetAVL Orders Mergesort.
-Require Import Coqlib Maps Ordered Errors Integers Floats.
+Require Import Coqlib Maps Ordered Errors Integers Floats Memory.
 Require Import AST Linking.
 Require Import Csharpminor Cminor.
 
@@ -216,16 +216,11 @@ with transl_lblstmt (cenv: compilenv) (xenv: exit_env) (ls: Csharpminor.lbl_stmt
   allocated a slot in the Cminor stack data.  Sufficient padding is
   inserted to ensure adequate alignment of addresses. *)
 
-Definition block_alignment (sz: Z) : Z :=
-  if zlt sz 2 then 1
-  else if zlt sz 4 then 2
-  else if zlt sz 8 then 4 else 8.
-
 Definition assign_variable
     (cenv_stacksize: compilenv * Z) (id_sz: ident * Z) : compilenv * Z :=
   let (id, sz) := id_sz in
   let (cenv, stacksize) := cenv_stacksize in
-  let ofs := align stacksize (block_alignment sz) in
+  let ofs := align stacksize (min_safe_alignment sz) in
   (PTree.set id ofs cenv, ofs + Z.max 0 sz).
 
 Definition assign_variables (cenv_stacksize: compilenv * Z) (vars: list (ident * Z)) : compilenv * Z :=

cfrontend/Cminorgenproof.v

@@ -885,21 +885,12 @@ Qed.
 
 (** Properties of the compilation environment produced by [build_compilenv] *)
 
-Remark block_alignment_pos:
-  forall sz, block_alignment sz > 0.
-Proof.
-  unfold block_alignment; intros.
-  destruct (zlt sz 2). lia.
-  destruct (zlt sz 4). lia.
-  destruct (zlt sz 8); lia.
-Qed.
-
 Remark assign_variable_incr:
   forall id sz cenv stksz cenv' stksz',
   assign_variable (cenv, stksz) (id, sz) = (cenv', stksz') -> stksz <= stksz'.
 Proof.
   simpl; intros. inv H.
-  generalize (align_le stksz (block_alignment sz) (block_alignment_pos sz)).
+  generalize (align_le stksz (min_safe_alignment sz) (min_safe_alignment_pos sz)).
   assert (0 <= Z.max 0 sz). apply Zmax_bound_l. lia.
   lia.
 Qed.
@@ -919,35 +910,22 @@ Qed.
 
 Remark inj_offset_aligned_block:
   forall stacksize sz,
-  Mem.inj_offset_aligned (align stacksize (block_alignment sz)) sz.
+  Mem.inj_offset_aligned (align stacksize (min_safe_alignment sz)) sz.
 Proof.
-  intros; red; intros.
-  apply Z.divide_trans with (block_alignment sz).
-  unfold align_chunk.  unfold block_alignment.
-  generalize Z.divide_1_l; intro.
-  generalize Z.divide_refl; intro.
-  assert (2 | 4). exists 2; auto.
-  assert (2 | 8). exists 4; auto.
-  assert (4 | 8). exists 2; auto.
-  destruct (zlt sz 2).
-  destruct chunk; simpl in *; auto; extlia.
-  destruct (zlt sz 4).
-  destruct chunk; simpl in *; auto; extlia.
-  destruct (zlt sz 8).
-  destruct chunk; simpl in *; auto; extlia.
-  destruct chunk; simpl; auto.
-  apply align_divides. apply block_alignment_pos.
+  intros; red; intros. eapply Z.divide_trans.
+  apply min_safe_alignment_sound; eauto.
+  apply align_divides. apply min_safe_alignment_pos.
 Qed.
 
 Remark inj_offset_aligned_block':
   forall stacksize sz,
-  Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Z.max 0 sz).
+  Mem.inj_offset_aligned (align stacksize (min_safe_alignment sz)) (Z.max 0 sz).
 Proof.
   intros.
-  replace (block_alignment sz) with (block_alignment (Z.max 0 sz)).
+  replace (min_safe_alignment sz) with (min_safe_alignment (Z.max 0 sz)).
   apply inj_offset_aligned_block.
   rewrite Zmax_spec. destruct (zlt sz 0); auto.
-  transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. lia.
+  transitivity 1. reflexivity. unfold min_safe_alignment. rewrite zlt_true. auto. lia.
 Qed.
 
 Lemma assign_variable_sound:
@@ -962,21 +940,22 @@ Lemma assign_variable_sound:
 Proof.
   unfold assign_variable; intros until vars; intros ASV NOREPET POS COMPAT SEP.
   inv ASV.
-  assert (LE: sz1 <= align sz1 (block_alignment sz)). apply align_le. apply block_alignment_pos.
+  assert (LE: sz1 <= align sz1 (min_safe_alignment sz)).
+  { apply align_le. apply min_safe_alignment_pos. }
   assert (EITHER: forall id' sz',
              In (id', sz') (vars ++ (id, sz) :: nil) ->
              In (id', sz') vars /\ id' <> id \/ (id', sz') = (id, sz)).
-    intros. rewrite in_app in H. destruct H.
+  { intros. rewrite in_app in H. destruct H.
     left; split; auto. red; intros; subst id'. elim NOREPET.
     change id with (fst (id, sz')). apply in_map; auto.
-    simpl in H. destruct H. auto. contradiction.
+    simpl in H. destruct H. auto. contradiction. }
   split; red; intros.
   apply EITHER in H. destruct H as [[P Q] | P].
   exploit COMPAT; eauto. intros [ofs [A [B [C D]]]].
   exists ofs.
   split. rewrite PTree.gso; auto.
   split. auto. split. auto. zify; lia.
-  inv P. exists (align sz1 (block_alignment sz)).
+  inv P. exists (align sz1 (min_safe_alignment sz)).
   split. apply PTree.gss.
   split. apply inj_offset_aligned_block.
   split. lia.

common/Memdata.v

@@ -126,6 +126,39 @@ Proof.
         | exists 8; reflexivity ].
 Qed.
 
+(** Given the size [sz] of a block, [min_safe_alignment sz] is the minimum
+    alignment that guarantees that all valid memory accesses in the block
+    have at least this alignment.  *)
+
+Definition min_safe_alignment (sz: Z) : Z :=
+  if zlt sz 2 then 1
+  else if zlt sz 4 then 2
+  else if zlt sz 8 then 4 else 8.
+
+Lemma min_safe_alignment_pos: forall sz,
+  min_safe_alignment sz > 0.
+Proof.
+  intros; unfold min_safe_alignment. repeat (destruct zlt); lia.
+Qed.
+
+Lemma min_safe_alignment_sound: forall sz chunk,
+  size_chunk chunk <= sz -> (align_chunk chunk | min_safe_alignment sz).
+Proof.
+  intros. exists (min_safe_alignment sz / align_chunk chunk).
+  unfold size_chunk, align_chunk, min_safe_alignment in *.
+  repeat destruct zlt; destruct chunk; reflexivity || lia.
+Qed.
+
+Lemma min_safe_alignment_8: forall sz,
+  (min_safe_alignment sz | 8).
+Proof.
+  intros. exists (8 / min_safe_alignment sz).
+  unfold min_safe_alignment. repeat destruct zlt; reflexivity.
+Qed.
+
+(** Memory quantities are a coarser variant of memory chunks, used to represent
+    the size of a pointer (32 or 64 bits). *)
+
 Inductive quantity : Type := Q32 | Q64.
 
 Definition quantity_eq (q1 q2: quantity) : {q1 = q2} + {q1 <> q2}.

lib/Camlcoq.ml

@@ -179,6 +179,8 @@ module Z = struct
   let le x y = (Z.compare x y <> Gt)
   let ge x y = (Z.compare x y <> Lt)
   let compare x y = match Z.compare x y with Lt -> -1 | Eq -> 0 | Gt -> 1
+  let max = Z.max
+  let min = Z.min
 
   let to_int = function
   | Z0 -> 0