From d4f854e5b2d6b10b50dee40831c4e107d76cc254 Mon Sep 17 00:00:00 2001 From: Akim Demaille Date: Thu, 11 Jun 2020 08:24:30 +0200 Subject: [PATCH] cex: also include the counterexamples in the report MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The report is the best place to show the details about counterexamples, since we have the state right under the nose. For instance: State 7 1 exp: exp . "⊕" exp 2 | exp . "+" exp 2 | exp "+" exp . [$end, "+", "⊕"] 3 | exp . "+" exp 3 | exp "+" exp . [$end, "+", "⊕"] "⊕" shift, and go to state 6 $end reduce using rule 2 (exp) $end [reduce using rule 3 (exp)] "+" reduce using rule 2 (exp) "+" [reduce using rule 3 (exp)] "⊕" [reduce using rule 2 (exp)] "⊕" [reduce using rule 3 (exp)] $default reduce using rule 2 (exp) Conflict between rule 2 and token "+" resolved as reduce (%left "+"). Shift/reduce conflict on token "⊕": 2 exp: exp "+" exp . 1 exp: exp . "⊕" exp Example exp "+" exp • "⊕" exp First derivation exp ::=[ exp ::=[ exp "+" exp • ] "⊕" exp ] Example exp "+" exp • "⊕" exp Second derivation exp ::=[ exp "+" exp ::=[ exp • "⊕" exp ] ] Reduce/reduce conflict on tokens $end, "+", "⊕": 2 exp: exp "+" exp . 3 exp: exp "+" exp . Example exp "+" exp • First derivation exp ::=[ exp "+" exp • ] Example exp "+" exp • Second derivation exp ::=[ exp "+" exp • ] Shift/reduce conflict on token "⊕": 3 exp: exp "+" exp . 1 exp: exp . "⊕" exp Example exp "+" exp • "⊕" exp First derivation exp ::=[ exp ::=[ exp "+" exp • ] "⊕" exp ] Example exp "+" exp • "⊕" exp Second derivation exp ::=[ exp "+" exp ::=[ exp • "⊕" exp ] ] * src/conflicts.h, src/conflicts.c (has_conflicts): New. * src/counterexample.h, src/counterexample.c (print_counterexample): Add a `prefix` argument. (counterexample_report_shift_reduce) (counterexample_report_reduce_reduce): Show the items when there's a prefix. * src/state-item.h, src/state-item.c (print_state_item): Add a `prefix` argument. * src/derivation.h, src/derivation.c (derivation_print) (derivation_print_leaves): Add a prefix argument. * src/print.c (print_state): When -Wcex is enabled, show the conflicts. * tests/report.at: Adjust. --- TODO | 20 ++++++++++++++ src/conflicts.c | 8 +++++- src/conflicts.h | 2 ++ src/counterexample.c | 56 ++++++++++++++++++++++++------------- src/counterexample.h | 2 +- src/derivation.c | 14 ++++++---- src/derivation.h | 4 +-- src/lssi.c | 2 +- src/parse-simulation.c | 9 +++--- src/print.c | 11 +++++++- src/state-item.c | 8 +++--- src/state-item.h | 2 +- tests/report.at | 63 ++++++++++++++++++++++++++++++++++++++++-- 13 files changed, 158 insertions(+), 43 deletions(-) diff --git a/TODO b/TODO index 33b1925b..c6f5a094 100644 --- a/TODO +++ b/TODO @@ -1,5 +1,6 @@ * Bison 3.7 ** Cex +*** Improve gnulib Don't do this (counterexample.c): // This is the fastest way to get the tail node from the gl_list API. @@ -12,6 +13,25 @@ list_get_end (gl_list_t list) return res; } +*** Ambiguous rewriting +If the user is stupid enough to have equal rules, then the derivations are +harder to read: + + Reduce/reduce conflict on tokens $end, "+", "⊕": + 2 exp: exp "+" exp . + 3 exp: exp "+" exp . + Example exp "+" exp • + First derivation exp ::=[ exp "+" exp • ] + Example exp "+" exp • + Second derivation exp ::=[ exp "+" exp • ] + +Do we care about this? In color, we use twice the same color here, but we +could try to use the same color for the same rule. + +*** XML reports +Show the counterexamples. This is going to be really hard and/or painful. +Unless we play it dumb (little structure). + ** glr.cc Get rid of global_tokens_and_yystype. diff --git a/src/conflicts.c b/src/conflicts.c index 6c28c56b..f33f1b1b 100644 --- a/src/conflicts.c +++ b/src/conflicts.c @@ -49,6 +49,12 @@ static struct obstack solved_conflicts_xml_obstack; static bitset shift_set; static bitset lookahead_set; +bool +has_conflicts (const state *s) +{ + return conflicts[s->number]; +} + enum conflict_resolution @@ -631,7 +637,7 @@ report_counterexamples (void) { for (state_number sn = 0; sn < nstates; ++sn) if (conflicts[sn]) - counterexample_report_state (states[sn], stderr); + counterexample_report_state (states[sn], stderr, ""); } /*------------------------------------------------. diff --git a/src/conflicts.h b/src/conflicts.h index 5b26efde..d4e679f0 100644 --- a/src/conflicts.h +++ b/src/conflicts.h @@ -41,6 +41,8 @@ int conflicts_total_count (void); void conflicts_output (FILE *out); void conflicts_free (void); +bool has_conflicts (const state *s); + /* Were there conflicts? */ extern int expected_sr_conflicts; extern int expected_rr_conflicts; diff --git a/src/counterexample.c b/src/counterexample.c index 283a484c..7e952828 100644 --- a/src/counterexample.c +++ b/src/counterexample.c @@ -100,17 +100,21 @@ free_counterexample (counterexample *cex) } static void -print_counterexample (counterexample *cex, FILE *out) +print_counterexample (counterexample *cex, FILE *out, const char *prefix) { - fprintf (out, " %-20s ", cex->unifying ? _("Example") : _("First example")); - derivation_print_leaves (cex->d1, out); - fprintf (out, " %-20s ", _("First derivation")); - derivation_print (cex->d1, out); + fprintf (out, " %s%-20s ", + prefix, cex->unifying ? _("Example") : _("First example")); + derivation_print_leaves (cex->d1, out, prefix); + fprintf (out, " %s%-20s ", + prefix, _("First derivation")); + derivation_print (cex->d1, out, prefix); - fprintf (out, " %-20s ", cex->unifying ? _("Example") : _("Second example")); - derivation_print_leaves (cex->d2, out); - fprintf (out, " %-20s ", _("Second derivation")); - derivation_print (cex->d2, out); + fprintf (out, " %s%-20s ", + prefix, cex->unifying ? _("Example") : _("Second example")); + derivation_print_leaves (cex->d2, out, prefix); + fprintf (out, " %s%-20s ", + prefix, _("Second derivation")); + derivation_print (cex->d2, out, prefix); fputc ('\n', out); } @@ -469,7 +473,7 @@ nonunifying_shift_path (gl_list_t reduce_path, state_item *shift_conflict) for (gl_list_iterator_t it = gl_list_iterator (result); state_item_list_next (&it, &sip); ) - print_state_item (sip, stderr); + print_state_item (sip, stderr, ""); } return result; } @@ -1175,7 +1179,7 @@ counterexample_free (void) static void counterexample_report (state_item_number itm1, state_item_number itm2, symbol_number next_sym, bool shift_reduce, - FILE *out) + FILE *out, const char *prefix) { // Compute the shortest lookahead-sensitive path and associated sets of // parser states. @@ -1204,23 +1208,32 @@ counterexample_report (state_item_number itm1, state_item_number itm2, : example_from_path (shift_reduce, itm2, shortest_path, next_sym); gl_list_free (shortest_path); - print_counterexample (cex, out); + print_counterexample (cex, out, prefix); free_counterexample (cex); } static void counterexample_report_shift_reduce (state_item_number itm1, state_item_number itm2, - symbol_number next_sym, FILE *out) + symbol_number next_sym, + FILE *out, const char *prefix) { + fputs (prefix, out); fprintf (out, _("Shift/reduce conflict on token %s:\n"), symbols[next_sym]->tag); - counterexample_report (itm1, itm2, next_sym, true, out); + if (*prefix) + { + print_state_item (&state_items[itm1], out, prefix); + print_state_item (&state_items[itm2], out, prefix); + } + counterexample_report (itm1, itm2, next_sym, true, out, prefix); } static void counterexample_report_reduce_reduce (state_item_number itm1, state_item_number itm2, - bitset conflict_syms, FILE *out) + bitset conflict_syms, + FILE *out, const char *prefix) { { + fputs (prefix, out); fputs (ngettext ("Reduce/reduce conflict on token", "Reduce/reduce conflict on tokens", bitset_count (conflict_syms)), out); @@ -1234,7 +1247,12 @@ counterexample_report_reduce_reduce (state_item_number itm1, state_item_number i } fputs (_(":\n"), out); } - counterexample_report (itm1, itm2, bitset_first (conflict_syms), false, out); + if (*prefix) + { + print_state_item (&state_items[itm1], out, prefix); + print_state_item (&state_items[itm2], out, prefix); + } + counterexample_report (itm1, itm2, bitset_first (conflict_syms), false, out, prefix); } static state_item_number @@ -1248,7 +1266,7 @@ find_state_item_number (const rule *r, state_number sn) } void -counterexample_report_state (const state *s, FILE *out) +counterexample_report_state (const state *s, FILE *out, const char *prefix) { const state_number sn = s->number; const reductions *reds = s->reductions; @@ -1265,7 +1283,7 @@ counterexample_report_state (const state *s, FILE *out) if (item_number_is_symbol_number (conf) && bitset_test (reds->lookahead_tokens[i], conf)) { - counterexample_report_shift_reduce (c1, j, conf, out); + counterexample_report_shift_reduce (c1, j, conf, out, prefix); break; } } @@ -1287,7 +1305,7 @@ counterexample_report_state (const state *s, FILE *out) const rule *r = item_rule (si->item); if (r == r2) { - counterexample_report_reduce_reduce (c1, k, conf, out); + counterexample_report_reduce_reduce (c1, k, conf, out, prefix); break; } } diff --git a/src/counterexample.h b/src/counterexample.h index 0dbf81e3..c251d319 100644 --- a/src/counterexample.h +++ b/src/counterexample.h @@ -25,6 +25,6 @@ void counterexample_init (void); void counterexample_free (void); -void counterexample_report_state (const state *s, FILE *out); +void counterexample_report_state (const state *s, FILE *out, const char *prefix); #endif /* COUNTEREXAMPLE_H */ diff --git a/src/derivation.c b/src/derivation.c index cc5145e5..14a8d852 100644 --- a/src/derivation.c +++ b/src/derivation.c @@ -180,18 +180,20 @@ derivation_print_impl (const derivation *deriv, FILE *f, } void -derivation_print (const derivation *deriv, FILE *f) +derivation_print (const derivation *deriv, FILE *out, const char *prefix) { int counter = 0; - derivation_print_impl (deriv, f, false, &counter); - fputc ('\n', f); + fputs (prefix, out); + derivation_print_impl (deriv, out, false, &counter); + fputc ('\n', out); } void -derivation_print_leaves (const derivation *deriv, FILE *f) +derivation_print_leaves (const derivation *deriv, FILE *out, const char *prefix) { int counter = 0; - derivation_print_impl (deriv, f, true, &counter); - fputc ('\n', f); + fputs (prefix, out); + derivation_print_impl (deriv, out, true, &counter); + fputc ('\n', out); } diff --git a/src/derivation.h b/src/derivation.h index 78714047..58852569 100644 --- a/src/derivation.h +++ b/src/derivation.h @@ -61,8 +61,8 @@ static inline derivation *derivation_new_leaf (symbol_number sym) return derivation_new (sym, NULL); } size_t derivation_size (const derivation *deriv); -void derivation_print (const derivation *deriv, FILE *f); -void derivation_print_leaves (const derivation *deriv, FILE *f); +void derivation_print (const derivation *deriv, FILE *out, const char *prefix); +void derivation_print_leaves (const derivation *deriv, FILE *out, const char *prefix); void derivation_free (derivation *deriv); void derivation_retain (derivation *deriv); diff --git a/src/lssi.c b/src/lssi.c index 6bd09551..17ff27dd 100644 --- a/src/lssi.c +++ b/src/lssi.c @@ -254,7 +254,7 @@ shortest_path_from_start (state_item_number target, symbol_number next_sym) gl_list_iterator_t it = gl_list_iterator (res); const void *sip; while (gl_list_iterator_next (&it, &sip, NULL)) - print_state_item ((state_item *) sip, stdout); + print_state_item ((state_item *) sip, stdout, ""); } return res; } diff --git a/src/parse-simulation.c b/src/parse-simulation.c index 098e4e70..615dbb2b 100644 --- a/src/parse-simulation.c +++ b/src/parse-simulation.c @@ -19,13 +19,14 @@ #include +#include "parse-simulation.h" + #include #include #include #include "lssi.h" #include "nullable.h" -#include "parse-simulation.h" typedef struct parse_state { @@ -595,9 +596,9 @@ print_parse_state (parse_state *ps) FILE *out = stderr; fprintf (out, "(size %zu depth %d rc %d)\n", ps->state_items.total_size, ps->depth, ps->reference_count); - print_state_item (ps->state_items.head_elt, out); - print_state_item (ps->state_items.tail_elt, out); + print_state_item (ps->state_items.head_elt, out, ""); + print_state_item (ps->state_items.tail_elt, out, ""); if (ps->derivs.total_size > 0) - derivation_print (ps->derivs.head_elt, out); + derivation_print (ps->derivs.head_elt, out, ""); putc ('\n', out); } diff --git a/src/print.c b/src/print.c index 4d679e82..e0940f3b 100644 --- a/src/print.c +++ b/src/print.c @@ -19,20 +19,24 @@ along with this program. If not, see . */ #include + +#include "print.h" + #include "system.h" #include #include #include "closure.h" +#include "complain.h" #include "conflicts.h" +#include "counterexample.h" #include "files.h" #include "getargs.h" #include "gram.h" #include "lalr.h" #include "lr0.h" #include "muscle-tab.h" -#include "print.h" #include "reader.h" #include "reduce.h" #include "state.h" @@ -352,6 +356,11 @@ print_state (FILE *out, const state *s) fputc ('\n', out); fputs (s->solved_conflicts, out); } + if (warning_is_enabled (Wcounterexamples) && has_conflicts (s)) + { + fputc ('\n', out); + counterexample_report_state (s, out, " "); + } } /*-----------------------------------------. diff --git a/src/state-item.c b/src/state-item.c index 21b276d3..c3931d6c 100644 --- a/src/state-item.c +++ b/src/state-item.c @@ -477,9 +477,9 @@ prune_disabled_paths (void) } void -print_state_item (const state_item *si, FILE *out) +print_state_item (const state_item *si, FILE *out, const char *prefix) { - fprintf (out, "%d:", si->state->number); + fputs (prefix, out); item_print (si->item, NULL, out); putc ('\n', out); } @@ -508,7 +508,7 @@ state_items_report (void) if (si->trans >= 0) { fputs (" -> ", stdout); - print_state_item (state_items + si->trans, stdout); + print_state_item (state_items + si->trans, stdout, ""); } bitset sets[2] = { si->prods, si->revs }; @@ -523,7 +523,7 @@ state_items_report (void) BITSET_FOR_EACH (biter, b, sin, 0) { fputs (txt[seti], stdout); - print_state_item (state_items + sin, stdout); + print_state_item (state_items + sin, stdout, ""); } } } diff --git a/src/state-item.h b/src/state-item.h index 63841a2a..8df79feb 100644 --- a/src/state-item.h +++ b/src/state-item.h @@ -87,7 +87,7 @@ state_item_index_lookup (state_number s, state_item_number off) } void state_items_init (void); -void print_state_item (const state_item *si, FILE *out); +void print_state_item (const state_item *si, FILE *out, const char *prefix); void state_items_free (void); bool production_allowed (const state_item *si, const state_item *next); diff --git a/tests/report.at b/tests/report.at index 21708070..67f3849c 100644 --- a/tests/report.at +++ b/tests/report.at @@ -1148,7 +1148,7 @@ AT_CLEANUP AT_SETUP([Reports with conflicts]) -AT_KEYWORDS([report]) +AT_KEYWORDS([cex report]) # We need UTF-8 support for correct screen-width computation of UTF-8 # characters. Skip the test if not available. @@ -1167,10 +1167,33 @@ exp | "Ñùṃéℝô" ]]) -AT_CHECK([LC_ALL="$locale" $5 bison -fno-caret -o input.cc -rall --graph=input.gv --xml input.y], [], [], +AT_CHECK([LC_ALL="$locale" bison -fno-caret -o input.cc -rall -Wcex --graph=input.gv --xml input.y], [], [], [[input.y: warning: 3 shift/reduce conflicts [-Wconflicts-sr] input.y: warning: 3 reduce/reduce conflicts [-Wconflicts-rr] -input.y: warning: rerun with option '-Wcounterexamples' to generate conflict counterexamples [-Wother] +Shift/reduce conflict on token "⊕": + Example exp "+" exp • "⊕" exp + First derivation exp ::=[ exp ::=[ exp "+" exp • ] "⊕" exp ] + Example exp "+" exp • "⊕" exp + Second derivation exp ::=[ exp "+" exp ::=[ exp • "⊕" exp ] ] + +Reduce/reduce conflict on tokens $end, "+", "⊕": + Example exp "+" exp • + First derivation exp ::=[ exp "+" exp • ] + Example exp "+" exp • + Second derivation exp ::=[ exp "+" exp • ] + +Shift/reduce conflict on token "⊕": + Example exp "+" exp • "⊕" exp + First derivation exp ::=[ exp ::=[ exp "+" exp • ] "⊕" exp ] + Example exp "+" exp • "⊕" exp + Second derivation exp ::=[ exp "+" exp ::=[ exp • "⊕" exp ] ] + +Shift/reduce conflict on token "⊕": + Example exp "⊕" exp • "⊕" exp + First derivation exp ::=[ exp ::=[ exp "⊕" exp • ] "⊕" exp ] + Example exp "⊕" exp • "⊕" exp + Second derivation exp ::=[ exp "⊕" exp ::=[ exp • "⊕" exp ] ] + input.y:6.3-13: warning: rule useless in parser due to conflicts [-Wother] ]]) @@ -1314,6 +1337,31 @@ State 7 Conflict between rule 2 and token "+" resolved as reduce (%left "+"). + Shift/reduce conflict on token "⊕": + 2 exp: exp "+" exp . + 1 exp: exp . "⊕" exp + Example exp "+" exp • "⊕" exp + First derivation exp ::=[ exp ::=[ exp "+" exp • ] "⊕" exp ] + Example exp "+" exp • "⊕" exp + Second derivation exp ::=[ exp "+" exp ::=[ exp • "⊕" exp ] ] + + Reduce/reduce conflict on tokens $end, "+", "⊕": + 2 exp: exp "+" exp . + 3 exp: exp "+" exp . + Example exp "+" exp • + First derivation exp ::=[ exp "+" exp • ] + Example exp "+" exp • + Second derivation exp ::=[ exp "+" exp • ] + + Shift/reduce conflict on token "⊕": + 3 exp: exp "+" exp . + 1 exp: exp . "⊕" exp + Example exp "+" exp • "⊕" exp + First derivation exp ::=[ exp ::=[ exp "+" exp • ] "⊕" exp ] + Example exp "+" exp • "⊕" exp + Second derivation exp ::=[ exp "+" exp ::=[ exp • "⊕" exp ] ] + + State 8 @@ -1328,6 +1376,15 @@ State 8 "+" [reduce using rule 1 (exp)] "⊕" [reduce using rule 1 (exp)] $default reduce using rule 1 (exp) + + Shift/reduce conflict on token "⊕": + 1 exp: exp "⊕" exp . + 1 exp: exp . "⊕" exp + Example exp "⊕" exp • "⊕" exp + First derivation exp ::=[ exp ::=[ exp "⊕" exp • ] "⊕" exp ] + Example exp "⊕" exp • "⊕" exp + Second derivation exp ::=[ exp "⊕" exp ::=[ exp • "⊕" exp ] ] + ]])