# Exercising Bison on counterexamples.                         -*- Autotest -*-

# Copyright (C) 2020 Free Software Foundation, Inc.

# This program is free software: you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, either version 3 of the License, or
# (at your option) any later version.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program.  If not, see <http://www.gnu.org/licenses/>.

AT_BANNER([[Counterexamples.]])

m4_define([AT_BISON_CHECK_CEX],
[AT_DATA([experr], [$4])
sed -e ['s/time limit exceeded: [0-9][.0-9]*/time limit exceeded: XXX/g'] \
  experr >expout
AT_BISON_CHECK([-Wcounterexample $1], [$2], [$3], [stderr])
AT_CHECK([[sed -e 's/time limit exceeded: [0-9][.0-9]*/time limit exceeded: XXX/g' stderr]],
         [], [expout])
])

## --------------------- ##
## Simple Unifying S/R.  ##
## --------------------- ##

AT_SETUP([Unifying S/R])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token A B C
%%
s: a x | y c;
a: A;
c: C;
x: B | B C;
y: A | A B;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
1:    3 a: A .
1:    8 y: A . B
On Symbol: B
Example  A  •  B  C
First  derivation  s ::=[ a ::=[ A  • ]  x ::=[ B  C ] ]
Second derivation  s ::=[ y ::=[ A  •  B ]  c ::=[ C ] ]

input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
input.y:4.4: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## ------------------- ##
## Deep Unifying S/R.  ##
## ------------------- ##

AT_SETUP([Deep Unifying S/R])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token A B C
%%
s: ac | a bc;
ac: A ac C | b;
b: B | B b;
a: A | A a;
bc: B bc C | B C;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
1:    7 a: A .
1:    5 b: . B
On Symbol: B
Example  A  •  B  C
First  derivation  s ::=[ a ::=[ A  • ]  bc ::=[ B  C ] ]
Second derivation  s ::=[ ac ::=[ A  ac ::=[ b ::=[ •  B ] ]  C ] ]

input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
input.y:6.4: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## ------------------------------------ ##
## S/R Conflict with Nullable Symbols.  ##
## ------------------------------------ ##

AT_SETUP([S/R Conflict with Nullable Symbols])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token A B X Y
%%
s: ax by | A xby;
ax: A x;
x: %empty | X x;
by: B y;
y: %empty | Y y;
xby: B | X xby Y;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
1:    4 x: . %empty
1:    9 xby: . B
On Symbol: B
Example  A  •  B  y
First  derivation  s ::=[ ax ::=[ A  x ::=[ • ] ]  by ::=[ B  y ] ]
Second derivation  s ::=[ A  xby ::=[ •  B ] ]

Shift-Reduce Conflict:
5:    4 x: . %empty
5:    9 xby: . B
On Symbol: B
First  Example A  X  •  B  y  $end
First  derivation  $accept ::=[ s ::=[ ax ::=[ A  x ::=[ X  x ::=[ • ] ] ]  by ::=[ B  y ] ]  $end ]
Second Example A  X  •  B  Y  $end
Second derivation  $accept ::=[ s ::=[ A  xby ::=[ X  xby ::=[ •  B ]  Y ] ]  $end ]

input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
input.y:5.4-9: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## ---------------------------- ##
## Non-unifying Ambiguous S/R.  ##
## ---------------------------- ##

AT_SETUP([Non-unifying Ambiguous S/R])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token A B C D E
%%
g: s | x;
s: A x E | A x D E;
x: b cd | bc;
b: B;
cd: C D;
bc: B C;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
2:    7 b: B .
2:    9 bc: B . C
On Symbol: C
First  Example B  •  C  D  $end
First  derivation  $accept ::=[ g ::=[ x ::=[ b ::=[ B  • ]  cd ::=[ C  D ] ] ]  $end ]
Second Example B  •  C  $end
Second derivation  $accept ::=[ g ::=[ x ::=[ bc ::=[ B  •  C ] ] ]  $end ]

input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
input.y:6.4: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## ------------------------------ ##
## Non-unifying Unambiguous S/R.  ##
## ------------------------------ ##

