Hi all, Counterexample generation is a feature intended to help debugging conflicts in amibuous grammars. It was initially developed in CUP by Andrew Myers and Chinawat Isradisaikul. Their paper on it can be found here: https://www.cs.cornell.edu/andru/papers/cupex/cupex.pdf
The gist of it is for each conflict, a (unifying) counterexample is generated like so: Shift-Reduce Conflict: 6: 1 e: e '+' e . 6: 1 e: e . '+' e On Symbol: '+' Example e '+' e • '+' e First derivation e ::=[ e ::=[ e '+' e • ] '+' e ] Second derivation e ::=[ e '+' e ::=[ e • '+' e ] ] Occasionally, such an example is hard or impossible to find. For example, if a grammar is lr2, the issue is not ambiguity, but a lack of looking far enough ahead. In these cases, two (non-unifying) examples are printed such that they both cause the parser to traverse the same states. Shift-Reduce Conflict: 2: 7 b: B . 2: 9 bc: B . C On Symbol: C First Example B • C D $end First derivation x ::=[ b ::=[ B • ] cd ::=[ C D ] ] Second Example B • C $end Second derivation x ::=[ bc ::=[ B • C ] ] The way this works is when counterexample generation is enabled, it generates a dag of state item pairs (state-items) where each edge is a shift or production. In brief, we start two "parser-simulations" at the conflict state, and simulate shifts and gotos on the same symbols for both simulations. Once both complete a reduction for both on the same symbol in the same state, a counterexample has been found. If nothing is found within the time limit, a non-unifying counterexample is generated through a graph bfs much faster than the original search. There's also a cumulative time limit on all counterexample generation, and I should probably make these cli options. I'd like some feedback as to where I should put these warnings. Right now they're emitted under -Wcounterexample, but I think some might want it in a file instead. Also, I think it might be a good idea to replace/amend the shift-reduce and reduce-reduce conflict counts with the print out of the two rules that are conflicting like above. However, it's important to note that counterexample generation iterates conflicts slightly differently, so the numbers won't be the same. As an aside, I've put off updating the results of my test suite until this is decided. I really tried to keep this brief and more focused on the user-facing changes. For more information you should check out the paper linked above or my comments in the new header files. I know this change is enormous so I'll try to be responsive in answering questions and addressing issues. There's also a version of this on github here that is probably more convenient to play with: https://github.com/akimd/bison/pull/15 Thanks, Vincent Imbimbo Vincent Imbimbo (5): State-item pair graph generation Parse simulator Counterexample search counterexample generation integration counterexample test suite src/complain.c | 2 + src/complain.h | 2 + src/conflicts.c | 67 +++ src/counterexample.c | 1194 +++++++++++++++++++++++++++++++++++++++ src/counterexample.h | 35 ++ src/derivation.c | 107 ++++ src/derivation.h | 47 ++ src/getargs.c | 2 + src/getargs.h | 1 + src/local.mk | 10 + src/lssi.c | 367 ++++++++++++ src/lssi.h | 56 ++ src/main.c | 3 + src/parse-simulation.c | 554 ++++++++++++++++++ src/parse-simulation.h | 131 +++++ src/state-item.c | 563 ++++++++++++++++++ src/state-item.h | 100 ++++ tests/counterexample.at | 357 ++++++++++++ tests/testsuite.at | 3 + 19 files changed, 3601 insertions(+) create mode 100644 src/counterexample.c create mode 100644 src/counterexample.h create mode 100644 src/derivation.c create mode 100644 src/derivation.h create mode 100644 src/lssi.c create mode 100644 src/lssi.h create mode 100644 src/parse-simulation.c create mode 100644 src/parse-simulation.h create mode 100644 src/state-item.c create mode 100644 src/state-item.h create mode 100644 tests/counterexample.at -- 2.20.1 (Apple Git-117)
