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); } }