Merge pull request #1340 from diffblue/verilog-size-cast

Verilog: explicit casts are assignments

Author: tautschnig

CHANGELOG

@@ -1,7 +1,8 @@
 # EBMC 5.8
 
-* SystemVerilog: cover sequence
 * Verilog: semantic fix for output register ports
+* SystemVerilog: cover sequence
+* SystemVerilog: semantics fix for explicit casts
 
 # EBMC 5.7
 

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.

regression/verilog/expressions/static_cast4.desc

@@ -0,0 +1,8 @@
+CORE
+static_cast4.sv
+--module main
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/expressions/static_cast4.sv

@@ -0,0 +1,17 @@
+module main;
+
+  // The standard suggests that casts can be applied to assignment patterns.
+  // VCS, Icarus Verilog and Xcelium error this.
+  // Questa allows it.
+  // Riviera throws an internal error.
+
+  typedef struct packed { int a, b; } S;
+
+  initial begin
+    S some_struct;
+    some_struct.a = 1;
+    some_struct.b = 2;
+    assert ((S'('{a: 1, b: 2})) == some_struct);
+  end
+
+endmodule

src/verilog/verilog_expr.h

@@ -2558,12 +2558,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 &
@@ -2659,11 +2653,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,27 @@ 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);
+    expr.type() = verilog_lowering(expr.type());
+    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 verilog_lowering(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);
+    expr.type() = verilog_lowering(expr.type());
+    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,22 @@ 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());
+
+    // In contrast to assignments, these can turn integers into enums
+    // (1800-2017 6.19.3).
+    if(expr.type().get(ID_C_verilog_type) == ID_verilog_enum)
+    {
+      expr.op() = typecast_exprt::conditional_cast(expr.op(), expr.type());
+    }
+    else
+    {
+      assignment_conversion(expr.op(), expr.type());
+    }
+
+    CHECK_RETURN(expr.op().type() == expr.type());
   }
   else if(expr.id() == ID_verilog_explicit_signing_cast)
   {
@@ -3327,6 +3340,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(