Future/bison
1
0
Fork 0
mirror of https://git.savannah.gnu.org/git/bison.git synced 2026-03-10 12:53:03 +00:00
Code Issues Packages Projects Releases Wiki Activity

cex: also include the counterexamples in the report

Browse Source 
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.
This commit is contained in:
Akim Demaille
2020-06-11 08:24:30 +02:00
parent 35c0fe6789
commit d4f854e5b2
13 changed files with 158 additions and 43 deletions
Download Patch File Download Diff File Expand all files Collapse all files

20
TODO
View File

@@ -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.

8
src/conflicts.c
View File

@@ -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, "");
}
/*------------------------------------------------.

2
src/conflicts.h
View File

@@ -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;

56
src/counterexample.c
View File

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

2
src/counterexample.h
View File

@@ -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 */

14
src/derivation.c
View File

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

4
src/derivation.h
View File

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

2
src/lssi.c
View File

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

9
src/parse-simulation.c
View File

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

11
src/print.c
View File

@@ -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, " ");
}
}
/*-----------------------------------------.

8
src/state-item.c
View File

@@ -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, "");
}
}
}

2
src/state-item.h
View File

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

63
tests/report.at
View File

@@ -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 ] ]
]])