[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PATCH 6/8] cex: also include the counterexamples in the report
From: |
Akim Demaille |
Subject: |
[PATCH 6/8] cex: also include the counterexamples in the report |
Date: |
Sun, 14 Jun 2020 10:25:00 +0200 |
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 | 58 ++++++++++++++++++++++++--------------
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, 159 insertions(+), 44 deletions(-)
diff --git a/TODO b/TODO
index 5d440169..5c9ea504 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).
+
** Bistromathic
- Hitting tab on a line with a syntax error is ugly
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, " %-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") : _("First example"));
+ derivation_print_leaves (cex->d1, out, prefix);
+ fprintf (out, " %s%-20s ",
+ prefix, _("First derivation"));
+ derivation_print (cex->d1, out, prefix);
+
+ 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 <config.h>
+#include "parse-simulation.h"
+
#include <gl_linked_list.h>
#include <gl_xlist.h>
#include <stdlib.h>
#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 <http://www.gnu.org/licenses/>. */
#include <config.h>
+
+#include "print.h"
+
#include "system.h"
#include <bitset.h>
#include <mbswidth.h>
#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 ] ]
+
]])
--
2.27.0
- [PATCH 0/8] cex: show counterexamples in the reports, Akim Demaille, 2020/06/14
- [PATCH 1/8] style: more uses of const, Akim Demaille, 2020/06/14
- [PATCH 2/8] cex: add an argument to the reporting functions to specify the stream, Akim Demaille, 2020/06/14
- [PATCH 3/8] cex: make sure traces go to stderr, Akim Demaille, 2020/06/14
- [PATCH 4/8] cex: don't report the items, Akim Demaille, 2020/06/14
- [PATCH 5/8] cex: indent the diagnostics to highlight the structure, Akim Demaille, 2020/06/14
- [PATCH 6/8] cex: also include the counterexamples in the report,
Akim Demaille <=
- [PATCH 7/8] cex: also include in the report on --report=counterexamples, Akim Demaille, 2020/06/14
- [PATCH 8/8] cex: factor the definition of "•", Akim Demaille, 2020/06/14
- Re: [PATCH 0/8] cex: show counterexamples in the reports, Akim Demaille, 2020/06/16