From 8ef73e70ceb3299d5c2e580c5ceb0d059bb350f1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Apr 2026 14:27:52 +0200 Subject: [PATCH 1/3] Introduce and use `Memdata.min_safe_alignment` This computation (of the minimal alignment for a block of a given size) used to be done in Cminorgen, but it's generally useful. --- cfrontend/Cminorgen.v | 9 ++------ cfrontend/Cminorgenproof.v | 47 +++++++++++--------------------------- common/Memdata.v | 33 ++++++++++++++++++++++++++ 3 files changed, 48 insertions(+), 41 deletions(-) diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index bfab7f098..7b59299c2 100644 --- a/cfrontend/Cminorgen.v +++ b/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 := diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 8f09febb7..53361409d 100644 --- a/cfrontend/Cminorgenproof.v +++ b/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. apply Z.divide_trans with (min_safe_alignment sz). +- apply min_safe_alignment_safe; auto. +- 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. diff --git a/common/Memdata.v b/common/Memdata.v index be8783d74..64e79d8f8 100644 --- a/common/Memdata.v +++ b/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_safe: forall sz chunk, + size_chunk chunk <= sz -> (align_chunk chunk | min_safe_alignment sz). +Proof. + intros. + generalize Z.divide_1_l Z.divide_refl; intros. + assert (2 | 4) by (exists 2; auto). + assert (2 | 8) by (exists 4; auto). + assert (4 | 8) by (exists 2; auto). + unfold size_chunk, align_chunk, min_safe_alignment in *. + destruct (zlt sz 2). destruct chunk; auto; lia. + destruct (zlt sz 4). destruct chunk; auto; lia. + destruct (zlt sz 8). destruct chunk; auto; lia. + destruct chunk; auto. +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}. From 492f9f4a4474cca041f277b195b26366dbde0813 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Apr 2026 15:24:28 +0200 Subject: [PATCH 2/3] Camlcoq: export Z.min, Z.max --- lib/Camlcoq.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index ad314e42a..48f6b9171 100644 --- a/lib/Camlcoq.ml +++ b/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 From 777d600608bb0bccc0ccd65e2bfc444026c666eb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Apr 2026 15:28:50 +0200 Subject: [PATCH 3/3] Enforce minimal safe alignment on global variables Currently, global variables are aligned according to their C types, e.g. `char c[4];` has alignment 1. However, the CompCert C semantics make it possible to cast `c` to `int *` and dereference this pointer, which requires 4-alignment of `c` to be safe on all platforms. This commit makes sure that the alignment of a global variable is at least the minimal safe alignment for its size, as defined in `Memdata.min_safe_alignment`. This ensures that any memory access (at offset 0) that fits within the bounds of the variable is aligned. Without `_Alignas` modifiers, the alignment of a C type is always <= the minimal safe alignment of the size of the type. However, `_Alignas` modifiers can increase the C alignment beyond the minimal safe alignment. We use the greater of the two alignments. --- cfrontend/C2C.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 3f36bffeb..37a8790c4 100644 --- a/cfrontend/C2C.ml +++ b/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