Verilog: explicit casts are assignments

Explicit casts, sich as size casts, act like assignments, and hence, use the
assignment conversion.

Author: kroening

CHANGELOG

@@ -1,5 +1,7 @@
 # EBMC 5.8
 
+* SystemVerilog: semantics fix for size casts
+
 # EBMC 5.7
 
 * Verilog: --initial-zero changes the default value from nondet to zero

regression/verilog/expressions/size_cast3.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 size_cast3.sv
 --module main
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This is not yet implemented.

regression/verilog/expressions/static_cast3.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 static_cast3.sv
 --module main
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This is not yet implemented.

src/verilog/verilog_expr.h

@@ -2554,12 +2554,6 @@ class verilog_explicit_size_cast_exprt : public binary_exprt
   {
     return op1();
   }
-
-  // lower to typecast
-  exprt lower() const
-  {
-    return typecast_exprt{op(), type()};
-  }
 };
 
 inline const verilog_explicit_size_cast_exprt &
@@ -2655,11 +2649,6 @@ class verilog_explicit_type_cast_exprt : public unary_exprt
         std::move(__type))
   {
   }
-
-  exprt lower() const
-  {
-    return typecast_exprt{op(), type()};
-  }
 };
 
 inline const verilog_explicit_type_cast_exprt &

src/verilog/verilog_lowering.cpp

@@ -471,16 +471,25 @@ exprt verilog_lowering(exprt expr)
   }
   else if(expr.id() == ID_verilog_explicit_type_cast)
   {
-    return verilog_lowering_cast(
-      to_typecast_expr(to_verilog_explicit_type_cast_expr(expr).lower()));
+    // These act like an assignment, and hence, the type checker
+    // has already converted the argument to the target type.
+    auto &type_cast = to_verilog_explicit_type_cast_expr(expr);
+    DATA_INVARIANT(
+      type_cast.op().type() == type_cast.type(), "type cast type consistency");
+    return type_cast.op();
   }
   else if(expr.id() == ID_verilog_explicit_signing_cast)
   {
     return to_verilog_explicit_signing_cast_expr(expr).lower();
   }
   else if(expr.id() == ID_verilog_explicit_size_cast)
   {
-    return to_verilog_explicit_size_cast_expr(expr).lower();
+    // These act like an assignment, and hence, the type checker
+    // has already converted the argument to the target type.
+    auto &size_cast = to_verilog_explicit_size_cast_expr(expr);
+    DATA_INVARIANT(
+      size_cast.op().type() == size_cast.type(), "size cast type consistency");
+    return size_cast.op();
   }
   else if(
     expr.id() == ID_verilog_streaming_concatenation_left_to_right ||

src/verilog/verilog_typecheck_expr.cpp

@@ -2694,9 +2694,10 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
   else if(expr.id() == ID_verilog_explicit_type_cast)
   {
     // SystemVerilog has got type'(expr). This is an explicit
-    // type cast.
+    // type cast. These are assignment contexts.
     convert_expr(expr.op());
     expr.type() = elaborate_type(expr.type());
+    assignment_conversion(expr.op(), expr.type());
   }
   else if(expr.id() == ID_verilog_explicit_signing_cast)
   {
@@ -3319,6 +3320,11 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
         << "cannot perform size cast on " << to_string(op_type);
     }
 
+    // These act like an assignment (1800-2017 6.24.1)
+    assignment_conversion(expr.rhs(), expr.type());
+
+    CHECK_RETURN(expr.rhs().type() == expr.type());
+
     return std::move(expr);
   }
   else if(