Verilog: get_width now returns mp_integer

This avoids checking for overflows when adding up widths.

Author: kroening

src/verilog/verilog_synthesis.cpp

@@ -300,7 +300,7 @@ 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
 
@@ -309,24 +309,24 @@ void verilog_synthesist::assignment_rec(
         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,
@@ -1638,7 +1638,7 @@ 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
 
@@ -1647,20 +1647,21 @@ void verilog_synthesist::synth_force_rec(
         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;

src/verilog/verilog_typecheck_base.h

@@ -39,8 +39,8 @@ class verilog_typecheck_baset:public typecheckt
   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

@@ -267,7 +267,7 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr)
         << "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<unsigned>(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<unsigned>(get_width(*it));
+          *it = typecast_exprt{*it, verilog_unsignedbv_typet{width_int}};
         }
     }
 
@@ -1994,13 +1995,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<unsigned>(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);
@@ -2277,9 +2279,9 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
     {
       auto padding_width = offset - op2;
       auto padding =
-        from_integer(0, unsignedbv_typet{(padding_width).to_ulong()});
+        from_integer(0, unsignedbv_typet{numeric_cast_v<unsigned>(padding_width)});
       auto new_type =
-        unsignedbv_typet{(get_width(op0.type()) + padding_width).to_ulong()};
+        unsignedbv_typet{numeric_cast_v<unsigned>(get_width(op0.type()) + padding_width)};
       expr.op0() = concatenation_exprt(expr.op0(), padding, new_type);
       op2 += padding_width;
       op1 += padding_width;
@@ -2289,15 +2291,15 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
     {
       auto padding_width = op1 - (width + offset) + 1;
       auto padding =
-        from_integer(0, unsignedbv_typet{padding_width.to_ulong()});
+        from_integer(0, unsignedbv_typet{numeric_cast_v<unsigned>(padding_width)});
       auto new_type =
-        unsignedbv_typet{(get_width(op0.type()) + padding_width).to_ulong()};
+        unsignedbv_typet{numeric_cast_v<unsigned>(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<unsigned>(op1 - op2 + 1)};
 
     op2 -= offset;
     op1 -= offset;