AT_SETUP([Non-unifying Unambiguous S/R])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token A B
%%
s: t | s t;
t: x | y;
x: A;
y: A A B;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
1:    5 x: A .
1:    6 y: A . A B
On Symbol: A
First  Example A  •  A  $end
First  derivation  $accept ::=[ s ::=[ s ::=[ t ::=[ x ::=[ A  • ] ] ]  t ::=[ x ::=[ A ] ] ]  $end ]
Second Example A  •  A  B  $end
Second derivation  $accept ::=[ s ::=[ t ::=[ y ::=[ A  •  A  B ] ] ]  $end ]

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

AT_CLEANUP

## ----------------------- ##
## S/R after first token.  ##
## ----------------------- ##

AT_SETUP([S/R after first token])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token A B X Y
%%
a: r t | s;
r: b;
b: B;
t: A xx | A x xy;
s: b A xx y;
x: X;
xx: X X;
xy: X Y;
y: Y;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
4:    3 r: b .
4:    7 s: b . A xx y
On Symbol: A
Example  b  •  A  X  X  Y
First  derivation  a ::=[ r ::=[ b  • ]  t ::=[ A  x ::=[ X ]  xy ::=[ X  Y ] ] ]
Second derivation  a ::=[ s ::=[ b  •  xx ::=[ A  X  X ]  y ::=[ Y ] ] ]

Shift-Reduce Conflict:
10:    8 x: X .
10:    9 xx: X . X
On Symbol: X
First  Example X  •  X  xy
First  derivation  a ::=[ x ::=[ X  • ]  t ::=[ X  xy ] ]
Second Example A  X  •  X
Second derivation  a ::=[ t ::=[ A  xx ::=[ X  •  X ] ] ]

input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
input.y:4.4: warning: rule useless in parser due to conflicts [-Wother]
input.y:8.4: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## ----------------------------- ##
## Unifying R/R counterexample.  ##
## ----------------------------- ##

AT_SETUP([Unifying R/R counterexample])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token A
%%
a : A b ;
b : A | b;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Reduce-Reduce Conflict:
4:    1 a: A b .
4:    3 b: b .
On Symbols: $end
Example  A  b  •
First  derivation  a ::=[ A  b  • ]
Second derivation  a ::=[ A  b ::=[ b  • ] ]

input.y: warning: 1 reduce/reduce conflict [-Wconflicts-rr]
input.y:4.9: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## ------------------------------- ##
## Non-unifying R/R lr1 conflict.  ##
## ------------------------------- ##

AT_SETUP([Non-unifying R/R lr1 conflict])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token A B C D
%%
s: a A | B a C | b C | B b A;
a: D;
b: D;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Reduce-Reduce Conflict:
2:    5 a: D .
2:    6 b: D .
On Symbols: A, C
First  Example D  •  A  $end
First  derivation  $accept ::=[ s ::=[ a ::=[ D  • ]  A ]  $end ]
Second Example B  D  •  A  $end
Second derivation  $accept ::=[ s ::=[ B  b ::=[ D  • ]  A ]  $end ]

input.y: warning: 2 reduce/reduce conflicts [-Wconflicts-rr]
input.y:5.4: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## ------------------------------- ##
## Non-unifying R/R lr2 conflict.  ##
## ------------------------------- ##

AT_SETUP([Non-unifying R/R lr2 conflict])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token H J K X
%%
s: a J;
a: H i;
i: X | i J K;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
5:    2 a: H i .
5:    4 i: i . J K
On Symbol: J
time limit exceeded: 6.000000
First  Example H  i  •  J  $end
First  derivation  $accept ::=[ s ::=[ a ::=[ H  i  • ]  J ]  $end ]
Second Example H  i  •  J  K  $end
Second derivation  $accept ::=[ a ::=[ H  i ::=[ i  •  J  K ] ]  $end ]

input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
input.y:4.4-6: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## -------------------- ##
## Cex Search Prepend.  ##
## -------------------- ##

# Tests prepend steps in uniying counterexample
# graph search

