From 8cf524fcbc60318ca046a5f8d504312bb9fc0bfc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 15 Dec 2020 12:18:47 +0000 Subject: [PATCH] Expression initialiser: do not generate nil for empty union Empty unions do not have a meaningful union_exprt as an initialiser, and thus the expression initialiser should make use of returning an optionalt{} instead. This test was generated using C-Reduce based on an example initially generated by CSmith. --- regression/cbmc/Union_Initialization3/main.c | 6 +++++ .../cbmc/Union_Initialization3/test.desc | 11 ++++++++ regression/cbmc/Union_Initialization4/main.c | 16 ++++++++++++ .../cbmc/Union_Initialization4/test.desc | 8 ++++++ src/ansi-c/c_typecheck_initializer.cpp | 21 +++++++++------ src/linking/static_lifetime_init.cpp | 26 ++++++++++++------- src/util/expr_initializer.cpp | 14 +++++++--- 7 files changed, 80 insertions(+), 22 deletions(-) create mode 100644 regression/cbmc/Union_Initialization3/main.c create mode 100644 regression/cbmc/Union_Initialization3/test.desc create mode 100644 regression/cbmc/Union_Initialization4/main.c create mode 100644 regression/cbmc/Union_Initialization4/test.desc diff --git a/regression/cbmc/Union_Initialization3/main.c b/regression/cbmc/Union_Initialization3/main.c new file mode 100644 index 00000000000..5419bdf27f5 --- /dev/null +++ b/regression/cbmc/Union_Initialization3/main.c @@ -0,0 +1,6 @@ +union { +} a; +main() +{ + __assert_fail("", 2, __PRETTY_FUNCTION__); +} diff --git a/regression/cbmc/Union_Initialization3/test.desc b/regression/cbmc/Union_Initialization3/test.desc new file mode 100644 index 00000000000..76996bcf5d4 --- /dev/null +++ b/regression/cbmc/Union_Initialization3/test.desc @@ -0,0 +1,11 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +CBMC would previously report "warning: ignoring nil" and eventually fail an +invariant in src/solvers/flattening/boolbv_width.cpp:199 function: get_entry. diff --git a/regression/cbmc/Union_Initialization4/main.c b/regression/cbmc/Union_Initialization4/main.c new file mode 100644 index 00000000000..70594df0745 --- /dev/null +++ b/regression/cbmc/Union_Initialization4/main.c @@ -0,0 +1,16 @@ +union empty { +}; + +struct S +{ + int x; + union empty e; + int y; +}; + +struct S s = {1}; + +int main() +{ + assert(s.x == 1 && s.y == 0); +} diff --git a/regression/cbmc/Union_Initialization4/test.desc b/regression/cbmc/Union_Initialization4/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/Union_Initialization4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 604ea0b61b0..8a86092b5fc 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -953,16 +953,21 @@ exprt c_typecheck_baset::do_initializer_list( full_type.id()==ID_union || full_type.id()==ID_vector) { - // start with zero everywhere - const auto zero = zero_initializer(type, value.source_location(), *this); - if(!zero.has_value()) + if( + full_type.id() != ID_union || + !to_union_type(full_type).components().empty()) { - error().source_location = value.source_location(); - error() << "cannot zero-initialize '" << to_string(full_type) << "'" - << eom; - throw 0; + // start with zero everywhere + const auto zero = zero_initializer(type, value.source_location(), *this); + if(!zero.has_value()) + { + error().source_location = value.source_location(); + error() << "cannot zero-initialize '" << to_string(full_type) << "'" + << eom; + throw 0; + } + result = *zero; } - result = *zero; } else if(full_type.id()==ID_array) { diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index a6ce0d83e5d..34742c6ea74 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -65,30 +65,36 @@ static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table) return {}; // do not initialize } - exprt rhs; + optionalt rhs; if((symbol.value.is_nil() && symbol.is_extern) || symbol.value.id() == ID_nondet) { // Nondet initialise if not linked, or if explicitly requested. // Compilers would usually complain about the unlinked symbol case. - const auto nondet = nondet_initializer(symbol.type, symbol.location, ns); - CHECK_RETURN(nondet.has_value()); - rhs = *nondet; + rhs = nondet_initializer(symbol.type, symbol.location, ns); } else if(symbol.value.is_nil()) { - const auto zero = zero_initializer(symbol.type, symbol.location, ns); - CHECK_RETURN(zero.has_value()); - rhs = *zero; + rhs = zero_initializer(symbol.type, symbol.location, ns); } else rhs = symbol.value; - code_assignt code(symbol.symbol_expr(), rhs); - code.add_source_location() = symbol.location; + if(rhs.has_value()) + { + code_assignt code(symbol.symbol_expr(), *rhs); + code.add_source_location() = symbol.location; + + return std::move(code); + } + else + { + code_expressiont code{typecast_exprt{symbol.symbol_expr(), empty_typet{}}}; + code.add_source_location() = symbol.location; - return std::move(code); + return std::move(code); + } } void static_lifetime_init( diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 6fe77314ca9..40d8e559ceb 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -192,6 +192,14 @@ optionalt expr_initializert::expr_initializer_rec( code_value.add_source_location()=source_location; value.add_to_operands(std::move(code_value)); } + else if( + c.type().id() == ID_union_tag && + ns.follow_tag(to_union_tag_type(c.type())).components().empty()) + { + union_exprt empty_union{irep_idt{}, nil_exprt{}, c.type()}; + empty_union.add_source_location() = source_location; + value.add_to_operands(std::move(empty_union)); + } else { const auto member = expr_initializer_rec(c.type(), source_location); @@ -235,10 +243,8 @@ optionalt expr_initializert::expr_initializer_rec( if(!found) { - // stupid empty union - union_exprt value(irep_idt(), nil_exprt(), type); - value.add_source_location() = source_location; - return std::move(value); + // empty union or no member of known size + return {}; } else {