SystemVerilog: IDs and classes for the explicit casts

regression/verilog/expressions/signing_cast1.desc

@@ -1,12 +1,12 @@
-KNOWNBUG
+CORE broken-smt-backend
 signing_cast1.sv
 --module main --bound 0
-^\[main\.p0\] always signed \[0:0\]'\(1'b1\) == -1: PROVED up to bound 0$
-^\[main\.p1\] always signed \[0:0\]'\(4'b1110\) == -2: PROVED up to bound 0$
-^\[main\.p2\] always signed \[0:0\]'\(4'b0111\) == 7: PROVED up to bound 0$
-^\[main\.p3\] always signed \[0:0\]'\(!0\) == -1: PROVED up to bound 0$
-^\[main\.p4\] always \[0:0\]'\(!0\) == 1: PROVED up to bound 0$
-^\[main\.p5\] always \[0:0\]'\(-1\) == 32'hFFFFFFFF: PROVED up to bound 0$
+^\[main\.p0\] always signed'\(1'b1\) == -1: PROVED up to bound 0$
+^\[main\.p1\] always signed'\(4'b1110\) == -2: PROVED up to bound 0$
+^\[main\.p2\] always signed'\(4'b0111\) == 7: PROVED up to bound 0$
+^\[main\.p3\] always signed'\(!0\) == -1: PROVED up to bound 0$
+^\[main\.p4\] always unsigned'\(!0\) == 1: PROVED up to bound 0$
+^\[main\.p5\] always unsigned'\(-1\) == 32'hFFFFFFFF: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/hw_cbmc_irep_ids.h

@@ -83,8 +83,10 @@ IREP_ID_ONE(verilog_logical_equality)
 IREP_ID_ONE(verilog_logical_inequality)
 IREP_ID_ONE(verilog_wildcard_equality)
 IREP_ID_ONE(verilog_wildcard_inequality)
-IREP_ID_ONE(verilog_explicit_cast)
-IREP_ID_ONE(verilog_size_cast)
+IREP_ID_ONE(verilog_explicit_const_cast)
+IREP_ID_ONE(verilog_explicit_signing_cast)
+IREP_ID_ONE(verilog_explicit_size_cast)
+IREP_ID_ONE(verilog_explicit_type_cast)
 IREP_ID_ONE(verilog_implicit_typecast)
 IREP_ID_ONE(verilog_inside)
 IREP_ID_ONE(verilog_unique)

src/verilog/expr2verilog.cpp

@@ -694,7 +694,7 @@ expr2verilogt::convert_typecast(const typecast_exprt &src)
 
 /*******************************************************************\
 
-Function: expr2verilogt::convert_explicit_cast
+Function: expr2verilogt::convert_explicit_const_cast
 
   Inputs:
 
@@ -704,8 +704,47 @@ Function: expr2verilogt::convert_explicit_cast
 
 \*******************************************************************/
 
-expr2verilogt::resultt
-expr2verilogt::convert_explicit_cast(const verilog_explicit_cast_exprt &src)
+expr2verilogt::resultt expr2verilogt::convert_explicit_const_cast(
+  const verilog_explicit_const_cast_exprt &src)
+{
+  return {verilog_precedencet::MAX, "const'(" + convert_rec(src.op()).s + ')'};
+}
+
+/*******************************************************************\
+
+Function: expr2verilogt::convert_explicit_signing_cast
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_explicit_signing_cast(
+  const verilog_explicit_signing_cast_exprt &src)
+{
+  std::string signing = src.is_signed() ? "signed" : "unsigned";
+
+  return {
+    verilog_precedencet::MAX, signing + "'(" + convert_rec(src.op()).s + ')'};
+}
+
+/*******************************************************************\
+
+Function: expr2verilogt::convert_explicit_type_cast
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_explicit_type_cast(
+  const verilog_explicit_type_cast_exprt &src)
 {
   return {
     verilog_precedencet::MAX,
@@ -714,7 +753,7 @@ expr2verilogt::convert_explicit_cast(const verilog_explicit_cast_exprt &src)
 
 /*******************************************************************\
 
-Function: expr2verilogt::convert_size_cast
+Function: expr2verilogt::convert_explicit_size_cast
 
   Inputs:
 
@@ -724,8 +763,8 @@ Function: expr2verilogt::convert_size_cast
 
 \*******************************************************************/
 
