From 1d93fa1d7c639ace232fbb05217e51a6e6090904 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 9 Jun 2018 16:19:34 +0100 Subject: [PATCH] Visual Studio packs bit-fields differently --- appveyor.yml | 1 - buildspec-windows.yml | 1 - regression/ansi-c/Struct_Padding3/main.c | 9 +- regression/ansi-c/Struct_Padding4/main.c | 132 +++++++++-- regression/ansi-c/Struct_Padding5/main.c | 40 ++++ regression/ansi-c/Union_Padding1/main.c | 32 +-- src/ansi-c/padding.cpp | 275 ++++++++++++++++++----- 7 files changed, 398 insertions(+), 92 deletions(-) diff --git a/appveyor.yml b/appveyor.yml index 2144555099..feaa7dc182 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -70,7 +70,6 @@ test_script: rmdir /s /q ansi-c\arch_flags_mthumb_good rmdir /s /q ansi-c\Forward_Declaration2 rmdir /s /q ansi-c\Incomplete_Type1 - rmdir /s /q ansi-c\Union_Padding1 rmdir /s /q ansi-c\Universal_characters1 rmdir /s /q ansi-c\gcc_attributes7 rmdir /s /q ansi-c\gcc_version1 diff --git a/buildspec-windows.yml b/buildspec-windows.yml index 810e149cb8..40213977cd 100644 --- a/buildspec-windows.yml +++ b/buildspec-windows.yml @@ -34,7 +34,6 @@ phases: Remove-Item ansi-c\arch_flags_mthumb_good -Force -Recurse Remove-Item ansi-c\Forward_Declaration2 -Force -Recurse Remove-Item ansi-c\Incomplete_Type1 -Force -Recurse - Remove-Item ansi-c\Union_Padding1 -Force -Recurse Remove-Item ansi-c\gcc_attributes7 -Force -Recurse Remove-Item ansi-c\gcc_version1 -Force -Recurse Remove-Item cbmc\Malloc23 -Force -Recurse diff --git a/regression/ansi-c/Struct_Padding3/main.c b/regression/ansi-c/Struct_Padding3/main.c index e74d3e6722..b98cbc0a25 100644 --- a/regression/ansi-c/Struct_Padding3/main.c +++ b/regression/ansi-c/Struct_Padding3/main.c @@ -99,8 +99,8 @@ struct my_struct3 { char ch3; long long i2; // this should be padded for 8-byte alignment char ch4; - int bf1:1; // this should not be padded - int bf2:1; // this should not be padded + int bf1 : 1; // MSVC pads this, the gcc/clang do not + int bf2 : 1; // MSVC pads this, the gcc/clang do not int i3; // this should be padded for 4-byte alignment }; @@ -110,7 +110,12 @@ STATIC_ASSERT(__builtin_offsetof(struct my_struct3, i1)==4); STATIC_ASSERT(__builtin_offsetof(struct my_struct3, ch3)==8); STATIC_ASSERT(__builtin_offsetof(struct my_struct3, i2)==16); STATIC_ASSERT(__builtin_offsetof(struct my_struct3, ch4)==24); + +#ifdef _MSC_VER +STATIC_ASSERT(__builtin_offsetof(struct my_struct3, i3) == 32); +#else STATIC_ASSERT(__builtin_offsetof(struct my_struct3, i3)==28); +#endif int main() { diff --git a/regression/ansi-c/Struct_Padding4/main.c b/regression/ansi-c/Struct_Padding4/main.c index 122ddf21db..5ec1bb6b37 100644 --- a/regression/ansi-c/Struct_Padding4/main.c +++ b/regression/ansi-c/Struct_Padding4/main.c @@ -7,7 +7,39 @@ struct Z1 int i:3; char ch2; // there is end-of-struct padding because of the int -} z1; +}; + +STATIC_ASSERT(_Alignof(struct Z1) == _Alignof(int)); + +#ifdef _MSC_VER +STATIC_ASSERT(sizeof(struct Z1) == 4 + 4 + 4); +#else +STATIC_ASSERT(sizeof(struct Z1) == 1 + 1 + 1 + 1); +#ifdef __GNUC__ +STATIC_ASSERT(__builtin_offsetof(struct Z1, ch2) == 2); +#endif +#endif + +#pragma pack(push, 1) +struct Z1_packed +{ + char ch; + int i : 3; + char ch2; + // there is no end-of-struct padding +}; +#pragma pack(pop) + +STATIC_ASSERT(_Alignof(struct Z1_packed) == 1); + +#ifdef _MSC_VER +STATIC_ASSERT(sizeof(struct Z1_packed) == 1 + 4 + 1); +#else +STATIC_ASSERT(sizeof(struct Z1_packed) == 1 + 1 + 1); +#ifdef __GNUC__ +STATIC_ASSERT(__builtin_offsetof(struct Z1_packed, ch2) == 2); +#endif +#endif struct Z2 { @@ -15,37 +47,111 @@ struct Z2 char i:3; char ch2; // there is no end-of-struct padding -} z2; +}; + +STATIC_ASSERT(sizeof(struct Z2) == 1 + 1 + 1); + +#pragma pack(push, 1) +struct Z2_packed +{ + char ch; + char i : 3; + char ch2; + // there is no end-of-struct padding +}; +#pragma pack(pop) + +STATIC_ASSERT(sizeof(struct Z2_packed) == 1 + 1 + 1); struct Z3 { char ch; - int i:3; // bit-fields do not get padding! -} z3; + int i : 3; // padded by MSVC, not by gcc/clang +}; + +#ifdef _MSC_VER +STATIC_ASSERT(sizeof(struct Z3) == 4 + 4); +#else +STATIC_ASSERT(sizeof(struct Z3) == 1 + 1 + 2); +#endif + +#pragma pack(push, 1) +struct Z3_packed +{ + char ch; + int i : 3; // padded by MSVC, not by gcc/clang +}; +#pragma pack(pop) + +#ifdef _MSC_VER +STATIC_ASSERT(sizeof(struct Z3_packed) == 1 + 4); +#else +STATIC_ASSERT(sizeof(struct Z3_packed) == 1 + 1); +#endif struct Z4 { int i; long long int x; // pads to 8 char ch; // 7 end-of-struct padding -} z4; +}; + +STATIC_ASSERT(sizeof(struct Z4) == 4 + 4 + 8 + 1 + 7); + +#pragma pack(push, 1) +struct Z4_packed +{ + int i; + long long int x; // no padding + char ch; // no end-of-struct padding +}; +#pragma pack(pop) + +STATIC_ASSERT(sizeof(struct Z4_packed) == 4 + 8 + 1); struct Z5 { char ch; long long int x[]; // pads to 8, but has no size -} z5; +}; -STATIC_ASSERT(sizeof(struct Z1)==1+1+1+1); +STATIC_ASSERT(sizeof(struct Z5) == 8); -#ifdef __GNUC__ -STATIC_ASSERT(__builtin_offsetof(struct Z1, ch2)==2); +#pragma pack(push, 1) +struct Z5_packed +{ + char ch; + long long int x[]; // pads to 8, but has no size +}; +#pragma pack(pop) + +STATIC_ASSERT(sizeof(struct Z5_packed) == 1); + +struct Z6 +{ + char ch; + int i : 16; // padded to int by MSVC, to short by gcc/clang +}; + +#ifdef _MSC_VER +STATIC_ASSERT(sizeof(struct Z6) == 4 + 4); +#else +STATIC_ASSERT(sizeof(struct Z6) == 1 + 1 + 2); #endif -STATIC_ASSERT(sizeof(struct Z2)==1+1+1); -STATIC_ASSERT(sizeof(struct Z3)==1+1+2); -STATIC_ASSERT(sizeof(struct Z4)==4+4+8+1+7); -STATIC_ASSERT(sizeof(struct Z5)==8); +#pragma pack(push, 1) +struct Z6_packed +{ + char ch; + int i : 16; // padded to int by MSC, but not aligned +}; +#pragma pack(pop) + +#ifdef _MSC_VER +STATIC_ASSERT(sizeof(struct Z6_packed) == 1 + 4); +#else +STATIC_ASSERT(sizeof(struct Z6_packed) == 1 + 2); +#endif int main() { diff --git a/regression/ansi-c/Struct_Padding5/main.c b/regression/ansi-c/Struct_Padding5/main.c index 397693adff..f53eb7eb79 100644 --- a/regression/ansi-c/Struct_Padding5/main.c +++ b/regression/ansi-c/Struct_Padding5/main.c @@ -28,6 +28,46 @@ STATIC_ASSERT(sizeof(struct flowi)==8); STATIC_ASSERT(__builtin_offsetof(struct flowi, flexible)==1); #endif +// bit-fields are very evil +#pragma pack(push, 1) +struct bit_field0 +{ + int i : 23; +}; + +struct bit_field1 +{ + int i : 1; + unsigned int j : 1; + // in MSC, it matters that the underlying type changes! + short c : 1; +}; + +struct bit_field2 +{ + int i : 23; + char ch; +}; +#pragma pack(pop) + +struct bit_field3 +{ + int i : 23; + char ch; +}; + +#ifdef _MSC_VER +STATIC_ASSERT(sizeof(struct bit_field0) == 4); +STATIC_ASSERT(sizeof(struct bit_field1) == 6); +STATIC_ASSERT(sizeof(struct bit_field2) == 5); +STATIC_ASSERT(sizeof(struct bit_field3) == 8); +#else +STATIC_ASSERT(sizeof(struct bit_field0) == 3); +STATIC_ASSERT(sizeof(struct bit_field1) == 1); +STATIC_ASSERT(sizeof(struct bit_field2) == 4); +STATIC_ASSERT(sizeof(struct bit_field3) == 4); +#endif + int main() { } diff --git a/regression/ansi-c/Union_Padding1/main.c b/regression/ansi-c/Union_Padding1/main.c index 4a5d22a562..6473c5cdaf 100644 --- a/regression/ansi-c/Union_Padding1/main.c +++ b/regression/ansi-c/Union_Padding1/main.c @@ -41,14 +41,16 @@ STATIC_ASSERT(sizeof(union some_union3)==sizeof(int)); #ifdef _MSC_VER // bit-fields are evil -#pragma pack(1) +#pragma pack(push, 1) union some_union4 { int i:23; }; +#pragma pack(pop) // Visual Studio ignores the 'packed' STATIC_ASSERT(sizeof(union some_union4)==sizeof(int)); +STATIC_ASSERT(__alignof(union some_union4) == 1); #else @@ -59,34 +61,38 @@ union some_union4 } __attribute__((__packed__)); STATIC_ASSERT(sizeof(union some_union4)==3); +STATIC_ASSERT(_Alignof(union some_union4) == 1); #endif +union some_union5 +{ + int i; +}; + #ifdef _MSC_VER - -union some_union5 -{ - int i; -}; - -STATIC_ASSERT(__alignof(union some_union5)==1); - +STATIC_ASSERT(__alignof(union some_union5) == 4); #else +STATIC_ASSERT(_Alignof(union some_union5) == 4); +#endif -union some_union5 -{ +#ifdef _MSC_VER +#pragma pack(push, 1) +union some_union6 { int i; }; +#pragma pack(pop) +// Packing may affect alignment +STATIC_ASSERT(__alignof(union some_union6) == 1); +#else union some_union6 { int i; } __attribute__((__packed__)); // Packing may affect alignment -STATIC_ASSERT(_Alignof(union some_union5)==4); STATIC_ASSERT(_Alignof(union some_union6)==1); - #endif int main() diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp index 3139df62e5..6aad2bc0e6 100644 --- a/src/ansi-c/padding.cpp +++ b/src/ansi-c/padding.cpp @@ -100,15 +100,177 @@ mp_integer alignment(const typet &type, const namespacet &ns) return result; } -void add_padding(struct_typet &type, const namespacet &ns) +static optionalt +underlying_width(const c_bit_field_typet &type, const namespacet &ns) +{ + const typet &subtype = type.subtype(); + + if(subtype.id() == ID_bool) + { + // This is the 'proper' bool. + return 1; + } + else if( + subtype.id() == ID_signedbv || subtype.id() == ID_unsignedbv || + subtype.id() == ID_c_bool) + { + return to_bitvector_type(subtype).get_width(); + } + else if(subtype.id() == ID_c_enum_tag) + { + // These point to an enum, which has a sub-subtype, + // which may be smaller or larger than int, and we thus have + // to check. + const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype)); + + if(c_enum_type.id() == ID_c_enum) + return c_enum_type.subtype().get_int(ID_width); + else + return {}; + } + else + return {}; +} + +static struct_typet::componentst::iterator pad_bit_field( + struct_typet::componentst &components, + struct_typet::componentst::iterator where, + std::size_t pad_bits) +{ + const c_bit_field_typet padding_type( + unsignedbv_typet(pad_bits), pad_bits); + + struct_typet::componentt component( + "$bit_field_pad" + std::to_string(where - components.begin()), + padding_type); + + component.set_is_padding(true); + + return std::next(components.insert(where, component)); +} + +static struct_typet::componentst::iterator pad( + struct_typet::componentst &components, + struct_typet::componentst::iterator where, + std::size_t pad_bits) +{ + const unsignedbv_typet padding_type(pad_bits); + + struct_typet::componentt component( + "$pad" + std::to_string(where - components.begin()), + padding_type); + + component.set_is_padding(true); + + return std::next(components.insert(where, component)); +} + +static void add_padding_msvc(struct_typet &type, const namespacet &ns) { struct_typet::componentst &components=type.components(); - // First do padding for bit-fields to make them - // appear on byte boundaries. + std::size_t bit_field_bits = 0, underlying_bits = 0; + mp_integer offset = 0; + bool is_packed = type.get_bool(ID_C_packed); + + for(struct_typet::componentst::iterator it = components.begin(); + it != components.end(); + it++) + { + // there is exactly one case in which padding is not added: + // if we continue a bit-field with size>0 and the same underlying width + + if( + it->type().id() == ID_c_bit_field && + to_c_bit_field_type(it->type()).get_width() != 0 && + underlying_width(to_c_bit_field_type(it->type()), ns).value_or(0) == + underlying_bits) + { + // do not add padding, but count the bits + const auto width = to_c_bit_field_type(it->type()).get_width(); + bit_field_bits += width; + } + else + { + // pad up any remaining bit field + if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0) + { + const std::size_t pad_bits = + underlying_bits - (bit_field_bits % underlying_bits); + it = pad_bit_field(components, it, pad_bits); + offset += (bit_field_bits + pad_bits) / config.ansi_c.char_width; + underlying_bits = bit_field_bits = 0; + } + + // pad up to underlying type unless the struct is packed + if(!is_packed) + { + const mp_integer a = alignment(it->type(), ns); + if(a > 1) + { + const mp_integer displacement = offset % a; + + if(displacement != 0) + { + const mp_integer pad_bytes = a - displacement; + std::size_t pad_bits = + integer2size_t(pad_bytes * config.ansi_c.char_width); + it = pad(components, it, pad_bits); + offset += pad_bytes; + } + } + } + + // do we start a new bit field? + if(it->type().id() == ID_c_bit_field) + { + underlying_bits = + underlying_width(to_c_bit_field_type(it->type()), ns).value_or(0); + const auto width = to_c_bit_field_type(it->type()).get_width(); + bit_field_bits += width; + } + else + { + // keep track of offset + const mp_integer size = pointer_offset_size(it->type(), ns); + if(size >= 1) + offset += size; + } + } + } + + // Add padding at the end? + // Bit-field + if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0) + { + const std::size_t pad = + underlying_bits - (bit_field_bits % underlying_bits); + pad_bit_field(components, components.end(), pad); + offset += (bit_field_bits + pad) / config.ansi_c.char_width; + } + + // alignment of the struct + // Note that this is done even if the struct is packed. + const mp_integer a = alignment(type, ns); + const mp_integer displacement = offset % a; + + if(displacement != 0) + { + const mp_integer pad_bytes = a - displacement; + const std::size_t pad_bits = + integer2size_t(pad_bytes * config.ansi_c.char_width); + pad(components, components.end(), pad_bits); + offset += pad_bytes; + } +} + +static void add_padding_gcc(struct_typet &type, const namespacet &ns) +{ + struct_typet::componentst &components = type.components(); + + // First make bit-fields appear on byte boundaries { - std::size_t padding_counter=0; std::size_t bit_field_bits=0; for(struct_typet::componentst::iterator @@ -120,27 +282,17 @@ void add_padding(struct_typet &type, const namespacet &ns) to_c_bit_field_type(it->type()).get_width()!=0) { // count the bits - std::size_t width=to_c_bit_field_type(it->type()).get_width(); + const std::size_t width = to_c_bit_field_type(it->type()).get_width(); bit_field_bits+=width; } else if(bit_field_bits!=0) { // not on a byte-boundary? - if((bit_field_bits%8)!=0) + if((bit_field_bits % config.ansi_c.char_width) != 0) { - std::size_t pad=8-bit_field_bits%8; - c_bit_field_typet padding_type(unsignedbv_typet(pad), pad); - - struct_typet::componentt component; - component.type()=padding_type; - component.set_name( - "$bit_field_pad"+std::to_string(padding_counter++)); - component.set_is_padding(true); - - it=components.insert(it, component); - it++; // skip over - - bit_field_bits+=pad; + const std::size_t pad = config.ansi_c.char_width - + bit_field_bits % config.ansi_c.char_width; + it = pad_bit_field(components, it, pad); } bit_field_bits=0; @@ -148,17 +300,11 @@ void add_padding(struct_typet &type, const namespacet &ns) } // Add padding at the end? - if((bit_field_bits%8)!=0) + if((bit_field_bits % config.ansi_c.char_width) != 0) { - std::size_t pad=8-bit_field_bits%8; - c_bit_field_typet padding_type(unsignedbv_typet(pad), pad); - - struct_typet::componentt component; - component.type()=padding_type; - component.set_name("$bit_field_pad"+std::to_string(padding_counter++)); - component.set_is_padding(true); - - components.push_back(component); + const std::size_t pad = + config.ansi_c.char_width - bit_field_bits % config.ansi_c.char_width; + pad_bit_field(components, components.end(), pad); } } @@ -168,7 +314,6 @@ void add_padding(struct_typet &type, const namespacet &ns) return; // done mp_integer offset=0; - std::size_t padding_counter=0; mp_integer max_alignment=0; std::size_t bit_field_bits=0; @@ -200,8 +345,8 @@ void add_padding(struct_typet &type, const namespacet &ns) std::size_t w=to_c_bit_field_type(it_type).get_width(); bit_field_bits += w; - const std::size_t bytes = bit_field_bits / 8; - bit_field_bits %= 8; + const std::size_t bytes = bit_field_bits / config.ansi_c.char_width; + bit_field_bits %= config.ansi_c.char_width; offset+=bytes; continue; } @@ -222,24 +367,15 @@ void add_padding(struct_typet &type, const namespacet &ns) if(a!=1) { // we may need to align it - mp_integer displacement=offset%a; + const mp_integer displacement = offset % a; if(displacement!=0) { - mp_integer pad=a-displacement; - - std::size_t width=integer2size_t(pad*8); - unsignedbv_typet padding_type(width); - - struct_typet::componentt component; - component.type()=padding_type; - component.set_name("$pad"+std::to_string(padding_counter++)); - component.set_is_padding(true); - - it=components.insert(it, component); - it++; // skip over - - offset+=pad; + const mp_integer pad_bytes = a - displacement; + const std::size_t pad_bits = + integer2size_t(pad_bytes * config.ansi_c.char_width); + it = pad(components, it, pad_bits); + offset += pad_bytes; } } @@ -277,25 +413,27 @@ void add_padding(struct_typet &type, const namespacet &ns) if(displacement!=0) { - mp_integer pad=max_alignment-displacement; - - std::size_t width=integer2size_t(pad*8); - unsignedbv_typet padding_type(width); - - // we insert after any final 'flexible member' - struct_typet::componentt component; - component.type()=padding_type; - component.set_name("$pad"+std::to_string(padding_counter++)); - component.set_is_padding(true); - - components.push_back(component); + mp_integer pad_bytes = max_alignment - displacement; + std::size_t pad_bits = + integer2size_t(pad_bytes * config.ansi_c.char_width); + pad(components, components.end(), pad_bits); } } } +void add_padding(struct_typet &type, const namespacet &ns) +{ + // padding depends greatly on compiler + if(config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO) + add_padding_msvc(type, ns); + else + add_padding_gcc(type, ns); +} + void add_padding(union_typet &type, const namespacet &ns) { - mp_integer max_alignment_bits=alignment(type, ns)*8; + mp_integer max_alignment_bits = + alignment(type, ns) * config.ansi_c.char_width; mp_integer size_bits=0; // check per component, and ignore those without fixed size @@ -309,8 +447,21 @@ void add_padding(union_typet &type, const namespacet &ns) // Is the union packed? if(type.get_bool(ID_C_packed)) { - // The size needs to be a multiple of 8 bits only. - max_alignment_bits=8; + // The size needs to be a multiple of 1 char only. + max_alignment_bits = config.ansi_c.char_width; + } + + if(config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO) + { + // Visual Studio pads up to the underlying width of + // any bit field. + for(const auto &c : type.components()) + if(c.type().id() == ID_c_bit_field) + { + auto w = underlying_width(to_c_bit_field_type(c.type()), ns); + if(w.has_value() && w.value() > max_alignment_bits) + max_alignment_bits = w.value(); + } } // The size must be a multiple of the alignment, or