SystemVerilog: $typename should return byte, int, shortint, etc.

When given byte, int, shortint, int, longint, $typename needs to return that
instead of the expansion.

Author: kroening

regression/verilog/data-types/signed2.sv

@@ -5,12 +5,18 @@ module main;
   assert final ($typename(bit unsigned[1:0]) == "bit[1:0]");
   assert final ($typename(bit signed) == "bit signed[0:0]");
   assert final ($typename(bit signed[1:0]) == "bit signed[1:0]");
-  assert final ($typename(byte) == "bit signed[7:0]");
-  assert final ($typename(byte unsigned) == "bit[7:0]");
-  assert final ($typename(byte signed) == "bit signed[7:0]");
-  assert final ($typename(int) == "bit signed[31:0]");
-  assert final ($typename(int unsigned) == "bit[31:0]");
-  assert final ($typename(int signed) == "bit signed[31:0]");
+  assert final ($typename(byte) == "byte");
+  assert final ($typename(byte unsigned) == "byte unsigned");
+  assert final ($typename(byte signed) == "byte");
+  assert final ($typename(int) == "int");
+  assert final ($typename(int unsigned) == "int unsigned");
+  assert final ($typename(int signed) == "int");
+  assert final ($typename(shortint) == "shortint");
+  assert final ($typename(shortint unsigned) == "shortint unsigned");
+  assert final ($typename(shortint signed) == "shortint");
+  assert final ($typename(longint) == "longint");
+  assert final ($typename(longint unsigned) == "longint unsigned");
+  assert final ($typename(longint signed) == "longint");
   assert final ($typename(integer) == "bit signed[31:0]");
   assert final ($typename(integer unsigned) == "bit[31:0]");
   assert final ($typename(integer signed) == "bit signed[31:0]");

regression/verilog/packages/package_typedef1.sv

@@ -8,6 +8,6 @@ module main;
 
   moo::my_type some_var;
 
-  assert final ($typename(some_var) == "bit signed[7:0]");
+  assert final ($typename(some_var) == "byte");
 
 endmodule

src/verilog/verilog_elaborate_type.cpp

@@ -219,7 +219,15 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
       auto rec = elaborate_type(subtype);
 
       if(rec.id() == ID_unsignedbv)
-        return signedbv_typet{to_unsignedbv_type(rec).width()};
+      {
+        auto dest = signedbv_typet{to_unsignedbv_type(rec).width()};
+
+        auto verilog_type = rec.get(ID_C_verilog_type);
+        if(verilog_type != irep_idt{})
+          dest.set(ID_C_verilog_type, verilog_type);
+
+        return dest;
+      }
       else if(rec.id() == ID_bool)
         return signedbv_typet{1};
       else
@@ -241,7 +249,15 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
       auto rec = elaborate_type(subtype);
 
       if(rec.id() == ID_signedbv)
-        return unsignedbv_typet{to_signedbv_type(rec).width()};
+      {
+        auto dest = unsignedbv_typet{to_signedbv_type(rec).width()};
+
+        auto verilog_type = rec.get(ID_C_verilog_type);
+        if(verilog_type != irep_idt{})
+          dest.set(ID_C_verilog_type, verilog_type);
+
+        return dest;
+      }
       else
         return rec;
     }
