From 844da97cb88bcd5f67f3aaadf03f1465807caa9d Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 5 Feb 2025 14:50:15 +0000
Subject: [PATCH] SystemVerilog: Parsing and type checking for queue types

This adds parsing and type checking for 1800-2017 7.10 queues.
---
 lib/cbmc                                  | 2 +-
 regression/verilog/data-types/queue1.desc | 6 +++---
 regression/verilog/data-types/queue1.sv   | 2 +-
 src/hw_cbmc_irep_ids.h                    | 1 +
 src/verilog/expr2verilog.cpp              | 6 ++++++
 src/verilog/parser.y                      | 8 ++++++++
 src/verilog/verilog_elaborate_type.cpp    | 4 ++++
 src/verilog/verilog_expr.cpp              | 3 ++-
 8 files changed, 26 insertions(+), 6 deletions(-)

diff --git a/lib/cbmc b/lib/cbmc
index fc4f7ca7..f2489e3e 160000
--- a/lib/cbmc
+++ b/lib/cbmc
@@ -1 +1 @@
-Subproject commit fc4f7ca71ddcbd290cea0d9ac58b6cc6f6b79cb0
+Subproject commit f2489e3edf77f95c5d43c4baf733607a073f8ccd
diff --git a/regression/verilog/data-types/queue1.desc b/regression/verilog/data-types/queue1.desc
index 92e35926..360fe4c7 100644
--- a/regression/verilog/data-types/queue1.desc
+++ b/regression/verilog/data-types/queue1.desc
@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 queue1.sv
 
-^EXIT=0$
+^no properties$
+^EXIT=10$
 ^SIGNAL=0$
 --
 --
-Parsing fails.
diff --git a/regression/verilog/data-types/queue1.sv b/regression/verilog/data-types/queue1.sv
index 5fb1508a..8d3f66ee 100644
--- a/regression/verilog/data-types/queue1.sv
+++ b/regression/verilog/data-types/queue1.sv
@@ -1,6 +1,6 @@
 module main;
 
   byte queue_of_bytes[$];
-  string queue_of_strings[$:10] = { "foobar" };
+  string queue_of_strings[$:10];
 
 endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 7efff7d9..c405df8d 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -94,6 +94,7 @@ IREP_ID_ONE(verilog_inside)
 IREP_ID_ONE(verilog_unique)
 IREP_ID_ONE(verilog_unique0)
 IREP_ID_ONE(verilog_priority)
+IREP_ID_ONE(verilog_queue)
 IREP_ID_ONE(verilog_new)
 IREP_ID_ONE(verilog_non_indexed_part_select)
 IREP_ID_ONE(verilog_indexed_part_select_plus)
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index 7a052d39..4b1a53d1 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -2074,6 +2074,12 @@ std::string expr2verilogt::convert(const typet &type)
   {
     return "enum";
   }
+  else if(type.id() == ID_verilog_queue)
+  {
+    std::string dest="queue of ";
+    dest += convert(to_type_with_subtype(type).subtype());
+    return dest;
+  }
   else if(type.id() == ID_struct)
   {
     return "struct";
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index dd31f867..d8f6d5dc 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -2114,6 +2114,7 @@ variable_dimension:
 	  unsized_dimension
 	| unpacked_dimension
 	| associative_dimension
+	| queue_dimension
 	;
 
 variable_dimension_brace:
@@ -2126,6 +2127,13 @@ variable_dimension_brace:
 	  }
 	;
 
+queue_dimension:
+	  '[' '$' ']'
+		{ init($$, ID_verilog_queue); stack_type($$).add_subtype().make_nil(); }
+	| '[' '$' TOK_COLON constant_expression ']'
+		{ init($$, ID_verilog_queue); stack_type($$).add_subtype().make_nil(); }
+	;
+
 unsized_dimension: '[' ']'
                 { init($$, "unsized"); }
 	;
diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp
index f5ada047..545fa1f4 100644
--- a/src/verilog/verilog_elaborate_type.cpp
+++ b/src/verilog/verilog_elaborate_type.cpp
@@ -447,6 +447,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
     // package::typedef
     return elaborate_package_scope_typedef(to_type_with_subtypes(src));
   }
+  else if(src.id() == ID_verilog_queue)
+  {
+    return src;
+  }
   else
   {
     throw errort().with_location(source_location)
diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp
index 4358ca60..0c0c4c7c 100644
--- a/src/verilog/verilog_expr.cpp
+++ b/src/verilog/verilog_expr.cpp
@@ -34,7 +34,8 @@ typet verilog_declaratort::merged_type(const typet &declaration_type) const
   typet *p = &result;
 
   while(p->id() == ID_verilog_unpacked_array ||
-        p->id() == ID_verilog_associative_array)
+        p->id() == ID_verilog_associative_array ||
+        p->id() == ID_verilog_queue)
   {
     p = &to_type_with_subtype(*p).subtype();
   }