Merge pull request #357 from diffblue/verilog-type-reference

Verilog: type references

Author: tautschnig

regression/verilog/data-types/type_operator.desc

@@ -0,0 +1,8 @@
+CORE
+type_operator.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/data-types/type_operator.sv

@@ -0,0 +1,12 @@
+module main;
+
+  wire [31:0] some_wire;
+  wire type(some_wire) other_wire;
+
+  typedef bit [31:0] some_type;
+  wire some_type next_wire;
+
+  p0: assert property ($bits(other_wire) == 32);
+  p1: assert property ($bits(next_wire) == 32);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -106,6 +106,7 @@ IREP_ID_ONE(uwire)
 IREP_ID_ONE(wand)
 IREP_ID_ONE(automatic)
 IREP_ID_ONE(verilog_enum)
+IREP_ID_ONE(verilog_type_reference)
 IREP_ID_ONE(enum_names)
 IREP_ID_ONE(var)
 IREP_ID_ONE(trireg)

src/verilog/expr2verilog.cpp

@@ -1180,6 +1180,14 @@ std::string expr2verilogt::convert(const typet &type)
   {
     return "enum";
   }
+  else if(type.id() == ID_verilog_type_reference)
+  {
+    auto &type_reference = to_verilog_type_reference(type);
+    if(type_reference.expression_op().is_not_nil())
+      return "type(" + convert(type_reference.expression_op()) + ")";
+    else
+      return "type(" + convert(type_reference.type_op()) + ")";
+  }
 
   return "IREP("+type.pretty()+")";
 }

src/verilog/parser.y

@@ -1255,6 +1255,7 @@ data_type:
 	/*
 	| ps_covergroup_identifier
 	*/
+	| type_reference
 	;
 
 enum_name_value_opt:
@@ -1388,6 +1389,13 @@ simple_type:
 data_type_or_void: data_type | TOK_VOID
 	;
 
+type_reference:
+	  TOK_TYPE '(' expression ')'
+		{ init($$, ID_verilog_type_reference); mto($$, $3); }
+	| TOK_TYPE '(' data_type ')'
+		{ init($$, ID_verilog_type_reference); addswap($$, ID_type_arg, $3); }
+	;
+
 // System Verilog standard 1800-2017
 // A.2.2.2 Strengths
 

src/verilog/verilog_typecheck_type.cpp

@@ -164,6 +164,19 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
       return std::move(result);
     }
   }
+  else if(src.id() == ID_verilog_type_reference)
+  {
+    auto &type_reference = to_verilog_type_reference(src);
+    if(type_reference.expression_op().is_not_nil())
+    {
+      // the expression is not evaluated
+      auto expr = type_reference.expression_op();
+      convert_expr(expr);
+      return expr.type();
+    }
+    else
+      return convert_type(type_reference.type_op());
+  }
   else
   {
     error().source_location = source_location;

src/verilog/verilog_types.h

@@ -407,4 +407,49 @@ inline verilog_enum_typet &to_verilog_enum_type(typet &type)
   return static_cast<verilog_enum_typet &>(type);
 }
 
+class verilog_type_referencet : public typet
+{
+public:
+  // This comes in two flavors: a reference to the type
+  // of a given type, or of a given expression.
+  const exprt &expression_op() const
+  {
+    if(get_sub().size() == 1)
+      return static_cast<const exprt &>(get_sub().front());
+    else
+      return static_cast<const exprt &>(get_nil_irep());
+  }
+
+  const typet &type_op() const
+  {
+    return static_cast<const typet &>(find(ID_type_arg));
+  }
+};
+
+/*! \brief Cast a generic typet to a \ref verilog_type_referencet
+ *
+ * This is an unchecked conversion. \a type must be known to be \ref
+ * verilog_type_referencet.
+ *
+ * \param type Source type
+ * \return Object of type \ref verilog_type_referencet
+ *
+ * \ingroup gr_std_types
+*/
+inline const verilog_type_referencet &
+to_verilog_type_reference(const typet &type)
+{
+  PRECONDITION(type.id() == ID_verilog_type_reference);
+  return static_cast<const verilog_type_referencet &>(type);
+}
+
+/*! \copydoc to_verilog_type_reference(const typet &)
+ * \ingroup gr_std_types
+*/
+inline verilog_type_referencet &to_verilog_type_reference(typet &type)
+{
+  PRECONDITION(type.id() == ID_verilog_type_reference);
+  return static_cast<verilog_type_referencet &>(type);
+}
+
 #endif