# 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([-Wcounterexamples $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], [], [],
[[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
Shift/reduce conflict on token B:
  Example              A . B C
  First derivation     s ::=[ a ::=[ A . ] x ::=[ B C ] ]
  Example              A . B C
  Second derivation    s ::=[ y ::=[ A . B ] c ::=[ C ] ]

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], [], [],
[[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
Shift/reduce conflict on token B:
  Example              A . B C
  First derivation     s ::=[ a ::=[ A . ] bc ::=[ B C ] ]
  Example              A . B C
  Second derivation    s ::=[ ac ::=[ A ac ::=[ b ::=[ . B ] ] C ] ]

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], [], [],
[[input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
Shift/reduce conflict on token B:
  Example              A . B y
  First derivation     s ::=[ ax ::=[ A x ::=[ . ] ] by ::=[ B y ] ]
  Example              A . B
  Second derivation    s ::=[ A xby ::=[ . B ] ]

Shift/reduce conflict on token 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: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], [], [],
[[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
Shift/reduce conflict on token 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: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], [], [],
[[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
Shift/reduce conflict on token 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 ]

]])

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], [], [],
[[input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
Shift/reduce conflict on token A:
  Example              b . A X X Y
  First derivation     a ::=[ r ::=[ b . ] t ::=[ A x ::=[ X ] xy ::=[ X Y ] ] ]
  Example              b . A X X Y
  Second derivation    a ::=[ s ::=[ b . xx ::=[ A X X ] y ::=[ Y ] ] ]

Shift/reduce conflict on token 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: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], [], [],
[[input.y: warning: 1 reduce/reduce conflict [-Wconflicts-rr]
Reduce/reduce conflict on token $end:
  Example              A b .
  First derivation     a ::=[ A b . ]
  Example              A b .
  Second derivation    a ::=[ A b ::=[ b . ] ]

input.y:4.9: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## --------------------------------- ##
## Non-unifying R/R LR(1) conflict.  ##
## --------------------------------- ##

AT_SETUP([Non-unifying R/R LR(1) 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], [], [],
[[input.y: warning: 2 reduce/reduce conflicts [-Wconflicts-rr]
Reduce/reduce conflict on tokens 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:5.4: warning: rule useless in parser due to conflicts [-Wother]
]])

AT_CLEANUP

## --------------------------------- ##
## Non-unifying R/R LR(2) conflict.  ##
## --------------------------------- ##

AT_SETUP([Non-unifying R/R LR(2) 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], [], [],
[[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
Shift/reduce conflict on token J:
time limit exceeded: XXX
  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: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], [], [],
[[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
Shift/reduce conflict on token B:
  Example              N A . B C
  First derivation     s ::=[ n ::=[ N a ::=[ A . ] B ] C ]
  Example              N A . B C
  Second derivation    s ::=[ n ::=[ N b ::=[ A . B C ] ] ]

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], [], [],
[[input.y: warning: 4 reduce/reduce conflicts [-Wconflicts-rr]
Reduce/reduce conflict on tokens b, c:
  Example              B . b A A c A
  First derivation     S ::=[ B ::=[ A ::=[ B . ] b A ] C ::=[ A c A ] ]
  Example              B . b A c A
  Second derivation    S ::=[ B C ::=[ A ::=[ B ::=[ A ::=[ . ] b A ] ] c A ] ]

Reduce/reduce conflict on tokens b, c:
  Example              C . c A A b A
  First derivation     S ::=[ C ::=[ A ::=[ C . ] c A ] B ::=[ A b A ] ]
  Example              C . c A b A
  Second derivation    S ::=[ C B ::=[ A ::=[ C ::=[ A ::=[ . ] c A ] ] b A ] ]

]])

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], [], [],
[[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
input.y: warning: 6 reduce/reduce conflicts [-Wconflicts-rr]
Reduce/reduce conflict on token 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 on token A:
time limit exceeded: XXX
  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 on token A:
time limit exceeded: XXX
  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 on token A:
time limit exceeded: XXX
  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 on token 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 on token 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 on token $end:
  Example              b d .
  First derivation     a ::=[ b d . ]
  Example              b d .
  Second derivation    a ::=[ b d ::=[ d . ] ]

Reduce/reduce conflict on token $end:
  Example              c d .
  First derivation     a ::=[ c d . ]
  Example              c d .
  Second derivation    a ::=[ c d ::=[ d . ] ]

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], [], [],
[[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
Shift/reduce conflict on token J:
  Example              H i J . J J
  First derivation     s ::=[ a ::=[ H i ::=[ i J . ] J J ] ]
  Example              H i J . J J
  Second derivation    s ::=[ a ::=[ H i J . J ] J ]

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], [], [],
[[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
Shift/reduce conflict on token D:
  Example              A a . D
  First derivation     s ::=[ A a a ::=[ b ::=[ c ::=[ . ] ] ] d ::=[ D ] ]
  Example              A a . D
  Second derivation    s ::=[ A a d ::=[ . D ] ]

]])

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], [], [],
[[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
Shift/reduce conflict on token 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 ]

]])

AT_CLEANUP