Skip to content

Commit 4ff1b27

Browse files
committed
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.
1 parent e1ffc63 commit 4ff1b27

1 file changed

Lines changed: 2 additions & 1 deletion

File tree

cfrontend/C2C.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1270,7 +1270,8 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
12701270
Debug.atom_global id id';
12711271
let ty' = convertTyp env ty in
12721272
let sz = Ctypes.sizeof !comp_env ty' in
1273-
let al = Ctypes.alignof !comp_env ty' in
1273+
let al =
1274+
Z.max (Ctypes.alignof !comp_env ty') (Memdata.min_safe_alignment sz) in
12741275
let attr = Cutil.attributes_of_type env ty in
12751276
let init' =
12761277
match optinit with

0 commit comments

Comments
 (0)