Skip to content

Commit 0f20b3c

Browse files
authored
Merge pull request #5705 from tautschnig/union-zero
Initialise union of static lifetime with zeros
2 parents c0b29cb + ac31213 commit 0f20b3c

File tree

11 files changed

+201
-24
lines changed

11 files changed

+201
-24
lines changed

regression/cbmc/Union_Initialization5/main.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,10 @@
11
#include <assert.h>
22

3+
union U_ok {
4+
int x;
5+
int y;
6+
} u_ok = {.x = 1, .y = 2};
7+
38
#ifndef _MSC_VER
49
union U {
510
int x;
@@ -8,11 +13,13 @@ union U {
813

914
int main()
1015
{
16+
assert(u_ok.y == 2);
1117
// the excess initializer (2) is ignored
1218
assert(u.x == 1);
1319
}
1420
#else
1521
int main()
1622
{
23+
assert(u_ok.y == 2);
1724
}
1825
#endif

regression/cbmc/union1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
3+
union U {
4+
int *p;
5+
unsigned long long p_int;
6+
} u = {.p_int = 42};
7+
8+
int main()
9+
{
10+
assert(u.p_int == 42);
11+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--dump-c
4+
=(\(signed int \*\))?42
5+
VERIFICATION SUCCESSFUL
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
irep
11+
--
12+
This test must pass compiling the output generated using dump-c, which implies
13+
that no irep strings can occur.

src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 24 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include "c_typecheck_base.h"
1313

1414
#include <util/arith_tools.h>
15+
#include <util/byte_operators.h>
1516
#include <util/c_types.h>
1617
#include <util/config.h>
1718
#include <util/cprover_prefix.h>
@@ -71,7 +72,10 @@ exprt c_typecheck_baset::do_initializer_rec(
7172
}
7273

7374
if(value.id()==ID_initializer_list)
74-
return do_initializer_list(value, type, force_constant);
75+
{
76+
return simplify_expr(
77+
do_initializer_list(value, type, force_constant), *this);
78+
}
7579

7680
if(
7781
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(
520524
{
521525
// Already right union component. We can initialize multiple submembers,
522526
// so do not overwrite this.
527+
dest = &(to_union_expr(*dest).op());
523528
}
524529
else
525530
{
526531
// The first component is not the maximum member, which the (default)
527532
// zero initializer prepared. Replace this by a component-specific
528533
// initializer; other bytes have an unspecified value (C Standard
529-
// 6.2.6.1(7)).
534+
// 6.2.6.1(7)). In practice, objects of static lifetime are fully zero
535+
// initialized.
530536
const auto zero =
531537
zero_initializer(component.type(), value.source_location(), *this);
532538
if(!zero.has_value())
@@ -536,12 +542,23 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
536542
<< to_string(component.type()) << "'" << eom;
537543
throw 0;
538544
}
539-
union_exprt union_expr(component.get_name(), *zero, type);
540-
union_expr.add_source_location()=value.source_location();
541-
*dest=union_expr;
542-
}
543545

544-
dest = &(to_union_expr(*dest).op());
546+
if(current_symbol.is_static_lifetime)
547+
{
548+
byte_update_exprt byte_update{
549+
byte_update_id(), *dest, from_integer(0, index_type()), *zero};
550+
byte_update.add_source_location() = value.source_location();
551+
*dest = std::move(byte_update);
552+
dest = &(to_byte_update_expr(*dest).op2());
553+
}
554+
else
555+
{
556+
union_exprt union_expr(component.get_name(), *zero, type);
557+
union_expr.add_source_location() = value.source_location();
558+
*dest = std::move(union_expr);
559+
dest = &(to_union_expr(*dest).op());
560+
}
561+
}
545562
}
546563
else
547564
UNREACHABLE;

src/ansi-c/expr2c.cpp

Lines changed: 36 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1911,12 +1911,8 @@ std::string expr2ct::convert_constant(
19111911
if(type.subtype().id()!=ID_empty)
19121912
dest="(("+convert(type)+")"+dest+")";
19131913
}
1914-
else
1914+
else if(src.operands().size() == 1)
19151915
{
1916-
// we prefer the annotation
1917-
if(src.operands().size()!=1)
1918-
return convert_norep(src, precedence);
1919-
19201916
const auto &annotation = to_unary_expr(src).op();
19211917

19221918
if(annotation.id() == ID_constant)
@@ -1933,6 +1929,12 @@ std::string expr2ct::convert_constant(
19331929
else
19341930
return convert_with_precedence(annotation, precedence);
19351931
}
1932+
else
1933+
{
1934+
const auto width = to_pointer_type(type).get_width();
1935+
mp_integer int_value = bvrep2integer(value, width, false);
1936+
return "(" + convert(type) + ")" + integer2string(int_value);
1937+
}
19361938
}
19371939
else if(type.id()==ID_string)
19381940
{
@@ -2280,10 +2282,36 @@ std::string expr2ct::convert_designated_initializer(const exprt &src)
22802282
return convert_norep(src, precedence);
22812283
}
22822284

2283-
std::string dest=".";
2284-
// TODO it->find(ID_member)
2285+
const exprt &value = to_unary_expr(src).op();
2286+
2287+
const exprt &designator = static_cast<const exprt &>(src.find(ID_designator));
2288+
if(designator.operands().size() != 1)
2289+
{
2290+
unsigned precedence;
2291+
return convert_norep(src, precedence);
2292+
}
2293+
2294+
const exprt &designator_id = to_unary_expr(designator).op();
2295+
2296+
std::string dest;
2297+
2298+
if(designator_id.id() == ID_member)
2299+
{
2300+
dest = "." + id2string(designator_id.get(ID_component_name));
2301+
}
2302+
else if(
2303+
designator_id.id() == ID_index && designator_id.operands().size() == 1)
2304+
{
2305+
dest = "[" + convert(to_unary_expr(designator_id).op()) + "]";
2306+
}
2307+
else
2308+
{
2309+
unsigned precedence;
2310+
return convert_norep(src, precedence);
2311+
}
2312+
22852313
dest+='=';
2286-
dest += convert(to_unary_expr(src).op());
2314+
dest += convert(value);
22872315

22882316
return dest;
22892317
}

src/ansi-c/parser.y

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -439,12 +439,11 @@ offsetof:
439439
offsetof_member_designator:
440440
member_name
441441
{
442-
init($$, ID_designated_initializer);
443-
parser_stack($$).operands().resize(1);
444-
auto &op = to_unary_expr(parser_stack($$)).op();
445-
op.id(ID_member);
442+
init($$);
443+
exprt op{ID_member};
446444
op.add_source_location()=parser_stack($1).source_location();
447445
op.set(ID_component_name, parser_stack($1).get(ID_C_base_name));
446+
parser_stack($$).add_to_operands(std::move(op));
448447
}
449448
| offsetof_member_designator '.' member_name
450449
{

src/goto-instrument/dump_c.cpp

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "dump_c.h"
1313

14+
#include <util/byte_operators.h>
1415
#include <util/config.h>
1516
#include <util/find_symbols.h>
1617
#include <util/get_base_name.h>
@@ -1413,6 +1414,60 @@ void dump_ct::cleanup_expr(exprt &expr)
14131414
}
14141415
#endif
14151416
}
1417+
else if(
1418+
expr.id() == ID_byte_update_little_endian ||
1419+
expr.id() == ID_byte_update_big_endian)
1420+
{
1421+
const byte_update_exprt &bu = to_byte_update_expr(expr);
1422+
1423+
if(bu.op().id() == ID_union && bu.offset().is_zero())
1424+
{
1425+
const union_exprt &union_expr = to_union_expr(bu.op());
1426+
const union_typet &union_type =
1427+
to_union_type(ns.follow(union_expr.type()));
1428+
1429+
for(const auto &comp : union_type.components())
1430+
{
1431+
if(bu.value().type() == comp.type())
1432+
{
1433+
exprt member1{ID_member};
1434+
member1.set(ID_component_name, union_expr.get_component_name());
1435+
exprt designated_initializer1{ID_designated_initializer};
1436+
designated_initializer1.add_to_operands(union_expr.op());
1437+
designated_initializer1.add(ID_designator).move_to_sub(member1);
1438+
1439+
exprt member2{ID_member};
1440+
member2.set(ID_component_name, comp.get_name());
1441+
exprt designated_initializer2{ID_designated_initializer};
1442+
designated_initializer2.add_to_operands(bu.value());
1443+
designated_initializer2.add(ID_designator).move_to_sub(member2);
1444+
1445+
binary_exprt initializer_list{std::move(designated_initializer1),
1446+
ID_initializer_list,
1447+
std::move(designated_initializer2)};
1448+
expr.swap(initializer_list);
1449+
break;
1450+
}
1451+
}
1452+
}
1453+
else if(
1454+
bu.op().id() == ID_side_effect &&
1455+
to_side_effect_expr(bu.op()).get_statement() == ID_nondet &&
1456+
ns.follow(bu.op().type()).id() == ID_union && bu.offset().is_zero())
1457+
{
1458+
const union_typet &union_type = to_union_type(ns.follow(bu.op().type()));
1459+
1460+
for(const auto &comp : union_type.components())
1461+
{
1462+
if(bu.value().type() == comp.type())
1463+
{
1464+
union_exprt union_expr{comp.get_name(), bu.value(), bu.op().type()};
1465+
expr.swap(union_expr);
1466+
break;
1467+
}
1468+
}
1469+
}
1470+
}
14161471
}
14171472

