Verilog: separate ID for explicit typecast expressions

src/hw_cbmc_irep_ids.h

@@ -35,6 +35,8 @@ IREP_ID_TWO(C_little_endian, #little_endian)
 IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)
+IREP_ID_ONE(verilog_explicit_cast)
+IREP_ID_ONE(verilog_implicit_typecast)
 IREP_ID_ONE(verilog_non_indexed_part_select)
 IREP_ID_ONE(verilog_indexed_part_select_plus)
 IREP_ID_ONE(verilog_indexed_part_select_minus)

src/verilog/parser.y

@@ -3140,7 +3140,9 @@ time_literal: TOK_TIME_LITERAL
 
 cast:
 	  casting_type '\'' '(' expression ')'
-		{ init($$, ID_typecast); stack_expr($$).type() = stack_type($1); mto($$, $4); }
+		{ init($$, ID_verilog_explicit_cast);
+		  stack_expr($$).type() = stack_type($1);
+		  mto($$, $4); }
 	;
 
 // System Verilog standard 1800-2017

src/verilog/verilog_elaborate.cpp

@@ -118,7 +118,7 @@ void verilog_typecheckt::collect_symbols(const typet &type)
       if(enum_name.value().is_not_nil())
         initializer = enum_name.value();
 
-      exprt value = typecast_exprt(initializer, tbd_type);
+      exprt value = verilog_implicit_typecast_exprt(initializer, tbd_type);
       value.add_source_location() = enum_name.source_location();
 
       const auto base_name = enum_name.base_name();
@@ -135,8 +135,9 @@ void verilog_typecheckt::collect_symbols(const typet &type)
       add_symbol(std::move(enum_name_symbol));
 
       initializer = plus_exprt(
-        typecast_exprt(initializer, tbd_type),
-        typecast_exprt(from_integer(1, integer_typet()), tbd_type));
+        verilog_implicit_typecast_exprt(initializer, tbd_type),
+        verilog_implicit_typecast_exprt(
+          from_integer(1, integer_typet()), tbd_type));
     }
 
     // Add a symbol for the enum to the symbol table.

src/verilog/verilog_expr.h

@@ -1843,4 +1843,30 @@ inline verilog_module_sourcet &to_verilog_module_source(irept &irep)
   return static_cast<verilog_module_sourcet &>(irep);
 }
 
+class verilog_implicit_typecast_exprt : public unary_exprt
+{
+public:
+  verilog_implicit_typecast_exprt(exprt __op, typet __type)
+    : unary_exprt(
+        ID_verilog_implicit_typecast,
+        std::move(__op),
+        std::move(__type))
+  {
+  }
+};
+
+inline const verilog_implicit_typecast_exprt &
+to_verilog_implicit_typecast_expr(const exprt &expr)
+{
+  verilog_implicit_typecast_exprt::check(expr);
+  return static_cast<const verilog_implicit_typecast_exprt &>(expr);
+}
+
+inline verilog_implicit_typecast_exprt &
+to_verilog_implicit_typecast_expr(exprt &expr)
+{
+  verilog_implicit_typecast_exprt::check(expr);
+  return static_cast<verilog_implicit_typecast_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_typecheck_expr.cpp

@@ -1877,12 +1877,20 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     make_boolean(expr.op());
     expr.type()=bool_typet();
   }
-  else if(expr.id() == ID_typecast)
+  else if(expr.id() == ID_verilog_explicit_cast)
   {
     // System Verilog has got type'(expr). This is an explicit
     // type cast.
     expr.type() = convert_type(expr.type());
     convert_expr(expr.op());
+    expr.id(ID_typecast);
+  }
+  else if(expr.id() == ID_verilog_implicit_typecast)
+  {
+    // We generate implict casts during elaboration.
+    expr.type() = convert_type(expr.type());
+    convert_expr(expr.op());
+    expr.id(ID_typecast);
   }
   else
   {