SystemVerilog: delay expansion of string literals

This delays the expansion of string literals to preserve these in property
descriptions.

Author: kroening

regression/verilog/system-functions/typename1.desc

@@ -1,13 +1,13 @@
 CORE
 typename1.sv
 --module main --bound 0
-^\[.*\] always \$typename\(main\.some_bit\) == 24'h626974: PROVED up to bound 0$
-^\[.*\] always \$typename\(main\.vector1\) == 72'h6269745B33313A305D: PROVED up to bound 0$
-^\[.*\] always \$typename\(main\.vector2\) == 72'h6269745B303A33315D: PROVED up to bound 0$
-^\[.*\] always \$typename\(main\.vector3\) == 128'h626974207369676E65645B33313A305D: PROVED up to bound 0$
-^\[.*\] always \$typename\(real'\(1\)\) == 32'h7265616C: PROVED up to bound 0$
-^\[.*\] always \$typename\(shortreal'\(1\)\) == 72'h73686F72747265616C: PROVED up to bound 0$
-^\[.*\] always \$typename\(realtime'\(1\)\) == 64'h7265616C74696D65: PROVED up to bound 0$
+^\[.*\] always \$typename\(main\.some_bit\) == "bit": PROVED up to bound 0$
+^\[.*\] always \$typename\(main\.vector1\) == "bit\[31:0\]": PROVED up to bound 0$
+^\[.*\] always \$typename\(main\.vector2\) == "bit\[0:31\]": PROVED up to bound 0$
+^\[.*\] always \$typename\(main\.vector3\) == "bit signed\[31:0\]": PROVED up to bound 0$
+^\[.*\] always \$typename\(real'\(1\)\) == "real": PROVED up to bound 0$
+^\[.*\] always \$typename\(shortreal'\(1\)\) == "shortreal": PROVED up to bound 0$
+^\[.*\] always \$typename\(realtime'\(1\)\) == "realtime": PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/verilog/expr2verilog.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 #include <cstdlib>
+#include <iomanip>
 #include <sstream>
 
 /*******************************************************************\
@@ -350,7 +351,10 @@ expr2verilogt::convert_function_call(const function_call_exprt &src)
     else
       dest+=", ";
 
-    dest += convert_rec(op).s;
+    if(op.id() == ID_type)
+      dest += convert(op.type());
+    else
+      dest += convert_rec(op).s;
   }
 
   dest+=")";
@@ -1208,6 +1212,54 @@ expr2verilogt::resultt expr2verilogt::convert_constant(
     ieee_float.from_expr(tmp);
     return {precedence, ieee_float.to_ansi_c_string()};
   }
+  else if(type.id() == ID_string)
+  {
+    dest = '"';
+
+    for(auto &ch : id2string(src.get_value()))
+    {
+      // Follows Table Table 5-1 in 1800-2017.
+      switch(ch)
+      {
+      case '\n':
+        dest += "\\n";
+        break;
+      case '\t':
+        dest += "\\t";
+        break;
+      case '\\':
+        dest += "\\\\";
+        break;
+      case '"':
+        dest += "\\\"";
+        break;
+      case '\v':
+        dest += "\\v";
+        break;
+      case '\f':
+        dest += "\\f";
+        break;
+      case '\a':
+        dest += "\\a";
+        break;
+      default:
+        if(
+          (unsigned(ch) >= ' ' && unsigned(ch) <= 126) ||
+          (unsigned(ch) >= 128 && unsigned(ch) <= 254))
+        {
+          dest += ch;
+        }
+        else
+        {
+          std::ostringstream oss;
+          oss << "\\x" << std::setw(2) << std::setfill('0') << std::hex << ch;
+          dest += oss.str();
+        }
+      }
+    }
+
+    dest += '"';
+  }
   else
     return convert_norep(src, precedence);
 

src/verilog/verilog_lowering.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/ieee_float.h>
 
 #include "aval_bval_encoding.h"
+#include "convert_literals.h"
 #include "verilog_bits.h"
 #include "verilog_expr.h"
 
@@ -182,12 +183,14 @@ exprt verilog_lowering(exprt expr)
 
   if(expr.id() == ID_constant)
   {
+    auto &constant_expr = to_constant_expr(expr);
+
     if(
       expr.type().id() == ID_verilog_unsignedbv ||
       expr.type().id() == ID_verilog_signedbv)
     {
       // encode into aval/bval
-      return lower_to_aval_bval(to_constant_expr(expr));
+      return lower_to_aval_bval(constant_expr);
     }
     else if(
       expr.type().id() == ID_verilog_real ||
@@ -198,6 +201,12 @@ exprt verilog_lowering(exprt expr)
       // no need to change value
       expr.type() = lower_verilog_real_types(expr.type());
     }
+    else if(expr.type().id() == ID_string)
+    {
+      auto result = convert_string_literal(constant_expr.get_value());
+      result.add_source_location() = expr.source_location();
+      expr = std::move(result);
+    }
 
     return expr;
   }

src/verilog/verilog_typecheck_expr.cpp

@@ -756,7 +756,10 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
   else
     s = "?";
 
-  return convert_constant(constant_exprt{s, string_typet{}});
+  auto result = convert_string_literal(s);
+  result.add_source_location() = expr.source_location();
+
+  return std::move(result);
 }
 
 /*******************************************************************\
@@ -1301,8 +1304,8 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
   if(expr.type().id()==ID_string)
   {
     auto result = convert_string_literal(expr.get_value());
-    result.add_source_location() = source_location;
-    return std::move(result);
+    // only add a typecast for now
+    return typecast_exprt{std::move(expr), std::move(result.type())};
   }
   else if(expr.type().id()==ID_unsignedbv ||
           expr.type().id()==ID_signedbv ||