Verilog: get_width now returns mp_integer

This avoids checking for overflows when adding up widths.

Author: kroening

src/verilog/verilog_synthesis.cpp

@@ -299,33 +299,33 @@ void verilog_synthesist::assignment_rec(
   {
     // TODO: split it up more intelligently;
     // bit-wise is wasteful.
-    unsigned offset=0;
-    
+    mp_integer offset = 0;
+
     // do it from right to left
 
     for(exprt::operandst::const_reverse_iterator
         it=lhs.operands().rbegin();
         it!=lhs.operands().rend();
         it++)
     {
-      constant_exprt offset_constant{std::to_string(offset), natural_typet{}};
+      auto offset_constant = from_integer(offset, natural_typet{});
 
       if(it->type().id()==ID_bool)
       {
         exprt bit_extract(ID_extractbit, it->type());
         bit_extract.add_to_operands(rhs);
         bit_extract.add_to_operands(offset_constant);
-        offset++;
+        ++offset;
 
         assignment_rec(*it, bit_extract, blocking);
       }
       else if(it->type().id()==ID_signedbv ||
               it->type().id()==ID_unsignedbv)
       {
-        unsigned width=get_width(it->type());
+        auto width = get_width(it->type());
 
-        constant_exprt offset_constant2{std::to_string(offset + width - 1),
-                                        natural_typet{}};
+        auto offset_constant2 =
+          from_integer(offset + width - 1, natural_typet{});
 
         // extractbits requires that upper >= lower, i.e. op1 >= op2
         extractbits_exprt bit_extract(rhs, offset_constant2, offset_constant,
@@ -1682,29 +1682,30 @@ void verilog_synthesist::synth_force_rec(
   if(lhs.id()==ID_concatenation)
   {
     // split it up
-    unsigned offset=0;
-    
+    mp_integer offset = 0;
+
     // do it from right to left
 
     for(exprt::operandst::const_reverse_iterator
         it=lhs.operands().rbegin();
         it!=lhs.operands().rend();
         it++)
     {
-      constant_exprt offset_constant{std::to_string(offset), natural_typet{}};
+      auto offset_constant = from_integer(offset, natural_typet{});
 
       if(it->type().id()==ID_bool)
       {
-        extractbit_exprt bit_extract(rhs, offset);
-        offset++;
+        extractbit_exprt bit_extract(rhs, offset_constant);
+        ++offset;
         synth_force_rec(*it, bit_extract);
       }
       else if(it->type().id()==ID_signedbv ||
               it->type().id()==ID_unsignedbv)
       {
-        unsigned width=get_width(it->type());
+        auto width = get_width(it->type());
+        auto sum_constant = from_integer(offset + width - 1, natural_typet{});
         extractbits_exprt bit_extract(
-          rhs, offset, offset + width - 1, it->type());
+          rhs, offset_constant, sum_constant, it->type());
         synth_force_rec(*it, bit_extract);
         offset+=width;
       }

src/verilog/verilog_typecheck_base.cpp

@@ -167,7 +167,7 @@ Function: verilog_typecheck_baset::get_width
 
 \*******************************************************************/
 
-std::size_t verilog_typecheck_baset::get_width(const typet &type)
+mp_integer verilog_typecheck_baset::get_width(const typet &type)
 {
   if(type.id()==ID_bool)
     return 1;
@@ -188,7 +188,7 @@ std::size_t verilog_typecheck_baset::get_width(const typet &type)
     mp_integer sum = 0;
     for(auto &component : to_struct_type(type).components())
       sum += get_width(component.type());
-    return sum.to_ulong();
+    return sum;
   }
 
   if(type.id() == ID_verilog_shortint)

src/verilog/verilog_typecheck_base.h

@@ -38,9 +38,12 @@ class verilog_typecheck_baset:public typecheckt
 protected:
   const namespacet &ns;
   const irep_idt mode;
-  
-  std::size_t get_width(const exprt &expr) { return get_width(expr.type()); }
-  std::size_t get_width(const typet &type);
+
+  mp_integer get_width(const exprt &expr)
+  {
+    return get_width(expr.type());
+  }
+  mp_integer get_width(const typet &type);
   mp_integer array_size(const array_typet &);
   mp_integer array_offset(const array_typet &);
   typet index_type(const array_typet &);

src/verilog/verilog_typecheck_expr.cpp

@@ -266,8 +266,8 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr)
       throw errort().with_location(expr.source_location())
         << "concatenation expected to have at least one operand";
     }
-    
-    unsigned width=0;
+
+    mp_integer width = 0;
     bool has_verilogbv=false;
 
     Forall_operands(it, expr)
@@ -300,23 +300,24 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr)
       if(op.type().id() == ID_signedbv || op.type().id() == ID_verilog_signedbv)
       {
         auto width = get_width(op);
+        auto width_int = numeric_cast_v<std::size_t>(width);
         if(op.type().id() == ID_verilog_signedbv)
-          op = typecast_exprt(op, verilog_unsignedbv_typet(width));
+          op = typecast_exprt{op, verilog_unsignedbv_typet{width_int}};
         else
-          op = typecast_exprt(op, unsignedbv_typet(width));
+          op = typecast_exprt{op, unsignedbv_typet{width_int}};
       }
     }
 
     expr.type()=typet(has_verilogbv?ID_verilog_unsignedbv:ID_unsignedbv);
-    expr.type().set(ID_width, width);
-    
+    expr.type().set(ID_width, integer2string(width));
+
     if(has_verilogbv)
     {
       Forall_operands(it, expr)
         if(it->type().id()!=ID_verilog_unsignedbv)
         {
-          unsigned width=get_width(*it);
-          *it = typecast_exprt{*it, verilog_unsignedbv_typet{width}};
+          auto width_int = numeric_cast_v<std::size_t>(get_width(*it));
+          *it = typecast_exprt{*it, verilog_unsignedbv_typet{width_int}};
         }
     }
 
@@ -2045,13 +2046,14 @@ exprt verilog_typecheck_exprt::convert_replication_expr(replication_exprt expr)
   {
     expr.op0()=from_integer(op0, natural_typet());
 
-    std::size_t new_width = op0.to_ulong() * width;
+    auto new_width = op0 * width;
+    auto new_width_int = numeric_cast_v<std::size_t>(new_width);
 
     if(op1.type().id()==ID_verilog_unsignedbv ||
        op1.type().id()==ID_verilog_signedbv)
-      expr.type()=verilog_unsignedbv_typet(new_width);
+      expr.type() = verilog_unsignedbv_typet{new_width_int};
     else
-      expr.type()=unsignedbv_typet(new_width);
+      expr.type() = unsignedbv_typet{new_width_int};
   }
 
   return std::move(expr);
@@ -2327,10 +2329,10 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
     if(op2 < offset)
     {
       auto padding_width = offset - op2;
-      auto padding =
-        from_integer(0, unsignedbv_typet{(padding_width).to_ulong()});
-      auto new_type =
-        unsignedbv_typet{(get_width(op0.type()) + padding_width).to_ulong()};
+      auto padding = from_integer(
+        0, unsignedbv_typet{numeric_cast_v<std::size_t>(padding_width)});
+      auto new_type = unsignedbv_typet{
+        numeric_cast_v<std::size_t>(get_width(op0.type()) + padding_width)};
       expr.op0() = concatenation_exprt(expr.op0(), padding, new_type);
       op2 += padding_width;
       op1 += padding_width;
@@ -2339,16 +2341,17 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
     if(op1 >= width + offset)
     {
       auto padding_width = op1 - (width + offset) + 1;
-      auto padding =
-        from_integer(0, unsignedbv_typet{padding_width.to_ulong()});
-      auto new_type =
-        unsignedbv_typet{(get_width(op0.type()) + padding_width).to_ulong()};
+      auto padding = from_integer(
+        0, unsignedbv_typet{numeric_cast_v<std::size_t>(padding_width)});
+      auto new_type = unsignedbv_typet{
+        numeric_cast_v<std::size_t>(get_width(op0.type()) + padding_width)};
       expr.op0() = concatenation_exprt(padding, expr.op0(), new_type);
     }
 
     // Part-select expressions are unsigned, even if the
     // entire expression is selected!
-    auto expr_type = unsignedbv_typet((op1 - op2).to_ulong() + 1);
+    auto expr_type =
+      unsignedbv_typet{numeric_cast_v<std::size_t>(op1 - op2 + 1)};
 
     op2 -= offset;
     op1 -= offset;

src/verilog/verilog_types.h

@@ -65,7 +65,8 @@ class verilog_signedbv_typet:public bitvector_typet
   {
   }
 
-  explicit inline verilog_signedbv_typet(unsigned width):bitvector_typet(ID_verilog_signedbv, width)
+  explicit inline verilog_signedbv_typet(std::size_t width)
+    : bitvector_typet(ID_verilog_signedbv, width)
   {
   }
 };
@@ -102,7 +103,8 @@ class verilog_unsignedbv_typet:public bitvector_typet
   {
   }
 
-  explicit inline verilog_unsignedbv_typet(unsigned width):bitvector_typet(ID_verilog_unsignedbv, width)
+  explicit inline verilog_unsignedbv_typet(std::size_t width)
+    : bitvector_typet(ID_verilog_unsignedbv, width)
   {
   }
 };