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. --- cparser/Elab.ml | 52 +++++++++++++++++++++++++++++++++++----------------- 1 file changed, 35 insertions(+), 17 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 173d3e03..5f785c04 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -495,36 +495,54 @@ let elab_gcc_attr loc env = function let is_power_of_two n = n > 0L && Int64.logand n (Int64.pred n) = 0L -let extract_alignas loc a = +(* Check alignment parameter *) +let check_alignment loc n = + if not (is_power_of_two n || n = 0L) then begin + error loc "requested alignment %Ld is not a power of 2" n; false + end else + if n <> Int64.of_int (Int64.to_int n) then begin + error loc "requested alignment %Ld is too large" n; false + end else + true + +(* Process GCC attributes that have special significance. Currently we + have two: "aligned" and "packed". *) +let enter_gcc_attr loc a = match a with | Attr(("aligned"|"__aligned__"), args) -> begin match args with - | [AInt n] when is_power_of_two n || n = 0L -> AAlignas (Int64.to_int n) - | [AInt n] -> error loc "requested alignment is not a power of 2"; a - | [_] -> error loc "requested alignment is not an integer constant"; a - | [] -> a (* Use the default alignment as the gcc does *) - | _ -> error loc "'aligned' attribute takes no more than 1 argument"; a + | [AInt n] -> + if check_alignment loc n then [AAlignas (Int64.to_int n)] else [] + | [_] -> error loc "requested alignment is not an integer constant"; [] + | [] -> [] (* Use default alignment, like gcc does *) + | _ -> error loc "'aligned' attribute takes no more than 1 argument"; [] end - | _ -> a + | Attr(("packed"|"__packed__"), args) -> + begin match args with + | [] -> [a] + | [AInt n] -> if check_alignment loc n then [a] else [] + | [AInt n; AInt p] -> + if check_alignment loc n && check_alignment loc p then [a] else [] + | [AInt n; AInt p; AInt q] -> + if check_alignment loc n && check_alignment loc p then [a] else [] + | _ -> error loc "ill-formed 'packed' attribute"; [] + end + | _ -> [a] let elab_attribute env = function | GCC_ATTR (l, loc) -> List.fold_left add_attributes [] - (List.map (fun attr -> [attr]) - (List.map (extract_alignas loc) - (List.flatten - (List.map (elab_gcc_attr loc env) l)))) + (List.map (enter_gcc_attr loc) + (List.flatten + (List.map (elab_gcc_attr loc env) l))) | PACKED_ATTR (args, loc) -> - [Attr("__packed__", List.map (elab_attr_arg loc env) args)] + enter_gcc_attr loc + (Attr("__packed__", List.map (elab_attr_arg loc env) args)) | ALIGNAS_ATTR ([a], loc) -> warning loc Celeven_extension "'_Alignas' is a C11 extension"; begin match elab_attr_arg loc env a with | AInt n -> - if is_power_of_two n || n = 0L then - [AAlignas (Int64.to_int n)] - else begin - error loc "requested alignment is not a power of 2"; [] - end + if check_alignment loc n then [AAlignas (Int64.to_int n)] else [] | _ -> error loc "requested alignment is not an integer constant"; [] | exception Wrong_attr_arg -> error loc "bad _Alignas value"; [] end -- cgit