statement_list_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. Both the
parser and lexer are now fully reentrant.

Author: tautschnig

src/statement-list/parser.y

@@ -23,8 +23,17 @@
 
 #include <iterator>
 
-int yystatement_listlex();
-extern char *yystatement_listtext;
+int yystatement_listlex(void *);
+char *yystatement_listget_text(void *);
+
+int yystatement_listerror(
+  statement_list_parsert &statement_list_parser,
+  void *scanner,
+  const std::string &error)
+{
+  statement_list_parser.parse_error(error, yystatement_listget_text(scanner));
+  return 0;
+}
 
 #define YYSTYPE unsigned
 #define YYSTYPE_IS_TRIVIAL 1
@@ -43,9 +52,13 @@ extern char *yystatement_listtext;
 // Disable warning for unreachable code.
 #pragma warning(disable:4702)
 #endif
+%}
+
+%parse-param {statement_list_parsert &statement_list_parser}
+%parse-param {void *scanner}
+%lex-param {void *scanner}
 
 /*** Token declaration *******************************************************/
-%}
 
 /*** STL file structure keywords *********************************************/
 %token TOK_VERSION              "VERSION"

src/statement-list/scanner.l

@@ -41,7 +41,7 @@ static int isatty(int) { return 0; }
 #endif
 
 // Value inside of statement_list_parser.h.
-#define PARSER statement_list_parser
+#define PARSER (*yyextra)
 
 // Sets the type of yystatement_listlval so that it can be used as the stack 
 // index.
@@ -58,22 +58,12 @@ static int isatty(int) { return 0; }
 #define loc() \
   { newstack(yystatement_listlval); \
     PARSER.set_source_location(parser_stack(yystatement_listlval)); }
-  
-#ifdef STATEMENT_LIST_DEBUG
-extern int yystatement_listdebug;
-#endif
-void statement_list_scanner_init()
-{
-#ifdef STATEMENT_LIST_DEBUG
-  yystatement_listdebug=1;
-#endif
-  YY_FLUSH_BUFFER;
-  BEGIN(0);
-}
 %}
 %option noyywrap
 %option noinput
 %option nounput
+%option reentrant
+%option extra-type="statement_list_parsert *"
 
 %x GRAMMAR
 %x TAG_NAME

src/statement-list/statement_list_language.cpp

@@ -60,12 +60,11 @@ bool statement_list_languaget::parse(
   const std::string &path,
   message_handlert &message_handler)
 {
-  statement_list_parser.clear();
+  statement_list_parsert statement_list_parser{message_handler};
   parse_path = path;
   statement_list_parser.set_line_no(0);
   statement_list_parser.set_file(path);
   statement_list_parser.in = &instream;
-  statement_list_scanner_init();
   bool result = statement_list_parser.parse();
 
   // store result

src/statement-list/statement_list_parser.cpp

@@ -21,10 +21,6 @@ Author: Matthias Weiss, [email protected]
 #include <iostream>
 #include <iterator>
 
-statement_list_parsert statement_list_parser;
-
-extern char *yystatement_listtext;
-
 /// Searches for the name of the TIA module inside of its root
 /// expression.
 /// \param root: Expression that includes the element's name as a
@@ -335,15 +331,23 @@ void statement_list_parsert::add_function(const exprt &function)
   parse_tree.add_function(fn);
 }
 
-bool statement_list_parsert::parse()
-{
-  return yystatement_listparse() != 0;
-}
+int yystatement_listlex_init_extra(statement_list_parsert *, void **);
+int yystatement_listlex_destroy(void *);
+/// Defined in statement_list_y.tab.cpp. Main function for the parse process
+/// generated by bison, performs all necessary steps to fill the parse tree.
+int yystatement_listparse(statement_list_parsert &, void *);
+void yystatement_listset_debug(int, void *);
 
-int yystatement_listerror(const std::string &error)
+bool statement_list_parsert::parse()
 {
-  statement_list_parser.parse_error(error, yystatement_listtext);
-  return 0;
+  void *scanner;
+  yystatement_listlex_init_extra(this, &scanner);
+#ifdef STATEMENT_LIST_DEBUG
+  yystatement_listset_debug(1, scanner);
+#endif
+  bool parse_fail = yystatement_listparse(*this, scanner) != 0;
+  yystatement_listlex_destroy(scanner);
+  return parse_fail;
 }
 
 void statement_list_parsert::clear()

src/statement-list/statement_list_parser.h

@@ -16,10 +16,6 @@ Author: Matthias Weiss, [email protected]
 
 #include "statement_list_parse_tree.h"
 
-/// Defined in statement_list_y.tab.cpp. Main function for the parse process
-/// generated by bison, performs all necessary steps to fill the parse tree.
-int yystatement_listparse();
-
 /// Responsible for starting the parse process and to translate the result into
 /// a statement_list_parse_treet. This parser works by using the expression
 /// stack of its base class. During the parse process, expressions with
@@ -34,6 +30,12 @@ int yystatement_listparse();
 class statement_list_parsert : public parsert
 {
 public:
+  /// Constructor
+  explicit statement_list_parsert(message_handlert &message_handler)
+    : parsert(message_handler)
+  {
+  }
+
   /// Starts the parsing process and saves the result inside of this instance's
   /// parse tree.
   /// \return False if successful.
@@ -71,17 +73,15 @@ class statement_list_parsert : public parsert
   statement_list_parse_treet parse_tree;
 };
 
-/// Instance of the parser, used by other modules.
-extern statement_list_parsert statement_list_parser;
-
 /// Forwards any errors that are encountered during the parse process. This
 /// function gets called by the generated files of flex and bison.
+/// \param parser: Parser object.
+/// \param scanner: Lexer state.
 /// \param error: Error message.
 /// \return Always 0.
-int yystatement_listerror(const std::string &error);
-
-/// Defined in scanner.l. This function initialises the scanner by setting
-/// debug flags (if present) and its initial state.
-void statement_list_scanner_init();
+int yystatement_listerror(
+  statement_list_parsert &parser,
+  void *scanner,
+  const std::string &error);
 
 #endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_PARSER_H