From b9fff6a4b1385be6a0c669a88f327961fe2e87cd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 26 Jul 2017 18:25:09 +0200 Subject: [PATCH] parseaut: make the scanner reentrant * spot/parseaut/parseaut.yy, spot/parseaut/parsedecl.hh, spot/parseaut/public.hh, spot/parseaut/scanaut.ll: Use a reentrant scanner, so that we can now parse multiple automaton streams at the same time. This is needed for the future autcross, which is going to read several individual automata produced by different tools, while reading the stream of automata to process. --- NEWS | 4 ++ spot/parseaut/parseaut.yy | 33 +++++++--- spot/parseaut/parsedecl.hh | 15 ++--- spot/parseaut/public.hh | 3 +- spot/parseaut/scanaut.ll | 123 ++++++++++++++++++++----------------- 5 files changed, 108 insertions(+), 70 deletions(-) diff --git a/NEWS b/NEWS index 471136894..0cd10ab2b 100644 --- a/NEWS +++ b/NEWS @@ -163,6 +163,10 @@ New in spot 2.3.5.dev (not yet released) (for efficiency reasons), in this version operator | is symmetrically grouping all Fin() terms. + - The automaton parser is now reentrant, making it possible to + process automata from different streams at the same time (i.e., + using multiple spot::automaton_stream_parser instances at once). + Python: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 3c405a0dc..5e9e37a0e 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -24,7 +24,8 @@ %name-prefix "hoayy" %debug %error-verbose -%lex-param { PARSE_ERROR_LIST } +%parse-param {void* scanner} +%lex-param {void* scanner} { PARSE_ERROR_LIST } %define api.location.type "spot::location" %code requires @@ -2382,32 +2383,50 @@ namespace spot { automaton_stream_parser::automaton_stream_parser(const std::string& name, automaton_parser_options opt) + try : filename_(name), opts_(opt) { - if (hoayyopen(name)) + if (hoayyopen(name, &scanner_)) throw std::runtime_error(std::string("Cannot open file ") + name); } + catch (...) + { + hoayyclose(scanner_); + throw; + } automaton_stream_parser::automaton_stream_parser(int fd, const std::string& name, automaton_parser_options opt) + try : filename_(name), opts_(opt) { - if (hoayyopen(fd)) + if (hoayyopen(fd, &scanner_)) throw std::runtime_error(std::string("Cannot open file ") + name); } + catch (...) + { + hoayyclose(scanner_); + throw; + } automaton_stream_parser::automaton_stream_parser(const char* data, const std::string& filename, automaton_parser_options opt) + try : filename_(filename), opts_(opt) { - hoayystring(data); + hoayystring(data, &scanner_); + } + catch (...) + { + hoayyclose(scanner_); + throw; } automaton_stream_parser::~automaton_stream_parser() { - hoayyclose(); + hoayyclose(scanner_); } static void raise_parse_error(const parsed_aut_ptr& pa) @@ -2437,10 +2456,10 @@ namespace spot else r.aut_or_ks = r.h->aut = make_twa_graph(dict); r.env = &env; - hoayy::parser parser(r, last_loc); + hoayy::parser parser(scanner_, r, last_loc); static bool env_debug = !!getenv("SPOT_DEBUG_PARSER"); parser.set_debug_level(opts_.debug || env_debug); - hoayyreset(); + hoayyreset(scanner_); try { if (parser.parse()) diff --git a/spot/parseaut/parsedecl.hh b/spot/parseaut/parsedecl.hh index a7b80802a..22ed90440 100644 --- a/spot/parseaut/parsedecl.hh +++ b/spot/parseaut/parsedecl.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement -// de l'EPITA. +// Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et +// Développement de l'EPITA. // // This file is part of Spot, a model checking library. // @@ -26,16 +26,17 @@ # define YY_DECL \ int hoayylex(hoayy::parser::semantic_type *yylval, \ spot::location *yylloc, \ + void* yyscanner, \ spot::parse_aut_error_list& error_list) YY_DECL; namespace spot { - void hoayyreset(); - int hoayyopen(const std::string& name); - int hoayyopen(int fd); - int hoayystring(const char* data); - void hoayyclose(); + void hoayyreset(void* scanner); + int hoayyopen(const std::string& name, void** scanner); + int hoayyopen(int fd, void** scanner); + int hoayystring(const char* data, void** scanner); + void hoayyclose(void* scanner); // This exception is thrown by the lexer when it reads "--ABORT--". struct hoa_abort diff --git a/spot/parseaut/public.hh b/spot/parseaut/public.hh index 17b549b91..b6332dd36 100644 --- a/spot/parseaut/public.hh +++ b/spot/parseaut/public.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -122,6 +122,7 @@ namespace spot spot::location last_loc; std::string filename_; automaton_parser_options opts_; + void* scanner_; public: /// \brief Parse from a file. /// diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll index 71db33836..aef870ae5 100644 --- a/spot/parseaut/scanaut.ll +++ b/spot/parseaut/scanaut.ll @@ -20,6 +20,9 @@ %option noyywrap %option prefix="hoayy" %option outfile="lex.yy.c" +%option reentrant +%option extra-type="struct extra_data*" + /* %option debug */ %{ @@ -29,16 +32,19 @@ #include "spot/priv/trim.hh" #define YY_USER_ACTION yylloc->columns(yyleng); -#define YY_NEVER_INTERACTIVE 1 typedef hoayy::parser::token token; -static unsigned comment_level = 0; -static unsigned parent_level = 0; -static int orig_cond = 0; -static bool lbtt_s = false; -static bool lbtt_t = false; -static unsigned lbtt_states = 0; -static bool yyin_close = true; + +struct extra_data +{ + unsigned comment_level = 0; + unsigned parent_level = 0; + int orig_cond = 0; + bool lbtt_s = false; + bool lbtt_t = false; + unsigned lbtt_states = 0; + bool yyin_close = true; +}; %} @@ -78,9 +84,9 @@ identifier [[:alpha:]_][[:alnum:]_.-]* {eol2} yylloc->lines(yyleng / 2); yylloc->step(); [ \t\v\f]+ yylloc->step(); "/*" { - orig_cond = YY_START; + yyextra->orig_cond = YY_START; BEGIN(in_COMMENT); - comment_level = 1; + yyextra->comment_level = 1; } "HOA:" BEGIN(in_HOA); return token::HOA; "--ABORT--" BEGIN(INITIAL); throw spot::hoa_abort{*yylloc}; @@ -105,7 +111,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]* "value too large")); yylval->num = 0; } - lbtt_states = yylval->num; + yyextra->lbtt_states = yylval->num; return token::LBTT; } @@ -179,7 +185,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]* "assert" return token::ASSERT; ("!"[ \t]*)?"(" { - parent_level = 1; + yyextra->parent_level = 1; BEGIN(in_NEVER_PAR); yylval->str = new std::string(yytext, yyleng); } @@ -205,24 +211,24 @@ identifier [[:alpha:]_][[:alnum:]_.-]* [0-9]+[st]* { BEGIN(in_LBTT_STATE); auto end = parse_int(); - lbtt_s = false; - lbtt_t = false; + yyextra->lbtt_s = false; + yyextra->lbtt_t = false; if (end) while (int c = *end++) { if (c == 's') - lbtt_s = true; + yyextra->lbtt_s = true; else // c == 't' - lbtt_t = true; + yyextra->lbtt_t = true; } - if (!lbtt_t) - lbtt_s = true; - if (lbtt_states == 0) + if (!yyextra->lbtt_t) + yyextra->lbtt_s = true; + if (yyextra->lbtt_states == 0) { BEGIN(INITIAL); return token::LBTT_EMPTY; } - if (lbtt_s && !lbtt_t) + if (yyextra->lbtt_s && !yyextra->lbtt_t) return token::INT_S; else return token::INT; @@ -236,7 +242,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]* } [01] { yylval->num = *yytext - '0'; - if (lbtt_s) + if (yyextra->lbtt_s) BEGIN(in_LBTT_S_ACC); else BEGIN(in_LBTT_TRANS); @@ -249,14 +255,14 @@ identifier [[:alpha:]_][[:alnum:]_.-]* { [0-9]+ { parse_int(); - if (lbtt_t) + if (yyextra->lbtt_t) BEGIN(in_LBTT_T_ACC); else BEGIN(in_LBTT_GUARD); return token::DEST_NUM; } "-1" { - if (--lbtt_states) + if (--yyextra->lbtt_states) { BEGIN(in_LBTT_STATE); yylloc->step(); @@ -282,21 +288,23 @@ identifier [[:alpha:]_][[:alnum:]_.-]* { - "/*" ++comment_level; + "/*" ++yyextra->comment_level; [^*/\n\r]* continue; "/"[^*\n\r]* continue; "*" continue; {eol} yylloc->lines(yyleng); yylloc->end.column = 1; {eol2} yylloc->lines(yyleng / 2); yylloc->end.column = 1; "*/" { - if (--comment_level == 0) + if (--yyextra->comment_level == 0) { yylloc->step(); - BEGIN(orig_cond); + int oc = yyextra->orig_cond; + BEGIN(oc); } } <> { - BEGIN(orig_cond); + int oc = yyextra->orig_cond; + BEGIN(oc); error_list.push_back( spot::parse_aut_error(*yylloc, "unclosed comment")); @@ -306,14 +314,15 @@ identifier [[:alpha:]_][[:alnum:]_.-]* /* matched late, so that the in_LBTT_GUARD pattern has precedence */ "\"" { - orig_cond = YY_START; + yyextra->orig_cond = YY_START; BEGIN(in_STRING); - comment_level = 1; + yyextra->comment_level = 1; } { \" { - BEGIN(orig_cond); + int oc = yyextra->orig_cond; + BEGIN(oc); yylval->str = new std::string(s); return token::STRING; } @@ -331,7 +340,8 @@ identifier [[:alpha:]_][[:alnum:]_.-]* error_list.push_back( spot::parse_aut_error(*yylloc, "unclosed string")); - BEGIN(orig_cond); + int oc = yyextra->orig_cond; + BEGIN(oc); yylval->str = new std::string(s); return token::STRING; } @@ -339,7 +349,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]* { "(" { - ++parent_level; + ++yyextra->parent_level; yylval->str->append(yytext, yyleng); } /* if we match ")&&(" or ")||(", stay in mode */ @@ -348,7 +358,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]* } ")" { yylval->str->append(yytext, yyleng); - if (!--parent_level) + if (!--yyextra->parent_level) { BEGIN(in_NEVER); spot::trim(*yylval->str); @@ -368,7 +378,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]* error_list.push_back( spot::parse_aut_error(*yylloc, "missing closing parenthese")); - yylval->str->append(parent_level, ')'); + yylval->str->append(yyextra->parent_level, ')'); BEGIN(in_NEVER); spot::trim(*yylval->str); return token::FORMULA; @@ -387,16 +397,20 @@ identifier [[:alpha:]_][[:alnum:]_.-]* namespace spot { void - hoayyreset() + hoayyreset(yyscan_t yyscanner) { + struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; BEGIN(INITIAL); - comment_level = 0; - parent_level = 0; + yyextra->comment_level = 0; + yyextra->parent_level = 0; } int - hoayyopen(const std::string &name) + hoayyopen(const std::string &name, yyscan_t* scanner) { + yylex_init_extra(new extra_data, scanner); + yyscan_t yyscanner = *scanner; + struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; bool want_interactive = false; // yy_flex_debug = 1; @@ -412,37 +426,37 @@ namespace spot want_interactive = true; yyin = stdin; - yyin_close = false; + yyextra->yyin_close = false; } else { yyin = fopen(name.c_str(), "r"); if (!yyin) return 1; - yyin_close = true; + yyextra->yyin_close = true; } - // Reset the lexer in case a previous parse - // ended badly. - YY_NEW_FILE; - hoayyreset(); + if (want_interactive) yy_set_interactive(1); return 0; } int - hoayystring(const char* data) + hoayystring(const char* data, yyscan_t* scanner) { - yy_scan_string(data); - hoayyreset(); + yylex_init_extra(new extra_data, scanner); + yy_scan_string(data, *scanner); return 0; } int - hoayyopen(int fd) + hoayyopen(int fd, yyscan_t* scanner) { + yylex_init_extra(new extra_data, scanner); + yyscan_t yyscanner = *scanner; + struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; bool want_interactive = false; - yyin_close = false; + yyextra->yyin_close = false; yyin = fdopen(fd, "r"); @@ -458,23 +472,22 @@ namespace spot if (S_ISFIFO(s.st_mode)) want_interactive = true; - // Reset the lexer in case a previous parse - // ended badly. - YY_NEW_FILE; - hoayyreset(); if (want_interactive) yy_set_interactive(1); return 0; } void - hoayyclose() + hoayyclose(yyscan_t yyscanner) { + struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; if (yyin) { - if (yyin_close) + if (yyextra->yyin_close) fclose(yyin); yyin = NULL; } + delete yyextra; + yylex_destroy(yyscanner); } }