Merge pull request #838 from diffblue/verilog_string

SystemVerilog: `string` data type

Author: tautschnig

CHANGELOG

@@ -8,7 +8,7 @@
 * Verilog: fix for nor/nand/xnor primitive gates
 * SystemVerilog: $bitstoreal/$bitstoshortreal, $realtobits/$shortrealtobits
 * SystemVerilog: $itor, $rtoi
-* SystemVerilog: chandle, event
+* SystemVerilog: chandle, event, string
 * SystemVerilog: package scope operator
 
 # EBMC 5.4

regression/verilog/data-types/string1.desc

@@ -0,0 +1,7 @@
+CORE
+string1.sv
+--bound 0
+^no properties$
+^EXIT=10$
+^SIGNAL=0$
+--

regression/verilog/data-types/string1.sv

@@ -0,0 +1,7 @@
+module main;
+
+  // IEEE 1800-2017 6.16
+  string xyz;
+  string my_string = xyz;
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -108,6 +108,7 @@ IREP_ID_ONE(verilog_chandle)
 IREP_ID_ONE(verilog_null)
 IREP_ID_ONE(verilog_event)
 IREP_ID_ONE(verilog_event_trigger)
+IREP_ID_ONE(verilog_string)
 IREP_ID_ONE(reg)
 IREP_ID_ONE(macromodule)
 IREP_ID_ONE(output_register)

src/verilog/expr2verilog.cpp

@@ -1988,6 +1988,8 @@ std::string expr2verilogt::convert(const typet &type)
     return "logic";
   else if(type.id() == ID_verilog_integer)
     return "integer";
+  else if(type.id() == ID_verilog_string)
+    return "string";
   else if(type.id() == ID_verilog_reg)
     return "reg";
   else if(type.id() == ID_verilog_time)

src/verilog/parser.y

@@ -1479,7 +1479,7 @@ data_type:
 	          stack_expr($$).set(ID_identifier, id);
 	        }
 	| TOK_STRING
-	        { init($$, ID_string); }
+	        { init($$, ID_verilog_string); }
 	| TOK_CHANDLE
 	        { init($$, ID_verilog_chandle); }
 	| TOK_VIRTUAL interface_opt interface_identifier

src/verilog/verilog_elaborate_type.cpp

@@ -379,6 +379,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
     return struct_union_typet{src.id(), std::move(components)}
       .with_source_location(src.source_location());
   }
+  else if(src.id() == ID_verilog_string)
+  {
+    return src;
+  }
   else if(src.id() == ID_type)
   {
     return src;

src/verilog/verilog_typecheck_expr.cpp

@@ -761,6 +761,10 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
   {
     s = "event";
   }
+  else if(type.id() == ID_verilog_string)
+  {
+    s = "string";
+  }
   else
     s = "?";
 
@@ -2331,6 +2335,21 @@ typet verilog_typecheck_exprt::max_type(
   if(vt0.is_event() || vt1.is_null())
     return t0;
 
+  if(
+    vt0.is_string() && (vt1.is_signed() || vt1.is_unsigned() ||
+                        vt1.is_verilog_signed() || vt1.is_verilog_unsigned()))
+  {
+    return t0;
+  }
+
+  if(
+    (vt0.is_signed() || vt0.is_unsigned() || vt0.is_verilog_signed() ||
+     vt0.is_verilog_unsigned()) &&
+    vt0.is_string())
+  {
+    return t1;
+  }
+
   if(vt0.is_other() || vt1.is_other())
     return static_cast<const typet &>(get_nil_irep());
 

src/verilog/vtype.cpp

@@ -83,6 +83,11 @@ vtypet::vtypet(const typet &type)
     vtype = EVENT;
     width = 32;
   }
+  else if(type.id() == ID_verilog_string)
+  {
+    vtype = STRING;
+    width = 0;
+  }
   else 
   {
     width=0;
@@ -136,6 +141,9 @@ std::ostream &operator << (std::ostream &out, const vtypet &vtype)
   case vtypet::EVENT:
     return out << "event";
 
+  case vtypet::STRING:
+    return out << "string";
+
   case vtypet::UNKNOWN:
   case vtypet::OTHER:
   default:

src/verilog/vtype.h

@@ -43,6 +43,10 @@ class vtypet
   {
     return vtype == EVENT;
   }
+  bool is_string() const
+  {
+    return vtype == STRING;
+  }
   inline bool is_other() const { return vtype==OTHER; }
 
 protected:
@@ -59,6 +63,7 @@ class vtypet
     NULL_TYPE,
     CHANDLE,
     EVENT,
+    STRING,
     OTHER
   } _vtypet;
   _vtypet vtype;