From ac4ae98a8c869dc09120641a9e3625f690a2e336 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 27 Dec 2018 12:48:16 +0000 Subject: [PATCH] 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. --- jbmc/src/java_bytecode/java_root_class.cpp | 4 +--- .../java_string_library_preprocess.cpp | 23 +++++++++---------- jbmc/src/java_bytecode/java_utils.cpp | 7 ++---- .../string_refinement/dependency_graph.cpp | 11 ++++----- .../string_symbol_resolution.cpp | 5 ++-- jbmc/unit/util/has_subtype.cpp | 9 +++----- src/ansi-c/c_typecheck_expr.cpp | 2 +- src/ansi-c/expr2c.cpp | 6 ++--- src/cpp/cpp_typecheck_compound_type.cpp | 13 ++++++----- src/cpp/cpp_typecheck_conversions.cpp | 18 +++++++-------- src/cpp/cpp_typecheck_expr.cpp | 2 +- src/cpp/cpp_typecheck_resolve.cpp | 2 +- src/goto-programs/remove_complex.cpp | 10 +++----- src/goto-programs/string_abstraction.cpp | 17 ++++---------- src/util/refined_string_type.cpp | 3 +-- src/util/std_types.h | 16 +++++++++++++ unit/pointer-analysis/value_set.cpp | 19 ++++++--------- unit/util/pointer_offset_size.cpp | 4 +--- 18 files changed, 77 insertions(+), 94 deletions(-) diff --git a/jbmc/src/java_bytecode/java_root_class.cpp b/jbmc/src/java_bytecode/java_root_class.cpp index 9ac91f56f4d..242da4c7d9a 100644 --- a/jbmc/src/java_bytecode/java_root_class.cpp +++ b/jbmc/src/java_bytecode/java_root_class.cpp @@ -25,10 +25,8 @@ void java_root_class(symbolt &class_symbol) { // the class identifier is used for stuff such as 'instanceof' - struct_typet::componentt component; - component.set_name("@class_identifier"); + struct_typet::componentt component("@class_identifier", string_typet()); component.set_pretty_name("@class_identifier"); - component.type()=string_typet(); // add at the beginning components.insert(components.begin(), component); diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 60b21341c13..2d7129d04a8 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1254,9 +1254,9 @@ java_string_library_preprocesst::get_primitive_value_of_object( const auto maybe_symbol = symbol_table.lookup(object_type->get_identifier())) { - struct_typet struct_type=to_struct_type(maybe_symbol->type); + const struct_typet &struct_type = to_struct_type(maybe_symbol->type); // Check that the type has a value field - const struct_union_typet::componentt value_comp= + const struct_union_typet::componentt &value_comp = struct_type.get_component("value"); if(!value_comp.is_nil()) { @@ -1454,17 +1454,16 @@ code_blockt java_string_library_preprocesst::make_string_format_code( // The argument can be: // a string, an integer, a floating point, a character, a boolean, // an object of which we take the hash code, or a date/time - struct_typet structured_type; + struct_typet structured_type({{"string_expr", refined_string_type}, + {ID_int, java_int_type()}, + {ID_float, java_float_type()}, + {ID_char, java_char_type()}, + {ID_boolean, java_boolean_type()}, + // TODO: hash_code not implemented for now + {"hashcode", java_int_type()}, + // TODO: date_time type not implemented for now + {"date_time", java_int_type()}}); structured_type.set_tag(CPROVER_PREFIX "string_formatter_variant"); - structured_type.components().emplace_back("string_expr", refined_string_type); - structured_type.components().emplace_back(ID_int, java_int_type()); - structured_type.components().emplace_back(ID_float, java_float_type()); - structured_type.components().emplace_back(ID_char, java_char_type()); - structured_type.components().emplace_back(ID_boolean, java_boolean_type()); - // TODO: hash_code not implemented for now - structured_type.components().emplace_back("hashcode", java_int_type()); - // TODO: date_time type not implemented for now - structured_type.components().emplace_back("date_time", java_int_type()); // We will process arguments so that each is converted to a `struct_exprt` // containing each possible type used in format specifiers. diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 4ed42f13d4f..8bc6a4ee378 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -239,11 +239,8 @@ void java_add_components_to_class( PRECONDITION(class_symbol.type.id()==ID_struct); struct_typet &struct_type=to_struct_type(class_symbol.type); struct_typet::componentst &components=struct_type.components(); - - for(const struct_union_typet::componentt &component : components_to_add) - { - components.push_back(component); - } + components.insert( + components.end(), components_to_add.begin(), components_to_add.end()); } /// Declare a function with the given name and type. diff --git a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp index 773c051e3e5..be2c4d72868 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp +++ b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp @@ -30,14 +30,13 @@ typet length_type() /// Make a struct with a pointer content and an integer length struct_exprt make_string_argument(std::string name) { - struct_typet type; const array_typet char_array(char_type(), infinity_exprt(length_type())); - type.components().emplace_back("length", length_type()); - type.components().emplace_back("content", pointer_type(char_array)); + struct_typet type( + {{"length", length_type()}, {"content", pointer_type(char_array)}}); - const symbol_exprt length(name + "_length", length_type()); - const symbol_exprt content(name + "_content", pointer_type(java_char_type())); - return struct_exprt({length, content}, type); + symbol_exprt length(name + "_length", length_type()); + symbol_exprt content(name + "_content", pointer_type(java_char_type())); + return struct_exprt({std::move(length), std::move(content)}, std::move(type)); } SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") diff --git a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp b/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp index e6559e82188..81f225ed78a 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp +++ b/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp @@ -36,9 +36,8 @@ SCENARIO("string_identifiers_resolution_from_equations", constant_exprt e("e", string_typet()); constant_exprt f("f", string_typet()); - struct_typet struct_type; - struct_type.components().emplace_back("str1", string_typet()); - struct_type.components().emplace_back("str2", string_typet()); + struct_typet struct_type( + {{"str1", string_typet()}, {"str2", string_typet()}}); struct_exprt struct_expr({a, f}, struct_type); symbol_exprt symbol_struct("sym_struct", struct_type); diff --git a/jbmc/unit/util/has_subtype.cpp b/jbmc/unit/util/has_subtype.cpp index eddf80aa18b..65ebd875c23 100644 --- a/jbmc/unit/util/has_subtype.cpp +++ b/jbmc/unit/util/has_subtype.cpp @@ -37,9 +37,8 @@ SCENARIO("has_subtype", "[core][utils][has_subtype]") GIVEN("a struct with char and int fields") { - struct_typet struct_type; - struct_type.components().emplace_back("char_field", char_type); - struct_type.components().emplace_back("int_field", int_type); + struct_typet struct_type( + {{"char_field", char_type}, {"int_field", int_type}}); THEN("char and int are subtypes") { REQUIRE(has_subtype(struct_type, is_type(char_type), ns)); @@ -67,9 +66,7 @@ SCENARIO("has_subtype", "[core][utils][has_subtype]") GIVEN("a recursive struct definition") { struct_tag_typet struct_tag("A-struct"); - struct_typet::componentt comp("ptr", pointer_type(struct_tag)); - struct_typet struct_type; - struct_type.components().push_back(comp); + struct_typet struct_type({{"ptr", pointer_type(struct_tag)}}); symbolt s; s.type = struct_type; diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b61bdb83f74..1c3f1b36c20 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1538,7 +1538,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr) expr.get(ID_component_name); // first try to find directly - struct_union_typet::componentt component= + const struct_union_typet::componentt &component = struct_union_type.get_component(component_name); // if that fails, search the anonymous members diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 5b4ca270dd7..d17eaa30da2 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1573,8 +1573,7 @@ std::string expr2ct::convert_member( if(component_name!="") { - const exprt comp_expr= - struct_union_type.get_component(component_name); + const exprt &comp_expr = struct_union_type.get_component(component_name); if(comp_expr.is_nil()) return convert_norep(src, precedence); @@ -1592,8 +1591,7 @@ std::string expr2ct::convert_member( if(n>=struct_union_type.components().size()) return convert_norep(src, precedence); - const exprt comp_expr= - struct_union_type.components()[n]; + const exprt &comp_expr = struct_union_type.components()[n]; dest+=comp_expr.get_string(ID_pretty_name); diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 3b3753d188b..05d031f1009 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -1699,14 +1699,15 @@ void cpp_typecheckt::make_ptr_typecast( assert(src_type.id()== ID_pointer); assert(dest_type.id()== ID_pointer); - struct_typet src_struct = - to_struct_type(static_cast(follow(src_type.subtype()))); + const struct_typet &src_struct = + to_struct_type(static_cast(follow(src_type.subtype()))); - struct_typet dest_struct = - to_struct_type(static_cast(follow(dest_type.subtype()))); + const struct_typet &dest_struct = + to_struct_type(static_cast(follow(dest_type.subtype()))); - assert(subtype_typecast(src_struct, dest_struct) || - subtype_typecast(dest_struct, src_struct)); + PRECONDITION( + subtype_typecast(src_struct, dest_struct) || + subtype_typecast(dest_struct, src_struct)); expr.make_typecast(dest_type); } diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index 54c425aee0a..20574722dc3 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -619,10 +619,10 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member( return true; } - struct_typet from_struct = to_struct_type( + const struct_typet &from_struct = to_struct_type( follow(static_cast(expr.type().find(ID_to_member)))); - struct_typet to_struct = + const struct_typet &to_struct = to_struct_type(follow(static_cast(type.find(ID_to_member)))); if(subtype_typecast(to_struct, from_struct)) @@ -1891,8 +1891,8 @@ bool cpp_typecheckt::static_typecast( if(!qual_to.is_subset_of(qual_from)) return false; - struct_typet from_struct=to_struct_type(from); - struct_typet subto_struct=to_struct_type(subto); + const struct_typet &from_struct = to_struct_type(from); + const struct_typet &subto_struct = to_struct_type(subto); if(subtype_typecast(subto_struct, from_struct)) { @@ -1975,8 +1975,8 @@ bool cpp_typecheckt::static_typecast( return false; } - struct_typet from_struct=to_struct_type(from); - struct_typet to_struct=to_struct_type(to); + const struct_typet &from_struct = to_struct_type(from); + const struct_typet &to_struct = to_struct_type(to); if(subtype_typecast(to_struct, from_struct)) { make_ptr_typecast(e, type); @@ -1994,10 +1994,10 @@ bool cpp_typecheckt::static_typecast( if(type.subtype()!=e.type().subtype()) return false; - struct_typet from_struct = to_struct_type( + const struct_typet &from_struct = to_struct_type( follow(static_cast(e.type().find(ID_to_member)))); - struct_typet to_struct = to_struct_type( + const struct_typet &to_struct = to_struct_type( follow(static_cast(type.find(ID_to_member)))); if(subtype_typecast(from_struct, to_struct)) @@ -2014,7 +2014,7 @@ bool cpp_typecheckt::static_typecast( if(type.subtype() != e.type().subtype()) return false; - struct_typet from_struct = to_struct_type( + const struct_typet &from_struct = to_struct_type( follow(static_cast(e.type().find(ID_to_member)))); new_expr = e; diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index af13a164613..2817746df83 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -1175,7 +1175,7 @@ void cpp_typecheckt::typecheck_expr_member( else { // it must be a static component - const struct_typet::componentt pcomp= + const struct_typet::componentt &pcomp = type.get_component(to_symbol_expr(symbol_expr).get_identifier()); if(pcomp.is_nil()) diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 9e8543e2dbf..ef05c7455a9 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -228,7 +228,7 @@ exprt cpp_typecheck_resolvet::convert_identifier( const struct_union_typet &struct_union_type= to_struct_union_type(compound_symbol.type); - const exprt component= + const exprt &component = struct_union_type.get_component(identifier.identifier); const typet &type=component.type(); diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp index df38ddb23b5..ece8ef4768f 100644 --- a/src/goto-programs/remove_complex.cpp +++ b/src/goto-programs/remove_complex.cpp @@ -257,15 +257,11 @@ static void remove_complex(typet &type) // Replace by a struct with two members. // The real part goes first. - struct_typet struct_type; + struct_typet struct_type( + {{ID_real, type.subtype()}, {ID_imag, type.subtype()}}); struct_type.add_source_location()=type.source_location(); - struct_type.components().resize(2); - struct_type.components()[0].type()=type.subtype(); - struct_type.components()[0].set_name(ID_real); - struct_type.components()[1].type()=type.subtype(); - struct_type.components()[1].set_name(ID_imag); - type=struct_type; + type = std::move(struct_type); } } diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 63fbf62155f..68f0d35e722 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -101,23 +101,14 @@ string_abstractiont::string_abstractiont( ns(_symbol_table), temporary_counter(0) { - struct_typet s; - - s.components().resize(3); - - s.components()[0].set_name("is_zero"); + struct_typet s({{"is_zero", build_type(whatt::IS_ZERO)}, + {"length", build_type(whatt::LENGTH)}, + {"size", build_type(whatt::SIZE)}}); s.components()[0].set_pretty_name("is_zero"); - s.components()[0].type()=build_type(whatt::IS_ZERO); - - s.components()[1].set_name("length"); s.components()[1].set_pretty_name("length"); - s.components()[1].type()=build_type(whatt::LENGTH); - - s.components()[2].set_name("size"); s.components()[2].set_pretty_name("size"); - s.components()[2].type()=build_type(whatt::SIZE); - string_struct=s; + string_struct = std::move(s); } typet string_abstractiont::build_type(whatt what) diff --git a/src/util/refined_string_type.cpp b/src/util/refined_string_type.cpp index 0e34d611329..109ba3dad4d 100644 --- a/src/util/refined_string_type.cpp +++ b/src/util/refined_string_type.cpp @@ -23,8 +23,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com refined_string_typet::refined_string_typet( const typet &index_type, const pointer_typet &content_type) + : struct_typet({{"length", index_type}, {"content", content_type}}) { - components().emplace_back("length", index_type); - components().emplace_back("content", content_type); set_tag(CPROVER_PREFIX"refined_string_type"); } diff --git a/src/util/std_types.h b/src/util/std_types.h index a89e1fb9481..644124c50c7 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -202,6 +202,12 @@ class struct_union_typet:public typet typedef std::vector componentst; + struct_union_typet(const irep_idt &_id, componentst &&_components) + : typet(_id) + { + components() = std::move(_components); + } + const componentst &components() const { return (const componentst &)(find(ID_components).get_sub()); @@ -292,6 +298,11 @@ class struct_typet:public struct_union_typet { } + explicit struct_typet(componentst &&_components) + : struct_union_typet(ID_struct, std::move(_components)) + { + } + bool is_prefix_of(const struct_typet &other) const; /// A struct may be a class, where members may have access restrictions. @@ -440,6 +451,11 @@ class union_typet:public struct_union_typet union_typet():struct_union_typet(ID_union) { } + + explicit union_typet(componentst &&_components) + : struct_union_typet(ID_union, std::move(_components)) + { + } }; /// Check whether a reference to a typet is a \ref union_typet. diff --git a/unit/pointer-analysis/value_set.cpp b/unit/pointer-analysis/value_set.cpp index f692a525dfd..76e3f5cdbfa 100644 --- a/unit/pointer-analysis/value_set.cpp +++ b/unit/pointer-analysis/value_set.cpp @@ -47,29 +47,24 @@ SCENARIO( { // Create struct A { A *x; A *y } - struct_typet struct_A; + struct_typet struct_A({{"x", pointer_typet(struct_tag_typet("A"), 64)}, + {"y", pointer_typet(struct_tag_typet("A"), 64)}}); struct_A.set_tag("A"); - struct_A.components().resize(2); - - type_symbolt A_symbol(struct_A); - A_symbol.name = "A"; - A_symbol.base_name = "A"; - A_symbol.pretty_name = "A"; auto &A_x = struct_A.components()[0]; auto &A_y = struct_A.components()[1]; - A_x.set_name("x"); A_x.set_base_name("x"); A_x.set_pretty_name("x"); - A_x.type() = pointer_typet(struct_tag_typet(A_symbol.name), 64); - A_y.set_name("y"); A_y.set_base_name("y"); A_y.set_pretty_name("y"); - A_y.type() = pointer_typet(struct_tag_typet(A_symbol.name), 64); - A_symbol.type = struct_A; + type_symbolt A_symbol(struct_A); + A_symbol.name = "A"; + A_symbol.base_name = "A"; + A_symbol.pretty_name = "A"; + symbol_table.add(A_symbol); // Create global symbols struct A a1, a2, a3; diff --git a/unit/util/pointer_offset_size.cpp b/unit/util/pointer_offset_size.cpp index 942918caef6..186a07864cc 100644 --- a/unit/util/pointer_offset_size.cpp +++ b/unit/util/pointer_offset_size.cpp @@ -79,9 +79,7 @@ TEST_CASE("Build subexpression to access element at offset into struct") const signedbv_typet t(32); - struct_typet st; - st.components().emplace_back("foo", t); - st.components().emplace_back("bar", t); + struct_typet st({{"foo", t}, {"bar", t}}); symbol_exprt s("struct", st);