cex: add tests

* tests/counterexample.at: New.
This commit is contained in:
Vincent Imbimbo
2020-05-12 22:01:39 -04:00
committed by Akim Demaille
parent af0441cfd2
commit dcb6c972a2
2 changed files with 359 additions and 0 deletions

356
tests/counterexample.at Normal file
View File

@@ -0,0 +1,356 @@
# 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.]])
## --------------------- ##
## Simple Unifying S/R. ##
## --------------------- ##
AT_SETUP([Unifying S/R])
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([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## ------------------- ##
## Deep Unifying S/R. ##
## ------------------- ##
AT_SETUP([Deep Unifying S/R])
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([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## ------------------------------------ ##
## S/R Conflict with Nullable Symbols. ##
## ------------------------------------ ##
AT_SETUP([S/R Conflict with Nullable Symbols])
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([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## ---------------------------- ##
## Non-unifying Ambiguous S/R. ##
## ---------------------------- ##
AT_SETUP([Non-unifying Ambiguous S/R])
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([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## ------------------------------ ##
## Non-unifying Unambiguous S/R. ##
## ------------------------------ ##
AT_SETUP([Non-unifying Unambiguous S/R])
AT_DATA([[input.y]],
[[%token A B
%%
s: t | s t;
t: x | y;
x: A;
y: A A B;
]])
AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## ----------------------- ##
## S/R after first token. ##
## ----------------------- ##
AT_SETUP([S/R after first token])
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([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## ----------------------------- ##
## Unifying R/R counterexample. ##
## ----------------------------- ##
AT_SETUP([Unifying R/R counterexample])
AT_DATA([[input.y]],
[[%token A
%%
a : A b ;
b : A | b;
]])
AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## ------------------------------- ##
## Non-unifying R/R lr1 conflict. ##
## ------------------------------- ##
AT_SETUP([Non-unifying R/R lr1 conflict])
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([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## ------------------------------- ##
## Non-unifying R/R lr2 conflict. ##
## ------------------------------- ##
AT_SETUP([Non-unifying R/R lr2 conflict])
AT_DATA([[input.y]],
[[%token H J K X
%%
s: a J;
a: H i;
i: X | i J K;
]])
AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## -------------------- ##
## Cex Search Prepend. ##
## -------------------- ##
# Tests prepend steps in uniying counterexample
# graph search
AT_SETUP([Cex Search Prepend])
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([-Wcounterexample input.y], 0, [],
[[
]])
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_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([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## ------------------- ##
## Null nonterminals. ##
## ------------------- ##
AT_SETUP([Null nonterminals])
AT_DATA([[input.y]],
[[%token A
%%
a : b d | c d ;
b : ;
c : ;
d : a | c A | d;
]])
AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## --------------------------- ##
## Non-unifying Prefix Share. ##
## --------------------------- ##
AT_SETUP([Non-unifying Prefix Share])
# 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([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## -------------------- ##
## Deep Null Unifying. ##
## ---------------------##
# Tests that nested nullable nonterminals
# are derived correctly.
AT_SETUP([Deep Null Unifying])
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([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP
## ------------------------ ##
## Deep Null Non-unifying. ##
## -------------------------##
# Tests that expand_to_conflict works with nullable sybols
AT_SETUP([Deep Null Non-unifying])
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([-Wcounterexample input.y], 0, [],
[[
]])
AT_CLEANUP