[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PATCH] doc: cex documentation
|
From: |
Akim Demaille |
|
Subject: |
Re: [PATCH] doc: cex documentation |
|
Date: |
Fri, 3 Jul 2020 07:12:09 +0200 |
> Le 2 juil. 2020 à 20:46, Akim Demaille <akim@lrde.epita.fr> a écrit :
>
> commit cf1f69b98723fab92c6b2c7be5c678e7cd0a5a80
> Author: Akim Demaille <akim.demaille@gmail.com>
> Date: Thu Jul 2 20:35:33 2020 +0200
>
> cex: give more details about -Wcex and -rcex
>
> * data/bison-default.css: Cobalt does not seem to be supported.
> * doc/bison.texi (Counterexamples): A new section.
> (Understanding): Show the counterexamples as it shows in the report:
> with its items.
> (Bison Options): Document -Wcex and -rcex.
My previous patch was incomplete. And I added an entry in the glossary.
commit 4daf99c0c5f4f07d7b0149753f918ca714d4dae8
Author: Akim Demaille <akim.demaille@gmail.com>
Date: Thu Jul 2 08:19:58 2020 +0200
cex: give more details about -Wcex and -rcex
* data/bison-default.css: Cobalt does not seem to be supported.
* doc/bison.texi (Counterexamples): A new section.
(Understanding): Show the counterexamples as it shows in the report:
with its items.
(Bison Options): Document -Wcex and -rcex.
diff --git a/data/bison-default.css b/data/bison-default.css
index 2652e03f..5248c294 100644
--- a/data/bison-default.css
+++ b/data/bison-default.css
@@ -44,7 +44,7 @@
.cex-0 { color: yellow; }
.cex-1 { color: green; }
.cex-2 { color: blue; }
-.cex-3 { color: cobalt; }
+.cex-3 { color: purple; }
.cex-4 { color: violet; }
.cex-5 { color: orange; }
.cex-6 { color: brown; }
diff --git a/doc/bison.texi b/doc/bison.texi
index 5409f36c..84a609cf 100644
--- a/doc/bison.texi
+++ b/doc/bison.texi
@@ -53,11 +53,11 @@
\gdef\colorBlue{%
\setcolor{\rgbBlue}%
}
-
-\gdef\rgbWarning{0.50 0 0.50}
-\gdef\colorWarning{%
- \setcolor{\rgbWarning}%
+\gdef\rgbPurple{0.50 0 0.50}
+\gdef\colorPurple{%
+ \setcolor{\rgbPurple}%
}
+
\gdef\rgbError{0.80 0 0}
\gdef\colorError{%
\setcolor{\rgbError}%
@@ -84,10 +84,10 @@
@macro colorBlue
@inlineraw{html, <b style="color:blue">}
@end macro
-
-@macro colorWarning
+@macro colorPurple
@inlineraw{html, <b style="color:darkviolet">}
@end macro
+
@macro colorError
@inlineraw{html, <b style="color:red">}
@end macro
@@ -115,8 +115,12 @@
@colorBlue{}\text\@colorOff{}
@end macro
+@macro purple{text}
+@colorPurple{}\text\@colorOff{}
+@end macro
+
@macro dwarning{text}
-@colorWarning{}\text\@colorOff{}
+@purple{\text\}
@end macro
@macro derror{text}
@@ -445,6 +449,7 @@ Handling Context Dependencies
Debugging Your Parser
+* Counterexamples:: Understanding conflicts.
* Understanding:: Understanding the structure of your parser.
* Graphviz:: Getting a visual representation of the parser.
* Xml:: Getting a markup representation of the parser.
@@ -9785,12 +9790,18 @@ clear the flag.
@chapter Debugging Your Parser
Developing a parser can be a challenge, especially if you don't understand
-the algorithm (@pxref{Algorithm}). This
-chapter explains how to understand and debug a parser.
-
-The first sections focus on the static part of the parser: its structure.
-They explain how to generate and read the detailed description of the
-automaton. There are several formats available:
+the algorithm (@pxref{Algorithm}). This chapter explains how to understand
+and debug a parser.
+
+The most frequent issue users face is solving their conflicts. To fix them,
+the first step is understanding how they arise in a given grammar. This is
+made much easier by automated generation of counterexamples, cover in the
+first section (@pxref{Counterexamples}).
+
+In most cases though, looking at the structure of the automaton is still
+needed. The following sections explain how to generate and read the
+detailed structural description of the automaton. There are several formats
+available:
@itemize @minus
@item
as text, see @ref{Understanding};
@@ -9807,19 +9818,175 @@ The last section focuses on the dynamic part of the
parser: how to enable
and understand the parser run-time traces (@pxref{Tracing}).
@menu
+* Counterexamples:: Understanding conflicts.
* Understanding:: Understanding the structure of your parser.
* Graphviz:: Getting a visual representation of the parser.
* Xml:: Getting a markup representation of the parser.
* Tracing:: Tracing the execution of your parser.
@end menu
+@node Counterexamples
+@section Generation of Counterexamples
+
+Solving conflicts is probably the most delicate part of the design of an LR
+parser, as demonstrated by the number of sections devoted to them in this
+very documentation. To solve a conflict, one must understand it: when does
+it occur? Is it because of a flaw in the grammar? Is it rather because
+LR(1) cannot cope with this grammar?
+
+On difficulty is that conflicts occur in the @emph{automaton}, and it can be
+tricky to related them to issues in the @emph{grammar} itself. With
+experience and patience, analysis the detailed description of the automaton
+(@pxref{Understanding}) allows to find example strings that reach these
conflicts.
+
+That task is made much easier thanks to the generation of counterexamples,
+initially developed by Chinawat Isradisaikul and Andrew Myers
+@pcite{Isradisaikul 2015}.
+
+As a first example, see the example grammar of @ref{Shift/Reduce}, which
+features on shift/reduce conflict:
+
+@example
+$ @kbd{bison if-then-else.y}
+if-then-else.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
+if-then-else.y: warning: rerun with option '-Wcounterexamples' to generate
conflict counterexamples [-Wother]
+@end example
+
+@noindent
+Let's rerun @command{bison} with the option
+@option{-Wcex}/@option{-Wcounterexamples}@inlinefmt{info, (the following
+output is actually in color)}:
+
+@ifhtml
+@example
+Shift/reduce conflict on token "else":
+@group
+ Example @yellow{"if" expr "then"} @blue{"if" expr "then" stmt}
@red{•} @yellow{"else" stmt}
+ First derivation @yellow{if_stmt ::=[ "if" expr "then"} @green{stmt ::=[}
@blue{if_stmt ::=[ "if" expr "then" stmt} @red{•} @blue{]} @green{]}
@yellow{"else" stmt ]}
+ Example @yellow{"if" expr "then"} @blue{"if" expr "then" stmt}
@red{•} @blue{"else" stmt}
+ Second derivation @yellow{if_stmt ::=[ "if" expr "then"} @green{stmt ::=[}
@blue{if_stmt ::=[ "if" expr "then" stmt} @red{•} @blue{"else" stmt ]}
@green{]} @yellow{]}
+@end group
+@end example
+@end ifhtml
+@ifnothtml
+@smallexample
+Shift/reduce conflict on token "else":
+@group
+ Example
+ @yellow{"if" expr "then"} @blue{"if" expr "then" stmt} @red{•}
@yellow{"else" stmt}
+ First derivation
+ @yellow{if_stmt ::=[ "if" expr "then"} @green{stmt ::=[} @blue{if_stmt
::=[ "if" expr "then" stmt} @red{•} @blue{]} @green{]} @yellow{"else" stmt ]}
+ Example
+ @yellow{"if" expr "then"} @blue{"if" expr "then" stmt} @red{•}
@blue{"else" stmt}
+ Second derivation
+ @yellow{if_stmt ::=[ "if" expr "then"} @green{stmt ::=[} @blue{if_stmt
::=[ "if" expr "then" stmt} @red{•} @blue{"else" stmt ]} @green{]} @yellow{]}
+@end group
+@end smallexample
+@end ifnothtml
+
+This shows two different derivations for one single expression. That
+demonstrates that the grammar is ambiguous.
+
+@sp 1
+
+As a more delicate example, consider the example grammar of
+@ref{Reduce/Reduce}, which features a reduce/reduce conflict:
+
+@example
+%%
+sequence:
+ %empty
+| maybeword
+| sequence "word"
+;
+maybeword:
+ %empty
+| "word"
+;
+@end example
+
+Bison generates the following counterexamples:
+
+@example
+$ @kbd{bison -Wcex sequence.y}
+sequence.y: @dwarning{warning}: 1 shift/reduce conflict
[@dwarning{-Wconflicts-sr}]
+sequence.y: @dwarning{warning}: 2 reduce/reduce conflicts
[@dwarning{-Wconflicts-rr}]
+Shift/reduce conflict on token "word":
+ Example @red{•} @yellow{"word"}
+ First derivation @yellow{sequence ::=[} @green{sequence ::=[} @red{•}
@green{]} @yellow{"word" ]}
+ Example @red{•} @green{"word"}
+ Second derivation @yellow{sequence ::=[} @green{maybeword ::=[} @red{•}
@green{"word" ]} @yellow{]}
+
+Reduce/reduce conflict on tokens $end, "word":
+ Example @red{•}
+ First derivation @yellow{sequence ::=[} @red{•} @yellow{]}
+ Example @red{•}
+ Second derivation @yellow{sequence ::=[} @green{maybeword ::=[} @red{•}
@green{]} @yellow{]}
+
+Shift/reduce conflict on token "word":
+ Example @red{•} @yellow{"word"}
+ First derivation @yellow{sequence ::=[} @green{sequence ::=[}
@blue{maybeword ::=[} @red{•} @blue{]} @green{]} @yellow{"word" ]}
+ Example @red{•} @green{"word"}
+ Second derivation @yellow{sequence ::=[} @green{maybeword ::=[} @red{•}
@green{"word" ]} @yellow{]}
+
+sequence.y:8.3-45: @dwarning{warning}: rule useless in parser due to conflicts
[@dwarning{-Wother}]
+ 8 | @dwarning{%empty @{ printf ("empty maybeword\n"); @}}
+ | @dwarning{^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}
+@end example
+
+Each of these three conflicts, again, prove that the grammar is ambiguous.
+For instance, the second conflict (the reduce/reduce one) shows that the
+grammar accept the empty input in two different ways.
+
+@sp 1
+
+Sometimes, the search will not find an example that can be derived in two
+ways. In these cases, counterexample generation will provide two examples
+that are the same up until the dot. Most notably, this will happen when
+your grammar requires a stronger parser (more lookahead, LR instead of
+LALR). The following example isn't LR(1):
+
+@example
+%token ID
+%%
+s: a ID
+a: expr
+expr: %empty | expr ID ','
+@end example
+
+@command{bison} reports:
+
+@smallexample
+Shift/reduce conflict on token ID:
+ First example @blue{expr} @red{•} @green{ID} @yellow{$end}
+ First derivation @yellow{$accept ::=[} @green{s ::=[} @blue{a ::=[ expr}
@red{•} @blue{]} @green{ID ]} @yellow{$end ]}
+ Second example @purple{expr} @red{•} @purple{ID ','} @green{ID}
@yellow{$end}
+ Second derivation @yellow{$accept ::=[} @green{s ::=[} @blue{a ::=[}
@purple{expr ::=[ expr} @red{•} @purple{ID ',' ]} @blue{]} @green{ID ]}
@yellow{$end ]}
+@end smallexample
+
+This conflict is caused by the parser not having enough information to know
+the difference between these two examples. The parser would need an
+additional lookahead token to know whether or not a comma follows the
+@code{ID} after @code{expr}. These types of conflicts tend to be more
+difficult to fix, and usually need a rework of the grammar. In this case,
+it can be fixed by changing around the recursion: @code{expr: ID | ',' expr
+ID}.
+
+Alternatively, you might also want to consider using a GLR parser
+(@pxref{GLR Parsers}).
+
+@sp 1
+
+On occasions, it is useful to look at counterexamples @emph{in situ}: with
+the automaton report (@xref{Understanding}, in particular @ref{state-8,,
+State 8}).
+
@node Understanding
@section Understanding Your Parser
-As documented elsewhere (@pxref{Algorithm}) Bison parsers are
-@dfn{shift/reduce automata}. In some cases (much more frequent than one
-would hope), looking at this automaton is required to tune or simply fix a
-parser.
+Bison parsers are @dfn{shift/reduce automata} (@pxref{Algorithm}). In some
+cases (much more frequent than one would hope), looking at this automaton is
+required to tune or simply fix a parser.
The textual file is generated when the options @option{--report} or
@option{--verbose} are specified, see @ref{Invocation}. Its name is made by
@@ -9877,62 +10044,6 @@ calc.y: @dwarning{warning}: 7 shift/reduce conflicts
[@dwarning{-Wconflicts-sr}]
calc.y: @dwarning{warning}: rerun with option '-Wcounterexamples' to generate
conflict counterexamples [@dwarning{-Wother}]
@end smallexample
-When given @option{-Wcounterexamples}, @command{bison} will run a search for
-strings in your grammar that better demonstrate you
-conflicts. Counterexample generation was initially developed by Chinawat
-Isradisaikul and Andrew Myers @pcite{Isradisaikul 2015}. For
-@file{calc.y}, the first printed example is:
-
-@example
-Shift/reduce conflict on token '/':
- Example @green{exp '+' exp} @red{•} @yellow{'/' exp}
- First derivation @yellow{exp ::=[} @green{exp ::=[ exp '+' exp} @red{•}
@green{]} @yellow{'/' exp ]}
- Example @yellow{exp '+'} @green{exp} @red{•} @green{'/' exp}
- Second derivation @yellow{exp ::=[ exp '+'} @green{exp ::=[ exp} @red{•}
@green{'/' exp ]} @yellow{]}
-@end example
-
-This shows two separate derivations in the grammar for the same @code{exp}:
-@samp{e1 + e2 / e3}. The derivations show how your rules would parse the
-given example. Here, the first derivation completes a reduction when seeing
-@samp{/}, causing @samp{e1 + e2} to be grouped as an @code{exp}. The second
-derivation shifts on @samp{/}, resulting in @samp{e2 / e3} being grouped as
-an @code{exp}. Therefore, it is easy to see that adding @code{%precedence}
-directives would fix this conflict.
-
-Sometimes, the search will not find an example that can be derived in two
-ways. In these cases, counterexample generation will provide two examples
-that are the same up until the dot. Most notably, this will happen when
-your grammar requires a stronger parser (more lookahead, LR instead of
-LALR). The following example isn't LR(1):
-
-@example
-%token ID
-%%
-s: a ID
-a: expr
-expr: %empty | expr ID ','
-@end example
-
-@command{bison} reports:
-
-@smallexample
-Shift/reduce conflict on token ID:
- First example @blue{expr} @red{•} @green{ID} @yellow{$end}
- First derivation @yellow{$accept ::=[} @green{s ::=[} @blue{a ::=[ expr}
@red{•} @blue{]} @green{ID ]} @yellow{$end ]}
- Second example @blue{expr} @red{•} @blue{ID ','} @green{ID}
@yellow{$end}
- Second derivation @yellow{$accept ::=[} @green{s ::=[} @blue{a ::=[ expr
::=[ expr} @red{•} @blue{ID ',' ] ]} @green{ID ]} @yellow{$end ]}
-@end smallexample
-
-This conflict is caused by the parser not having enough information to know
-the difference between these two examples. The parser would need an
-additional lookahead token to know whether or not a comma follows the
-@code{ID} after @code{expr}. These types of conflicts tend to be more
-difficult to fix, and usually need a rework of the grammar. In this case,
-it can be fixed by changing around the recursion: @code{expr: ID | ',' expr
-ID}.
-
-Counterexamples can also be written to a file with @option{--report=cex}.
-
Going back to the calc example, when given @option{--report=state},
in addition to @file{calc.tab.c}, it creates a file @file{calc.output}
with contents detailed below. The order of the output and the exact
@@ -10164,6 +10275,7 @@ State 7
exp go to state 11
@end example
+@anchor{state-8}
As was announced in beginning of the report, @samp{State 8 conflicts:
1 shift/reduce}:
@@ -10237,6 +10349,27 @@ Conflict between rule 1 and token '-' resolved as
reduce (%left '-').
Conflict between rule 1 and token '*' resolved as shift ('+' < '*').
@end example
+When given @option{--report=counterexamples}, @command{bison} will generate
+counterexamples within the report, augmented with the corresponding items
+(@pxref{Counterexamples}).
+
+@example
+Shift/reduce conflict on token '/':
+ 1 exp: exp '+' exp •
+ 4 exp: exp • '/' exp
+ Example @green{exp '+' exp} @red{•} @yellow{'/' exp}
+ First derivation @yellow{exp ::=[} @green{exp ::=[ exp '+' exp} @red{•}
@green{]} @yellow{'/' exp ]}
+ Example @yellow{exp '+'} @green{exp} @red{•} @green{'/' exp}
+ Second derivation @yellow{exp ::=[ exp '+'} @green{exp ::=[ exp} @red{•}
@green{'/' exp ]} @yellow{]}
+@end example
+
+This shows two separate derivations in the grammar for the same @code{exp}:
+@samp{e1 + e2 / e3}. The derivations show how your rules would parse the
+given example. Here, the first derivation completes a reduction when seeing
+@samp{/}, causing @samp{e1 + e2} to be grouped as an @code{exp}. The second
+derivation shifts on @samp{/}, resulting in @samp{e2 / e3} being grouped as
+an @code{exp}. Therefore, it is easy to see that adding @code{%precedence}
+directives would fix this conflict.
The remaining states are similar:
@@ -11084,6 +11217,13 @@ unexpected number of conflicts is an error, and an
expected number of
conflicts is not reported, so @option{-W} and @option{--warning} then have
no effect on the conflict report.
+@item counterexamples
+@itemx cex
+Provide counterexamples for conflicts. @xref{Counterexamples}.
+Counterexamples take time to compute. The option @option{-Wcex} should be
+used by the developer when working on the grammar; it hardly makes sense to
+use it in a CI.
+
@item dangling-alias
Report string literals that are not bound to a token symbol.
@@ -11458,6 +11598,13 @@ each rule's lookahead set.
Implies @code{state}. Explain how conflicts were solved thanks to
precedence and associativity directives.
+@item counterexamples
+@itemx cex
+Look for counterexamples for the conflicts. @xref{Counterexamples}.
+Counterexamples take time to compute. The option @option{-rcex} should be
+used by the developer when working on the grammar; it hardly makes sense to
+use it in a CI.
+
@item all
Enable all the items.
@@ -15121,6 +15268,18 @@ Thus, if there is a rule which says that an integer
can be used as an
expression, integers are allowed @emph{anywhere} an expression is
permitted. @xref{Language and Grammar}.
+@item Counterexample
+A sequence of tokens and/or nonterminals, with one dot, that demonstrates a
+conflict. The dot marks the place where the conflict occurs.
+
+A @emph{unifying} counterexample is a single string that has two different
+parses; its existence proves that the grammar is ambiguous. When a unifying
+counterexample cannot be found in reasonable time, a @emph{nonunifying}
+counterexample is built: @emph{two} different string sharing the prefix up
+to the dot.
+
+@xref{Counterexamples}
+
@item Default reduction
The reduction that a parser should perform if the current parser state
contains no other action for the lookahead token. In permitted parser
@@ -15507,7 +15666,9 @@ London, Department of Computer Science, TR-00-12
(December 2000).
@c LocalWords: ResourceBundle myResources getString getName getToken ylwrap
@c LocalWords: getLocation getExpectedTokens reportSyntaxError bistromathic
@c LocalWords: TokenKind Automake's rtti Wcounterexamples Chinawat PLDI
-@c LocalWords: Isradisaikul
+@c LocalWords: Isradisaikul tcite pcite rgbGreen colorGreen rgbYellow Wcex
+@c LocalWords: colorYellow rgbRed colorRed rgbBlue colorBlue rgbPurple
+@c LocalWords: colorPurple ifhtml ifnothtml situ rcex
@c Local Variables:
@c ispell-dictionary: "american"