diff --git a/regression/cbmc/Union_Initialization5/main.c b/regression/cbmc/Union_Initialization5/main.c index 484246f1d34..d697725e27a 100644 --- a/regression/cbmc/Union_Initialization5/main.c +++ b/regression/cbmc/Union_Initialization5/main.c @@ -1,5 +1,10 @@ #include +union U_ok { + int x; + int y; +} u_ok = {.x = 1, .y = 2}; + #ifndef _MSC_VER union U { int x; @@ -8,11 +13,13 @@ union U { int main() { + assert(u_ok.y == 2); // the excess initializer (2) is ignored assert(u.x == 1); } #else int main() { + assert(u_ok.y == 2); } #endif diff --git a/regression/cbmc/union1/test.desc b/regression/cbmc/union1/test.desc index 52168c7eba4..9efefbc7362 100644 --- a/regression/cbmc/union1/test.desc +++ b/regression/cbmc/union1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=0$ diff --git a/regression/goto-instrument/dump-union/main.c b/regression/goto-instrument/dump-union/main.c new file mode 100644 index 00000000000..d15593d12fc --- /dev/null +++ b/regression/goto-instrument/dump-union/main.c @@ -0,0 +1,11 @@ +#include + +union U { + int *p; + unsigned long long p_int; +} u = {.p_int = 42}; + +int main() +{ + assert(u.p_int == 42); +} diff --git a/regression/goto-instrument/dump-union/test.desc b/regression/goto-instrument/dump-union/test.desc new file mode 100644 index 00000000000..f4b511c9c74 --- /dev/null +++ b/regression/goto-instrument/dump-union/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--dump-c +=(\(signed int \*\))?42 +VERIFICATION SUCCESSFUL +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +irep +-- +This test must pass compiling the output generated using dump-c, which implies +that no irep strings can occur. diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index c364c148a21..c8a8065a644 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_typecheck_base.h" #include +#include #include #include #include @@ -71,7 +72,10 @@ exprt c_typecheck_baset::do_initializer_rec( } if(value.id()==ID_initializer_list) - return do_initializer_list(value, type, force_constant); + { + return simplify_expr( + do_initializer_list(value, type, force_constant), *this); + } if( value.id() == ID_array && value.get_bool(ID_C_string_constant) && @@ -520,13 +524,15 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( { // Already right union component. We can initialize multiple submembers, // so do not overwrite this. + dest = &(to_union_expr(*dest).op()); } else { // The first component is not the maximum member, which the (default) // zero initializer prepared. Replace this by a component-specific // initializer; other bytes have an unspecified value (C Standard - // 6.2.6.1(7)). + // 6.2.6.1(7)). In practice, objects of static lifetime are fully zero + // initialized. const auto zero = zero_initializer(component.type(), value.source_location(), *this); if(!zero.has_value()) @@ -536,12 +542,23 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( << to_string(component.type()) << "'" << eom; throw 0; } - union_exprt union_expr(component.get_name(), *zero, type); - union_expr.add_source_location()=value.source_location(); - *dest=union_expr; - } - dest = &(to_union_expr(*dest).op()); + if(current_symbol.is_static_lifetime) + { + byte_update_exprt byte_update{ + byte_update_id(), *dest, from_integer(0, index_type()), *zero}; + byte_update.add_source_location() = value.source_location(); + *dest = std::move(byte_update); + dest = &(to_byte_update_expr(*dest).op2()); + } + else + { + union_exprt union_expr(component.get_name(), *zero, type); + union_expr.add_source_location() = value.source_location(); + *dest = std::move(union_expr); + dest = &(to_union_expr(*dest).op()); + } + } } else UNREACHABLE; diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 1a316f2c131..028d759aa05 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1911,12 +1911,8 @@ std::string expr2ct::convert_constant( if(type.subtype().id()!=ID_empty) dest="(("+convert(type)+")"+dest+")"; } - else + else if(src.operands().size() == 1) { - // we prefer the annotation - if(src.operands().size()!=1) - return convert_norep(src, precedence); - const auto &annotation = to_unary_expr(src).op(); if(annotation.id() == ID_constant) @@ -1933,6 +1929,12 @@ std::string expr2ct::convert_constant( else return convert_with_precedence(annotation, precedence); } + else + { + const auto width = to_pointer_type(type).get_width(); + mp_integer int_value = bvrep2integer(value, width, false); + return "(" + convert(type) + ")" + integer2string(int_value); + } } else if(type.id()==ID_string) { @@ -2280,10 +2282,36 @@ std::string expr2ct::convert_designated_initializer(const exprt &src) return convert_norep(src, precedence); } - std::string dest="."; - // TODO it->find(ID_member) + const exprt &value = to_unary_expr(src).op(); + + const exprt &designator = static_cast(src.find(ID_designator)); + if(designator.operands().size() != 1) + { + unsigned precedence; + return convert_norep(src, precedence); + } + + const exprt &designator_id = to_unary_expr(designator).op(); + + std::string dest; + + if(designator_id.id() == ID_member) + { + dest = "." + id2string(designator_id.get(ID_component_name)); + } + else if( + designator_id.id() == ID_index && designator_id.operands().size() == 1) + { + dest = "[" + convert(to_unary_expr(designator_id).op()) + "]"; + } + else + { + unsigned precedence; + return convert_norep(src, precedence); + } + dest+='='; - dest += convert(to_unary_expr(src).op()); + dest += convert(value); return dest; } diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index e8a8c6ad37e..9cddd1b67c8 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -439,12 +439,11 @@ offsetof: offsetof_member_designator: member_name { - init($$, ID_designated_initializer); - parser_stack($$).operands().resize(1); - auto &op = to_unary_expr(parser_stack($$)).op(); - op.id(ID_member); + init($$); + exprt op{ID_member}; op.add_source_location()=parser_stack($1).source_location(); op.set(ID_component_name, parser_stack($1).get(ID_C_base_name)); + parser_stack($$).add_to_operands(std::move(op)); } | offsetof_member_designator '.' member_name { diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index de05e7288ed..ada5dfeb645 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "dump_c.h" +#include #include #include #include @@ -1413,6 +1414,60 @@ void dump_ct::cleanup_expr(exprt &expr) } #endif } + else if( + expr.id() == ID_byte_update_little_endian || + expr.id() == ID_byte_update_big_endian) + { + const byte_update_exprt &bu = to_byte_update_expr(expr); + + if(bu.op().id() == ID_union && bu.offset().is_zero()) + { + const union_exprt &union_expr = to_union_expr(bu.op()); + const union_typet &union_type = + to_union_type(ns.follow(union_expr.type())); + + for(const auto &comp : union_type.components()) + { + if(bu.value().type() == comp.type()) + { + exprt member1{ID_member}; + member1.set(ID_component_name, union_expr.get_component_name()); + exprt designated_initializer1{ID_designated_initializer}; + designated_initializer1.add_to_operands(union_expr.op()); + designated_initializer1.add(ID_designator).move_to_sub(member1); + + exprt member2{ID_member}; + member2.set(ID_component_name, comp.get_name()); + exprt designated_initializer2{ID_designated_initializer}; + designated_initializer2.add_to_operands(bu.value()); + designated_initializer2.add(ID_designator).move_to_sub(member2); + + binary_exprt initializer_list{std::move(designated_initializer1), + ID_initializer_list, + std::move(designated_initializer2)}; + expr.swap(initializer_list); + break; + } + } + } + else if( + bu.op().id() == ID_side_effect && + to_side_effect_expr(bu.op()).get_statement() == ID_nondet && + ns.follow(bu.op().type()).id() == ID_union && bu.offset().is_zero()) + { + const union_typet &union_type = to_union_type(ns.follow(bu.op().type())); + + for(const auto &comp : union_type.components()) + { + if(bu.value().type() == comp.type()) + { + union_exprt union_expr{comp.get_name(), bu.value(), bu.op().type()}; + expr.swap(union_expr); + break; + } + } + } + } } void dump_ct::cleanup_type(typet &type) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 391da92a6d7..bbc29895995 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -308,7 +308,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) encode(pointer_logic.get_null_object(), bv); else { - mp_integer i=string2integer(id2string(value), 2); + mp_integer i = bvrep2integer(value, bits, false); bv=bv_utils.build_constant(i, bits); } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 2caf0303aa3..608f0592b9b 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1753,6 +1753,40 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) return changed(simplify_byte_extract(be)); } + // update bits in a constant + const auto offset_int = numeric_cast(offset); + if( + root_size.has_value() && *root_size >= 0 && val_size.has_value() && + *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 && + *offset_int + *val_size <= *root_size) + { + auto root_bits = + expr2bits(root, expr.id() == ID_byte_update_little_endian, ns); + + if(root_bits.has_value()) + { + const auto val_bits = + expr2bits(value, expr.id() == ID_byte_update_little_endian, ns); + + if(val_bits.has_value()) + { + root_bits->replace( + numeric_cast_v(*offset_int * 8), + numeric_cast_v(*val_size), + *val_bits); + + auto tmp = bits2expr( + *root_bits, + expr.type(), + expr.id() == ID_byte_update_little_endian, + ns); + + if(tmp.has_value()) + return std::move(*tmp); + } + } + } + /* * byte_update(root, offset, * extract(root, offset) WITH component:=value) @@ -1836,7 +1870,6 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) } // the following require a constant offset - const auto offset_int = numeric_cast(offset); if(!offset_int.has_value() || *offset_int < 0) return unchanged(expr); diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index a8d07a88e6e..9ed4c4d3a25 100644 --- a/src/util/simplify_utils.cpp +++ b/src/util/simplify_utils.cpp @@ -185,8 +185,15 @@ optionalt bits2expr( // bits start at lowest memory address auto type_bits = pointer_offset_bits(type, ns); - if(!type_bits.has_value() || *type_bits != bits.size()) + if( + !type_bits.has_value() || + (type.id() != ID_union && type.id() != ID_union_tag && + *type_bits != bits.size()) || + ((type.id() == ID_union || type.id() == ID_union_tag) && + *type_bits < bits.size())) + { return {}; + } if( type.id() == ID_unsignedbv || type.id() == ID_signedbv || @@ -194,6 +201,13 @@ optionalt bits2expr( type.id() == ID_c_bit_field || type.id() == ID_pointer || type.id() == ID_bv || type.id() == ID_c_bool) { + if( + type.id() == ID_pointer && config.ansi_c.NULL_is_zero && + bits.find('1') == std::string::npos) + { + return null_pointer_exprt(to_pointer_type(type)); + } + endianness_mapt map(type, little_endian, ns); std::string tmp = bits; @@ -403,7 +417,7 @@ expr2bits(const exprt &expr, bool little_endian, const namespacet &ns) else if(type.id() == ID_pointer) { if(value == ID_NULL && config.ansi_c.NULL_is_zero) - return std::string('0', to_bitvector_type(type).get_width()); + return std::string(to_bitvector_type(type).get_width(), '0'); else return {}; }