Verilog: extract code for $typename, $left, $right into separate file

src/verilog/Makefile

@@ -2,6 +2,7 @@ SRC = aval_bval_encoding.cpp \
       convert_literals.cpp \
       expr2verilog.cpp \
       sva_expr.cpp \
+      typename.cpp \
       verilog_bits.cpp \
       verilog_elaborate.cpp \
       verilog_elaborate_type.cpp \

src/verilog/typename.cpp

@@ -0,0 +1,156 @@
+/*******************************************************************\
+
+Module: $typename
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "typename.h"
+
+#include <util/arith_tools.h>
+
+#include "verilog_bits.h"
+
+// unpacked array: left bound
+// packed array: index of most significant element
+// 0 otherwise
+mp_integer verilog_left(const typet &type)
+{
+  if(
+    type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+    type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
+    type.id() == ID_bool)
+  {
+    auto offset = type.get_int(ID_C_offset);
+    if(type.get_bool(ID_C_increasing))
+      return offset;
+    else
+      return offset + verilog_bits(type) - 1;
+  }
+  else if(type.id() == ID_array)
+  {
+    auto offset = numeric_cast_v<mp_integer>(
+      to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
+    if(type.get_bool(ID_C_increasing))
+      return offset;
+    else
+    {
+      return offset +
+             numeric_cast_v<mp_integer>(
+               to_constant_expr(to_array_type(type).size())) -
+             1;
+    }
+  }
+  else
+    return 0;
+}
+
+// unpacked array: right bound
+// packed array: index of least significant element
+// 0 otherwise
+mp_integer verilog_right(const typet &type)
+{
+  if(
+    type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+    type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
+    type.id() == ID_bool)
+  {
+    auto offset = type.get_int(ID_C_offset);
+    if(type.get_bool(ID_C_increasing))
+      return offset + verilog_bits(type) - 1;
+    else
+      return offset;
+  }
+  else if(type.id() == ID_array)
+  {
+    auto offset = numeric_cast_v<mp_integer>(
+      to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
+    if(type.get_bool(ID_C_increasing))
+    {
+      return offset +
+             numeric_cast_v<mp_integer>(
+               to_constant_expr(to_array_type(type).size())) -
+             1;
+    }
+    else
+      return offset;
+  }
+  else
+    return 0;
+}
+
+std::string verilog_typename(const typet &type)
+{
+  const auto verilog_type = type.get(ID_C_verilog_type);
+
+  auto left = [](const typet &type)
+  { return integer2string(verilog_left(type)); };
+  auto right = [](const typet &type)
+  { return integer2string(verilog_right(type)); };
+
+  if(type.id() == ID_unsignedbv)
+  {
+    if(verilog_type == ID_verilog_byte)
+      return "byte unsigned";
+    else if(verilog_type == ID_verilog_int)
+      return "int unsigned";
+    else if(verilog_type == ID_verilog_longint)
+      return "longint unsigned";
+    else if(verilog_type == ID_verilog_shortint)
+      return "shortint unsigned";
+    else
+      return "bit[" + left(type) + ":" + right(type) + "]";
+  }
+  else if(type.id() == ID_verilog_unsignedbv)
+  {
+    return "logic[" + left(type) + ":" + right(type) + "]";
+  }
+  else if(type.id() == ID_bool)
+  {
+    return "bit";
+  }
+  else if(type.id() == ID_signedbv)
+  {
+    if(verilog_type == ID_verilog_byte)
+      return "byte";
+    else if(verilog_type == ID_verilog_int)
+      return "int";
+    else if(verilog_type == ID_verilog_longint)
+      return "longint";
+    else if(verilog_type == ID_verilog_shortint)
+      return "shortint";
+    else
+      return "bit signed[" + left(type) + ":" + right(type) + "]";
+  }
+  else if(type.id() == ID_verilog_signedbv)
+  {
+    return "logic signed[" + left(type) + ":" + right(type) + "]";
+  }
+  else if(type.id() == ID_verilog_realtime)
+  {
+    return "realtime";
+  }
+  else if(type.id() == ID_verilog_real)
+  {
+    return "real";
+  }
+  else if(type.id() == ID_verilog_shortreal)
+  {
+    return "shortreal";
+  }
+  else if(type.id() == ID_verilog_chandle)
+  {
+    return "chandle";
+  }
+  else if(type.id() == ID_verilog_event)
+  {
+    return "event";
+  }
+  else if(type.id() == ID_verilog_string)
+  {
+    return "string";
+  }
+  else
+    return "?";
+}

src/verilog/typename.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: $typename
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_VERILOG_TYPENAME_H
+#define CPROVER_VERILOG_TYPENAME_H
+
+#include <util/mp_arith.h>
+
+class typet;
+
+/// Verilog's $left
+mp_integer verilog_left(const typet &);
+
+/// Verilog's $right
+mp_integer verilog_right(const typet &);
+
+/// Verilog's $typename
+std::string verilog_typename(const typet &);
+
+#endif

src/verilog/verilog_typecheck_expr.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include "aval_bval_encoding.h"
 #include "convert_literals.h"
 #include "expr2verilog.h"
+#include "typename.h"
 #include "verilog_bits.h"
 #include "verilog_expr.h"
 #include "verilog_lowering.h"
@@ -746,40 +747,7 @@ Function: verilog_typecheck_exprt::left
 
 constant_exprt verilog_typecheck_exprt::left(const exprt &expr)
 {
-  // unpacked array: left bound
-  // packed array: index of most significant element
-  // 0 otherwise
-  auto left = [](const typet &type) -> mp_integer {
-    if(
-      type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
-      type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
-      type.id() == ID_bool)
-    {
-      auto offset = type.get_int(ID_C_offset);
-      if(type.get_bool(ID_C_increasing))
-        return offset;
-      else
-        return offset + get_width(type) - 1;
-    }
-    else if(type.id() == ID_array)
-    {
-      auto offset = numeric_cast_v<mp_integer>(
-        to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
-      if(type.get_bool(ID_C_increasing))
-        return offset;
-      else
-      {
-        return offset +
-               numeric_cast_v<mp_integer>(
-                 to_constant_expr(to_array_type(type).size())) -
-               1;
-      }
-    }
-    else
-      return 0;
-  };
-
-  return from_integer(left(expr.type()), integer_typet{});
+  return from_integer(verilog_left(expr.type()), integer_typet{});
 }
 
 /*******************************************************************\
@@ -796,40 +764,7 @@ Function: verilog_typecheck_exprt::right
 
 constant_exprt verilog_typecheck_exprt::right(const exprt &expr)
 {
-  // unpacked array: right bound
-  // packed array: index of least significant element
-  // 0 otherwise
-  auto right = [](const typet &type) -> mp_integer {
-    if(
-      type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
-      type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
-      type.id() == ID_bool)
-    {
-      auto offset = type.get_int(ID_C_offset);
-      if(type.get_bool(ID_C_increasing))
-        return offset + get_width(type) - 1;
-      else
-        return offset;
-    }
-    else if(type.id() == ID_array)
-    {
-      auto offset = numeric_cast_v<mp_integer>(
-        to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
-      if(type.get_bool(ID_C_increasing))
-      {
-        return offset +
-               numeric_cast_v<mp_integer>(
-                 to_constant_expr(to_array_type(type).size())) -
-               1;
-      }
-      else
-        return offset;
-    }
-    else
-      return 0;
-  };
-
-  return from_integer(right(expr.type()), integer_typet{});
+  return from_integer(verilog_right(expr.type()), integer_typet{});
 }
 
 /*******************************************************************\
@@ -950,84 +885,8 @@ Function: verilog_typecheck_exprt::typename_string
 
 exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
 {
-  auto &type = expr.type();
-
-  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)
-  {
-    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_verilog_unsignedbv)
-  {
-    s = "logic[" + to_string(left) + ":" + to_string(right) + "]";
-  }
-  else if(type.id() == ID_bool)
-  {
-    s = "bit";
-  }
-  else if(type.id() == ID_signedbv)
-  {
-    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_signedbv)
-  {
-    s = "logic signed[" + to_string(left) + ":" + to_string(right) + "]";
-  }
-  else if(type.id() == ID_verilog_realtime)
-  {
-    s = "realtime";
-  }
-  else if(type.id() == ID_verilog_real)
-  {
-    s = "real";
-  }
-  else if(type.id() == ID_verilog_shortreal)
-  {
-    s = "shortreal";
-  }
-  else if(type.id() == ID_verilog_chandle)
-  {
-    s = "chandle";
-  }
-  else if(type.id() == ID_verilog_event)
-  {
-    s = "event";
-  }
-  else if(type.id() == ID_verilog_string)
-  {
-    s = "string";
-  }
-  else
-    s = "?";
-
-  auto result = convert_string_literal(s);
-  result.add_source_location() = expr.source_location();
-
-  return std::move(result);
+  auto s = verilog_typename(expr.type());
+  return convert_string_literal(s).with_source_location(expr);
 }
 
 /*******************************************************************\

unit/Makefile

@@ -11,6 +11,7 @@ SRC += smvlang/expr2smv.cpp \
        temporal-logic/sva_to_ltl.cpp \
        temporal-logic/nnf.cpp \
        temporal-logic/trivial_sva.cpp \
+       verilog/typename.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I . -I $(CPROVER_DIR)/unit -I $(CPROVER_DIR)/src