Verilog: rename convert_type method to elaborate_type

This renames the method that elaborates types, given that it follows the
elaboration procedure in the Verilog standard.

Author: kroening

src/verilog/Makefile

@@ -2,6 +2,7 @@ SRC = aval_bval_encoding.cpp \
       expr2verilog.cpp \
       sva_expr.cpp \
       verilog_elaborate.cpp \
+      verilog_elaborate_type.cpp \
       verilog_expr.cpp \
       verilog_generate.cpp \
       verilog_interfaces.cpp \
@@ -20,7 +21,6 @@ SRC = aval_bval_encoding.cpp \
       verilog_typecheck.cpp \
       verilog_typecheck_base.cpp \
       verilog_typecheck_expr.cpp \
-      verilog_typecheck_type.cpp \
       verilog_y.tab.cpp \
       vtype.cpp
 

src/verilog/verilog_elaborate.cpp

@@ -34,7 +34,7 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl)
   else
   {
     // add the symbol
-    typet type = convert_type(declarator.merged_type(decl.type()));
+    typet type = elaborate_type(declarator.merged_type(decl.type()));
 
     symbolt new_symbol{identifier, type, mode};
 
@@ -245,7 +245,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
         symbol.base_name = declarator.base_name();
         symbol.location = declarator.source_location();
-        symbol.type = convert_type(declarator.merged_type(decl.type()));
+        symbol.type = elaborate_type(declarator.merged_type(decl.type()));
 
         if(symbol.base_name.empty())
         {
@@ -330,7 +330,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
             << "empty symbol name";
         }
 
-        symbol.type = convert_type(declarator.merged_type(decl.type()));
+        symbol.type = elaborate_type(declarator.merged_type(decl.type()));
         symbol.name = hierarchical_identifier(symbol.base_name);
         symbol.pretty_name = strip_verilog_prefix(symbol.name);
 
@@ -409,7 +409,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
       symbol.base_name = declarator.base_name();
       symbol.location = declarator.source_location();
-      symbol.type = convert_type(declarator.merged_type(decl.type()));
+      symbol.type = elaborate_type(declarator.merged_type(decl.type()));
 
       if(symbol.base_name.empty())
       {
@@ -470,7 +470,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
       symbol.base_name = declarator.base_name();
       symbol.location = declarator.source_location();
-      symbol.type = convert_type(declarator.merged_type(decl.type()));
+      symbol.type = elaborate_type(declarator.merged_type(decl.type()));
 
       if(symbol.base_name.empty())
       {
@@ -524,7 +524,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
     typet return_type;
 
     if(decl_class == ID_function)
-      return_type = convert_type(decl.type());
+      return_type = elaborate_type(decl.type());
     else
       return_type = empty_typet();
 
@@ -941,7 +941,7 @@ void verilog_typecheckt::elaborate_symbol_rec(irep_idt identifier)
     {
       // No, elaborate the type.
       auto elaborated_type =
-        convert_type(to_type_with_subtype(symbol.type).subtype());
+        elaborate_type(to_type_with_subtype(symbol.type).subtype());
       symbol.type = elaborated_type;
 
       // Now elaborate the value, possibly recursively, if any.

src/verilog/verilog_typecheck_type.cpp renamed to src/verilog/verilog_elaborate_type.cpp

@@ -69,7 +69,7 @@ array_typet verilog_typecheck_exprt::convert_unpacked_array_type(
   }
 
   // recursively convert element_type
-  typet element_type = convert_type(src.subtype());
+  typet element_type = elaborate_type(src.subtype());
 
   const exprt final_size_expr = from_integer(size, integer_typet());
   auto result = array_typet{element_type, final_size_expr};
@@ -81,7 +81,7 @@ array_typet verilog_typecheck_exprt::convert_unpacked_array_type(
 
 /*******************************************************************\
 
-Function: verilog_typecheck_exprt::convert_type
+Function: verilog_typecheck_exprt::elaborate_type
 
   Inputs:
 
@@ -91,11 +91,11 @@ Function: verilog_typecheck_exprt::convert_type
 
 \*******************************************************************/
 
-typet verilog_typecheck_exprt::convert_type(const typet &src)
+typet verilog_typecheck_exprt::elaborate_type(const typet &src)
 {
   const auto &source_location = src.source_location();
 
-  if(src.is_nil() || src.id()==ID_reg)
+  if(src.is_nil() || src.id() == ID_reg)
   {
     // it's just a bit
     return bool_typet().with_source_location(source_location);
@@ -170,15 +170,15 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     // The default base type is 'int'.
     auto &enum_type = to_verilog_enum_type(src);
     auto result = enum_type.has_base_type()
-                    ? convert_type(enum_type.base_type())
+                    ? elaborate_type(enum_type.base_type())
                     : signedbv_typet(32);
     result.set(ID_C_verilog_type, ID_verilog_enum);
     result.set(ID_C_identifier, enum_type.identifier());
     return result.with_source_location(source_location);
   }
   else if(src.id() == ID_verilog_packed_array)
   {
-    const exprt &range=static_cast<const exprt &>(src.find(ID_range));
+    const exprt &range = static_cast<const exprt &>(src.find(ID_range));
 
     mp_integer msb, lsb;
     convert_range(range, msb, lsb);
@@ -201,7 +201,8 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     {
       // we have a bit-vector type, not an array
 
-      bitvector_typet dest(subtype.id()==ID_signed?ID_signedbv:ID_unsignedbv);
+      bitvector_typet dest(
+        subtype.id() == ID_signed ? ID_signedbv : ID_unsignedbv);
 
       dest.add_source_location() = source_location;
       dest.set_width(width.to_ulong());
@@ -214,8 +215,8 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     {
       // We have a multi-dimensional packed array,
       // and do a recursive call.
-      const exprt size=from_integer(width, integer_typet());
-      typet s=convert_type(subtype);
+      const exprt size = from_integer(width, integer_typet());
+      typet s = elaborate_type(subtype);
 
       array_typet result(s, size);
       result.add_source_location() = source_location;
@@ -239,12 +240,12 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
       return expr.type().with_source_location(source_location);
     }
     else
-      return convert_type(type_reference.type_op());
+      return elaborate_type(type_reference.type_op());
   }
   else if(src.id() == ID_to_be_elaborated)
   {
     // recursive call
-    return convert_type(to_to_be_elaborated_type(src).subtype());
+    return elaborate_type(to_to_be_elaborated_type(src).subtype());
   }
   else if(src.id() == ID_struct || src.id() == ID_union)
   {
@@ -259,7 +260,7 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
         declaration.id() == ID_decl, "struct type must have declarations");
 
       // Convert the type
-      auto type = convert_type(declaration_expr.type());
+      auto type = elaborate_type(declaration_expr.type());
 
       // Convert the declarators
       for(auto &declarator_expr : declaration_expr.operands())

src/verilog/verilog_typecheck_expr.cpp

@@ -916,7 +916,7 @@ exprt verilog_typecheck_exprt::convert_nullary_expr(nullary_exprt expr)
   else if(expr.id() == ID_type)
   {
     // Used, e.g., for $bits
-    expr.type() = convert_type(expr.type());
+    expr.type() = elaborate_type(expr.type());
     return std::move(expr);
   }
   else
@@ -2432,13 +2432,13 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     // SystemVerilog has got type'(expr). This is an explicit
     // type cast.
     convert_expr(expr.op());
-    auto new_type = convert_type(expr.type());
+    auto new_type = elaborate_type(expr.type());
     return typecast_exprt{expr.op(), new_type}.with_source_location(expr);
   }
   else if(expr.id() == ID_verilog_implicit_typecast)
   {
     // We generate implict casts during elaboration.
-    expr.type() = convert_type(expr.type());
+    expr.type() = elaborate_type(expr.type());
     convert_expr(expr.op());
     expr.id(ID_typecast);
   }

src/verilog/verilog_typecheck_expr.h

@@ -60,7 +60,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 
   void propagate_type(exprt &expr, const typet &type);
 
-  typet convert_type(const typet &);
+  typet elaborate_type(const typet &);
   typet convert_enum(const class verilog_enum_typet &);
   array_typet convert_unpacked_array_type(const type_with_subtypet &);