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. --- test/regression/Results/packedstruct1-32 | 12 +++++++++ test/regression/Results/packedstruct1-64 | 12 +++++++++ test/regression/packedstruct1.c | 42 +++++++++++++++++++++++++++----- 3 files changed, 60 insertions(+), 6 deletions(-) (limited to 'test/regression') diff --git a/test/regression/Results/packedstruct1-32 b/test/regression/Results/packedstruct1-32 index e4bca769..e7d1c296 100644 --- a/test/regression/Results/packedstruct1-32 +++ b/test/regression/Results/packedstruct1-32 @@ -1,25 +1,37 @@ sizeof(struct s1) = 14 +precomputed sizeof(struct s1) = 14 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 +precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 s1 = {x = 123, y = -456, z = 3.14159} sizeof(struct s2) = 16 +precomputed sizeof(struct s2) = 16 &s2 mod 16 = 0 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 +precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 s2 = {x = 57, y = -456, z = 3.14159} sizeof(struct s3) = 31 +precomputed sizeof(struct s3) = 31 offsetof(s) = 29 +precomputed offsetof(s) = 29 s3 = {x = 123, y = 45678, z = 2147483649, v = -456, w = -1234567, p is ok, t = {111,222,333}, s = {'o','k'}} sizeof(struct s4) = 16 +precomputed sizeof(struct s4) = 16 offsetof(x) = 0, offsetof(y) = 4, offsetof(z) = 8 +precomputed offsetof(x) = 0, offsetof(y) = 4, offsetof(z) = 8 s4 = {x = 123, y = -456, z = 3.14159} sizeof(struct s5) = 14 +precomputed sizeof(struct s5) = 14 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 +precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 s5 = {x = 123, y = -456, z = 3.14159} sizeof(struct s6) = 14 +precomputed sizeof(struct s6) = 14 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 +precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 s62 = {x = 123, y = -456, z = 3.14159} diff --git a/test/regression/Results/packedstruct1-64 b/test/regression/Results/packedstruct1-64 index c2a8bcd2..d255595f 100644 --- a/test/regression/Results/packedstruct1-64 +++ b/test/regression/Results/packedstruct1-64 @@ -1,25 +1,37 @@ sizeof(struct s1) = 14 +precomputed sizeof(struct s1) = 14 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 +precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 s1 = {x = 123, y = -456, z = 3.14159} sizeof(struct s2) = 16 +precomputed sizeof(struct s2) = 16 &s2 mod 16 = 0 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 +precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 s2 = {x = 57, y = -456, z = 3.14159} sizeof(struct s3) = 35 +precomputed sizeof(struct s3) = 35 offsetof(s) = 33 +precomputed offsetof(s) = 33 s3 = {x = 123, y = 45678, z = 2147483649, v = -456, w = -1234567, p is ok, t = {111,222,333}, s = {'o','k'}} sizeof(struct s4) = 16 +precomputed sizeof(struct s4) = 16 offsetof(x) = 0, offsetof(y) = 4, offsetof(z) = 8 +precomputed offsetof(x) = 0, offsetof(y) = 4, offsetof(z) = 8 s4 = {x = 123, y = -456, z = 3.14159} sizeof(struct s5) = 14 +precomputed sizeof(struct s5) = 14 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 +precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 s5 = {x = 123, y = -456, z = 3.14159} sizeof(struct s6) = 14 +precomputed sizeof(struct s6) = 14 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 +precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6 s62 = {x = 123, y = -456, z = 3.14159} diff --git a/test/regression/packedstruct1.c b/test/regression/packedstruct1.c index 8b138dd4..5d3e7124 100644 --- a/test/regression/packedstruct1.c +++ b/test/regression/packedstruct1.c @@ -2,8 +2,18 @@ #include +/* offsetof is the offset computed by the verified front-end (cfrontend/) */ #define offsetof(s,f) (int)&(((struct s *)0)->f) +/* boffsetof is the offset computed by the elaborator (cparser/) */ +#define boffsetof(s,f) (int)__builtin_offsetof(struct s, f) + +/* szof is the size computed by the verified front-end (cfrontend/) */ +#define szof(s) (int) sizeof(struct s) + +/* bszof is the size computed by the elaborator (cparser/) */ +#define bszof(s) (int) sizeof(char [sizeof(struct s)]) + /* Simple packing */ struct __packed__(1) s1 { unsigned short x; int y; double z; }; @@ -11,9 +21,12 @@ struct __packed__(1) s1 { unsigned short x; int y; double z; }; void test1(void) { struct s1 s1; - printf("sizeof(struct s1) = %d\n", sizeof(struct s1)); + printf("sizeof(struct s1) = %d\n", szof(s1)); + printf("precomputed sizeof(struct s1) = %d\n", bszof(s1)); printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n", offsetof(s1,x), offsetof(s1,y), offsetof(s1,z)); + printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n", + boffsetof(s1,x), boffsetof(s1,y), boffsetof(s1,z)); s1.x = 123; s1.y = -456; s1.z = 3.14159; printf("s1 = {x = %d, y = %d, z = %.5f}\n\n", s1.x, s1.y, s1.z); } @@ -28,10 +41,13 @@ struct s2 s2; void test2(void) { - printf("sizeof(struct s2) = %d\n", sizeof(struct s2)); + printf("sizeof(struct s2) = %d\n", szof(s2)); + printf("precomputed sizeof(struct s2) = %d\n", bszof(s2)); printf("&s2 mod 16 = %d\n", ((int) &s2) & 0xF); printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n", offsetof(s2,x), offsetof(s2,y), offsetof(s2,z)); + printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n", + boffsetof(s2,x), boffsetof(s2,y), boffsetof(s2,z)); s2.x = 12345; s2.y = -456; s2.z = 3.14159; printf("s2 = {x = %d, y = %d, z = %.5f}\n\n", s2.x, s2.y, s2.z); } @@ -55,8 +71,10 @@ void test3(void) { char xx; - printf("sizeof(struct s3) = %d\n", sizeof(struct s3)); + printf("sizeof(struct s3) = %d\n", szof(s3)); + printf("precomputed sizeof(struct s3) = %d\n", bszof(s3)); printf("offsetof(s) = %d\n", offsetof(s3,s)); + printf("precomputed offsetof(s) = %d\n", boffsetof(s3,s)); s3.x = 123; s3.y = 45678; s3.z = 0x80000001U; @@ -82,9 +100,13 @@ struct s4 { unsigned short x; int y; double z; }; void test4(void) { struct s4 s4; - printf("sizeof(struct s4) = %d\n", sizeof(struct s4)); + + printf("sizeof(struct s4) = %d\n", szof(s4)); + printf("precomputed sizeof(struct s4) = %d\n", bszof(s4)); printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n", offsetof(s4,x), offsetof(s4,y), offsetof(s4,z)); + printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n", + boffsetof(s4,x), boffsetof(s4,y), boffsetof(s4,z)); s4.x = 123; s4.y = -456; s4.z = 3.14159; printf("s4 = {x = %d, y = %d, z = %.5f}\n\n", s4.x, s4.y, s4.z); } @@ -96,9 +118,13 @@ struct __attribute((packed)) s5 { unsigned short x; int y; double z; }; void test5(void) { struct s5 s5; - printf("sizeof(struct s5) = %d\n", sizeof(struct s5)); + + printf("sizeof(struct s5) = %d\n", szof(s5)); + printf("precomputed sizeof(struct s5) = %d\n", bszof(s5)); printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n", offsetof(s5,x), offsetof(s5,y), offsetof(s5,z)); + printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n", + boffsetof(s5,x), boffsetof(s5,y), boffsetof(s5,z)); s5.x = 123; s5.y = -456; s5.z = 3.14159; printf("s5 = {x = %d, y = %d, z = %.5f}\n\n", s5.x, s5.y, s5.z); } @@ -110,9 +136,13 @@ struct s6 { unsigned short x; int y; double z; } __attribute((packed)) const s6 void test6(void) { struct s6 s62; - printf("sizeof(struct s6) = %d\n", sizeof(struct s6)); + + printf("sizeof(struct s6) = %d\n", szof(s6)); + printf("precomputed sizeof(struct s6) = %d\n", bszof(s6)); printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n", offsetof(s6,x), offsetof(s6,y), offsetof(s6,z)); + printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n", + boffsetof(s6,x), boffsetof(s6,y), boffsetof(s6,z)); s62.x = 123; s62.y = -456; s62.z = 3.14159; printf("s62 = {x = %d, y = %d, z = %.5f}\n\n", s62.x, s62.y, s62.z); } -- cgit