From 12d94bb234c972a8840400406a14c16815778ffb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 20 Dec 2023 09:26:40 +0000 Subject: [PATCH 1/2] Permit constructing parsert with a message handler This is to provide a path to remove the long-deprecated messaget() constructor. Uses of this new constructor will be added in separate commits. --- src/util/parser.h | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/util/parser.h b/src/util/parser.h index 70a796ec4a9..c19aeb58977 100644 --- a/src/util/parser.h +++ b/src/util/parser.h @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_PARSER_H #define CPROVER_UTIL_PARSER_H +#include "deprecate.h" #include "expr.h" #include "message.h" @@ -39,7 +40,13 @@ class parsert last_line.clear(); } + DEPRECATED(SINCE(2023, 12, 20, "use parsert(message_handler) instead")) parsert():in(nullptr) { clear(); } + explicit parsert(message_handlert &message_handler) + : in(nullptr), log(message_handler) + { + clear(); + } virtual ~parsert() { } // The following are for the benefit of the scanner From c49b489f94b8f81cc4f79be51606f7fcc99f06b2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 20 Dec 2023 13:23:54 +0000 Subject: [PATCH 2/2] jsil_parsert: construct with message handler This both avoids an object of static lifetime as well as it fixes the (transitive) use of the deprecated messaget() constructor. --- src/jsil/jsil_language.cpp | 7 ++----- src/jsil/jsil_parser.cpp | 10 ---------- src/jsil/jsil_parser.h | 17 ++++++++++------- src/jsil/parser.y | 16 +++++++++++++++- src/jsil/scanner.l | 20 +++++++++++--------- 5 files changed, 38 insertions(+), 32 deletions(-) diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp index c363a5396e0..8b0d543c949 100644 --- a/src/jsil/jsil_language.cpp +++ b/src/jsil/jsil_language.cpp @@ -62,12 +62,11 @@ bool jsil_languaget::parse( parse_path=path; // parsing + jsil_parsert jsil_parser{message_handler}; jsil_parser.clear(); jsil_parser.set_file(path); jsil_parser.in=&instream; - jsil_parser.log.set_message_handler(message_handler); - jsil_scanner_init(); bool result=jsil_parser.parse(); // save result @@ -137,12 +136,10 @@ bool jsil_languaget::to_expr( std::istringstream instream(code); // parsing - + jsil_parsert jsil_parser{message_handler}; jsil_parser.clear(); jsil_parser.set_file(irep_idt()); jsil_parser.in=&instream; - jsil_parser.log.set_message_handler(message_handler); - jsil_scanner_init(); bool result=jsil_parser.parse(); diff --git a/src/jsil/jsil_parser.cpp b/src/jsil/jsil_parser.cpp index de11bc731e8..234f6510212 100644 --- a/src/jsil/jsil_parser.cpp +++ b/src/jsil/jsil_parser.cpp @@ -10,13 +10,3 @@ Author: Michael Tautschnig, tautschn@amazon.com /// Jsil Language #include "jsil_parser.h" - -jsil_parsert jsil_parser; - -extern char *yyjsiltext; - -int yyjsilerror(const std::string &error) -{ - jsil_parser.parse_error(error, yyjsiltext); - return 0; -} diff --git a/src/jsil/jsil_parser.h b/src/jsil/jsil_parser.h index 2aad7767e34..c77e492259b 100644 --- a/src/jsil/jsil_parser.h +++ b/src/jsil/jsil_parser.h @@ -16,16 +16,24 @@ Author: Michael Tautschnig, tautschn@amazon.com #include "jsil_parse_tree.h" -int yyjsilparse(); +class jsil_parsert; +int yyjsilparse(jsil_parsert &); +void jsil_scanner_init(jsil_parsert &); class jsil_parsert:public parsert { public: + explicit jsil_parsert(message_handlert &message_handler) + : parsert(message_handler) + { + } + jsil_parse_treet parse_tree; virtual bool parse() override { - return yyjsilparse()!=0; + jsil_scanner_init(*this); + return yyjsilparse(*this) != 0; } virtual void clear() override @@ -41,9 +49,4 @@ class jsil_parsert:public parsert std::string string_literal; }; -extern jsil_parsert jsil_parser; - -int yyjsilerror(const std::string &error); -void jsil_scanner_init(); - #endif // CPROVER_JSIL_JSIL_PARSER_H diff --git a/src/jsil/parser.y b/src/jsil/parser.y index 7488353d034..31c96d972ed 100644 --- a/src/jsil/parser.y +++ b/src/jsil/parser.y @@ -1,13 +1,27 @@ %{ // #define YYDEBUG 1 -#define PARSER jsil_parser +#define PARSER (*jsil_parser) #include "jsil_parser.h" int yyjsillex(); extern char *yyjsiltext; +static jsil_parsert *jsil_parser; +int yyjsilparse(void); +int yyjsilparse(jsil_parsert &_jsil_parser) +{ + jsil_parser = &_jsil_parser; + return yyjsilparse(); +} + +int yyjsilerror(const std::string &error) +{ + jsil_parser->parse_error(error, yyjsiltext); + return 0; +} + #define YYSTYPE unsigned #define YYSTYPE_IS_TRIVIAL 1 diff --git a/src/jsil/scanner.l b/src/jsil/scanner.l index 1ed37abebfa..4ec6cef9336 100755 --- a/src/jsil/scanner.l +++ b/src/jsil/scanner.l @@ -17,13 +17,23 @@ #include #include -#define PARSER jsil_parser +#define PARSER (*jsil_parser) #define YYSTYPE unsigned #include "jsil_parser.h" #include "jsil_y.tab.h" // extern int yyjsildebug; +static jsil_parsert *jsil_parser; +void jsil_scanner_init(jsil_parsert &_jsil_parser) +{ + jsil_parser = &_jsil_parser; + YY_FLUSH_BUFFER; + BEGIN(0); +} + +int yyjsilerror(const std::string &error); + #define loc() \ { newstack(yyjsillval); PARSER.set_source_location(parser_stack(yyjsillval)); } @@ -71,14 +81,6 @@ string_lit ["]{s_char}*["] %x STRING_LITERAL_COMMENT %x STATEMENTS -%{ -void jsil_scanner_init() -{ - // yyjsildebug=1; - YY_FLUSH_BUFFER; - BEGIN(0); -} -%} /* %option debug */ %%