RFC: Conflict counterexamples

Hi all,

Vincent Imbimbo recently contributed a complete system to generate counterexamples when there are conflicts.  It works well, and will be the foremost feature of Bison 3.7.

$ bison -Wcounterexample foo.y
Shift-Reduce Conflict:
7:    1 exp: "if" exp "then" exp .
7:    2 exp: "if" exp "then" exp . "else" exp
On Symbol: "else"
Example  "if"  exp  "then"  "if"  exp  "then"  exp  •  "else"  exp
First  derivation  exp ::=[ "if"  exp  "then"  exp ::=[ "if"  exp  "then"  exp  • ]  "else"  exp ]
Second derivation  exp ::=[ "if"  exp  "then"  exp ::=[ "if"  exp  "then"  exp  •  "else"  exp ] ]
foo.y: avertissement: 1 conflit par décalage/réduction [-Wconflicts-sr]


However, there is a number of design decisions to make.


1. Where

We need to decide where the counterexamples should appear.  Vincent has added a -Wcounterexample flag, and the diagnostics are then on stderr.

Historically if you wanted to understand your conflicts, you had to read the *.output file; on this regard, I believe it makes more sense to issue this additional information into the *.output file too.  However, one could also claim that now, precisely thanks to -Wcounterexample, in many cases you no longer need to go to your *.output, the diagnostic may suffice.

One answer, of course, could be that it should be the user's choice: --report=counterexample adds this information in the report, and -Wcounterexample does that for the diagnostics.


2. When

Vincent had originally included -Wcounterexample into -Wall (I think that was more by accident than by design).  I removed it from -Wall, because looking for counterexamples can be very costly (after all, grammar ambiguity is undecidable...).  There's a timeout mechanism that guarantees that bison terminates, but still, running these computations when you don't actually care about them (i.e., when you accepted your conflicts and use the -Wall in your CI) is a pure waste of time and resources.

If -Wcounterexample is not part of -Wall, then people should be told of its existence, since most of them don't read the manual or/and NEWS.  I think we should issue a message such as:

$ bison -Wall foo.y
foo.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
foo.y: warning: counterexamples can be generated.  Rerun with option '-Wcounterexample'. [-Wother]


3. How

There might be other ways to display the diagnostics.  For instance, I have been playing with colors (if you're reading the mail in text, that won't work here):

$ bison -Wcounterexample foo.y
Shift-Reduce Conflict:
7:    1 exp: "if" exp "then" exp .
7:    2 exp: "if" exp "then" exp . "else" exp
On Symbol: "else"
Example  "if"  exp  "then"  "if"  exp  "then"  exp  •  "else"  exp
First  derivation  exp ::=[ "if"  exp  "then"  exp ::=[ "if"  exp  "then"  exp  • ]  "else"  exp ]
"if"  exp  "then"  "if"  exp  "then"  exp  •  "else"  exp

Second derivation  exp ::=[ "if"  exp  "then"  exp ::=[ "if"  exp  "then"  exp  •  "else"  exp ] ]
"if"  exp  "then"  "if"  exp  "then"  exp  •  "else"  exp

foo.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]

But there are certainly other ways we could display the derivations, say:

First  derivation
  exp
  |
  +- "if"  exp  "then" exp "else"  exp
                       |
                       +- "if"  exp  "then"  exp  •

Second derivation
  exp
  |
  +- "if"  exp  "then"  exp
                        |
                        +- "if"  exp  "then"  exp  •  "else"  exp


or

First  derivation
  [exp]
  => "if"  exp  "then" [exp] "else"  exp
  => "if"  exp  "then" "if" exp "then"  exp •  "else"  exp

Second derivation
  [exp]
  => "if"  exp  "then" [exp]
  => "if"  exp  "then" "if" exp "then"  exp  •  "else"  exp

We could also use graphviz to generate images.  I don't think I can attach images here, but if you have graphviz/dot, I attach both the result and the dot sources for two different ways to render the counterexamples.

Opinions, suggestions, comments would be most welcome.  Cheers!