AT_SETUP([Cex Search Prepend])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token N A B C D
%%
s: n | n C;
n: N n D | N n C | N a B | N b;
a: A;
b: A B C | A B D;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
4:    7 a: A .
4:    8 b: A . B C
On Symbol: B
Example  N  A  •  B  C
First  derivation  s ::=[ n ::=[ N  a ::=[ A  • ]  B ]  C ]
Second derivation  s ::=[ n ::=[ N  b ::=[ A  •  B  C ] ] ]

input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
input.y:5.4: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## ------------------- ##
## R/R cex with prec.  ##
## ------------------- ##

# Tests that counterexamples containing rules using
# precedence/associativity directives work.

AT_SETUP([R/R cex with prec])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%left b
%right c
%%
S: B C | C B;
A : B  | C  | %empty;
B : A b A;
C : A c A;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Reduce-Reduce Conflict:
3:    3 A: B .
3:    5 A: . %empty
On Symbols: b, c
Example  B  •  b  A  A  c  A
First  derivation  S ::=[ B ::=[ A ::=[ B  • ]  b  A ]  C ::=[ A  c  A ] ]
Second derivation  S ::=[ B  C ::=[ A ::=[ B ::=[ A ::=[ • ]  b  A ] ]  c  A ] ]

Reduce-Reduce Conflict:
4:    4 A: C .
4:    5 A: . %empty
On Symbols: b, c
Example  C  •  c  A  A  b  A
First  derivation  S ::=[ C ::=[ A ::=[ C  • ]  c  A ]  B ::=[ A  b  A ] ]
Second derivation  S ::=[ C  B ::=[ A ::=[ C ::=[ A ::=[ • ]  c  A ] ]  b  A ] ]

input.y: warning: 4 reduce/reduce conflicts [-Wconflicts-rr]
]])

AT_CLEANUP

## ------------------- ##
## Null nonterminals.  ##
## ------------------- ##

AT_SETUP([Null nonterminals])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token A
%%
a : b d | c d ;
b : ;
c : ;
d : a | c A | d;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Reduce-Reduce Conflict:
0:    3 b: . %empty
0:    4 c: . %empty
On Symbols: A
First  Example •  c  A  A  $end
First  derivation  $accept ::=[ a ::=[ b ::=[ • ]  d ::=[ c  A  A ] ]  $end ]
Second Example •  c  A  A  $end
Second derivation  $accept ::=[ a ::=[ c ::=[ • ]  d ::=[ c  A  A ] ]  $end ]

Reduce-Reduce Conflict:
2:    3 b: . %empty
2:    4 c: . %empty
On Symbols: A
time limit exceeded: 6.000000
First  Example b  •  c  A  A  $end
First  derivation  $accept ::=[ a ::=[ b  d ::=[ a ::=[ b ::=[ • ]  d ::=[ c  A  A ] ] ] ]  $end ]
Second Example b  •  A  $end
Second derivation  $accept ::=[ a ::=[ b  d ::=[ c ::=[ • ]  A ] ]  $end ]

Reduce-Reduce Conflict:
3:    3 b: . %empty
3:    4 c: . %empty
On Symbols: A
time limit exceeded: 6.000000
First  Example c  •  c  A  A  $end
First  derivation  $accept ::=[ a ::=[ c  d ::=[ a ::=[ b ::=[ • ]  d ::=[ c  A  A ] ] ] ]  $end ]
Second Example c  •  A  $end
Second derivation  $accept ::=[ a ::=[ c  d ::=[ c ::=[ • ]  A ] ]  $end ]

Shift-Reduce Conflict:
6:    3 b: . %empty
6:    6 d: c . A
On Symbol: A
time limit exceeded: 6.000000
First  Example b  c  •  c  A  A  $end
First  derivation  $accept ::=[ a ::=[ b  d ::=[ a ::=[ c  d ::=[ a ::=[ b ::=[ • ]  d ::=[ c  A  A ] ] ] ] ] ]  $end ]
Second Example b  c  •  A
Second derivation  a ::=[ b  d ::=[ c  •  A ] ]

