[PATCH 0/5] Conflict Counterexample Generation

[Vincent Imbimbo]

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)