From 1d962f79ac7a9c6967bfd0ea4c9d98f85809b978 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 20 Nov 2014 12:29:18 +0100 Subject: [PATCH] hoa: make the parser more resilient to errors * src/hoaparse/hoaparse.yy: Improve error recovery, and fix location tracking in streams. * src/hoaparse/public.hh: Store the last location so that the next parse start at the correct position. * src/bin/autfilt.cc: Stop parsing a stream on irrecoverable errors. * src/tgbatest/hoaparse.test: Adjust tests. --- src/bin/autfilt.cc | 3 +- src/hoaparse/hoaparse.yy | 194 +++++++++++++++++++++++++------------ src/hoaparse/public.hh | 1 + src/tgbatest/hoaparse.test | 34 ++++--- 4 files changed, 152 insertions(+), 80 deletions(-) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index e9399286c..49c91db89 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -343,13 +343,14 @@ namespace for (;;) { + pel.clear(); auto haut = hp.parse(pel, b); if (!haut && pel.empty()) break; if (spot::format_hoa_parse_errors(std::cerr, filename, pel)) err = 2; if (!haut) - error(0, 0, "failed to read automaton from %s", filename); + error(2, 0, "failed to read automaton from %s", filename); else process_automaton(haut, filename); } diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 7f3cd712d..f4758e8a9 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -35,6 +35,11 @@ #include "ltlast/constant.hh" #include "public.hh" + // Note: because this parser is meant to be used on a stream of + // automata, it tries hard to recover from errors, so that we get a + // chance to reach the end of the current automaton in order to + // process the next one. Several variables below are used to keep + // track of various error conditions. struct result_ { spot::hoa_aut_ptr h; @@ -45,6 +50,7 @@ spot::location state_label_loc; spot::location start_loc; spot::location accset_loc; + spot::location last_loc; unsigned cur_state; int start = -1; int states = -1; @@ -54,12 +60,23 @@ bdd cur_label; bool has_state_label = false; bool has_trans_label = false; + bool ignore_more_ap = false; // Set to true after the first "AP:" + // line has been read. + bool ignore_acc = false; // Set to true in case of missing + // Acceptance: lines. + bool ignore_acc_silent = false; + bool ignore_more_acc = false; // Set to true after the first + // "Acceptance:" line has been read. spot::acc_cond::mark_t acc_state; }; } %parse-param {spot::hoa_parse_error_list& error_list} %parse-param {result_& res} +%parse-param {spot::location initial_loc} + +%initial-action { @$ = initial_loc; } + %union { std::string* str; @@ -115,7 +132,11 @@ %printer { debug_stream() << $$; } %% -hoa: header "--BODY--" body "--END--" { YYACCEPT; } +hoa: header "--BODY--" body "--END--" + { + res.last_loc = @$; + YYACCEPT; + } hoa: ENDOFFILE { YYABORT; } string_opt: | STRING @@ -126,7 +147,7 @@ header: format-version header-items if (res.accset < 0) { error(@$, "missing 'Acceptance:' header"); - YYABORT; + res.ignore_acc = true; } } @@ -160,9 +181,9 @@ header-item: "States:" INT error(res.start_loc, "initial state number is larger than state count..."); error(@$, "... declared here."); - YYABORT; } - int missing = res.states - res.h->aut->num_states(); + int missing = std::max(res.states, res.start + 1) + - res.h->aut->num_states(); assert(missing >= 0); res.h->aut->new_states(missing); } @@ -183,24 +204,31 @@ header-item: "States:" INT res.start_loc = @$; } | "AP:" INT { - if (res.ap_count != -1) - { - error(@1, "redeclaration of APs..."); - error(res.ap_loc, "... previously defined here."); - YYABORT; - } - res.ap_count = $2; res.ap.reserve($2); + if (res.ignore_more_ap) + { + error(@1, "ignoring this redeclaration of APs..."); + error(res.ap_loc, "... previously declared here."); + } + else + { + res.ap_count = $2; + res.ap.reserve($2); + } } ap-names { - res.ap_loc = @1 + @2; - if ((int) res.ap.size() != res.ap_count) + if (!res.ignore_more_ap) { - std::ostringstream out; - out << "found " << res.ap.size() - << " atomic propositions instead of the " - << res.ap_count << " announced"; - error(@$, out.str()); + res.ap_loc = @1 + @2; + if ((int) res.ap.size() != res.ap_count) + { + std::ostringstream out; + out << "found " << res.ap.size() + << " atomic propositions instead of the " + << res.ap_count << " announced"; + error(@$, out.str()); + } + res.ignore_more_ap = true; } } | "Alias:" ANAME label-expr @@ -210,27 +238,30 @@ header-item: "States:" INT } | "Acceptance:" INT { - if (res.accset >= 0) - { - error(@1 + @2, "redefinition of the acceptance condition..."); - error(res.accset_loc, "... previously defined here."); - YYABORT; - } - else if ($2 > 8 * sizeof(spot::acc_cond::mark_t::value_t)) - { - error(@1 + @2, - "this implementation cannot support such a large " - "number of acceptance sets"); - YYABORT; - } - else - { - res.h->aut->acc().add_sets($2); - res.accset = $2; - res.accset_loc = @1 + @2; - } + if (res.ignore_more_acc) + { + error(@1 + @2, "ignoring this redefinition of the " + "acceptance condition..."); + error(res.accset_loc, "... previously defined here."); + } + else if ($2 > 8 * sizeof(spot::acc_cond::mark_t::value_t)) + { + error(@1 + @2, + "this implementation cannot support such a large " + "number of acceptance sets"); + YYABORT; + } + else + { + res.h->aut->acc().add_sets($2); + res.accset = $2; + res.accset_loc = @1 + @2; + } } acceptance-cond + { + res.ignore_more_acc = true; + } | "acc-name:" IDENTIFIER acc-spec { delete $2; @@ -249,20 +280,24 @@ header-item: "States:" INT ap-names: | ap-names ap-name ap-name: STRING { - auto f = res.env->require(*$1); - if (f == nullptr) + if (!res.ignore_more_ap) { - std::ostringstream out; - out << "unknown atomic proposition \"" << *$1 << "\""; - delete $1; - error(@1, out.str()); - YYABORT; + auto f = res.env->require(*$1); + if (f == nullptr) + { + std::ostringstream out; + out << "unknown atomic proposition \"" << *$1 << "\""; + delete $1; + error(@1, out.str()); + f = spot::ltl::default_environment::instance() + .require("$unknown$"); + } + auto b = + res.h->aut->get_dict()->register_proposition(f, res.h->aut); + f->destroy(); + res.ap.push_back(b); } delete $1; - auto b = - res.h->aut->get_dict()->register_proposition(f, res.h->aut); - f->destroy(); - res.ap.push_back(b); } acc-spec: | acc-spec BOOLEAN @@ -343,24 +378,30 @@ acc-set: INT { if ((int) $1 >= res.accset) { - error(@1, "number is larger than the count " - "of acceptance sets..."); - error(res.accset_loc, "... declared here."); - YYABORT; + if (!res.ignore_acc) + { + error(@1, "number is larger than the count " + "of acceptance sets..."); + error(res.accset_loc, "... declared here."); + } + $$ = -1U; + } + else + { + $$ = $1; } - $$ = $1; } acceptance-cond: IDENTIFIER '(' acc-set ')' { - if (*$1 != "Inf") + if (!res.ignore_more_acc && *$1 != "Inf") error(@1, "this implementation only supports " "'Inf' acceptance"); delete $1; } | IDENTIFIER '(' '!' acc-set ')' { - error(@1, "this implementation does not support " + error(@3 + @4, "this implementation does not support " "negated sets"); delete $1; } @@ -368,10 +409,17 @@ acceptance-cond: IDENTIFIER '(' acc-set ')' | acceptance-cond '&' acceptance-cond | acceptance-cond '|' acceptance-cond { - error(@1, "this implementation does not support " - "disjunction in acceptance conditions"); + if (!res.ignore_more_acc) + error(@2, "this implementation does not support " + "disjunction in acceptance conditions"); } - | BOOLEAN + | 't' + | 'f' + { + if (!res.ignore_more_acc) + error(@$, "this implementation does not support " + "false acceptance"); + } body: states @@ -429,12 +477,31 @@ trans-label_opt: { res.has_trans_label = false; } } } -acc-sig_opt: { $$ = spot::acc_cond::mark_t(0U); } - | '{' acc-sets '}' { $$ = $2; } -acc-sets: { $$ = spot::acc_cond::mark_t(0U); } +acc-sig_opt: + { + $$ = spot::acc_cond::mark_t(0U); + } + | '{' acc-sets '}' + { + $$ = $2; + if (res.ignore_acc && !res.ignore_acc_silent) + { + error(@$, "ignoring acceptance sets because of " + "missing acceptance condition"); + // Emit this message only once. + res.ignore_acc_silent = true; + } + } +acc-sets: + { + $$ = spot::acc_cond::mark_t(0U); + } | acc-sets acc-set { - $$ = $1 | res.h->aut->acc().mark($2); + if (res.ignore_acc || $2 == -1U) + $$ = spot::acc_cond::mark_t(0U); + else + $$ = $1 | res.h->aut->acc().mark($2); } edges: | edges edge edge: trans-label_opt state-num acc-sig_opt @@ -487,10 +554,11 @@ namespace spot r.h = std::make_shared(); r.h->aut = make_tgba_digraph(dict); r.env = &env; - hoayy::parser parser(error_list, r); + hoayy::parser parser(error_list, r, last_loc); parser.set_debug_level(debug); if (parser.parse()) r.h->aut = nullptr; + last_loc = r.last_loc; if (!r.h->aut) return nullptr; if (r.start != -1) diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh index 2d97b6e2b..7f1941632 100644 --- a/src/hoaparse/public.hh +++ b/src/hoaparse/public.hh @@ -53,6 +53,7 @@ namespace spot class SPOT_API hoa_stream_parser { + spot::location last_loc; public: hoa_stream_parser(const std::string& filename); ~hoa_stream_parser(); diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index e28a374ee..7a5ac2d39 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -26,7 +26,7 @@ set -e expecterr() { cat >$1.exp - ../ltl2tgba -XH $1 2>$1.err && exit 1 + ../../bin/autfilt $1 2>$1.err && exit 1 test $? = 2 cat $1.err diff $1.err $1.exp @@ -100,8 +100,8 @@ Acceptance: 0 t EOF expecterr input <input <input <input <input <