SystemVerilog: size casts

This adds SystemVerilog size cast expressions.

Author: kroening

regression/verilog/casts/size_cast1.desc

@@ -0,0 +1,7 @@
+CORE
+size_cast1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/casts/size_cast1.sv

@@ -0,0 +1,9 @@
+module main;
+
+  parameter P = 20;
+
+  p0: assert property ($bits(10'(1)) == 10);
+  p1: assert property ($bits(P'(1)) == 20);
+  p2: assert property (10'(-1) == -1);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -36,6 +36,7 @@ IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)
 IREP_ID_ONE(verilog_explicit_cast)
+IREP_ID_ONE(verilog_size_cast)
 IREP_ID_ONE(verilog_implicit_typecast)
 IREP_ID_ONE(verilog_unique)
 IREP_ID_ONE(verilog_unique0)

src/verilog/parser.y

@@ -1208,6 +1208,8 @@ lifetime:
 
 casting_type:
 	  simple_type
+	| constant_primary
+		{ init($$, ID_verilog_size_cast); mto($$, $1); }
 	| signing
 	| TOK_STRING
 	| TOK_CONST
@@ -3216,6 +3218,9 @@ primary_literal:
         | time_literal
         ;
 
+constant_primary: primary
+	;
+
 // This is equivalent to two System Verilog 1800-2017 productions
 // hierarchical_identifier select.
 hierarchical_identifier_select:
@@ -3246,9 +3251,18 @@ time_literal: TOK_TIME_LITERAL
 
 cast:
 	  casting_type '\'' '(' expression ')'
-		{ init($$, ID_verilog_explicit_cast);
-		  stack_expr($$).type() = stack_type($1);
-		  mto($$, $4); }
+		{ 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);
+		  }
+		}
 	;
 
 // System Verilog standard 1800-2017

src/verilog/verilog_typecheck_expr.cpp

@@ -1879,11 +1879,12 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
   }
   else if(expr.id() == ID_verilog_explicit_cast)
   {
-    // System Verilog has got type'(expr). This is an explicit
+    // SystemVerilog has got type'(expr). This is an explicit
     // type cast.
-    expr.type() = convert_type(expr.type());
     convert_expr(expr.op());
-    expr.id(ID_typecast);
+    auto new_type = convert_type(expr.type());
+    return typecast_exprt{expr.op(), new_type}.with_source_location<exprt>(
+      expr);
   }
   else if(expr.id() == ID_verilog_implicit_typecast)
   {
@@ -2247,6 +2248,31 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     return convert_hierarchical_identifier(
       to_hierarchical_identifier_expr(std::move(expr)));
   }
+  else if(expr.id() == ID_verilog_size_cast)
+  {
+    // SystemVerilog has got expr'(expr). This is an explicit
+    // type cast, to change the size (in bits) of the rhs to the
+    // number given as lhs.
+    convert_expr(expr.rhs());
+    auto new_size = convert_integer_constant_expression(expr.lhs());
+    auto new_size_int = numeric_cast_v<std::size_t>(new_size);
+    auto &op_type = expr.rhs().type();
+    if(op_type.id() == ID_signedbv)
+    {
+      return typecast_exprt{expr.rhs(), signedbv_typet{new_size_int}}
+        .with_source_location<exprt>(expr);
+    }
+    else if(op_type.id() == ID_unsignedbv)
+    {
+      return typecast_exprt{expr.rhs(), unsignedbv_typet{new_size_int}}
+        .with_source_location<exprt>(expr);
+    }
+    else
+    {
+      throw errort().with_location(expr.source_location())
+        << "cannot perform size cast on " << to_string(op_type);
+    }
+  }
   else
   {
     // type is guessed for now