From 2e75751ed28713cab6ee9300ef1fd0baf59cfd24 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 28 Jan 2025 09:25:18 +0000
Subject: [PATCH] Verilog: extract scope data structure from parser

This extracts the scope data structure from the parser class into a separate
file, as the scopes need to be preserved until all Verilog parsing is
finished.
---
 src/verilog/Makefile          |  1 +
 src/verilog/verilog_parser.h  |  1 +
 src/verilog/verilog_scope.cpp |  9 ++++++
 src/verilog/verilog_scope.h   | 54 +++++++++++++++++++++++++++++++++++
 4 files changed, 65 insertions(+)
 create mode 100644 src/verilog/verilog_scope.cpp
 create mode 100644 src/verilog/verilog_scope.h

diff --git a/src/verilog/Makefile b/src/verilog/Makefile
index 895bc6466..d4b6c3272 100644
--- a/src/verilog/Makefile
+++ b/src/verilog/Makefile
@@ -18,6 +18,7 @@ SRC = aval_bval_encoding.cpp \
       verilog_preprocessor.cpp \
       verilog_preprocessor_lex.yy.cpp \
       verilog_preprocessor_tokenizer.cpp \
+      verilog_scope.cpp \
       verilog_simplifier.cpp \
       verilog_standard.cpp \
       verilog_symbol_table.cpp \
diff --git a/src/verilog/verilog_parser.h b/src/verilog/verilog_parser.h
index f8e3fe0ed..8cf7edb93 100644
--- a/src/verilog/verilog_parser.h
+++ b/src/verilog/verilog_parser.h
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/parser.h>
 
 #include "verilog_parse_tree.h"
+#include "verilog_scope.h"
 #include "verilog_standard.h"
 
 #include <map>
diff --git a/src/verilog/verilog_scope.cpp b/src/verilog/verilog_scope.cpp
new file mode 100644
index 000000000..07bee68dc
--- /dev/null
+++ b/src/verilog/verilog_scope.cpp
@@ -0,0 +1,9 @@
+/*******************************************************************\
+
+Module: Verilog Scope
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "verilog_scope.h"
diff --git a/src/verilog/verilog_scope.h b/src/verilog/verilog_scope.h
new file mode 100644
index 000000000..eb9471bc2
--- /dev/null
+++ b/src/verilog/verilog_scope.h
@@ -0,0 +1,54 @@
+/*******************************************************************\
+
+Module: Verilog Scopes
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_VERILOG_SCOPE_H
+#define CPROVER_VERILOG_SCOPE_H
+
+#include <util/irep.h>
+
+#include <map>
+
+// parser scopes and identifiers
+struct scopet
+{
+  scopet() : parent(nullptr), prefix("Verilog::")
+  {
+  }
+
+  explicit scopet(
+    irep_idt _base_name,
+    const std::string &separator,
+    scopet *_parent)
+    : parent(_parent),
+      __base_name(_base_name),
+      prefix(id2string(_parent->prefix) + id2string(_base_name) + separator)
+  {
+  }
+
+  scopet *parent = nullptr;
+  bool is_type = false;
+  irep_idt __base_name;
+  std::string prefix;
+
+  irep_idt identifier() const
+  {
+    PRECONDITION(parent != nullptr);
+    return parent->prefix + id2string(__base_name);
+  }
+
+  const irep_idt &base_name() const
+  {
+    return __base_name;
+  }
+
+  // sub-scopes
+  using scope_mapt = std::map<irep_idt, scopet>;
+  scope_mapt scope_map;
+};
+
+#endif