Skip to content

Commit 0c26344

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 06887e8 commit 0c26344

18 files changed

+83
-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: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1261,9 +1261,9 @@ java_string_library_preprocesst::get_primitive_value_of_object(
12611261
const auto maybe_symbol =
12621262
symbol_table.lookup(object_type->get_identifier()))
12631263
{
1264-
struct_typet struct_type=to_struct_type(maybe_symbol->type);
1264+
const struct_typet &struct_type = to_struct_type(maybe_symbol->type);
12651265
// Check that the type has a value field
1266-
const struct_union_typet::componentt value_comp=
1266+
const struct_union_typet::componentt &value_comp =
12671267
struct_type.get_component("value");
12681268
if(!value_comp.is_nil())
12691269
{
@@ -1456,16 +1456,16 @@ code_blockt java_string_library_preprocesst::make_string_format_code(
14561456
// The argument can be:
14571457
// a string, an integer, a floating point, a character, a boolean,
14581458
// an object of which we take the hash code, or a date/time
1459-
struct_typet structured_type;
1460-
structured_type.components().emplace_back("string_expr", refined_string_type);
1461-
structured_type.components().emplace_back(ID_int, java_int_type());
1462-
structured_type.components().emplace_back(ID_float, java_float_type());
1463-
structured_type.components().emplace_back(ID_char, java_char_type());
1464-
structured_type.components().emplace_back(ID_boolean, java_boolean_type());
1459+
struct_typet structured_type({
1460+
{"string_expr", refined_string_type},
1461+
{ID_int, java_int_type()},
1462+
{ID_float, java_float_type()},
1463+
{ID_char, java_char_type()},
1464+
{ID_boolean, java_boolean_type()},
14651465
// TODO: hash_code not implemented for now
1466-
structured_type.components().emplace_back("hashcode", java_int_type());
1466+
{"hashcode", java_int_type()},
14671467
// TODO: date_time type not implemented for now
1468-
structured_type.components().emplace_back("date_time", java_int_type());
1468+
{"date_time", java_int_type()}});
14691469

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

jbmc/src/java_bytecode/java_utils.cpp

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -239,11 +239,7 @@ 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(components.end(), components_to_add.begin(), components_to_add.end());
247243
}
248244

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

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

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -30,16 +30,15 @@ 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));
37-
38-
const symbol_exprt length(name + "_length", length_type());
39-
const symbol_exprt content(name + "_content", pointer_type(java_char_type()));
40-
struct_exprt expr(type);
41-
expr.operands().push_back(length);
42-
expr.operands().push_back(content);
34+
struct_typet type({
35+
{"length", length_type()},
36+
{"content", pointer_type(char_array)}});
37+
38+
symbol_exprt length(name + "_length", length_type());
39+
symbol_exprt content(name + "_content", pointer_type(java_char_type()));
40+
struct_exprt expr(std::move(type));
41+
expr.add_to_operands(std::move(length), std::move(content));
4342
return expr;
4443
}
4544

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

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -36,12 +36,11 @@ 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());
42-
struct_exprt struct_expr(struct_type);
43-
struct_expr.operands().push_back(a);
44-
struct_expr.operands().push_back(f);
39+
struct_typet struct_type({
40+
{"str1", string_typet()},
41+
{"str2", string_typet()}});
42+
struct_exprt struct_expr(std::move(struct_type));
43+
struct_expr.add_to_operands(a, f);
4544
symbol_exprt symbol_struct("sym_struct", struct_type);
4645

4746
std::vector<equal_exprt> equations;

jbmc/unit/util/has_subtype.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -37,9 +37,9 @@ 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},
42+
{"int_field", int_type}});
4343
THEN("char and int are subtypes")
4444
{
4545
REQUIRE(has_subtype(struct_type, is_type(char_type), ns));
@@ -67,9 +67,7 @@ SCENARIO("has_subtype", "[core][utils][has_subtype]")
6767
GIVEN("a recursive struct definition")
6868
{
6969
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);
70+
struct_typet struct_type({{"ptr", pointer_type(struct_tag)}});
7371

7472
symbolt s;
7573
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
@@ -1557,7 +1557,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr)
15571557
expr.get(ID_component_name);
15581558

15591559
// first try to find directly
1560-
struct_union_typet::componentt component=
1560+
const struct_union_typet::componentt &component =
15611561
struct_union_type.get_component(component_name);
15621562

15631563
// if that fails, search the anonymous members

