[PATCH 6/8] cex: also include the counterexamples in the report

[Akim Demaille]

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