Verilog: use zero_extend_exprt

This replaces a custom encoding via typecast_exprt used in the Verilog
front-end by zero_extend_exprt.

Author: kroening

src/verilog/expr2verilog.cpp

@@ -2007,6 +2007,9 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return convert_function(src.id_string(), src);
   }
 
+  else if(src.id() == ID_zero_extend)
+    return convert_rec(to_zero_extend_expr(src).op());
+
   // no VERILOG language expression for internal representation
   return convert_norep(src);
 }

src/verilog/verilog_lowering.cpp

@@ -625,6 +625,36 @@ exprt verilog_lowering(exprt expr)
     else
       return expr;
   }
+  else if(expr.id() == ID_zero_extend)
+  {
+    auto tmp_op = to_zero_extend_expr(expr).op();
+
+    if(tmp_op.type().id() == ID_bool)
+    {
+      tmp_op = typecast_exprt{expr, unsignedbv_typet{1}};
+    }
+    else if(expr.type().id() == ID_integer)
+    {
+      tmp_op = typecast_exprt{expr, unsignedbv_typet{32}};
+    }
+
+    auto old_width = to_bitvector_type(tmp_op.type()).get_width();
+
+    // first make unsigned
+    typet tmp_type;
+
+    if(expr.type().id() == ID_unsignedbv)
+      tmp_type = unsignedbv_typet{old_width};
+    else if(expr.type().id() == ID_verilog_unsignedbv)
+      tmp_type = verilog_unsignedbv_typet{old_width};
+    else
+      PRECONDITION(false);
+
+    auto unsigned_op = verilog_lowering_cast(typecast_exprt{tmp_op, tmp_type});
+
+    // then cast to target type
+    return verilog_lowering_cast(typecast_exprt{unsigned_op, expr.type()});
+  }
   else
     return expr; // leave as is
 

src/verilog/verilog_typecheck_expr.cpp

@@ -222,39 +222,6 @@ void verilog_typecheck_exprt::propagate_type(
 
 /*******************************************************************\
 
-Function: zero_extend
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-static exprt zero_extend(const exprt &expr, const typet &type)
-{
-  auto old_width = expr.type().id() == ID_bool ? 1
-                   : expr.type().id() == ID_integer
-                     ? 32
-                     : to_bitvector_type(expr.type()).get_width();
-
-  // first make unsigned
-  typet tmp_type;
-
-  if(type.id() == ID_unsignedbv)
-    tmp_type = unsignedbv_typet{old_width};
-  else if(type.id() == ID_verilog_unsignedbv)
-    tmp_type = verilog_unsignedbv_typet{old_width};
-  else
-    PRECONDITION(false);
-
-  return typecast_exprt::conditional_cast(
-    typecast_exprt::conditional_cast(expr, tmp_type), type);
-}
-
-/*******************************************************************\
-
 Function: verilog_typecheck_exprt::downwards_type_progatation
 
   Inputs:
@@ -331,7 +298,7 @@ void verilog_typecheck_exprt::downwards_type_propagation(
     // "If the operand shall be extended, then it shall be sign-extended only
     // if the propagated type is signed."
     // A typecast from signed to a larger unsigned would sign extend.
-    expr = zero_extend(expr, type);
+    expr = zero_extend_exprt{expr, type};
   }
   else
   {