src/ansi-c/expr2c.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1613,7 +1613,7 @@ std::string expr2ct::convert_member(
16131613

16141614
if(component_name!="")
16151615
{
1616-
const exprt comp_expr=
1616+
const exprt &comp_expr =
16171617
struct_union_type.get_component(component_name);
16181618

16191619
if(comp_expr.is_nil())
@@ -1632,7 +1632,7 @@ std::string expr2ct::convert_member(
16321632
if(n>=struct_union_type.components().size())
16331633
return convert_norep(src, precedence);
16341634

1635-
const exprt comp_expr=
1635+
const exprt &comp_expr =
16361636
struct_union_type.components()[n];
16371637

16381638
dest+=comp_expr.get_string(ID_pretty_name);

src/cpp/cpp_typecheck_compound_type.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1695,10 +1695,10 @@ void cpp_typecheckt::make_ptr_typecast(
16951695
assert(src_type.id()== ID_pointer);
16961696
assert(dest_type.id()== ID_pointer);
16971697

1698-
struct_typet src_struct =
1698+
const struct_typet &src_struct =
16991699
to_struct_type(static_cast<const typet&>(follow(src_type.subtype())));
17001700

1701-
struct_typet dest_struct =
1701+
const struct_typet &dest_struct =
17021702
to_struct_type(static_cast<const typet&>(follow(dest_type.subtype())));
17031703

17041704
assert(subtype_typecast(src_struct, dest_struct) ||

src/cpp/cpp_typecheck_conversions.cpp

Lines changed: 10 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -609,11 +609,11 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
609609
return true;
610610
}
611611

612-
struct_typet from_struct =
612+
const struct_typet &from_struct =
613613
to_struct_type(follow(static_cast<const typet &>
614614
(expr.type().find("to-member"))));
615615

616-
struct_typet to_struct =
616+
const struct_typet &to_struct =
617617
to_struct_type(follow(static_cast<const typet &>
618618
(type.find("to-member"))));
619619

@@ -923,12 +923,6 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
923923
}
924924
else
925925
{
926-
struct_typet from_struct;
927-
from_struct.make_nil();
928-
929-
if(from.id()==ID_struct)
930-
from_struct=to_struct_type(from);
931-
932926
bool found=false;
933927

934928
for(const auto &component : to_struct_type(to).components())
@@ -1012,7 +1006,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
10121006
rank += tmp_rank;
10131007
}
10141008
}
1015-
else if(from_struct.is_not_nil() && arg1_struct.is_not_nil())
1009+
else if(from.id() == ID_struct && arg1_struct.is_not_nil())
10161010
{
10171011
// try derived-to-base conversion
10181012
address_of_exprt expr_pfrom(expr, pointer_type(expr.type()));
@@ -1897,8 +1891,8 @@ bool cpp_typecheckt::static_typecast(
18971891
if(!qual_to.is_subset_of(qual_from))
18981892
return false;
18991893

1900-
struct_typet from_struct=to_struct_type(from);
1901-
struct_typet subto_struct=to_struct_type(subto);
1894+
const struct_typet &from_struct = to_struct_type(from);
1895+
const struct_typet &subto_struct = to_struct_type(subto);
19021896

19031897
if(subtype_typecast(subto_struct, from_struct))
19041898
{
@@ -1982,8 +1976,8 @@ bool cpp_typecheckt::static_typecast(
19821976
return false;
19831977
}
19841978

1985-
struct_typet from_struct=to_struct_type(from);
1986-
struct_typet to_struct=to_struct_type(to);
1979+
const struct_typet &from_struct = to_struct_type(from);
1980+
const struct_typet &to_struct = to_struct_type(to);
19871981
if(subtype_typecast(to_struct, from_struct))
19881982
{
19891983
make_ptr_typecast(e, type);
@@ -2000,11 +1994,11 @@ bool cpp_typecheckt::static_typecast(
20001994
if(type.subtype()!=e.type().subtype())
20011995
return false;
20021996

2003-
struct_typet from_struct=
1997+
const struct_typet &from_struct =
20041998
to_struct_type(
20051999
follow(static_cast<const typet&>(e.type().find("to-member"))));
20062000

2007-
struct_typet to_struct=
2001+
const struct_typet &to_struct =
20082002
to_struct_type(
20092003
follow(static_cast<const typet&>(type.find("to-member"))));
20102004

@@ -2022,7 +2016,7 @@ bool cpp_typecheckt::static_typecast(
20222016
if(type.subtype() != e.type().subtype())
20232017
return false;
20242018

2025-
struct_typet from_struct = to_struct_type(
2019+
const struct_typet &from_struct = to_struct_type(
20262020
follow(static_cast<const typet &>(e.type().find("to-member"))));
20272021

20282022
new_expr = e;

src/cpp/cpp_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1182,7 +1182,7 @@ void cpp_typecheckt::typecheck_expr_member(
11821182
else
11831183
{
11841184
// it must be a static component
1185-
const struct_typet::componentt pcomp=
1185+
const struct_typet::componentt &pcomp =
11861186
type.get_component(to_symbol_expr(symbol_expr).get_identifier());
11871187

11881188
if(pcomp.is_nil())

src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -230,7 +230,7 @@ exprt cpp_typecheck_resolvet::convert_identifier(
230230
const struct_union_typet &struct_union_type=
231231
to_struct_union_type(compound_symbol.type);
232232

233-
const exprt component=
233+
const exprt &component =
234234
struct_union_type.get_component(identifier.identifier);
235235

236236
const typet &type=component.type();
@@ -2211,10 +2211,10 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
22112211

22122212
if(id.is_member)
22132213
{
2214-
struct_typet struct_type=
2214+
const struct_typet &struct_type =
22152215
static_cast<const struct_typet &>(
22162216
cpp_typecheck.lookup(id.class_identifier).type);
2217-
const exprt pcomp=struct_type.get_component(identifier);
2217+
const exprt &pcomp = struct_type.get_component(identifier);
22182218
assert(pcomp.is_not_nil());
22192219
assert(pcomp.get_bool(ID_is_type));
22202220
const typet &type=pcomp.type();

src/goto-programs/remove_complex.cpp

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -266,15 +266,12 @@ static void remove_complex(typet &type)
266266

267267
// Replace by a struct with two members.
268268
// The real part goes first.
269-
struct_typet struct_type;
269+
struct_typet struct_type({
270+
{ID_real, type.subtype()},
271+
{ID_imag, type.subtype()}});
270272
struct_type.add_source_location()=type.source_location();
271-
struct_type.components().resize(2);
272-
struct_type.components()[0].type()=type.subtype();
273-
struct_type.components()[0].set_name(ID_real);
274-
struct_type.components()[1].type()=type.subtype();
275-
struct_type.components()[1].set_name(ID_imag);
276273

277-
type=struct_type;
274+
type = std::move(struct_type);
278275
}
279276
}
280277

src/goto-programs/string_abstraction.cpp

Lines changed: 5 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -100,23 +100,15 @@ string_abstractiont::string_abstractiont(
100100
ns(_symbol_table),
101101
temporary_counter(0)
102102
{
103-
struct_typet s;
104-
105-
s.components().resize(3);
106-
107-
s.components()[0].set_name("is_zero");
103+
struct_typet s({
104+
{"is_zero", build_type(whatt::IS_ZERO)},
105+
{"length", build_type(whatt::LENGTH)},
106+
{"size", build_type(whatt::SIZE) }});
108107
s.components()[0].set_pretty_name("is_zero");
109-
s.components()[0].type()=build_type(whatt::IS_ZERO);
110-
111-
s.components()[1].set_name("length");
112108
s.components()[1].set_pretty_name("length");
113-
s.components()[1].type()=build_type(whatt::LENGTH);
114-
115-
s.components()[2].set_name("size");
116109
s.components()[2].set_pretty_name("size");
117-
s.components()[2].type()=build_type(whatt::SIZE);
118110

119-
string_struct=s;
111+
string_struct = std::move(s);
120112
}
121113

122114
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
@@ -118,6 +118,12 @@ class struct_union_typet:public typet
118118
{
119119
}
120120

121+
struct_union_typet(const irep_idt &_id, componentst &&_components)
122+
: typet(_id)
123+
{
124+
components() = std::move(_components);
125+
}
126+
121127
class componentt:public exprt
122128
{
123129
public:
@@ -280,6 +286,11 @@ class struct_typet:public struct_union_typet
280286
{
281287
}
282288

289+
explicit struct_typet(componentst &&_components)
290+
: struct_union_typet(ID_struct, std::move(_components))
291+
{
292+
}
293+
283294
bool is_prefix_of(const struct_typet &other) const;
284295

285296
/// A struct may be a class, where members may have access restrictions.
@@ -428,6 +439,11 @@ class union_typet:public struct_union_typet
428439
union_typet():struct_union_typet(ID_union)
429440
{
430441
}
442+
443+
explicit union_typet(componentst &&_components)
444+
: struct_union_typet(ID_union, std::move(_components))
445+
{
446+
}
431447
};
432448

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

0 commit comments

Comments
 (0)