-expr2verilogt::resultt
-expr2verilogt::convert_size_cast(const verilog_size_cast_exprt &src)
+expr2verilogt::resultt expr2verilogt::convert_explicit_size_cast(
+  const verilog_explicit_size_cast_exprt &src)
 {
   return {
     verilog_precedencet::MAX,
@@ -1490,11 +1529,19 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return convert_unary(
       to_bitnot_expr(src), "~", precedence = verilog_precedencet::NOT);
 
-  else if(src.id() == ID_verilog_explicit_cast)
-    return convert_explicit_cast(to_verilog_explicit_cast_expr(src));
+  else if(src.id() == ID_verilog_explicit_const_cast)
+    return convert_explicit_const_cast(
+      to_verilog_explicit_const_cast_expr(src));
+
+  else if(src.id() == ID_verilog_explicit_size_cast)
+    return convert_explicit_size_cast(to_verilog_explicit_size_cast_expr(src));
+
+  else if(src.id() == ID_verilog_explicit_signing_cast)
+    return convert_explicit_signing_cast(
+      to_verilog_explicit_signing_cast_expr(src));
 
-  else if(src.id() == ID_verilog_size_cast)
-    return convert_size_cast(to_verilog_size_cast_expr(src));
+  else if(src.id() == ID_verilog_explicit_type_cast)
+    return convert_explicit_type_cast(to_verilog_explicit_type_cast_expr(src));
 
   else if(src.id()==ID_typecast)
     return convert_typecast(to_typecast_expr(src));

src/verilog/expr2verilog_class.h

@@ -105,11 +105,19 @@ class expr2verilogt
 
   resultt convert_constant(const constant_exprt &, verilog_precedencet &);
 
-  resultt convert_explicit_cast(const class verilog_explicit_cast_exprt &);
+  resultt
+  convert_explicit_const_cast(const class verilog_explicit_const_cast_exprt &);
+
+  resultt convert_explicit_signing_cast(
+    const class verilog_explicit_signing_cast_exprt &);
+
+  resultt
+  convert_explicit_type_cast(const class verilog_explicit_type_cast_exprt &);
 
   resultt convert_typecast(const typecast_exprt &);
 
-  resultt convert_size_cast(const class verilog_size_cast_exprt &);
+  resultt
+  convert_explicit_size_cast(const class verilog_explicit_size_cast_exprt &);
 
   resultt
   convert_concatenation(const concatenation_exprt &, verilog_precedencet);

src/verilog/parser.y

@@ -1419,11 +1419,27 @@ lifetime:
 
 casting_type:
 	  simple_type
+		{
+		  init($$, ID_verilog_explicit_type_cast);
+		  stack_expr($$).type() = stack_type($1);
+		}
 	| constant_primary
-		{ init($$, ID_verilog_size_cast); mto($$, $1); }
+		{ init($$, ID_verilog_explicit_size_cast); mto($$, $1); }
 	| signing
+		{
+		  init($$, ID_verilog_explicit_signing_cast);
+		  stack_expr($$).type() = stack_type($1);
+		}
 	| TOK_STRING
+		{
+		  init($$, ID_verilog_explicit_type_cast);
+		  stack_expr($$).type() = stack_type($1);
+		}
 	| TOK_CONST
+		{
+		  init($$, ID_verilog_explicit_const_cast);
+		  stack_expr($$).type() = stack_type($1);
+		}
 	;
 
 data_type:
@@ -4044,18 +4060,7 @@ time_literal: TOK_TIME_LITERAL
 
 cast:
 	  casting_type '\'' '(' expression ')'
-		{ if(stack_expr($1).id() == ID_verilog_size_cast)
-		  {
-		    $$ = $1; 
-		    mto($$, $4);
-		  }
-		  else
-		  {
-		    init($$, ID_verilog_explicit_cast);
-		    stack_expr($$).type() = stack_type($1);
-		    mto($$, $4);
-		  }
-		}
+		{ $$ = $1; mto($$, $4); }
 	;
 
 // System Verilog standard 1800-2017

src/verilog/verilog_expr.h

@@ -2462,13 +2462,13 @@ inline verilog_udpt &to_verilog_udp(irept &irep)
 }
 
 /// size'(expression)
-class verilog_size_cast_exprt : public binary_exprt
+class verilog_explicit_size_cast_exprt : public binary_exprt
 {
 public:
-  verilog_size_cast_exprt(exprt __size, exprt __op, typet __type)
+  verilog_explicit_size_cast_exprt(exprt __size, exprt __op, typet __type)
     : binary_exprt(
         std::move(__size),
-        ID_verilog_size_cast,
+        ID_verilog_explicit_size_cast,
         std::move(__op),
         std::move(__type))
   {
@@ -2501,24 +2501,97 @@ class verilog_size_cast_exprt : public binary_exprt
   }
 };
 
-inline const verilog_size_cast_exprt &
-to_verilog_size_cast_expr(const exprt &expr)
+inline const verilog_explicit_size_cast_exprt &
+to_verilog_explicit_size_cast_expr(const exprt &expr)
 {
-  verilog_size_cast_exprt::check(expr);
-  return static_cast<const verilog_size_cast_exprt &>(expr);
+  verilog_explicit_size_cast_exprt::check(expr);
+  return static_cast<const verilog_explicit_size_cast_exprt &>(expr);
 }
 
-inline verilog_size_cast_exprt &to_verilog_size_cast_expr(exprt &expr)
+inline verilog_explicit_size_cast_exprt &
+to_verilog_explicit_size_cast_expr(exprt &expr)
 {
-  verilog_size_cast_exprt::check(expr);
-  return static_cast<verilog_size_cast_exprt &>(expr);
+  verilog_explicit_size_cast_exprt::check(expr);
+  return static_cast<verilog_explicit_size_cast_exprt &>(expr);
 }
 
-class verilog_explicit_cast_exprt : public unary_exprt
+class verilog_explicit_const_cast_exprt : public unary_exprt
 {
 public:
-  verilog_explicit_cast_exprt(exprt __op, typet __type)
-    : unary_exprt(ID_verilog_explicit_cast, std::move(__op), std::move(__type))
+  verilog_explicit_const_cast_exprt(exprt __op, typet __type)
+    : unary_exprt(
+        ID_verilog_explicit_const_cast,
+        std::move(__op),
+        std::move(__type))
+  {
+  }
+
+  exprt lower() const
+  {
+    return typecast_exprt{op(), type()};
+  }
+};
+
+inline const verilog_explicit_const_cast_exprt &
+to_verilog_explicit_const_cast_expr(const exprt &expr)
+{
+  verilog_explicit_const_cast_exprt::check(expr);
+  return static_cast<const verilog_explicit_const_cast_exprt &>(expr);
+}
+
+inline verilog_explicit_const_cast_exprt &
+to_verilog_explicit_const_cast_expr(exprt &expr)
+{
+  verilog_explicit_const_cast_exprt::check(expr);
+  return static_cast<verilog_explicit_const_cast_exprt &>(expr);
+}
+
+class verilog_explicit_signing_cast_exprt : public unary_exprt
+{
+public:
+  verilog_explicit_signing_cast_exprt(exprt __op, typet __type)
+    : unary_exprt(
+        ID_verilog_explicit_signing_cast,
+        std::move(__op),
+        std::move(__type))
+  {
+  }
+
+  bool is_signed() const
+  {
+    auto &dest_type = type();
+    return dest_type.id() == ID_signedbv ||
+           dest_type.id() == ID_verilog_signedbv;
+  }
+
+  exprt lower() const
+  {
+    return typecast_exprt{op(), type()};
+  }
+};
+
+inline const verilog_explicit_signing_cast_exprt &
+to_verilog_explicit_signing_cast_expr(const exprt &expr)
+{
+  verilog_explicit_signing_cast_exprt::check(expr);
+  return static_cast<const verilog_explicit_signing_cast_exprt &>(expr);
+}
+
+inline verilog_explicit_signing_cast_exprt &
+to_verilog_explicit_signing_cast_expr(exprt &expr)
+{
+  verilog_explicit_signing_cast_exprt::check(expr);
+  return static_cast<verilog_explicit_signing_cast_exprt &>(expr);
+}
+
+class verilog_explicit_type_cast_exprt : public unary_exprt
+{
+public:
+  verilog_explicit_type_cast_exprt(exprt __op, typet __type)
+    : unary_exprt(
+        ID_verilog_explicit_type_cast,
+        std::move(__op),
+        std::move(__type))
   {
   }
 
@@ -2528,17 +2601,18 @@ class verilog_explicit_cast_exprt : public unary_exprt
   }
 };
 
