From b16c7d7cd40584244b1cca4f3439055ff553a5d1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 11 Feb 2022 13:17:17 +0000 Subject: [PATCH] Support non-heap allocated flexible arrays This addresses an existing todo in the code base: we need to come up with a new type based on the actual initializer. Fixes: #3653, #4206 Co-authored-by: Chengyu Zhang Co-authored-by: Andreas Tiemeyer --- regression/cbmc/struct16/main.c | 49 +++++++++++++++++++++ regression/cbmc/struct16/test.desc | 10 +++++ src/ansi-c/c_typecheck_initializer.cpp | 61 ++++++++++++++++++++------ 3 files changed, 107 insertions(+), 13 deletions(-) create mode 100644 regression/cbmc/struct16/main.c create mode 100644 regression/cbmc/struct16/test.desc diff --git a/regression/cbmc/struct16/main.c b/regression/cbmc/struct16/main.c new file mode 100644 index 00000000000..ae0bfa0e2cd --- /dev/null +++ b/regression/cbmc/struct16/main.c @@ -0,0 +1,49 @@ +#include +#include + +typedef int T[]; + +struct f +{ + int w; + T x; +}; + +static struct f before = {0xdeadbeef}; +static struct f f = {4, {0, 1, 2, 3, 4}}; +static struct f after = {0xcafecafe}; + +struct St +{ + char c; + int d[]; +}; +struct St s = {'a', {11, 5}}; + +int main() +{ + int i; + for(i = 0; i < f.w; ++i) + { + if(f.x[i] != i) + { + assert(0); + } + } + assert(sizeof(f) == sizeof(struct f)); + assert(before.w == 0xdeadbeef); + assert(after.w == 0xcafecafe); + printf("%llx\n", &before); + printf("%llx\n", &f); + printf("%llx\n", &after); + + unsigned char c; + c = c && 1; + assert(c == 0 || c == 1); + assert(s.d[1] == 5); + s.d[1] += c; + assert(s.d[1] < 8); + assert(s.d[0] == 11); + + return 0; +} diff --git a/regression/cbmc/struct16/test.desc b/regression/cbmc/struct16/test.desc new file mode 100644 index 00000000000..9927cd18857 --- /dev/null +++ b/regression/cbmc/struct16/test.desc @@ -0,0 +1,10 @@ +CORE +main.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test demonstrates support for flexible array members with non-heap allocated +objects. diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 8f6671e28f7..a1af1242dc2 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -9,8 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// ANSI-C Conversion / Type Checking -#include "c_typecheck_base.h" - #include #include #include @@ -22,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "anonymous_member.h" +#include "c_typecheck_base.h" +#include "type2name.h" void c_typecheck_baset::do_initializer( exprt &initializer, @@ -240,13 +240,12 @@ void c_typecheck_baset::do_initializer(symbolt &symbol) typecheck_expr(symbol.value); do_initializer(symbol.value, symbol.type, true); - // need to adjust size? - if( - !symbol.is_macro && symbol.type.id() == ID_array && - to_array_type(symbol.type).size().is_nil()) - { + // A flexible array may have been initialized, which entails a type change. + // Note that the type equality test is important: we want to preserve + // annotations like typedefs or const-ness when the type is otherwise the + // same. + if(!symbol.is_macro && symbol.type != symbol.value.type()) symbol.type = symbol.value.type(); - } } if(symbol.is_macro) @@ -428,8 +427,6 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( } dest->operands().resize( numeric_cast_v(index) + 1, *zero); - - // todo: adjust type! } else { @@ -1007,11 +1004,49 @@ exprt c_typecheck_baset::do_initializer_list( increment_designator(current_designator); } - // make sure we didn't mess up index computation if(full_type.id()==ID_struct) { - assert(result.operands().size()== - to_struct_type(full_type).components().size()); + const struct_typet &full_struct_type = to_struct_type(full_type); + const struct_typet::componentst &components = full_struct_type.components(); + // make sure we didn't mess up index computation + CHECK_RETURN(result.operands().size() == components.size()); + + if( + !components.empty() && + components.back().type().get_bool(ID_C_flexible_array_member)) + { + const auto array_size = numeric_cast( + to_array_type(components.back().type()).size()); + array_exprt &init_array = to_array_expr(result.operands().back()); + if( + !array_size.has_value() || + (*array_size <= 1 && init_array.operands().size() != *array_size)) + { + struct_typet actual_struct_type = full_struct_type; + array_typet &actual_array_type = + to_array_type(actual_struct_type.components().back().type()); + actual_array_type.size() = from_integer( + init_array.operands().size(), actual_array_type.index_type()); + actual_array_type.set(ID_C_flexible_array_member, true); + init_array.type() = actual_array_type; + + // mimic bits of typecheck_compound_type to produce a new struct tag + actual_struct_type.remove(ID_tag); + type_symbolt compound_symbol{actual_struct_type}; + compound_symbol.mode = mode; + compound_symbol.location = value.source_location(); + std::string typestr = type2name(compound_symbol.type, *this); + compound_symbol.base_name = "#anon#" + typestr; + compound_symbol.name = "tag-#anon#" + typestr; + irep_idt tag_identifier = compound_symbol.name; + + // We might already have the same anonymous struct, which is fine as it + // will be exactly the same type. + symbol_table.insert(std::move(compound_symbol)); + + result.type() = struct_tag_typet{tag_identifier}; + } + } } if(full_type.id()==ID_array &&