Verilog: extract verilog_bits(...) function

src/verilog/Makefile

@@ -1,6 +1,7 @@
 SRC = aval_bval_encoding.cpp \
       expr2verilog.cpp \
       sva_expr.cpp \
+      verilog_bits.cpp \
       verilog_elaborate.cpp \
       verilog_elaborate_type.cpp \
       verilog_expr.cpp \

src/verilog/verilog_bits.cpp

@@ -0,0 +1,89 @@
+/*******************************************************************\
+
+Module: Verilog Type Width
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "verilog_bits.h"
+
+#include <util/arith_tools.h>
+
+#include <ebmc/ebmc_error.h>
+
+#include "verilog_types.h"
+
+std::optional<mp_integer> verilog_bits_opt(const typet &type)
+{
+  if(type.id() == ID_bool)
+    return 1;
+
+  if(
+    type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+    type.id() == ID_verilog_signedbv || type.id() == ID_verilog_unsignedbv)
+    return type.get_int(ID_width);
+
+  if(type.id() == ID_array)
+  {
+    auto &array_type = to_array_type(type);
+    auto element_width_opt = verilog_bits_opt(array_type.element_type());
+    auto size_opt = numeric_cast<mp_integer>(array_type.size());
+
+    if(element_width_opt.has_value() && size_opt.has_value())
+    {
+      return element_width_opt.value() * size_opt.value();
+    }
+    else
+      return {};
+  }
+
+  if(type.id() == ID_struct)
+  {
+    // add them up
+    mp_integer sum = 0;
+    for(auto &component : to_struct_type(type).components())
+    {
+      auto component_width = verilog_bits_opt(component.type());
+      if(!component_width.has_value())
+        return {};
+      sum += *component_width;
+    }
+    return sum;
+  }
+
+  if(type.id() == ID_union)
+  {
+    // find the biggest
+    mp_integer max = 0;
+    for(auto &component : to_verilog_union_type(type).components())
+      max = std::max(max, verilog_bits(component.type()));
+    return max;
+  }
+
+  if(type.id() == ID_verilog_shortint)
+    return 16;
+  else if(type.id() == ID_verilog_int)
+    return 32;
+  else if(type.id() == ID_verilog_longint)
+    return 64;
+  else if(type.id() == ID_verilog_integer)
+    return 32;
+  else if(type.id() == ID_verilog_time)
+    return 64;
+
+  return {};
+}
+
+mp_integer verilog_bits(const typet &type)
+{
+  auto bits_opt = verilog_bits_opt(type);
+
+  if(bits_opt.has_value())
+    return std::move(bits_opt.value());
+  else
+  {
+    throw ebmc_errort() << "type `" << type.id()
+                        << "' has unknown number of bits";
+  }
+}

src/verilog/verilog_bits.h

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Verilog Type Width
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_VERILOG_BITS_H
+#define CPROVER_VERILOG_BITS_H
+
+#include <util/expr.h>
+#include <util/mp_arith.h>
+
+/// $bits -- throws an exception if no width
+mp_integer verilog_bits(const typet &);
+
+/// $bits -- throws an exception if no width
+inline mp_integer verilog_bits(const exprt &expr)
+{
+  return verilog_bits(expr.type());
+}
+
+/// $bits
+std::optional<mp_integer> verilog_bits_opt(const typet &);
+
+#endif

src/verilog/verilog_typecheck_base.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 
 #include "expr2verilog.h"
+#include "verilog_bits.h"
 #include "verilog_types.h"
 
 /*******************************************************************\
@@ -159,74 +160,6 @@ mp_integer verilog_typecheck_baset::array_offset(const array_typet &type)
 
 /*******************************************************************\
 
-Function: verilog_typecheck_baset::get_width_opt
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-std::optional<mp_integer>
-verilog_typecheck_baset::get_width_opt(const typet &type)
-{
-  if(type.id()==ID_bool)
-    return 1;
-
-  if(type.id()==ID_unsignedbv || type.id()==ID_signedbv ||
-     type.id()==ID_verilog_signedbv || type.id()==ID_verilog_unsignedbv)
-    return type.get_int(ID_width);
-
-  if(type.id()==ID_array)
-  {
-    auto element_width = get_width_opt(to_array_type(type).element_type());
-    if(element_width.has_value())
-      return array_size(to_array_type(type)) * element_width.value();
-    else
-      return {};
-  }
-
-  if(type.id() == ID_struct)
-  {
-    // add them up
-    mp_integer sum = 0;
-    for(auto &component : to_struct_type(type).components())
-    {
-      auto component_width = get_width_opt(component.type());
-      if(!component_width.has_value())
-        return {};
-      sum += *component_width;
-    }
-    return sum;
-  }
-
-  if(type.id() == ID_union)
-  {
-    // find the biggest
-    mp_integer max = 0;
-    for(auto &component : to_verilog_union_type(type).components())
-      max = std::max(max, get_width(component.type()));
-    return max;
-  }
-
-  if(type.id() == ID_verilog_shortint)
-    return 16;
-  else if(type.id() == ID_verilog_int)
-    return 32;
-  else if(type.id() == ID_verilog_longint)
-    return 64;
-  else if(type.id() == ID_verilog_integer)
-    return 32;
-  else if(type.id() == ID_verilog_time)
-    return 64;
-
-  return {};
-}
-
-/*******************************************************************\
-
 Function: verilog_typecheck_baset::get_width
 
   Inputs:
@@ -239,13 +172,13 @@ Function: verilog_typecheck_baset::get_width
 
 mp_integer verilog_typecheck_baset::get_width(const typet &type)
 {
-  auto width_opt = get_width_opt(type);
+  auto bits_opt = verilog_bits_opt(type);
 
-  if(width_opt.has_value())
-    return std::move(width_opt.value());
+  if(bits_opt.has_value())
+    return std::move(bits_opt.value());
   else
     throw errort().with_location(type.source_location())
-      << "type `" << type.id() << "' has unknown width";
+      << "type `" << type.id() << "' has unknown number of bits";
 }
 
 /*******************************************************************\

src/verilog/verilog_typecheck_base.h

@@ -51,7 +51,6 @@ class verilog_typecheck_baset:public typecheckt
   }
 
   static mp_integer get_width(const typet &);
-  static std::optional<mp_integer> get_width_opt(const typet &);
   static mp_integer array_size(const array_typet &);
   static mp_integer array_offset(const array_typet &);
   static typet index_type(const array_typet &);

src/verilog/verilog_typecheck_expr.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/string2int.h>
 
 #include "expr2verilog.h"
+#include "verilog_bits.h"
 #include "verilog_expr.h"
 #include "verilog_types.h"
 #include "vtype.h"
@@ -447,15 +448,16 @@ Function: verilog_typecheck_exprt::bits
 
 exprt verilog_typecheck_exprt::bits(const exprt &expr)
 {
-  auto width_opt = get_width_opt(expr.type());
+  auto bits_opt = verilog_bits_opt(expr.type());
 
-  if(!width_opt.has_value())
+  if(!bits_opt.has_value())
   {
     throw errort().with_location(expr.source_location())
       << "failed to determine number of bits of " << to_string(expr);
   }
 
-  return from_integer(width_opt.value(), integer_typet());
+  return from_integer(bits_opt.value(), integer_typet())
+    .with_source_location(expr.source_location());
 }
 
 /*******************************************************************\

src/verilog/verilog_types.h

@@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_VERILOG_TYPES_H
 #define CPROVER_VERILOG_TYPES_H
 
-#include <util/std_types.h>
+#include <util/bitvector_types.h>
 
 /// Used during elaboration only,
 /// to signal that a symbol is yet to be elaborated.