alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

parseaut: make the scanner reentrant

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2017-07-26 18:25:09 +02:00
parent 6c3e09489e
commit b9fff6a4b1
5 changed files with 108 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -163,6 +163,10 @@ New in spot 2.3.5.dev (not yet released)
(for efficiency reasons), in this version operator | is (for efficiency reasons), in this version operator | is
symmetrically grouping all Fin() terms. 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: Python:
- The 'spot.gen' package exports the functions from libspotgen. - The 'spot.gen' package exports the functions from libspotgen.

33
spot/parseaut/parseaut.yy
View file

@ -24,7 +24,8 @@
%name-prefix "hoayy" %name-prefix "hoayy"
%debug %debug
%error-verbose %error-verbose
%lex-param { PARSE_ERROR_LIST } %parse-param {void* scanner}
%lex-param {void* scanner} { PARSE_ERROR_LIST }
%define api.location.type "spot::location" %define api.location.type "spot::location"
%code requires %code requires
@ -2382,32 +2383,50 @@ namespace spot
{ {
automaton_stream_parser::automaton_stream_parser(const std::string& name, automaton_stream_parser::automaton_stream_parser(const std::string& name,
automaton_parser_options opt) automaton_parser_options opt)
try
: filename_(name), opts_(opt) : filename_(name), opts_(opt)
{ {
if (hoayyopen(name)) if (hoayyopen(name, &scanner_))
throw std::runtime_error(std::string("Cannot open file ") + name); throw std::runtime_error(std::string("Cannot open file ") + name);
} }
catch (...)
{
hoayyclose(scanner_);
throw;
}
automaton_stream_parser::automaton_stream_parser(int fd, automaton_stream_parser::automaton_stream_parser(int fd,
const std::string& name, const std::string& name,
automaton_parser_options opt) automaton_parser_options opt)
try
: filename_(name), opts_(opt) : filename_(name), opts_(opt)
{ {
if (hoayyopen(fd)) if (hoayyopen(fd, &scanner_))
throw std::runtime_error(std::string("Cannot open file ") + name); throw std::runtime_error(std::string("Cannot open file ") + name);
} }
catch (...)
{
hoayyclose(scanner_);
throw;
}
automaton_stream_parser::automaton_stream_parser(const char* data, automaton_stream_parser::automaton_stream_parser(const char* data,
const std::string& filename, const std::string& filename,
automaton_parser_options opt) automaton_parser_options opt)
try
: filename_(filename), opts_(opt) : filename_(filename), opts_(opt)
{ {
hoayystring(data); hoayystring(data, &scanner_);
}
catch (...)
{
hoayyclose(scanner_);
throw;
} }
automaton_stream_parser::~automaton_stream_parser() automaton_stream_parser::~automaton_stream_parser()
{ {
hoayyclose(); hoayyclose(scanner_);
} }
static void raise_parse_error(const parsed_aut_ptr& pa) static void raise_parse_error(const parsed_aut_ptr& pa)
@ -2437,10 +2456,10 @@ namespace spot
else else
r.aut_or_ks = r.h->aut = make_twa_graph(dict); r.aut_or_ks = r.h->aut = make_twa_graph(dict);
r.env = &env; r.env = &env;
hoayy::parser parser(r, last_loc); hoayy::parser parser(scanner_, r, last_loc);
static bool env_debug = !!getenv("SPOT_DEBUG_PARSER"); static bool env_debug = !!getenv("SPOT_DEBUG_PARSER");
parser.set_debug_level(opts_.debug || env_debug); parser.set_debug_level(opts_.debug || env_debug);
hoayyreset(); hoayyreset(scanner_);
try try
{ {
if (parser.parse()) if (parser.parse())

15
spot/parseaut/parsedecl.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement // Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et
// de l'EPITA. // Développement de l'EPITA.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -26,16 +26,17 @@
# define YY_DECL \ # define YY_DECL \
int hoayylex(hoayy::parser::semantic_type *yylval, \ int hoayylex(hoayy::parser::semantic_type *yylval, \
spot::location *yylloc, \ spot::location *yylloc, \
void* yyscanner, \
spot::parse_aut_error_list& error_list) spot::parse_aut_error_list& error_list)
YY_DECL; YY_DECL;
namespace spot namespace spot
{ {
void hoayyreset(); void hoayyreset(void* scanner);
int hoayyopen(const std::string& name); int hoayyopen(const std::string& name, void** scanner);
int hoayyopen(int fd); int hoayyopen(int fd, void** scanner);
int hoayystring(const char* data); int hoayystring(const char* data, void** scanner);
void hoayyclose(); void hoayyclose(void* scanner);
// This exception is thrown by the lexer when it reads "--ABORT--". // This exception is thrown by the lexer when it reads "--ABORT--".
struct hoa_abort struct hoa_abort

3
spot/parseaut/public.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -122,6 +122,7 @@ namespace spot
spot::location last_loc; spot::location last_loc;
std::string filename_; std::string filename_;
automaton_parser_options opts_; automaton_parser_options opts_;
void* scanner_;
public: public:
/// \brief Parse from a file. /// \brief Parse from a file.
/// ///

123
spot/parseaut/scanaut.ll
View file

@ -20,6 +20,9 @@
%option noyywrap %option noyywrap
%option prefix="hoayy" %option prefix="hoayy"
%option outfile="lex.yy.c" %option outfile="lex.yy.c"
%option reentrant
%option extra-type="struct extra_data*"
/* %option debug */ /* %option debug */
%{ %{
@ -29,16 +32,19 @@
#include "spot/priv/trim.hh" #include "spot/priv/trim.hh"
#define YY_USER_ACTION yylloc->columns(yyleng); #define YY_USER_ACTION yylloc->columns(yyleng);
#define YY_NEVER_INTERACTIVE 1
typedef hoayy::parser::token token; typedef hoayy::parser::token token;
static unsigned comment_level = 0;
static unsigned parent_level = 0; struct extra_data
static int orig_cond = 0; {
static bool lbtt_s = false; unsigned comment_level = 0;
static bool lbtt_t = false; unsigned parent_level = 0;
static unsigned lbtt_states = 0; int orig_cond = 0;
static bool yyin_close = true; 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(); {eol2} yylloc->lines(yyleng / 2); yylloc->step();
[ \t\v\f]+ yylloc->step(); [ \t\v\f]+ yylloc->step();
"/*" { "/*" {
orig_cond = YY_START; yyextra->orig_cond = YY_START;
BEGIN(in_COMMENT); BEGIN(in_COMMENT);
comment_level = 1; yyextra->comment_level = 1;
} }
<INITIAL>"HOA:" BEGIN(in_HOA); return token::HOA; <INITIAL>"HOA:" BEGIN(in_HOA); return token::HOA;
<INITIAL,in_HOA>"--ABORT--" BEGIN(INITIAL); throw spot::hoa_abort{*yylloc}; <INITIAL,in_HOA>"--ABORT--" BEGIN(INITIAL); throw spot::hoa_abort{*yylloc};
@ -105,7 +111,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
"value too large")); "value too large"));
yylval->num = 0; yylval->num = 0;
} }
lbtt_states = yylval->num; yyextra->lbtt_states = yylval->num;
return token::LBTT; return token::LBTT;
} }
@ -179,7 +185,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
"assert" return token::ASSERT; "assert" return token::ASSERT;
("!"[ \t]*)?"(" { ("!"[ \t]*)?"(" {
parent_level = 1; yyextra->parent_level = 1;
BEGIN(in_NEVER_PAR); BEGIN(in_NEVER_PAR);
yylval->str = new std::string(yytext, yyleng); yylval->str = new std::string(yytext, yyleng);
} }
@ -205,24 +211,24 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
[0-9]+[st]* { [0-9]+[st]* {
BEGIN(in_LBTT_STATE); BEGIN(in_LBTT_STATE);
auto end = parse_int(); auto end = parse_int();
lbtt_s = false; yyextra->lbtt_s = false;
lbtt_t = false; yyextra->lbtt_t = false;
if (end) if (end)
while (int c = *end++) while (int c = *end++)
{ {
if (c == 's') if (c == 's')
lbtt_s = true; yyextra->lbtt_s = true;
else // c == 't' else // c == 't'
lbtt_t = true; yyextra->lbtt_t = true;
} }
if (!lbtt_t) if (!yyextra->lbtt_t)
lbtt_s = true; yyextra->lbtt_s = true;
if (lbtt_states == 0) if (yyextra->lbtt_states == 0)
{ {
BEGIN(INITIAL); BEGIN(INITIAL);
return token::LBTT_EMPTY; return token::LBTT_EMPTY;
} }
if (lbtt_s && !lbtt_t) if (yyextra->lbtt_s && !yyextra->lbtt_t)
return token::INT_S; return token::INT_S;
else else
return token::INT; return token::INT;
@ -236,7 +242,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
} }
<in_LBTT_INIT>[01] { <in_LBTT_INIT>[01] {
yylval->num = *yytext - '0'; yylval->num = *yytext - '0';
if (lbtt_s) if (yyextra->lbtt_s)
BEGIN(in_LBTT_S_ACC); BEGIN(in_LBTT_S_ACC);
else else
BEGIN(in_LBTT_TRANS); BEGIN(in_LBTT_TRANS);
@ -249,14 +255,14 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
<in_LBTT_TRANS>{ <in_LBTT_TRANS>{
[0-9]+ { [0-9]+ {
parse_int(); parse_int();
if (lbtt_t) if (yyextra->lbtt_t)
BEGIN(in_LBTT_T_ACC); BEGIN(in_LBTT_T_ACC);
else else
BEGIN(in_LBTT_GUARD); BEGIN(in_LBTT_GUARD);
return token::DEST_NUM; return token::DEST_NUM;
} }
"-1" { "-1" {
if (--lbtt_states) if (--yyextra->lbtt_states)
{ {
BEGIN(in_LBTT_STATE); BEGIN(in_LBTT_STATE);
yylloc->step(); yylloc->step();
@ -282,21 +288,23 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
<in_COMMENT>{ <in_COMMENT>{
"/*" ++comment_level; "/*" ++yyextra->comment_level;
[^*/\n\r]* continue; [^*/\n\r]* continue;
"/"[^*\n\r]* continue; "/"[^*\n\r]* continue;
"*" continue; "*" continue;
{eol} yylloc->lines(yyleng); yylloc->end.column = 1; {eol} yylloc->lines(yyleng); yylloc->end.column = 1;
{eol2} yylloc->lines(yyleng / 2); yylloc->end.column = 1; {eol2} yylloc->lines(yyleng / 2); yylloc->end.column = 1;
"*/" { "*/" {
if (--comment_level == 0) if (--yyextra->comment_level == 0)
{ {
yylloc->step(); yylloc->step();
BEGIN(orig_cond); int oc = yyextra->orig_cond;
BEGIN(oc);
} }
} }
<<EOF>> { <<EOF>> {
BEGIN(orig_cond); int oc = yyextra->orig_cond;
BEGIN(oc);
error_list.push_back( error_list.push_back(
spot::parse_aut_error(*yylloc, spot::parse_aut_error(*yylloc,
"unclosed comment")); "unclosed comment"));
@ -306,14 +314,15 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
/* matched late, so that the in_LBTT_GUARD pattern has precedence */ /* matched late, so that the in_LBTT_GUARD pattern has precedence */
"\"" { "\"" {
orig_cond = YY_START; yyextra->orig_cond = YY_START;
BEGIN(in_STRING); BEGIN(in_STRING);
comment_level = 1; yyextra->comment_level = 1;
} }
<in_STRING>{ <in_STRING>{
\" { \" {
BEGIN(orig_cond); int oc = yyextra->orig_cond;
BEGIN(oc);
yylval->str = new std::string(s); yylval->str = new std::string(s);
return token::STRING; return token::STRING;
} }
@ -331,7 +340,8 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
error_list.push_back( error_list.push_back(
spot::parse_aut_error(*yylloc, spot::parse_aut_error(*yylloc,
"unclosed string")); "unclosed string"));
BEGIN(orig_cond); int oc = yyextra->orig_cond;
BEGIN(oc);
yylval->str = new std::string(s); yylval->str = new std::string(s);
return token::STRING; return token::STRING;
} }
@ -339,7 +349,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
<in_NEVER_PAR>{ <in_NEVER_PAR>{
"(" { "(" {
++parent_level; ++yyextra->parent_level;
yylval->str->append(yytext, yyleng); yylval->str->append(yytext, yyleng);
} }
/* if we match ")&&(" or ")||(", stay in <in_NEVER_PAR> mode */ /* if we match ")&&(" or ")||(", stay in <in_NEVER_PAR> mode */
@ -348,7 +358,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
} }
")" { ")" {
yylval->str->append(yytext, yyleng); yylval->str->append(yytext, yyleng);
if (!--parent_level) if (!--yyextra->parent_level)
{ {
BEGIN(in_NEVER); BEGIN(in_NEVER);
spot::trim(*yylval->str); spot::trim(*yylval->str);
@ -368,7 +378,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
error_list.push_back( error_list.push_back(
spot::parse_aut_error(*yylloc, spot::parse_aut_error(*yylloc,
"missing closing parenthese")); "missing closing parenthese"));
yylval->str->append(parent_level, ')'); yylval->str->append(yyextra->parent_level, ')');
BEGIN(in_NEVER); BEGIN(in_NEVER);
spot::trim(*yylval->str); spot::trim(*yylval->str);
return token::FORMULA; return token::FORMULA;
@ -387,16 +397,20 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
namespace spot namespace spot
{ {
void void
hoayyreset() hoayyreset(yyscan_t yyscanner)
{ {
struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
BEGIN(INITIAL); BEGIN(INITIAL);
comment_level = 0; yyextra->comment_level = 0;
parent_level = 0; yyextra->parent_level = 0;
} }
int 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; bool want_interactive = false;
// yy_flex_debug = 1; // yy_flex_debug = 1;
@ -412,37 +426,37 @@ namespace spot
want_interactive = true; want_interactive = true;
yyin = stdin; yyin = stdin;
yyin_close = false; yyextra->yyin_close = false;
} }
else else
{ {
yyin = fopen(name.c_str(), "r"); yyin = fopen(name.c_str(), "r");
if (!yyin) if (!yyin)
return 1; 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) if (want_interactive)
yy_set_interactive(1); yy_set_interactive(1);
return 0; return 0;
} }
int int
hoayystring(const char* data) hoayystring(const char* data, yyscan_t* scanner)
{ {
yy_scan_string(data); yylex_init_extra(new extra_data, scanner);
hoayyreset(); yy_scan_string(data, *scanner);
return 0; return 0;
} }
int 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; bool want_interactive = false;
yyin_close = false; yyextra->yyin_close = false;
yyin = fdopen(fd, "r"); yyin = fdopen(fd, "r");
@ -458,23 +472,22 @@ namespace spot
if (S_ISFIFO(s.st_mode)) if (S_ISFIFO(s.st_mode))
want_interactive = true; want_interactive = true;
// Reset the lexer in case a previous parse
// ended badly.
YY_NEW_FILE;
hoayyreset();
if (want_interactive) if (want_interactive)
yy_set_interactive(1); yy_set_interactive(1);
return 0; return 0;
} }
void void
hoayyclose() hoayyclose(yyscan_t yyscanner)
{ {
struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
if (yyin) if (yyin)
{ {
if (yyin_close) if (yyextra->yyin_close)
fclose(yyin); fclose(yyin);
yyin = NULL; yyin = NULL;
} }
delete yyextra;
yylex_destroy(yyscanner);
} }
} }