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_typecheck_expr.cpp

@@ -2438,7 +2438,7 @@ void verilog_typecheck_exprt::tc_binary_expr(
 }
 
 /*******************************************************************\
-
+ 
 Function: zero_extend
 
   Inputs:
@@ -2451,10 +2451,17 @@ Function: zero_extend
 
 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();
+  if(expr.type().id() == ID_bool)
+  {
+    return zero_extend(typecast_exprt{expr, unsignedbv_typet{1}}, type);
+  }
+  else if(expr.type().id() == ID_integer)
+  {
+    return zero_extend(typecast_exprt{expr, unsignedbv_typet{32}}, type);
+  }
+
+#if 0
+  auto old_width = to_bitvector_type(expr.type()).get_width();
 
   // first make unsigned
   typet tmp_type;
@@ -2468,6 +2475,8 @@ static exprt zero_extend(const exprt &expr, const typet &type)
 
   return typecast_exprt::conditional_cast(
     typecast_exprt::conditional_cast(expr, tmp_type), type);
+#endif
+  return zero_extend_exprt{expr, type};
 }
 
 /*******************************************************************\