1 # Exercising Bison on counterexamples. -*- Autotest -*-
3 # Copyright (C) 2020-2022 Free Software Foundation, Inc.
5 # This program is free software: you can redistribute it and/or modify
6 # it under the terms of the GNU General Public License as published by
7 # the Free Software Foundation, either version 3 of the License, or
8 # (at your option) any later version.
10 # This program is distributed in the hope that it will be useful,
11 # but WITHOUT ANY WARRANTY; without even the implied warranty of
12 # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 # GNU General Public License for more details.
15 # You should have received a copy of the GNU General Public License
16 # along with this program. If not, see <https://www.gnu.org/licenses/>.
18 AT_BANNER([[Counterexamples.]])
20 # AT_BISON_CHECK_CEX(TREE, FLAT)
21 # ------------------------------
22 m4_define([AT_BISON_CHECK_CEX],
25 AT_BISON_CHECK([-Wcounterexamples input.y], [0], [], [stderr])
26 # FIXME: Avoid trailing white spaces.
27 AT_CHECK([[sed -e 's/time limit exceeded: [0-9][.0-9]*/time limit exceeded: XXX/g;s/ *$//;' stderr]],
30 m4_pushdef([AT_SET_ENV_IF],
31 [[YYFLAT=1; export YYFLAT;]]m4_defn([AT_SET_ENV_IF]))
32 AT_BISON_CHECK([-Wcounterexamples input.y], [0], [], [stderr])
33 AT_CHECK([[sed -e 's/time limit exceeded: [0-9][.0-9]*/time limit exceeded: XXX/g' stderr]],
35 m4_popdef([AT_SET_ENV_IF])
39 ## --------------------- ##
40 ## Simple Unifying S/R. ##
41 ## --------------------- ##
43 AT_SETUP([Unifying S/R])
56 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
57 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
67 input.y:4.4: warning: rule useless in parser due to conflicts [-Wother]
69 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
70 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
72 Shift derivation s -> [ y -> [ A . B ] c -> [ C ] ]
73 Reduce derivation s -> [ a -> [ A . ] x -> [ B C ] ]
74 input.y:4.4: warning: rule useless in parser due to conflicts [-Wother]
79 ## ------------------- ##
80 ## Deep Unifying S/R. ##
81 ## ------------------- ##
83 AT_SETUP([Deep Unifying S/R])
96 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
97 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
108 `-> 7: A . `-> 10: B C
109 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
110 Example: A A . B B C C
122 `-> 8: A a `-> 9: B bc C
123 `-> 7: A . `-> 10: B C
124 input.y:6.4: warning: rule useless in parser due to conflicts [-Wother]
126 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
127 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
129 Shift derivation s -> [ ac -> [ A ac -> [ b -> [ . B ] ] C ] ]
130 Reduce derivation s -> [ a -> [ A . ] bc -> [ B C ] ]
131 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
132 Example A A . B B C C
133 Shift derivation s -> [ ac -> [ A ac -> [ A ac -> [ b -> [ . b -> [ B B ] ] ] C ] C ] ]
134 Reduce derivation s -> [ a -> [ A a -> [ A . ] ] bc -> [ B bc -> [ B C ] C ] ]
135 input.y:6.4: warning: rule useless in parser due to conflicts [-Wother]
140 ## ------------------------------------ ##
141 ## S/R Conflict with Nullable Symbols. ##
142 ## ------------------------------------ ##
144 AT_SETUP([S/R Conflict with Nullable Symbols])
158 [[input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
159 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
168 `-> 3: A x `-> 6: B y
169 `-> 4: %empty . `-> 6: %empty
170 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
171 First example: A X . B Y $end
178 Second example: A X . B y $end
183 `-> 3: A x `-> 6: B y
186 input.y:5.4-9: warning: rule useless in parser due to conflicts [-Wother]
188 [[input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
189 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
191 Shift derivation s -> [ A xby -> [ . B ] ]
192 Reduce derivation s -> [ ax -> [ A x -> [ . ] ] by -> [ B y -> [ ] ] ]
193 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
194 First example A X . B Y $end
195 Shift derivation $accept -> [ s -> [ A xby -> [ X xby -> [ . B ] Y ] ] $end ]
196 Second example A X . B y $end
197 Reduce derivation $accept -> [ s -> [ ax -> [ A x -> [ X x -> [ . ] ] ] by -> [ B y ] ] $end ]
198 input.y:5.4-9: warning: rule useless in parser due to conflicts [-Wother]
203 ## ---------------------------- ##
204 ## Non-unifying Ambiguous S/R. ##
205 ## ---------------------------- ##
207 AT_SETUP([Non-unifying Ambiguous S/R])
221 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
222 input.y: warning: shift/reduce conflict on token C [-Wcounterexamples]
223 First example: B . C $end
230 Second example: B . C D $end
236 `-> 7: B . `-> 8: C D
237 input.y:6.4: warning: rule useless in parser due to conflicts [-Wother]
239 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
240 input.y: warning: shift/reduce conflict on token C [-Wcounterexamples]
241 First example B . C $end
242 Shift derivation $accept -> [ g -> [ x -> [ bc -> [ B . C ] ] ] $end ]
243 Second example B . C D $end
244 Reduce derivation $accept -> [ g -> [ x -> [ b -> [ B . ] cd -> [ C D ] ] ] $end ]
245 input.y:6.4: warning: rule useless in parser due to conflicts [-Wother]
250 ## ------------------------------ ##
251 ## Non-unifying Unambiguous S/R. ##
252 ## ------------------------------ ##
254 AT_SETUP([Non-unifying Unambiguous S/R])
266 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
267 input.y: warning: shift/reduce conflict on token A [-Wcounterexamples]
268 First example: A . A B $end
275 Second example: A . A $end
284 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
285 input.y: warning: shift/reduce conflict on token A [-Wcounterexamples]
286 First example A . A B $end
287 Shift derivation $accept -> [ s -> [ t -> [ y -> [ A . A B ] ] ] $end ]
288 Second example A . A $end
289 Reduce derivation $accept -> [ s -> [ s -> [ t -> [ x -> [ A . ] ] ] t -> [ x -> [ A ] ] ] $end ]
294 ## ----------------------- ##
295 ## S/R after first token. ##
296 ## ----------------------- ##
298 AT_SETUP([S/R after first token])
315 [[input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
316 input.y: warning: shift/reduce conflict on token A [-Wcounterexamples]
322 `-> 9: A X X `-> 11: Y
326 `-> 3: b . `-> 6: A x xy
328 input.y: warning: shift/reduce conflict on token X [-Wcounterexamples]
329 First example: A X . X
335 Second example: X . X xy
339 `-> 8: X . `-> 6: X xy
340 input.y:4.4: warning: rule useless in parser due to conflicts [-Wother]
341 input.y:8.4: warning: rule useless in parser due to conflicts [-Wother]
343 [[input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
344 input.y: warning: shift/reduce conflict on token A [-Wcounterexamples]
346 Shift derivation a -> [ s -> [ b . xx -> [ A X X ] y -> [ Y ] ] ]
347 Reduce derivation a -> [ r -> [ b . ] t -> [ A x -> [ X ] xy -> [ X Y ] ] ]
348 input.y: warning: shift/reduce conflict on token X [-Wcounterexamples]
349 First example A X . X
350 Shift derivation a -> [ t -> [ A xx -> [ X . X ] ] ]
351 Second example X . X xy
352 Reduce derivation a -> [ x -> [ X . ] t -> [ X xy ] ]
353 input.y:4.4: warning: rule useless in parser due to conflicts [-Wother]
354 input.y:8.4: warning: rule useless in parser due to conflicts [-Wother]
359 ## ----------------------------- ##
360 ## Unifying R/R counterexample. ##
361 ## ----------------------------- ##
363 AT_SETUP([Unifying R/R counterexample])
373 [[input.y: warning: 1 reduce/reduce conflict [-Wconflicts-rr]
374 input.y: warning: reduce/reduce conflict on token $end [-Wcounterexamples]
376 First reduce derivation
379 Second reduce derivation
383 input.y:4.9: warning: rule useless in parser due to conflicts [-Wother]
385 [[input.y: warning: 1 reduce/reduce conflict [-Wconflicts-rr]
386 input.y: warning: reduce/reduce conflict on token $end [-Wcounterexamples]
388 First reduce derivation a -> [ A b . ]
389 Second reduce derivation a -> [ A b -> [ b . ] ]
390 input.y:4.9: warning: rule useless in parser due to conflicts [-Wother]
395 ## --------------------------------- ##
396 ## Non-unifying R/R LR(1) conflict. ##
397 ## --------------------------------- ##
399 AT_SETUP([Non-unifying R/R LR(1) conflict])
404 s: a A | B a C | b C | B b A;
410 [[input.y: warning: 2 reduce/reduce conflicts [-Wconflicts-rr]
411 input.y: warning: reduce/reduce conflict on tokens A, C [-Wcounterexamples]
412 First example: D . A $end
413 First reduce derivation
418 Second example: B D . A $end
419 Second reduce derivation
424 input.y:5.4: warning: rule useless in parser due to conflicts [-Wother]
426 [[input.y: warning: 2 reduce/reduce conflicts [-Wconflicts-rr]
427 input.y: warning: reduce/reduce conflict on tokens A, C [-Wcounterexamples]
428 First example D . A $end
429 First reduce derivation $accept -> [ s -> [ a -> [ D . ] A ] $end ]
430 Second example B D . A $end
431 Second reduce derivation $accept -> [ s -> [ B b -> [ D . ] A ] $end ]
432 input.y:5.4: warning: rule useless in parser due to conflicts [-Wother]
437 ## --------------------------------- ##
438 ## Non-unifying R/R LR(2) conflict. ##
439 ## --------------------------------- ##
441 AT_SETUP([Non-unifying R/R LR(2) conflict])
452 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
453 input.y: warning: shift/reduce conflict on token J [-Wcounterexamples]
454 time limit exceeded: XXX
455 First example: H i . J K $end
461 Second example: H i . J $end
467 input.y:4.4-6: warning: rule useless in parser due to conflicts [-Wother]
469 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
470 input.y: warning: shift/reduce conflict on token J [-Wcounterexamples]
471 time limit exceeded: XXX
472 First example H i . J K $end
473 Shift derivation $accept -> [ a -> [ H i -> [ i . J K ] ] $end ]
474 Second example H i . J $end
475 Reduce derivation $accept -> [ s -> [ a -> [ H i . ] J ] $end ]
476 input.y:4.4-6: warning: rule useless in parser due to conflicts [-Wother]
481 ## -------------------- ##
482 ## Cex Search Prepend. ##
483 ## -------------------- ##
485 # Tests prepend steps in uniying counterexample
488 AT_SETUP([Cex Search Prepend])
494 n: N n D | N n C | N a B | N b;
500 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
501 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
513 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
514 Example: N N A . B D C
527 input.y:5.4: warning: rule useless in parser due to conflicts [-Wother]
529 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
530 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
532 Shift derivation s -> [ n -> [ N b -> [ A . B C ] ] ]
533 Reduce derivation s -> [ n -> [ N a -> [ A . ] B ] C ]
534 input.y: warning: shift/reduce conflict on token B [-Wcounterexamples]
535 Example N N A . B D C
536 Shift derivation s -> [ n -> [ N n -> [ N b -> [ A . B D ] ] C ] ]
537 Reduce derivation s -> [ n -> [ N n -> [ N a -> [ A . ] B ] D ] C ]
538 input.y:5.4: warning: rule useless in parser due to conflicts [-Wother]
543 ## ------------------- ##
544 ## R/R cex with prec. ##
545 ## ------------------- ##
547 # Tests that counterexamples containing rules using
548 # precedence/associativity directives work.
550 AT_SETUP([R/R cex with prec])
563 [[input.y: warning: 4 reduce/reduce conflicts [-Wconflicts-rr]
564 input.y: warning: reduce/reduce conflict on tokens b, c [-Wcounterexamples]
566 First reduce derivation
569 `-> 6: A b A `-> 7: A c A
570 `-> 3: B . `-> 6: %empty `-> 7: %empty `-> 7: %empty
571 Second reduce derivation
575 `-> 3: B `-> 7: %empty
577 `-> 5: %empty . `-> 6: %empty
578 input.y: warning: reduce/reduce conflict on tokens b, c [-Wcounterexamples]
580 First reduce derivation
583 `-> 7: A c A `-> 6: A b A
584 `-> 4: C . `-> 7: %empty `-> 6: %empty `-> 6: %empty
585 Second reduce derivation
589 `-> 4: C `-> 6: %empty
591 `-> 5: %empty . `-> 7: %empty
593 [[input.y: warning: 4 reduce/reduce conflicts [-Wconflicts-rr]
594 input.y: warning: reduce/reduce conflict on tokens b, c [-Wcounterexamples]
596 First reduce derivation S -> [ B -> [ A -> [ B . ] b A -> [ ] ] C -> [ A -> [ ] c A -> [ ] ] ]
597 Second reduce derivation S -> [ B C -> [ A -> [ B -> [ A -> [ . ] b A -> [ ] ] ] c A -> [ ] ] ]
598 input.y: warning: reduce/reduce conflict on tokens b, c [-Wcounterexamples]
600 First reduce derivation S -> [ C -> [ A -> [ C . ] c A -> [ ] ] B -> [ A -> [ ] b A -> [ ] ] ]
601 Second reduce derivation S -> [ C B -> [ A -> [ C -> [ A -> [ . ] c A -> [ ] ] ] b A -> [ ] ] ]
606 ## ------------------- ##
607 ## Null nonterminals. ##
608 ## ------------------- ##
610 AT_SETUP([Null nonterminals])
622 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
623 input.y: warning: 6 reduce/reduce conflicts [-Wconflicts-rr]
624 input.y: warning: reduce/reduce conflict on token A [-Wcounterexamples]
625 First example: . c A A $end
626 First reduce derivation
630 `-> 3: %empty . `-> 6: c A A
631 Second example: . c A A $end
632 Second reduce derivation
636 `-> 4: %empty . `-> 6: c A A
637 input.y: warning: reduce/reduce conflict on token A [-Wcounterexamples]
638 time limit exceeded: XXX
639 First example: b . c A A $end
640 First reduce derivation
646 `-> 3: %empty . `-> 6: c A A
647 Second example: b . A $end
648 Second reduce derivation
654 input.y: warning: reduce/reduce conflict on token A [-Wcounterexamples]
655 time limit exceeded: XXX
656 First example: c . c A A $end
657 First reduce derivation
663 `-> 3: %empty . `-> 6: c A A
664 Second example: c . A $end
665 Second reduce derivation
671 input.y: warning: shift/reduce conflict on token A [-Wcounterexamples]
672 time limit exceeded: XXX
673 First example: b c . A
678 Second example: b c . c A A $end
687 `-> 3: %empty . `-> 6: c A A
688 input.y: warning: reduce/reduce conflict on token A [-Wcounterexamples]
689 First example: b c . c A A $end
690 First reduce derivation
698 `-> 3: %empty . `-> 6: c A A
699 Second example: b c . A $end
700 Second reduce derivation
708 input.y: warning: shift/reduce conflict on token A [-Wcounterexamples]
709 First example: b c . A
714 Second example: b c . A $end
723 input.y: warning: reduce/reduce conflict on token $end [-Wcounterexamples]
725 First reduce derivation
728 Second reduce derivation
732 input.y: warning: reduce/reduce conflict on token $end [-Wcounterexamples]
734 First reduce derivation
737 Second reduce derivation
741 input.y:5.4: warning: rule useless in parser due to conflicts [-Wother]
742 input.y:6.15: warning: rule useless in parser due to conflicts [-Wother]
744 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
745 input.y: warning: 6 reduce/reduce conflicts [-Wconflicts-rr]
746 input.y: warning: reduce/reduce conflict on token A [-Wcounterexamples]
747 First example . c A A $end
748 First reduce derivation $accept -> [ a -> [ b -> [ . ] d -> [ c A A ] ] $end ]
749 Second example . c A A $end
750 Second reduce derivation $accept -> [ a -> [ c -> [ . ] d -> [ c A A ] ] $end ]
751 input.y: warning: reduce/reduce conflict on token A [-Wcounterexamples]
752 time limit exceeded: XXX
753 First example b . c A A $end
754 First reduce derivation $accept -> [ a -> [ b d -> [ a -> [ b -> [ . ] d -> [ c A A ] ] ] ] $end ]
755 Second example b . A $end
756 Second reduce derivation $accept -> [ a -> [ b d -> [ c -> [ . ] A ] ] $end ]
757 input.y: warning: reduce/reduce conflict on token A [-Wcounterexamples]
758 time limit exceeded: XXX
759 First example c . c A A $end
760 First reduce derivation $accept -> [ a -> [ c d -> [ a -> [ b -> [ . ] d -> [ c A A ] ] ] ] $end ]
761 Second example c . A $end
762 Second reduce derivation $accept -> [ a -> [ c d -> [ c -> [ . ] A ] ] $end ]
763 input.y: warning: shift/reduce conflict on token A [-Wcounterexamples]
764 time limit exceeded: XXX
765 First example b c . A
766 Shift derivation a -> [ b d -> [ c . A ] ]
767 Second example b c . c A A $end
768 Reduce derivation $accept -> [ a -> [ b d -> [ a -> [ c d -> [ a -> [ b -> [ . ] d -> [ c A A ] ] ] ] ] ] $end ]
769 input.y: warning: reduce/reduce conflict on token A [-Wcounterexamples]
770 First example b c . c A A $end
771 First reduce derivation $accept -> [ a -> [ b d -> [ a -> [ c d -> [ a -> [ b -> [ . ] d -> [ c A A ] ] ] ] ] ] $end ]
772 Second example b c . A $end
773 Second reduce derivation $accept -> [ a -> [ b d -> [ a -> [ c d -> [ c -> [ . ] A ] ] ] ] $end ]
774 input.y: warning: shift/reduce conflict on token A [-Wcounterexamples]
775 First example b c . A
776 Shift derivation a -> [ b d -> [ c . A ] ]
777 Second example b c . A $end
778 Reduce derivation $accept -> [ a -> [ b d -> [ a -> [ c d -> [ c -> [ . ] A ] ] ] ] $end ]
779 input.y: warning: reduce/reduce conflict on token $end [-Wcounterexamples]
781 First reduce derivation a -> [ b d . ]
782 Second reduce derivation a -> [ b d -> [ d . ] ]
783 input.y: warning: reduce/reduce conflict on token $end [-Wcounterexamples]
785 First reduce derivation a -> [ c d . ]
786 Second reduce derivation a -> [ c d -> [ d . ] ]
787 input.y:5.4: warning: rule useless in parser due to conflicts [-Wother]
788 input.y:6.15: warning: rule useless in parser due to conflicts [-Wother]
793 ## --------------------------- ##
794 ## Non-unifying Prefix Share. ##
795 ## --------------------------- ##
797 AT_SETUP([Non-unifying Prefix Share])
799 # Tests for a counterexample which should start its derivation
800 # at a shared symbol rather than the start symbol.
811 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
812 input.y: warning: shift/reduce conflict on token J [-Wcounterexamples]
823 input.y:5.13-15: warning: rule useless in parser due to conflicts [-Wother]
825 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
826 input.y: warning: shift/reduce conflict on token J [-Wcounterexamples]
828 Shift derivation s -> [ a -> [ H i J . J ] J ]
829 Reduce derivation s -> [ a -> [ H i -> [ i J . ] J J ] ]
830 input.y:5.13-15: warning: rule useless in parser due to conflicts [-Wother]
835 ## -------------------- ##
836 ## Deep Null Unifying. ##
837 ## ---------------------##
839 # Tests that nested nullable nonterminals
840 # are derived correctly.
842 AT_SETUP([Deep Null Unifying])
855 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
856 input.y: warning: shift/reduce conflict on token D [-Wcounterexamples]
869 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
870 input.y: warning: shift/reduce conflict on token D [-Wcounterexamples]
872 Shift derivation s -> [ A a d -> [ . D ] ]
873 Reduce derivation s -> [ A a a -> [ b -> [ c -> [ . ] ] ] d -> [ D ] ]
878 ## ------------------------ ##
879 ## Deep Null Non-unifying. ##
880 ## -------------------------##
882 # Tests that expand_to_conflict works with nullable sybols
884 AT_SETUP([Deep Null Non-unifying])
889 s: A a d | A a a d E;
897 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
898 input.y: warning: shift/reduce conflict on token D [-Wcounterexamples]
899 First example: A a . D $end
905 Second example: A a . D E $end
914 [[input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
915 input.y: warning: shift/reduce conflict on token D [-Wcounterexamples]
916 First example A a . D $end
917 Shift derivation $accept -> [ s -> [ A a d -> [ . D ] ] $end ]
918 Second example A a . D E $end
919 Reduce derivation $accept -> [ s -> [ A a a -> [ b -> [ c -> [ . ] ] ] d -> [ D ] E ] $end ]