-inline const verilog_explicit_cast_exprt &
-to_verilog_explicit_cast_expr(const exprt &expr)
+inline const verilog_explicit_type_cast_exprt &
+to_verilog_explicit_type_cast_expr(const exprt &expr)
 {
-  verilog_explicit_cast_exprt::check(expr);
-  return static_cast<const verilog_explicit_cast_exprt &>(expr);
+  verilog_explicit_type_cast_exprt::check(expr);
+  return static_cast<const verilog_explicit_type_cast_exprt &>(expr);
 }
 
-inline verilog_explicit_cast_exprt &to_verilog_explicit_cast_expr(exprt &expr)
+inline verilog_explicit_type_cast_exprt &
+to_verilog_explicit_type_cast_expr(exprt &expr)
 {
-  verilog_explicit_cast_exprt::check(expr);
-  return static_cast<verilog_explicit_cast_exprt &>(expr);
+  verilog_explicit_type_cast_exprt::check(expr);
+  return static_cast<verilog_explicit_type_cast_exprt &>(expr);
 }
 
 class verilog_implicit_typecast_exprt : public unary_exprt

src/verilog/verilog_lowering.cpp

@@ -274,13 +274,17 @@ exprt verilog_lowering(exprt expr)
 
     return expr;
   }
-  else if(expr.id() == ID_verilog_explicit_cast)
+  else if(expr.id() == ID_verilog_explicit_type_cast)
   {
-    return to_verilog_explicit_cast_expr(expr).lower();
+    return to_verilog_explicit_type_cast_expr(expr).lower();
   }
-  else if(expr.id() == ID_verilog_size_cast)
+  else if(expr.id() == ID_verilog_explicit_signing_cast)
   {
-    return to_verilog_size_cast_expr(expr).lower();
+    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();
   }
   else if(
     expr.id() == ID_verilog_streaming_concatenation_left_to_right ||