14181473
void dump_ct::cleanup_type(typet &type)

src/solvers/flattening/bv_pointers.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -308,7 +308,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
308308
encode(pointer_logic.get_null_object(), bv);
309309
else
310310
{
311-
mp_integer i=string2integer(id2string(value), 2);
311+
mp_integer i = bvrep2integer(value, bits, false);
312312
bv=bv_utils.build_constant(i, bits);
313313
}
314314

src/util/simplify_expr.cpp

Lines changed: 34 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1753,6 +1753,40 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
17531753
return changed(simplify_byte_extract(be));
17541754
}
17551755

1756+
// update bits in a constant
1757+
const auto offset_int = numeric_cast<mp_integer>(offset);
1758+
if(
1759+
root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
1760+
*val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
1761+
*offset_int + *val_size <= *root_size)
1762+
{
1763+
auto root_bits =
1764+
expr2bits(root, expr.id() == ID_byte_update_little_endian, ns);
1765+
1766+
if(root_bits.has_value())
1767+
{
1768+
const auto val_bits =
1769+
expr2bits(value, expr.id() == ID_byte_update_little_endian, ns);
1770+
1771+
if(val_bits.has_value())
1772+
{
1773+
root_bits->replace(
1774+
numeric_cast_v<std::size_t>(*offset_int * 8),
1775+
numeric_cast_v<std::size_t>(*val_size),
1776+
*val_bits);
1777+
1778+
auto tmp = bits2expr(
1779+
*root_bits,
1780+
expr.type(),
1781+
expr.id() == ID_byte_update_little_endian,
1782+
ns);
1783+
1784+
if(tmp.has_value())
1785+
return std::move(*tmp);
1786+
}
1787+
}
1788+
}
1789+
17561790
/*
17571791
* byte_update(root, offset,
17581792
* extract(root, offset) WITH component:=value)
@@ -1836,7 +1870,6 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
18361870
}
18371871

18381872
// the following require a constant offset
1839-
const auto offset_int = numeric_cast<mp_integer>(offset);
18401873
if(!offset_int.has_value() || *offset_int < 0)
18411874
return unchanged(expr);
18421875

0 commit comments

Comments
 (0)