From 999bea31a252dae1b0709166cf3c9540bda9dbb0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 17 Aug 2018 10:35:59 +0200 Subject: Issue with packed structs and sizeof, alignof, offsetof in cparser/ CompCert has two implementations of sizeof, alignof and offsetof (byte offset of a struct field): - the reference implementation, in Coq, from cfrontend/Ctypes.v - the implementation used during elaboration, in OCaml, from cparser/Cutil.ml The reference Coq implementation is used as much as possible, but sometimes during elaboration the size of a type must be computed (e.g. to compute array sizes), or the offset of a field (e.g. to evaluate __builtin_offsetof), in which case the OCaml implementation is used. This causes issues with packed structs. Currently, the cparser/Cutil.ml functions ignore the "packed" attribute on structs. Their results disagree with the "true" sizes, alignments and offsets computed by the cfrontend/Ctypes.v functions after source-to-source transformation of packed structs as done in cparser/PackedStruct.ml. For example: ``` struct __packed__(1) s { char c; short s; int i; }; assert (__builtin_offsetof(struct s, i) == 3); assert (sizeof(struct s) = sizeof(char[sizeof(struct s)])); ``` The two assertions fail. In the first assertion, __builtin_offsetof is elaborated to 4, because the packed attribute is ignored during elaboration. In the second assertion, the type `char[sizeof(struct s)]` is elaborated to `char[8]`, again because the packed attribute is ignored during elaboration, while the other `sizeof(struct s)` is computed as 7 after the source-to-source transformation of packed structs. This commit changes the cparser/Cutil.ml functions so that they take the packed attribute into account when computing sizeof, alignof, offsetof, and struct_layout. Related changes: * cparser/Cutil: add `packing_parameters` function to extract packing info from attributes * cparser/Cutil: refactor and share more code between sizeof_struct, offsetof, and struct_layout * cparser/Elab: check the alignment parameters given in packed attributes. (The check was previously done in cparser/PackedStruct.ml but now it would come too late.) * cparser/Elab: refactor the checking of alignment parameters between _Alignas, attribute((aligned)), __packed__, and attribute((packed)). * cparser/PackedStructs: simplify the code, some functionality was moved to cparser/Cutil, other to cparser/Elab * cfrontend/C2C: raise an "unsupported" error if a packed struct is defined and -fpacked-structs is not given. Before, the packed attribute would be silently ignored, but now doing so would cause inconsistencies between cfrontend/ and cparser/. * test/regression/packedstruct1.c: add tests to compare the sizes and the offsets produced by the elaborator with those obtained after elaboration. --- cfrontend/C2C.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index ce1f2c0e..ecaffbc6 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -610,9 +610,11 @@ let convertField env f = (intern_string f.fld_name, convertTyp env f.fld_typ) let convertCompositedef env su id attr members = + if Cutil.find_custom_attributes ["packed";"__packed__"] attr <> [] then + unsupported "packed struct (consider adding option -fpacked-structs)"; let t = match su with | C.Struct -> - let layout = Cutil.struct_layout env members in + let layout = Cutil.struct_layout env attr members in List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout; TStruct (id,attr) | C.Union -> TUnion (id,attr) in -- cgit