Merge pull request #3623 from tautschnig/struct-union-constructor

tautschnig · web-flow · commit 1c1254362100 · 2019-01-21T14:59:31.000Z
Add initializer list constructor to struct/union typet and cleanup API use [blocks: #3597]
diff --git 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
@@ -1257,9 +1257,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())
     {
@@ -1457,17 +1457,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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1571,8 +1571,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);
@@ -1590,8 +1589,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
@@ -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<const typet&>(follow(src_type.subtype())));
+  const struct_typet &src_struct =
+    to_struct_type(static_cast<const typet &>(follow(src_type.subtype())));
 
-  struct_typet dest_struct =
-    to_struct_type(static_cast<const typet&>(follow(dest_type.subtype())));
+  const struct_typet &dest_struct =
+    to_struct_type(static_cast<const typet &>(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
@@ -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<const typet &>(expr.type().find(ID_to_member))));
 
-  struct_typet to_struct =
+  const struct_typet &to_struct =
     to_struct_type(follow(static_cast<const typet &>(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<const typet &>(e.type().find(ID_to_member))));
 
-      struct_typet to_struct = to_struct_type(
+      const struct_typet &to_struct = to_struct_type(
         follow(static_cast<const typet &>(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<const typet &>(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
@@ -1177,7 +1177,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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -202,6 +202,12 @@ class struct_union_typet:public typet
 
   typedef std::vector<componentt> 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
@@ -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
@@ -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);
 
