Skip to content

Commit 22d614d

Browse files
committed
Add initializer list constructor to struct/union typet and cleanup API use
Use the rvalue constructor and also review any other use of constructors to avoid unnecessary copies.
1 parent 73ebbb4 commit 22d614d

18 files changed

+78
-101
lines changed

jbmc/src/java_bytecode/java_root_class.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,10 +25,8 @@ void java_root_class(symbolt &class_symbol)
2525

2626
{
2727
// the class identifier is used for stuff such as 'instanceof'
28-
struct_typet::componentt component;
29-
component.set_name("@class_identifier");
28+
struct_typet::componentt component("@class_identifier", string_typet());
3029
component.set_pretty_name("@class_identifier");
31-
component.type()=string_typet();
3230

3331
// add at the beginning
3432
components.insert(components.begin(), component);

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1254,9 +1254,9 @@ java_string_library_preprocesst::get_primitive_value_of_object(
12541254
const auto maybe_symbol =
12551255
symbol_table.lookup(object_type->get_identifier()))
12561256
{
1257-
struct_typet struct_type=to_struct_type(maybe_symbol->type);
1257+
const struct_typet &struct_type = to_struct_type(maybe_symbol->type);
12581258
// Check that the type has a value field
1259-
const struct_union_typet::componentt value_comp=
1259+
const struct_union_typet::componentt &value_comp =
12601260
struct_type.get_component("value");
12611261
if(!value_comp.is_nil())
12621262
{
@@ -1454,17 +1454,16 @@ code_blockt java_string_library_preprocesst::make_string_format_code(
14541454
// The argument can be:
14551455
// a string, an integer, a floating point, a character, a boolean,
14561456
// an object of which we take the hash code, or a date/time
1457-
struct_typet structured_type;
1457+
struct_typet structured_type({{"string_expr", refined_string_type},
1458+
{ID_int, java_int_type()},
1459+
{ID_float, java_float_type()},
1460+
{ID_char, java_char_type()},
1461+
{ID_boolean, java_boolean_type()},
1462+
// TODO: hash_code not implemented for now
1463+
{"hashcode", java_int_type()},
1464+
// TODO: date_time type not implemented for now
1465+
{"date_time", java_int_type()}});
14581466
structured_type.set_tag(CPROVER_PREFIX "string_formatter_variant");
1459-
structured_type.components().emplace_back("string_expr", refined_string_type);
1460-
structured_type.components().emplace_back(ID_int, java_int_type());
1461-
structured_type.components().emplace_back(ID_float, java_float_type());
1462-
structured_type.components().emplace_back(ID_char, java_char_type());
1463-
structured_type.components().emplace_back(ID_boolean, java_boolean_type());
1464-
// TODO: hash_code not implemented for now
1465-
structured_type.components().emplace_back("hashcode", java_int_type());
1466-
// TODO: date_time type not implemented for now
1467-
structured_type.components().emplace_back("date_time", java_int_type());
14681467

14691468
// We will process arguments so that each is converted to a `struct_exprt`
14701469
// containing each possible type used in format specifiers.

jbmc/src/java_bytecode/java_utils.cpp

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -239,11 +239,8 @@ void java_add_components_to_class(
239239
PRECONDITION(class_symbol.type.id()==ID_struct);
240240
struct_typet &struct_type=to_struct_type(class_symbol.type);
241241
struct_typet::componentst &components=struct_type.components();
242-
243-
for(const struct_union_typet::componentt &component : components_to_add)
244-
{
245-
components.push_back(component);
246-
}
242+
components.insert(
243+
components.end(), components_to_add.begin(), components_to_add.end());
247244
}
248245

249246
/// Declare a function with the given name and type.

jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,14 +30,13 @@ typet length_type()
3030
/// Make a struct with a pointer content and an integer length
3131
struct_exprt make_string_argument(std::string name)
3232
{
33-
struct_typet type;
3433
const array_typet char_array(char_type(), infinity_exprt(length_type()));
35-
type.components().emplace_back("length", length_type());
36-
type.components().emplace_back("content", pointer_type(char_array));
34+
struct_typet type(
35+
{{"length", length_type()}, {"content", pointer_type(char_array)}});
3736

38-
const symbol_exprt length(name + "_length", length_type());
39-
const symbol_exprt content(name + "_content", pointer_type(java_char_type()));
40-
return struct_exprt({length, content}, type);
37+
symbol_exprt length(name + "_length", length_type());
38+
symbol_exprt content(name + "_content", pointer_type(java_char_type()));
39+
return struct_exprt({std::move(length), std::move(content)}, std::move(type));
4140
}
4241

4342
SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")

jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -36,9 +36,8 @@ SCENARIO("string_identifiers_resolution_from_equations",
3636
constant_exprt e("e", string_typet());
3737
constant_exprt f("f", string_typet());
3838

39-
struct_typet struct_type;
40-
struct_type.components().emplace_back("str1", string_typet());
41-
struct_type.components().emplace_back("str2", string_typet());
39+
struct_typet struct_type(
40+
{{"str1", string_typet()}, {"str2", string_typet()}});
4241
struct_exprt struct_expr({a, f}, struct_type);
4342
symbol_exprt symbol_struct("sym_struct", struct_type);
4443

jbmc/unit/util/has_subtype.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -37,9 +37,8 @@ SCENARIO("has_subtype", "[core][utils][has_subtype]")
3737

3838
GIVEN("a struct with char and int fields")
3939
{
40-
struct_typet struct_type;
41-
struct_type.components().emplace_back("char_field", char_type);
42-
struct_type.components().emplace_back("int_field", int_type);
40+
struct_typet struct_type(
41+
{{"char_field", char_type}, {"int_field", int_type}});
4342
THEN("char and int are subtypes")
4443
{
4544
REQUIRE(has_subtype(struct_type, is_type(char_type), ns));
@@ -67,9 +66,7 @@ SCENARIO("has_subtype", "[core][utils][has_subtype]")
6766
GIVEN("a recursive struct definition")
6867
{
6968
struct_tag_typet struct_tag("A-struct");
70-
struct_typet::componentt comp("ptr", pointer_type(struct_tag));
71-
struct_typet struct_type;
72-
struct_type.components().push_back(comp);
69+
struct_typet struct_type({{"ptr", pointer_type(struct_tag)}});
7370

7471
symbolt s;
7572
s.type = struct_type;

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1538,7 +1538,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr)
15381538
expr.get(ID_component_name);
15391539

15401540
// first try to find directly
1541-
struct_union_typet::componentt component=
1541+
const struct_union_typet::componentt &component =
15421542
struct_union_type.get_component(component_name);
15431543

15441544
// if that fails, search the anonymous members

src/ansi-c/expr2c.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1573,8 +1573,7 @@ std::string expr2ct::convert_member(
15731573

15741574
if(component_name!="")
15751575
{
1576-
const exprt comp_expr=
1577-
struct_union_type.get_component(component_name);
1576+
const exprt &comp_expr = struct_union_type.get_component(component_name);
15781577

15791578
if(comp_expr.is_nil())
15801579
return convert_norep(src, precedence);
@@ -1592,8 +1591,7 @@ std::string expr2ct::convert_member(
15921591
if(n>=struct_union_type.components().size())
15931592
return convert_norep(src, precedence);
15941593

1595-
const exprt comp_expr=
1596-
struct_union_type.components()[n];
1594+
const exprt &comp_expr = struct_union_type.components()[n];
15971595

15981596
dest+=comp_expr.get_string(ID_pretty_name);
15991597

src/cpp/cpp_typecheck_compound_type.cpp

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1699,14 +1699,15 @@ void cpp_typecheckt::make_ptr_typecast(
16991699
assert(src_type.id()== ID_pointer);
17001700
assert(dest_type.id()== ID_pointer);
17011701

1702-
struct_typet src_struct =
1703-
to_struct_type(static_cast<const typet&>(follow(src_type.subtype())));
1702+
const struct_typet &src_struct =
1703+
to_struct_type(static_cast<const typet &>(follow(src_type.subtype())));
17041704

1705-
struct_typet dest_struct =
1706-
to_struct_type(static_cast<const typet&>(follow(dest_type.subtype())));
1705+
const struct_typet &dest_struct =
1706+
to_struct_type(static_cast<const typet &>(follow(dest_type.subtype())));
17071707

1708-
assert(subtype_typecast(src_struct, dest_struct) ||
1709-
subtype_typecast(dest_struct, src_struct));
1708+
PRECONDITION(
1709+
subtype_typecast(src_struct, dest_struct) ||
1710+
subtype_typecast(dest_struct, src_struct));
17101711

17111712
expr.make_typecast(dest_type);
17121713
}

src/cpp/cpp_typecheck_conversions.cpp

Lines changed: 10 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -619,10 +619,10 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
619619
return true;
620620
}
621621

622-
struct_typet from_struct = to_struct_type(
622+
const struct_typet &from_struct = to_struct_type(
623623
follow(static_cast<const typet &>(expr.type().find(ID_to_member))));
624624

625-
struct_typet to_struct =
625+
const struct_typet &to_struct =
626626
to_struct_type(follow(static_cast<const typet &>(type.find(ID_to_member))));
627627

628628
if(subtype_typecast(to_struct, from_struct))
@@ -931,12 +931,6 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
931931
}
932932
else
933933
{
934-
struct_typet from_struct;
935-
from_struct.make_nil();
936-
937-
if(from.id()==ID_struct)
938-
from_struct=to_struct_type(from);
939-
940934
bool found=false;
941935

942936
for(const auto &component : to_struct_type(to).components())
@@ -1020,7 +1014,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
10201014
rank += tmp_rank;
10211015
}
10221016
}
1023-
else if(from_struct.is_not_nil() && arg1_struct.is_not_nil())
1017+
else if(from.id() == ID_struct && arg1_struct.is_not_nil())
10241018
{
10251019
// try derived-to-base conversion
10261020
address_of_exprt expr_pfrom(expr, pointer_type(expr.type()));
@@ -1905,8 +1899,8 @@ bool cpp_typecheckt::static_typecast(
19051899
if(!qual_to.is_subset_of(qual_from))
19061900
return false;
19071901

1908-
struct_typet from_struct=to_struct_type(from);
1909-
struct_typet subto_struct=to_struct_type(subto);
1902+
const struct_typet &from_struct = to_struct_type(from);
1903+
const struct_typet &subto_struct = to_struct_type(subto);
19101904

19111905
if(subtype_typecast(subto_struct, from_struct))
19121906
{
@@ -1989,8 +1983,8 @@ bool cpp_typecheckt::static_typecast(
19891983
return false;
19901984
}
19911985

1992-
struct_typet from_struct=to_struct_type(from);
1993-
struct_typet to_struct=to_struct_type(to);
1986+
const struct_typet &from_struct = to_struct_type(from);
1987+
const struct_typet &to_struct = to_struct_type(to);
19941988
if(subtype_typecast(to_struct, from_struct))
19951989
{
19961990
make_ptr_typecast(e, type);
@@ -2008,10 +2002,10 @@ bool cpp_typecheckt::static_typecast(
20082002
if(type.subtype()!=e.type().subtype())
20092003
return false;
20102004

2011-
struct_typet from_struct = to_struct_type(
2005+
const struct_typet &from_struct = to_struct_type(
20122006
follow(static_cast<const typet &>(e.type().find(ID_to_member))));
20132007

2014-
struct_typet to_struct = to_struct_type(
2008+
const struct_typet &to_struct = to_struct_type(
20152009
follow(static_cast<const typet &>(type.find(ID_to_member))));
20162010

20172011
if(subtype_typecast(from_struct, to_struct))
@@ -2028,7 +2022,7 @@ bool cpp_typecheckt::static_typecast(
20282022
if(type.subtype() != e.type().subtype())
20292023
return false;
20302024

2031-
struct_typet from_struct = to_struct_type(
2025+
const struct_typet &from_struct = to_struct_type(
20322026
follow(static_cast<const typet &>(e.type().find(ID_to_member))));
20332027

20342028
new_expr = e;

src/cpp/cpp_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1174,7 +1174,7 @@ void cpp_typecheckt::typecheck_expr_member(
11741174
else
11751175
{
11761176
// it must be a static component
1177-
const struct_typet::componentt pcomp=
1177+
const struct_typet::componentt &pcomp =
11781178
type.get_component(to_symbol_expr(symbol_expr).get_identifier());
11791179

11801180
if(pcomp.is_nil())

src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -228,7 +228,7 @@ exprt cpp_typecheck_resolvet::convert_identifier(
228228
const struct_union_typet &struct_union_type=
229229
to_struct_union_type(compound_symbol.type);
230230

231-
const exprt component=
231+
const exprt &component =
232232
struct_union_type.get_component(identifier.identifier);
233233

234234
const typet &type=component.type();

src/goto-programs/remove_complex.cpp

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -257,15 +257,11 @@ static void remove_complex(typet &type)
257257

258258
// Replace by a struct with two members.
259259
// The real part goes first.
260-
struct_typet struct_type;
260+
struct_typet struct_type(
261+
{{ID_real, type.subtype()}, {ID_imag, type.subtype()}});
261262
struct_type.add_source_location()=type.source_location();
262-
struct_type.components().resize(2);
263-
struct_type.components()[0].type()=type.subtype();
264-
struct_type.components()[0].set_name(ID_real);
265-
struct_type.components()[1].type()=type.subtype();
266-
struct_type.components()[1].set_name(ID_imag);
267263

268-
type=struct_type;
264+
type = std::move(struct_type);
269265
}
270266
}
271267

src/goto-programs/string_abstraction.cpp

Lines changed: 4 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -101,23 +101,14 @@ string_abstractiont::string_abstractiont(
101101
ns(_symbol_table),
102102
temporary_counter(0)
103103
{
104-
struct_typet s;
105-
106-
s.components().resize(3);
107-
108-
s.components()[0].set_name("is_zero");
104+
struct_typet s({{"is_zero", build_type(whatt::IS_ZERO)},
105+
{"length", build_type(whatt::LENGTH)},
106+
{"size", build_type(whatt::SIZE)}});
109107
s.components()[0].set_pretty_name("is_zero");
110-
s.components()[0].type()=build_type(whatt::IS_ZERO);
111-
112-
s.components()[1].set_name("length");
113108
s.components()[1].set_pretty_name("length");
114-
s.components()[1].type()=build_type(whatt::LENGTH);
115-
116-
s.components()[2].set_name("size");
117109
s.components()[2].set_pretty_name("size");
118-
s.components()[2].type()=build_type(whatt::SIZE);
119110

120-
string_struct=s;
111+
string_struct = std::move(s);
121112
}
122113

123114
typet string_abstractiont::build_type(whatt what)

src/util/refined_string_type.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,7 @@ Author: Romain Brenguier, [email protected]
2323
refined_string_typet::refined_string_typet(
2424
const typet &index_type,
2525
const pointer_typet &content_type)
26+
: struct_typet({{"length", index_type}, {"content", content_type}})
2627
{
27-
components().emplace_back("length", index_type);
28-
components().emplace_back("content", content_type);
2928
set_tag(CPROVER_PREFIX"refined_string_type");
3029
}

src/util/std_types.h

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,12 @@ class struct_union_typet:public typet
202202

203203
typedef std::vector<componentt> componentst;
204204

205+
struct_union_typet(const irep_idt &_id, componentst &&_components)
206+
: typet(_id)
207+
{
208+
components() = std::move(_components);
209+
}
210+
205211
const componentst &components() const
206212
{
207213
return (const componentst &)(find(ID_components).get_sub());
@@ -292,6 +298,11 @@ class struct_typet:public struct_union_typet
292298
{
293299
}
294300

301+
explicit struct_typet(componentst &&_components)
302+
: struct_union_typet(ID_struct, std::move(_components))
303+
{
304+
}
305+
295306
bool is_prefix_of(const struct_typet &other) const;
296307

297308
/// A struct may be a class, where members may have access restrictions.
@@ -440,6 +451,11 @@ class union_typet:public struct_union_typet
440451
union_typet():struct_union_typet(ID_union)
441452
{
442453
}
454+
455+
explicit union_typet(componentst &&_components)
456+
: struct_union_typet(ID_union, std::move(_components))
457+
{
458+
}
443459
};
444460

445461
/// Check whether a reference to a typet is a \ref union_typet.

unit/pointer-analysis/value_set.cpp

Lines changed: 7 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -47,29 +47,24 @@ SCENARIO(
4747
{
4848
// Create struct A { A *x; A *y }
4949

50-
struct_typet struct_A;
50+
struct_typet struct_A({{"x", pointer_typet(struct_tag_typet("A"), 64)},
51+
{"y", pointer_typet(struct_tag_typet("A"), 64)}});
5152
struct_A.set_tag("A");
52-
struct_A.components().resize(2);
53-
54-
type_symbolt A_symbol(struct_A);
55-
A_symbol.name = "A";
56-
A_symbol.base_name = "A";
57-
A_symbol.pretty_name = "A";
5853

5954
auto &A_x = struct_A.components()[0];
6055
auto &A_y = struct_A.components()[1];
6156

62-
A_x.set_name("x");
6357
A_x.set_base_name("x");
6458
A_x.set_pretty_name("x");
65-
A_x.type() = pointer_typet(struct_tag_typet(A_symbol.name), 64);
6659

67-
A_y.set_name("y");
6860
A_y.set_base_name("y");
6961
A_y.set_pretty_name("y");
70-
A_y.type() = pointer_typet(struct_tag_typet(A_symbol.name), 64);
7162

72-
A_symbol.type = struct_A;
63+
type_symbolt A_symbol(struct_A);
64+
A_symbol.name = "A";
65+
A_symbol.base_name = "A";
66+
A_symbol.pretty_name = "A";
67+
7368
symbol_table.add(A_symbol);
7469

7570
// Create global symbols struct A a1, a2, a3;

0 commit comments

Comments
 (0)