Re: Conflict counterexamples

[Akim Demaille]

Hi Adrian!

> Le 6 juin 2020 à 10:45, Adrian Vogelsgesang <avogelsgesang@tableau.com> a 
> écrit :
> 
> > To me, expecting counterexamples from the CI is comparable to using the CI 
> > to see if a C program compiles.
> I guess I should have phrased this more concisely. I am not planning to abuse 
> our CI to produce counter-examples.
> However, the build scripts we are using for the CI and locally are the same.

Ah, I see.

> To make matters worse, our builds in Bazel are sanboxed/dockerized, also on 
> the local machines, and it’s a pain to get any file out of those containers.

You can add a "cat" in your process.


> > Besides, the HTML output […] Something the terminal cannot give you.
> Wow, I totally missed the HTML output so far. I guess I will use this from 
> now on :)

It's super useful when shoehorning a grammar to fit Bison's restrictions.  I 
also like the graphical rendering the automaton 
(https://www.gnu.org/software/bison/manual/html_node/Graphviz.html).  
Unfortunately that does not scale well the size of grammar.  It might be 
interesting to try to use -Wcounterexample to restrict the automaton to only 
the part involved in the conflict.

I have also been fantasizing about binding this to the runtime traces to have a 
more visual debugger.


> > conflicts and counterexamples are on a completely different level: they are 
> > related to the automaton, its states and transitions. They don't have a 
> > location in the source file.
> Hm… maybe I misunderstood that then… In my mind, counterexamples also had an 
> associated location. To, a conflict has a “conflict root”, i.e. the common 
> rule from which on the derivations start to differ (not sure if there is a 
> better, established term for that).
>  
> E.g., for the if-else example:
> The “exp”-rule is probably part of a larger grammar and “exp” itself is not 
> the grammar’s entry point. Instead, “program” is the grammar’s entry point. 
> Still, the conflict is local to the “exp”, and hence I would mentally attach 
> it to the “exp” node and not to the overall “program”. Yes, “program” is 
> ambiguous, but that’s the case because “exp” is ambiguous, and hence I would 
> attribute the error to “exp” and not at the “program”.
> I would report the error at the line in which “exp” was defined.

Indeed, Vincent's work cleans the counterexamples from details such as the path 
to the conflict, it focuses on the rules truly involved with the conflict, 
exactly as you described.

However, it does not make much sense to point to "the line in which exp was 
defined".  There is single of definition (you can use "exp:" several times) and 
the definition does not even need to be contiguous.  For instance

exp:  exp '+'  term
term: term '*' fact
fact: '0'
exp:  exp
term: fact

is perfectly valid.

So IMHO you would rather point to the lines of the _rules_ involved, not the 
symbol.



> > 2. One way to draw the derivations
> > https://www.lrde.epita.fr/~akim/private/bison/deriv.pdf
> > 3. Another one
> > https://www.lrde.epita.fr/~akim/private/bison/deriv-2.pdf
> 
> Those renderings are really useful. Of all the variants (including the 
> single-line color-coded variant which was so far my favorite), those trees 
> are now my new favorite.
> However, I don’t think they can be rendered in a good way as an ASCII art.

Agreed, so far I don't see a good way to do it.  However, GCC10 has set a new 
standard for ASCII arts in diagnostics 
(https://developers.redhat.com/blog/2020/03/26/static-analysis-in-gcc-10/), so 
there might be a way :)



> I quickly went ahead and sketched what I currently have in my mind. You can 
> find my approach attached to this email (maybe, if the mailing list is 
> friendly to me) or alternatively on 
> https://github.com/vogelsgesang/bison/blob/cd42b5e0146d25db17f213e74b12b0319256f43f/deriv_colored.svg
>  

I like this very much!


Cheers!