From 9b9a14908f2252fdf08a2def6885f89ea18adad7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening 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/parser.y | 12 ++--- src/verilog/scanner.l | 2 +- src/verilog/verilog_parser.cpp | 29 ----------- src/verilog/verilog_parser.h | 69 ++------------------------ src/verilog/verilog_scope.cpp | 26 ++++++++++ src/verilog/verilog_scope.h | 91 ++++++++++++++++++++++++++++++++++ 7 files changed, 128 insertions(+), 102 deletions(-) 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/parser.y b/src/verilog/parser.y index a041d68ff..08ff54b1c 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -28,8 +28,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #define mts(x, y) stack_expr(x).move_to_sub((irept &)stack_expr(y)) #define swapop(x, y) stack_expr(x).operands().swap(stack_expr(y).operands()) #define addswap(x, y, z) stack_expr(x).add(y).swap(stack_expr(z)) -#define push_scope(x, y) PARSER.push_scope(x, y) -#define pop_scope() PARSER.pop_scope(); +#define push_scope(x, y) PARSER.scopes.push_scope(x, y) +#define pop_scope() PARSER.scopes.pop_scope(); int yyveriloglex(); extern char *yyverilogtext; @@ -1442,7 +1442,7 @@ net_declaration: type_declaration: TOK_TYPEDEF data_type new_identifier ';' { // add to the scope as a type name - auto &name = PARSER.add_name(stack_expr($3).get(ID_identifier), ""); + auto &name = PARSER.scopes.add_name(stack_expr($3).get(ID_identifier), ""); name.is_type = true; init($$, ID_decl); @@ -1535,7 +1535,7 @@ data_type: // We attach a dummy id to distinguish two syntactically // identical enum types. - auto id = PARSER.current_scope->prefix + "enum-" + PARSER.get_next_id(); + auto id = PARSER.scopes.current_scope->prefix + "enum-" + PARSER.get_next_id(); stack_expr($$).set(ID_identifier, id); } | TOK_STRING @@ -1569,7 +1569,7 @@ enum_name_declaration: TOK_NON_TYPE_IDENTIFIER enum_name_value_opt { init($$); - auto &scope = PARSER.add_name(stack_expr($1).id(), ""); + auto &scope = PARSER.scopes.add_name(stack_expr($1).id(), ""); stack_expr($$).set(ID_base_name, scope.base_name()); stack_expr($$).set(ID_identifier, scope.identifier()); stack_expr($$).add(ID_value).swap(stack_expr($2)); @@ -4416,7 +4416,7 @@ type_identifier: TOK_TYPE_IDENTIFIER init($$, ID_typedef_type); auto base_name = stack_expr($1).id(); stack_expr($$).set(ID_base_name, base_name); - stack_expr($$).set(ID_identifier, PARSER.current_scope->prefix+id2string(base_name)); + stack_expr($$).set(ID_identifier, PARSER.scopes.current_scope->prefix+id2string(base_name)); } ; diff --git a/src/verilog/scanner.l b/src/verilog/scanner.l index 0d01f7046..4885bfe5a 100644 --- a/src/verilog/scanner.l +++ b/src/verilog/scanner.l @@ -65,7 +65,7 @@ static void preprocessor() { newstack(yyveriloglval); \ irep_idt irep_id = text; \ stack_expr(yyveriloglval).id(irep_id); \ - auto name = PARSER.lookup(irep_id); \ + auto name = PARSER.scopes.lookup(irep_id); \ return name == nullptr ? TOK_NON_TYPE_IDENTIFIER : \ name->is_type ? TOK_TYPE_IDENTIFIER : \ TOK_NON_TYPE_IDENTIFIER; \ diff --git a/src/verilog/verilog_parser.cpp b/src/verilog/verilog_parser.cpp index 900ba8e45..8912864a7 100644 --- a/src/verilog/verilog_parser.cpp +++ b/src/verilog/verilog_parser.cpp @@ -53,32 +53,3 @@ bool parse_verilog_file(const std::string &filename, verilog_standardt standard) return verilog_parser.parse(); } - -/*******************************************************************\ - -Function: verilog_parsert::lookup - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -const verilog_parsert::scopet *verilog_parsert::lookup(irep_idt name) const -{ - // we start from the current scope, and walk upwards to the root - auto scope = current_scope; - while(scope != nullptr) - { - auto name_it = scope->scope_map.find(name); - if(name_it == scope->scope_map.end()) - scope = scope->parent; - else - return &name_it->second; // found it - } - - // not found, give up - return nullptr; -} diff --git a/src/verilog/verilog_parser.h b/src/verilog/verilog_parser.h index f8e3fe0ed..f5fecc4da 100644 --- a/src/verilog/verilog_parser.h +++ b/src/verilog/verilog_parser.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "verilog_parse_tree.h" +#include "verilog_scope.h" #include "verilog_standard.h" #include @@ -53,73 +54,9 @@ class verilog_parsert:public parsert } // 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; - scope_mapt scope_map; - }; - - scopet top_scope, *current_scope = &top_scope; - - scopet &add_name(irep_idt _base_name, const std::string &separator) - { - auto result = current_scope->scope_map.emplace( - _base_name, scopet{_base_name, separator, current_scope}); - return result.first->second; - } - - // Create the given sub-scope of the current scope. - void push_scope(irep_idt _base_name, const std::string &separator) - { - current_scope = &add_name(_base_name, separator); - } + using scopet = verilog_scopet; - void pop_scope() - { - PRECONDITION(current_scope->parent != nullptr); - current_scope = current_scope->parent; - } - - // Look up an identifier, starting from the current scope, - // going upwards until found. Returns nullptr when not found. - const scopet *lookup(irep_idt base_name) const; - - bool is_type(irep_idt base_name) const - { - auto scope_ptr = lookup(base_name); - return scope_ptr == nullptr ? false : scope_ptr->is_type; - } + verilog_scopest scopes; // These are used for anonymous gate instances // and to create a unique identifier for enum types. diff --git a/src/verilog/verilog_scope.cpp b/src/verilog/verilog_scope.cpp new file mode 100644 index 000000000..66d96e302 --- /dev/null +++ b/src/verilog/verilog_scope.cpp @@ -0,0 +1,26 @@ +/*******************************************************************\ + +Module: Verilog Scope + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "verilog_scope.h" + +const verilog_scopet *verilog_scopest::lookup(irep_idt name) const +{ + // we start from the current scope, and walk upwards to the root + auto scope = current_scope; + while(scope != nullptr) + { + auto name_it = scope->scope_map.find(name); + if(name_it == scope->scope_map.end()) + scope = scope->parent; + else + return &name_it->second; // found it + } + + // not found, give up + return nullptr; +} diff --git a/src/verilog/verilog_scope.h b/src/verilog/verilog_scope.h new file mode 100644 index 000000000..76b85afa3 --- /dev/null +++ b/src/verilog/verilog_scope.h @@ -0,0 +1,91 @@ +/*******************************************************************\ + +Module: Verilog Scopes + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_VERILOG_SCOPE_H +#define CPROVER_VERILOG_SCOPE_H + +#include + +#include + +// parser scopes and identifiers +struct verilog_scopet +{ + verilog_scopet() : parent(nullptr), prefix("Verilog::") + { + } + + verilog_scopet( + irep_idt _base_name, + const std::string &separator, + verilog_scopet *_parent) + : parent(_parent), + __base_name(_base_name), + prefix(id2string(_parent->prefix) + id2string(_base_name) + separator) + { + } + + verilog_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; + scope_mapt scope_map; +}; + +class verilog_scopest +{ +public: + using scopet = verilog_scopet; + + scopet top_scope, *current_scope = &top_scope; + + scopet &add_name(irep_idt _base_name, const std::string &separator) + { + auto result = current_scope->scope_map.emplace( + _base_name, scopet{_base_name, separator, current_scope}); + return result.first->second; + } + + // Create the given sub-scope of the current scope. + void push_scope(irep_idt _base_name, const std::string &separator) + { + current_scope = &add_name(_base_name, separator); + } + + void pop_scope() + { + PRECONDITION(current_scope->parent != nullptr); + current_scope = current_scope->parent; + } + + // Look up an identifier, starting from the current scope, + // going upwards until found. Returns nullptr when not found. + const scopet *lookup(irep_idt base_name) const; + + bool is_type(irep_idt base_name) const + { + auto scope_ptr = lookup(base_name); + return scope_ptr == nullptr ? false : scope_ptr->is_type; + } +}; + +#endif