SystemVerilog: delay expansion of string literals

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

Author: kroening

src/verilog/expr2verilog.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 #include <cstdlib>
+#include <iomanip>
 #include <sstream>
 
 /*******************************************************************\
@@ -1208,6 +1209,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"
 
@@ -167,12 +168,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 ||
@@ -183,6 +186,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

@@ -1278,8 +1278,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 ||