From 1abd53256c740a63fa7e5c1704e828bd563d4e9f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 4 Feb 2025 11:54:45 +0000 Subject: [PATCH] SystemVerilog: separate scanner and parser state This introduces a new data structure for the state of the Verilog scanner, as opposed to using the data structure for the parser state. --- src/verilog/scanner.l | 30 ++++++++++++++++-------------- src/verilog/verilog_parser.h | 9 +++++---- src/verilog/verilog_scanner.h | 29 +++++++++++++++++++++++++++++ 3 files changed, 50 insertions(+), 18 deletions(-) create mode 100644 src/verilog/verilog_scanner.h diff --git a/src/verilog/scanner.l b/src/verilog/scanner.l index 1d924fcf..99b59260 100644 --- a/src/verilog/scanner.l +++ b/src/verilog/scanner.l @@ -18,10 +18,12 @@ static int isatty(int) { return 0; } #include #define PARSER (*verilog_parser_ptr) +#define SCANNER (PARSER.scanner) #define YYSTYPE unsigned #include "verilog_parser.h" #include "verilog_y.tab.h" +#include "verilog_scanner.h" int yyverilogerror(const char *error); @@ -68,34 +70,34 @@ static void preprocessor() return PARSER.scopes.identifier_token(irep_id); \ } #define KEYWORD(s, x) \ - { if(PARSER.parse_tree.standard >= verilog_standardt::s) \ + { if(SCANNER.standard >= verilog_standardt::s) \ return x; \ else \ IDENTIFIER(yytext); \ } #define SYSTEM_VERILOG_OPERATOR(token, text) \ - { if(PARSER.parse_tree.standard >= verilog_standardt::SV2005) \ + { if(SCANNER.standard >= verilog_standardt::SV2005) \ return token; \ else \ yyverilogerror(text " is a System Verilog operator"); \ } #define VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(x) \ - { if(PARSER.parse_tree.standard >= verilog_standardt::SV2005 || \ - PARSER.parse_tree.standard == verilog_standardt::V2005_SMV) \ + { if(SCANNER.standard >= verilog_standardt::SV2005 || \ + SCANNER.standard == verilog_standardt::V2005_SMV) \ return x; \ else \ IDENTIFIER(yytext); \ } #define VL2SMV_VERILOG_KEYWORD(x) \ - { if(PARSER.parse_tree.standard == verilog_standardt::V2005_SMV) \ + { if(SCANNER.standard == verilog_standardt::V2005_SMV) \ return x; \ else \ IDENTIFIER(yytext); \ } #define VIS_OR_VL2SMV_OR_SYSTEM_VERILOG_KEYWORD(x) \ - { if(PARSER.parse_tree.standard >= verilog_standardt::SV2005 || \ - PARSER.parse_tree.standard == verilog_standardt::V2005_SMV || \ - PARSER.parse_tree.standard == verilog_standardt::V2005_VIS) \ + { if(SCANNER.standard >= verilog_standardt::SV2005 || \ + SCANNER.standard == verilog_standardt::V2005_SMV || \ + SCANNER.standard == verilog_standardt::V2005_VIS) \ return x; \ else \ IDENTIFIER(yytext); \ @@ -161,7 +163,7 @@ void verilog_scanner_init() { "\"" { BEGIN(GRAMMAR); - stack_expr(yyveriloglval).id(PARSER.string_literal); + stack_expr(yyveriloglval).id(SCANNER.string_literal); return TOK_QSTRING; } @@ -169,10 +171,10 @@ void verilog_scanner_init() return TOK_SCANNER_ERROR; } - "\\n" { PARSER.string_literal += '\n'; } // NL (0x0a) */ - "\\t" { PARSER.string_literal += '\t'; } // HT (0x09) */ - "\\". { PARSER.string_literal += yytext[1]; } // ignore the backslash - [^\\\"\n]* { PARSER.string_literal += &yytext[0]; } // everything else + "\\n" { SCANNER.string_literal += '\n'; } // NL (0x0a) */ + "\\t" { SCANNER.string_literal += '\t'; } // HT (0x09) */ + "\\". { SCANNER.string_literal += yytext[1]; } // ignore the backslash + [^\\\"\n]* { SCANNER.string_literal += &yytext[0]; } // everything else \n { yyverilogerror("Unterminated string constant"); return TOK_SCANNER_ERROR; @@ -186,7 +188,7 @@ void verilog_scanner_init() "/*" { BEGIN COMMENT; continue; } "\"" { BEGIN(STRING); newstack(yyveriloglval); - PARSER.string_literal.clear(); + SCANNER.string_literal.clear(); } /* Attributes */ diff --git a/src/verilog/verilog_parser.h b/src/verilog/verilog_parser.h index f5fecc4d..c36bce7c 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_scanner.h" #include "verilog_scope.h" #include "verilog_standard.h" @@ -28,9 +29,9 @@ class verilog_parsert:public parsert public: verilog_parse_treet parse_tree; - // for lexing strings - std::string string_literal; - + // scanner state + verilog_scannert scanner; + typedef enum { LANGUAGE, EXPRESSION, TYPE } grammart; grammart grammar; @@ -42,7 +43,7 @@ class verilog_parsert:public parsert explicit verilog_parsert( verilog_standardt standard, message_handlert &message_handler) - : parsert(message_handler), parse_tree(standard) + : parsert(message_handler), parse_tree(standard), scanner(standard) { PRECONDITION(verilog_parser_ptr == nullptr); verilog_parser_ptr = this; diff --git a/src/verilog/verilog_scanner.h b/src/verilog/verilog_scanner.h new file mode 100644 index 00000000..41f4ec3b --- /dev/null +++ b/src/verilog/verilog_scanner.h @@ -0,0 +1,29 @@ +/*******************************************************************\ + +Module: Verilog Scanner + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_VERILOG_SCANNER_H +#define CPROVER_VERILOG_SCANNER_H + +#include "verilog_standard.h" + +/// the state of the Verilog scanner +class verilog_scannert +{ +public: + explicit verilog_scannert(verilog_standardt __standard) : standard(__standard) + { + } + + // to determine the set of keyworkds + verilog_standardt standard; + + // for lexing strings + std::string string_literal; +}; + +#endif