Verilog: use instance_array for width of primitive gates

This switches the "range" annotation on primitive gates to the unpacked
array as required by 1800-2017.

Author: kroening

src/verilog/parser.y

@@ -3125,12 +3125,7 @@ name_of_gate_instance:
 	  TOK_NON_TYPE_IDENTIFIER unpacked_dimension_brace
 	        { init($$, ID_inst);
 	          addswap($$, ID_base_name, $1);
-	          if(stack_expr($2).is_not_nil())
-	          {
-	            auto &range = stack_expr($$).add(ID_range);
-	            range = stack_expr($2).find(ID_range);
-	            range.id(ID_range);
-	          }
+	          addswap($$, ID_verilog_instance_array, $2);
 	        }
 	;
 

src/verilog/verilog_expr.h

@@ -903,6 +903,11 @@ class verilog_inst_baset : public verilog_module_itemt
              connections.front().id() == ID_named_port_connection;
     }
 
+    bool has_instance_array() const
+    {
+      return instance_array().is_not_nil();
+    }
+
     const typet &instance_array() const
     {
       return static_cast<const typet &>(find(ID_verilog_instance_array));

src/verilog/verilog_interfaces.cpp

@@ -177,21 +177,16 @@ void verilog_typecheckt::interface_inst(
   const verilog_inst_baset &statement,
   const verilog_instt::instancet &op)
 {
-  if(op.instance_array().is_not_nil())
+  bool primitive = statement.id() == ID_inst_builtin;
+
+  if(op.has_instance_array() && !primitive)
   {
     throw errort().with_location(op.source_location())
       << "no support for instance arrays";
   }
 
-  bool primitive=statement.id()==ID_inst_builtin;
-  const exprt &range_expr = static_cast<const exprt &>(op.find(ID_range));
-
-  ranget range;
-
-  if(range_expr.is_nil() || range_expr.id().empty())
-    range = ranget{0, 0};
-  else
-    range = convert_range(range_expr);
+  if(op.has_instance_array())
+    (void)elaborate_type(op.instance_array());
 
   irep_idt instantiated_module_identifier =
     verilog_module_symbol(id2string(statement.get(ID_module)));

src/verilog/verilog_typecheck.cpp

@@ -206,28 +206,15 @@ Function: verilog_typecheckt::typecheck_builtin_port_connections
 void verilog_typecheckt::typecheck_builtin_port_connections(
   verilog_inst_baset::instancet &inst)
 {
-  exprt &range_expr = static_cast<exprt &>(inst.add(ID_range));
-
-  ranget range;
-
-  if(range_expr.is_nil() || range_expr.id() == irep_idt{})
-    range = ranget{0, 0};
-  else
-    range = convert_range(range_expr);
-
-  if(range.lsb > range.msb)
-    std::swap(range.lsb, range.msb);
-  mp_integer width = range.length();
-
-  inst.remove(ID_range);
-
-  typet &type=inst.type();
-  if(width==1)
-    type.id(ID_bool);
+  if(!inst.has_instance_array())
+    inst.type() = bool_typet{};
   else
   {
-    type.id(ID_unsignedbv);
-    type.set(ID_width, integer2string(width));
+    // We'll turn a one-dimensional array into a bit-vector
+    auto &array_type = to_array_type(inst.instance_array());
+    auto width =
+      numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
+    inst.type() = unsignedbv_typet{width};
   }
 
   for(auto &connection : inst.connections())
@@ -247,7 +234,7 @@ void verilog_typecheckt::typecheck_builtin_port_connections(
     }
 
     // like an assignment
-    assignment_conversion(connection, type);
+    assignment_conversion(connection, inst.type());
   }
 }
 
@@ -543,10 +530,16 @@ Function: verilog_typecheckt::convert_inst_builtin
 void verilog_typecheckt::convert_inst_builtin(
   verilog_inst_builtint &inst)
 {
-  const irep_idt &inst_module=inst.get_module();
-
+  const irep_idt &inst_module = inst.get_module();
   for(auto &instance : inst.instances())
   {
+    // typecheck the instance array type, if any
+    if(instance.has_instance_array())
+    {
+      auto &instance_array = instance.instance_array();
+      instance_array = elaborate_type(instance_array);
+    }
+
     typecheck_builtin_port_connections(instance);
 
     // check built-in ones