@@ -255,23 +271,21 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
   }
   else if(src.id() == ID_verilog_byte)
   {
-    // two-valued type, signed
-    return signedbv_typet{8}.with_source_location(source_location);
+    return verilog_byte_typet{}.lower().with_source_location(source_location);
   }
   else if(src.id() == ID_verilog_shortint)
   {
-    // two-valued type, signed
-    return signedbv_typet{16}.with_source_location(source_location);
+    return verilog_shortint_typet{}.lower().with_source_location(
+      source_location);
   }
   else if(src.id() == ID_verilog_int)
   {
-    // two-valued type, signed
-    return signedbv_typet{32}.with_source_location(source_location);
+    return verilog_int_typet{}.lower().with_source_location(source_location);
   }
   else if(src.id() == ID_verilog_longint)
   {
-    // two-valued type, signed
-    return signedbv_typet{64}.with_source_location(source_location);
+    return verilog_longint_typet{}.lower().with_source_location(
+      source_location);
   }
   else if(src.id() == ID_verilog_integer)
   {

src/verilog/verilog_typecheck_expr.cpp

@@ -727,19 +727,39 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
   auto left = this->left(expr);
   auto right = this->right(expr);
 
+  const auto verilog_type = type.get(ID_C_verilog_type);
+
   std::string s;
 
   if(type.id() == ID_unsignedbv || type.id() == ID_verilog_unsignedbv)
   {
-    s = "bit[" + to_string(left) + ":" + to_string(right) + "]";
+    if(verilog_type == ID_verilog_byte)
+      s = "byte unsigned";
+    else if(verilog_type == ID_verilog_int)
+      s = "int unsigned";
+    else if(verilog_type == ID_verilog_longint)
+      s = "longint unsigned";
+    else if(verilog_type == ID_verilog_shortint)
+      s = "shortint unsigned";
+    else
+      s = "bit[" + to_string(left) + ":" + to_string(right) + "]";
   }
   else if(type.id() == ID_bool)
   {
     s = "bit";
   }
   else if(type.id() == ID_signedbv || type.id() == ID_verilog_signedbv)
   {
-    s = "bit signed[" + to_string(left) + ":" + to_string(right) + "]";
+    if(verilog_type == ID_verilog_byte)
+      s = "byte";
+    else if(verilog_type == ID_verilog_int)
+      s = "int";
+    else if(verilog_type == ID_verilog_longint)
+      s = "longint";
+    else if(verilog_type == ID_verilog_shortint)
+      s = "shortint";
+    else
+      s = "bit signed[" + to_string(left) + ":" + to_string(right) + "]";
   }
   else if(type.id() == ID_verilog_realtime)
   {

src/verilog/verilog_types.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_VERILOG_TYPES_H
 
 #include <util/bitvector_types.h>
+#include <util/ieee_float.h>
 
 /// Used during elaboration only,
 /// to signal that a symbol is yet to be elaborated.
@@ -162,6 +163,13 @@ class verilog_real_typet:public typet
   {
     return 64;
   }
+
+  typet lower() const
+  {
+    auto type = ieee_float_spect::double_precision().to_type();
+    type.set(ID_C_verilog_type, ID_verilog_real);
+    return type;
+  }
 };
 
 /// 32-bit floating point
@@ -176,6 +184,13 @@ class verilog_shortreal_typet:public typet
   {
     return 32;
   }
+
+  typet lower() const
+  {
+    auto type = ieee_float_spect::single_precision().to_type();
+    type.set(ID_C_verilog_type, ID_verilog_shortreal);
+    return type;
+  }
 };
 
 /// 64-bit floating point
@@ -190,6 +205,13 @@ class verilog_realtime_typet:public typet
   {
     return 64;
   }
+
+  typet lower() const
+  {
+    auto type = ieee_float_spect::double_precision().to_type();
+    type.set(ID_C_verilog_type, ID_verilog_realtime);
+    return type;
+  }
 };
 
 /// 2-state data type, 16-bit signed integer
@@ -204,6 +226,13 @@ class verilog_shortint_typet : public typet
   {
     return 16;
   }
+
+  typet lower() const
+  {
+    auto type = signedbv_typet{width()};
+    type.set(ID_C_verilog_type, ID_verilog_shortint);
+    return type;
+  }
 };
 
 /// 2-state data type, 32-bit signed integer
@@ -221,7 +250,9 @@ class verilog_int_typet : public typet
 
   typet lower() const
   {
-    return signedbv_typet{width()};
+    auto type = signedbv_typet{width()};
+    type.set(ID_C_verilog_type, ID_verilog_int);
+    return type;
   }
 };
 
@@ -237,6 +268,13 @@ class verilog_longint_typet : public typet
   {
     return 64;
   }
+
+  typet lower() const
+  {
+    auto type = signedbv_typet{width()};
+    type.set(ID_C_verilog_type, ID_verilog_longint);
+    return type;
+  }
 };
 
 /// 2-state data type, 8-bit signed integer
@@ -251,6 +289,13 @@ class verilog_byte_typet : public typet
   {
     return 8;
   }
+
+  typet lower() const
+  {
+    auto type = signedbv_typet{width()};
+    type.set(ID_C_verilog_type, ID_verilog_byte);
+    return type;
+  }
 };
 
 /// 2-state data type, for vectors, unsigned