Reduce-Reduce Conflict:
6:    3 b: . %empty
6:    4 c: . %empty
On Symbols: A
First  Example b  c  •  c  A  A  $end
First  derivation  $accept ::=[ a ::=[ b  d ::=[ a ::=[ c  d ::=[ a ::=[ b ::=[ • ]  d ::=[ c  A  A ] ] ] ] ] ]  $end ]
Second Example b  c  •  A  $end
Second derivation  $accept ::=[ a ::=[ b  d ::=[ a ::=[ c  d ::=[ c ::=[ • ]  A ] ] ] ]  $end ]

Shift-Reduce Conflict:
6:    4 c: . %empty
6:    6 d: c . A
On Symbol: A
First  Example b  c  •  A  $end
First  derivation  $accept ::=[ a ::=[ b  d ::=[ a ::=[ c  d ::=[ c ::=[ • ]  A ] ] ] ]  $end ]
Second Example b  c  •  A
Second derivation  a ::=[ b  d ::=[ c  •  A ] ]

Reduce-Reduce Conflict:
7:    1 a: b d .
7:    7 d: d .
On Symbols: $end
Example  b  d  •
First  derivation  a ::=[ b  d  • ]
Second derivation  a ::=[ b  d ::=[ d  • ] ]

Reduce-Reduce Conflict:
8:    2 a: c d .
8:    7 d: d .
On Symbols: $end
Example  c  d  •
First  derivation  a ::=[ c  d  • ]
Second derivation  a ::=[ c  d ::=[ d  • ] ]

input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
input.y: warning: 6 reduce/reduce conflicts [-Wconflicts-rr]
input.y:5.4: warning: rule useless in parser due to conflicts [-Wother]
input.y:6.15: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## --------------------------- ##
## Non-unifying Prefix Share.  ##
## --------------------------- ##

AT_SETUP([Non-unifying Prefix Share])
AT_KEYWORDS([cex])

# Tests for a counterexample which should start its derivation
# at a shared symbol rather than the start symbol.

AT_DATA([[input.y]],
[[%token H J
%%
s: a | a J;
a: H i J J
i: %empty | i J;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
7:    5 i: i J .
7:    3 a: H i J . J
On Symbol: J
Example  H  i  J  •  J  J
First  derivation  s ::=[ a ::=[ H  i ::=[ i  J  • ]  J  J ] ]
Second derivation  s ::=[ a ::=[ H  i  J  •  J ]  J ]

input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
input.y:5.13-15: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## -------------------- ##
## Deep Null Unifying.  ##
## ---------------------##

# Tests that nested nullable nonterminals
# are derived correctly.

AT_SETUP([Deep Null Unifying])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token a d
%%
S: a A D | a A A D;
A: B;
B: C
C: %empty
D: d;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
3:    5 C: . %empty
3:    6 D: . d
On Symbol: d
Example  a  A  •  d
First  derivation  S ::=[ a  A  A ::=[ B ::=[ C ::=[ • ] ] ]  D ::=[ d ] ]
Second derivation  S ::=[ a  A  D ::=[ •  d ] ]

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

AT_CLEANUP

## ------------------------ ##
## Deep Null Non-unifying.  ##
## -------------------------##

# Tests that expand_to_conflict works with nullable sybols

AT_SETUP([Deep Null Non-unifying])
AT_KEYWORDS([cex])

AT_DATA([[input.y]],
[[%token a d e
%%
S: a A D | a A A D e;
A: B;
B: C
C: %empty
D: d;
]])

AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift-Reduce Conflict:
3:    5 C: . %empty
3:    6 D: . d
On Symbol: d
First  Example a  A  •  d  e  $end
First  derivation  $accept ::=[ S ::=[ a  A  A ::=[ B ::=[ C ::=[ • ] ] ]  D ::=[ d ]  e ]  $end ]
Second Example a  A  •  d  $end
Second derivation  $accept ::=[ S ::=[ a  A  D ::=[ •  d ] ]  $end ]

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

AT_CLEANUP