diff --git a/regression/cbmc/Union_Initialization2/main.c b/regression/cbmc/Union_Initialization2/main.c new file mode 100644 index 00000000000..a746b4828f3 --- /dev/null +++ b/regression/cbmc/Union_Initialization2/main.c @@ -0,0 +1,14 @@ +union U { +}; + +struct S +{ + int a; + union U u; + int b; +} s; + +int main() +{ + __CPROVER_assert(0, ""); +} diff --git a/regression/cbmc/Union_Initialization2/test.desc b/regression/cbmc/Union_Initialization2/test.desc new file mode 100644 index 00000000000..006285b6052 --- /dev/null +++ b/regression/cbmc/Union_Initialization2/test.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +^Invariant check failed diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 68090ff2e9d..f158b2164a7 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -183,6 +183,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr) return convert_struct(to_struct_expr(expr)); else if(expr.id()==ID_union) return convert_union(to_union_expr(expr)); + else if(expr.id() == ID_empty_union) + return convert_empty_union(to_empty_union_expr(expr)); else if(expr.id()==ID_string_constant) return convert_bitvector( to_string_constant(expr).to_array_expr()); diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 20d5d78a7e2..58b84da58ee 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -162,6 +162,7 @@ class boolbvt:public arrayst virtual bvt convert_let(const let_exprt &); virtual bvt convert_array_of(const array_of_exprt &expr); virtual bvt convert_union(const union_exprt &expr); + virtual bvt convert_empty_union(const empty_union_exprt &expr); virtual bvt convert_bv_typecast(const typecast_exprt &expr); virtual bvt convert_add_sub(const exprt &expr); virtual bvt convert_mult(const mult_exprt &expr); diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index 0f24d839b2a..a4471aad3ef 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -139,7 +139,8 @@ exprt boolbvt::bv_get_rec( const union_typet &union_type=to_union_type(type); const union_typet::componentst &components=union_type.components(); - assert(!components.empty()); + if(components.empty()) + return empty_union_exprt(type); // Any idea that's better than just returning the first component? std::size_t component_nr=0; diff --git a/src/solvers/flattening/boolbv_union.cpp b/src/solvers/flattening/boolbv_union.cpp index b6202dc288c..197d03f96f5 100644 --- a/src/solvers/flattening/boolbv_union.cpp +++ b/src/solvers/flattening/boolbv_union.cpp @@ -37,3 +37,8 @@ bvt boolbvt::convert_union(const union_exprt &expr) return bv; } + +bvt boolbvt::convert_empty_union(const empty_union_exprt &expr) +{ + return {}; +} diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index fd700efe1e2..768eb69452e 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -2126,6 +2126,10 @@ void smt2_convt::convert_expr(const exprt &expr) { convert_expr(simplify_expr(to_count_trailing_zeros_expr(expr).lower(), ns)); } + else if(expr.id() == ID_empty_union) + { + out << "()"; + } else INVARIANT_WITH_DIAGNOSTICS( false, @@ -4403,7 +4407,9 @@ void smt2_convt::set_to(const exprt &expr, bool value) if(expr.id() == ID_equal && value) { const equal_exprt &equal_expr=to_equal_expr(expr); - if(equal_expr.lhs().type().id() == ID_empty) + if( + equal_expr.lhs().type().id() == ID_empty || + equal_expr.rhs().id() == ID_empty_union) { // ignore equality checking over expressions with empty (void) type return; @@ -4891,7 +4897,9 @@ void smt2_convt::convert_type(const typet &type) else if(type.id() == ID_union || type.id() == ID_union_tag) { std::size_t width=boolbv_width(type); - CHECK_RETURN_WITH_DIAGNOSTICS(width != 0, "failed to get width of union"); + CHECK_RETURN_WITH_DIAGNOSTICS( + to_union_type(ns.follow(type)).components().empty() || width != 0, + "failed to get width of union"); out << "(_ BitVec " << width << ")"; } diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 6fe77314ca9..6d80f3d1bd2 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -208,51 +208,29 @@ optionalt expr_initializert::expr_initializer_rec( } else if(type_id==ID_union) { - const union_typet::componentst &components= - to_union_type(type).components(); + const union_typet &union_type = to_union_type(type); - union_typet::componentt component; - bool found=false; - mp_integer component_size=0; - - // we need to find the largest member - - for(const auto &c : components) - { - // skip methods - if(c.type().id() == ID_code) - continue; - - auto bits = pointer_offset_bits(c.type(), ns); - - if(bits.has_value() && *bits > component_size) - { - component = c; - found=true; - component_size = *bits; - } - } - - if(!found) + if(union_type.components().empty()) { - // stupid empty union - union_exprt value(irep_idt(), nil_exprt(), type); + empty_union_exprt value{type}; value.add_source_location() = source_location; return std::move(value); } - else - { - auto component_value = - expr_initializer_rec(component.type(), source_location); - if(!component_value.has_value()) - return {}; + const auto &widest_member = union_type.find_widest_union_component(ns); + if(!widest_member.has_value()) + return {}; - union_exprt value(component.get_name(), *component_value, type); - value.add_source_location() = source_location; + auto component_value = + expr_initializer_rec(widest_member->first.type(), source_location); - return std::move(value); - } + if(!component_value.has_value()) + return {}; + + union_exprt value{widest_member->first.get_name(), *component_value, type}; + value.add_source_location() = source_location; + + return std::move(value); } else if(type_id==ID_c_enum_tag) { diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index d85676fedea..8a793b6651b 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -862,6 +862,7 @@ IREP_ID_TWO(vector_gt, vector->) IREP_ID_TWO(vector_lt, vector-<) IREP_ID_ONE(shuffle_vector) IREP_ID_ONE(count_trailing_zeros) +IREP_ID_ONE(empty_union) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 427cc3e5dc6..61c8f5ecf6b 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -1662,6 +1662,51 @@ inline union_exprt &to_union_expr(exprt &expr) return ret; } +/// \brief Union constructor to support unions without any member (a GCC/Clang +/// feature). +class empty_union_exprt : public nullary_exprt +{ +public: + explicit empty_union_exprt(typet _type) + : nullary_exprt(ID_empty_union, std::move(_type)) + { + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_empty_union; +} + +inline void validate_expr(const empty_union_exprt &value) +{ + validate_operands( + value, 0, "Empty-union constructor must not have any operand"); +} + +/// \brief Cast an exprt to an \ref empty_union_exprt +/// +/// \a expr must be known to be \ref empty_union_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref empty_union_exprt +inline const empty_union_exprt &to_empty_union_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_empty_union); + const empty_union_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; +} + +/// \copydoc to_empty_union_expr(const exprt &) +inline empty_union_exprt &to_empty_union_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_empty_union); + empty_union_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; +} /// \brief Struct constructor from list of elements class struct_exprt : public multi_ary_exprt