diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-08-17 10:35:59 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-08-17 14:01:08 +0200 |
commit | 999bea31a252dae1b0709166cf3c9540bda9dbb0 (patch) | |
tree | 7f203b9f97dcd398807d19c0dbeec866b0a63e1f /cparser/PackedStructs.ml | |
parent | 11837beafc84f226878b4706a791e9c13301e01f (diff) | |
download | compcert-kvx-999bea31a252dae1b0709166cf3c9540bda9dbb0.tar.gz compcert-kvx-999bea31a252dae1b0709166cf3c9540bda9dbb0.zip |
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.
Diffstat (limited to 'cparser/PackedStructs.ml')
-rw-r--r-- | cparser/PackedStructs.ml | 44 |
1 files changed, 15 insertions, 29 deletions
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index e1287eb8..a2c91c0a 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -81,47 +81,33 @@ let transf_field_decl mfa swapped loc env struct_id f = (* Rewriting struct declarations *) let transf_struct_decl mfa msa swapped loc env struct_id attrs ml = + let attrs' = + remove_custom_attributes ["packed";"__packed__"] attrs in let ml' = List.map (transf_field_decl mfa swapped loc env struct_id) ml in - if msa = 0 then (attrs, ml') else begin - let al' = (* natural alignment of the transformed struct *) - List.fold_left - (fun a f' -> max a (safe_alignof loc env f'.fld_typ)) - 1 ml' in - (set_alignas_attr (max msa al') attrs, ml') + if msa = 0 then (attrs', ml') else begin + (* [Cutil.composite_info_def] takes packing parameters into account. + Hence the alignment it returns is the correct alignment for + the transformed struct. *) + let ci = Cutil.composite_info_def env Struct attrs ml in + match ci.ci_alignof with + | None -> error loc "incomplete struct"; (attrs', ml') + | Some al -> (set_alignas_attr al attrs', ml') end (* Rewriting composite declarations *) -let is_pow2 n = n > 0 && n land (n - 1) = 0 - -let packed_param_value loc n = - let m = Int64.to_int n in - if n <> Int64.of_int m then - (error loc "__packed__ parameter `%Ld' is too large" n; 0) - else if m = 0 || is_pow2 m then - m - else - (error loc "__packed__ parameter `%Ld' must be a power of 2" n; 0) - let transf_composite loc env su id attrs ml = match su with | Union -> (attrs, ml) | Struct -> let (mfa, msa, swapped) = match find_custom_attributes ["packed";"__packed__"] attrs with - | [] -> (0L, 0L, false) - | [[]] -> (1L, 0L, false) - | [[AInt n]] -> (n, 0L, false) - | [[AInt n; AInt p]] -> (n, p, false) - | [[AInt n; AInt p; AInt q]] -> (n, p, q <> 0L) - | _ -> - error loc "ill-formed or ambiguous __packed__ attribute"; - (0L, 0L, false) in - let mfa = packed_param_value loc mfa in - let msa = packed_param_value loc msa in - let attrs' = remove_custom_attributes ["packed";"__packed__"] attrs in - transf_struct_decl mfa msa swapped loc env id attrs' ml + | [] -> (0, 0, false) + | [_] -> Cutil.packing_parameters attrs + | _ -> error loc "multiple __packed__ attributes"; + (0, 0, false) in + transf_struct_decl mfa msa swapped loc env id attrs ml (* Accessor functions *) |