On Mon, 2014-09-22 at 19:13 +0200, Martin Walch wrote:
> expr_eliminate_dups2() in scripts/kconfig/expr.c applies two bad
> inference rules:
>
> (FOO || BAR) && (!FOO && !BAR) -> n
> (FOO && BAR) || (!FOO || !BAR) -> y
>
> They would be correct in propositional logic, but this is a three-valued
> logic, and here it is wrong in that it changes semantics. It becomes
> immediately visible when substituting FOO and BAR with m.
Well, not to me. When I apply the rules under "Menu dependencies" in
Documentation/kbuild/kconfig-language.txt, in embarrassingly small
steps, I get:
(m || m) && (!m && !m) ->
(1 || 1) && ((2 - 1) && (2 - 1)) ->
(1 || 1) && (1 && 1) ->
max(1, 1) && min(1, 1) ->
1 && 1 ->
min(1, 1) ->
1 -> m
and
(m && m) || (!m || !m) ->
(1 && 1) || ((2 - 1) || (2 - 1)) ->
(1 && 1) || (1 || 1) ->
min(1, 1) || max(1, 1) ->
1 || 1 ->
max(1, 1) ->
1 -> m
Did I do that right? Anyway, perhaps you'd like to add a line or two how
these two expressions actually evaluate when FOO and BAR are m.
> Fix it by removing expr_eliminate_dups2() and the functions that have no use
> anywhere else: expr_extract_eq_and(), expr_extract_eq_or(),
> and expr_extract_eq() from scripts/kconfig/expr.[ch]
>
> Currently the bug is not triggered in mainline, so this patch does not modify
> the configuration space there.
>
> As a side effect, this reduces code size in expr.c by roughly 10% and slightly
> improves startup time for all configuration frontends.
>
> Signed-off-by: Martin Walch <[email protected]>
Does Yann still care about Kconfig? Yann has been rather quiet for a
while now.
Paul Bolle
CC: Michal added
Paul Bolle <[email protected]> writes:
> On Mon, 2014-09-22 at 19:13 +0200, Martin Walch wrote:
>> expr_eliminate_dups2() in scripts/kconfig/expr.c applies two bad
>> inference rules:
>>
>> (FOO || BAR) && (!FOO && !BAR) -> n
>> (FOO && BAR) || (!FOO || !BAR) -> y
>>
>> They would be correct in propositional logic, but this is a three-valued
>> logic, and here it is wrong in that it changes semantics. It becomes
>> immediately visible when substituting FOO and BAR with m.
>
> Well, not to me. When I apply the rules under "Menu dependencies" in
> Documentation/kbuild/kconfig-language.txt, in embarrassingly small
> steps, I get:
> (m || m) && (!m && !m) ->
> (1 || 1) && ((2 - 1) && (2 - 1)) ->
> (1 || 1) && (1 && 1) ->
> max(1, 1) && min(1, 1) ->
> 1 && 1 ->
> min(1, 1) ->
> 1 -> m
>
> and
> (m && m) || (!m || !m) ->
> (1 && 1) || ((2 - 1) || (2 - 1)) ->
> (1 && 1) || (1 || 1) ->
> min(1, 1) || max(1, 1) ->
> 1 || 1 ->
> max(1, 1) ->
> 1 -> m
>
> Did I do that right? Anyway, perhaps you'd like to add a line or two how
> these two expressions actually evaluate when FOO and BAR are m.
Perhaps, it helps to use a Kconfig file that visualizes the problem:
mainmenu "Expr Test"
config expr-config
bool "Expr Config"
depends on (m || m) && (!m && !m)
# depends on (m && m) || (!m || !m)
config dummy
bool "Dummy"
config modules
bool
option modules
default y
Those two depends, according to your calculation and if I understood
correctly also to Martin's, should evaluate to 'm' and thus the menu
entry should always be visible, because both depends should evaluate to
'm'. But because of expr_eliminate_dups2() it is either invisible (the
first depends becomes 'n') or always visible (the second depends becomes
'y').
Dirk
>> Fix it by removing expr_eliminate_dups2() and the functions that have no use
>> anywhere else: expr_extract_eq_and(), expr_extract_eq_or(),
>> and expr_extract_eq() from scripts/kconfig/expr.[ch]
>>
>> Currently the bug is not triggered in mainline, so this patch does not modify
>> the configuration space there.
>>
>> As a side effect, this reduces code size in expr.c by roughly 10% and slightly
>> improves startup time for all configuration frontends.
>>
>> Signed-off-by: Martin Walch <[email protected]>
>
> Does Yann still care about Kconfig? Yann has been rather quiet for a
> while now.
>
>
> Paul Bolle
>
> --
> To unsubscribe from this list: send the line "unsubscribe linux-kbuild" in
> the body of a message to [email protected]
> More majordomo info at http://vger.kernel.org/majordomo-info.html
On Tuesday 07 October 2014 11:21:51 Dirk Gouders wrote:
> Paul Bolle <[email protected]> writes:
>
> > On Mon, 2014-09-22 at 19:13 +0200, Martin Walch wrote:
> >> expr_eliminate_dups2() in scripts/kconfig/expr.c applies two bad
> >> inference rules:
> >>
> >> (FOO || BAR) && (!FOO && !BAR) -> n
> >> (FOO && BAR) || (!FOO || !BAR) -> y
> >>
> >> They would be correct in propositional logic, but this is a three-valued
> >> logic, and here it is wrong in that it changes semantics. It becomes
> >> immediately visible when substituting FOO and BAR with m.
> >
> > Well, not to me. When I apply the rules under "Menu dependencies" in
> > Documentation/kbuild/kconfig-language.txt, in embarrassingly small
> > steps, I get:
> > (m || m) && (!m && !m) ->
> > (1 || 1) && ((2 - 1) && (2 - 1)) ->
> > (1 || 1) && (1 && 1) ->
> > max(1, 1) && min(1, 1) ->
> > 1 && 1 ->
> > min(1, 1) ->
> > 1 -> m
> >
> > and
> > (m && m) || (!m || !m) ->
> > (1 && 1) || ((2 - 1) || (2 - 1)) ->
> > (1 && 1) || (1 || 1) ->
> > min(1, 1) || max(1, 1) ->
> > 1 || 1 ->
> > max(1, 1) ->
> > 1 -> m
> >
> > Did I do that right? Anyway, perhaps you'd like to add a line or two how
> > these two expressions actually evaluate when FOO and BAR are m.
Yes, this is a proper evaluation.
To explain the problem in more detail, I will describe it a bit more formal.
First of all, this is a thing about the formal system of the configuration
logic, so I think it is a good idea to distinguish between syntax and
semantics.
Any expression, e.g. "(FOO || BAR)" is pure syntax. It consists of
non-constant symbols (FOO, BAR...), constant symbols (n, m, y),
operators (||, &&, !), and parenthesis.
Semantics is when evaluating an expression by assigning values to the
constant and the non-constant symbols and functions to the operators
(overriding operator precedence with parenthesis), and then calculating
an actual value.
So, this is pure syntax:
(FOO || BAR) && (!FOO && !BAR)
And semantics is:
* an assignment of 0, 1, or 2 to each of the non-constant symbols (arbitrary)
* the fixed assignments of 0 to n, 1 to m, and 2 to y
* applying the functions to values that correspond to the respective operators
So, e.g. when assigning 2 to FOO and 0 to BAR, then the evaluation of
(FOO || BAR) && (!FOO && !BAR)
is
min(max(2, 0), min(2-2, 2-0)) = 0
Above, we saw that assigning 1 to FOO as well as to BAR yields 1 for the
whole expression.
Now getting back to the problem: the configuration system makes some
syntactical transformations according to some rules, so they are easier to
read in the user interfaces (e.g. mconf). In formal logic, such rules are
called "inference rules". Obviously, inference rules are purely syntactical
transformations, e.g. one rule could be to replace "FOO && FOO" with only
"FOO". Another rule could replace "FOO || BAR" with "FOO && BAR". The
difference between these two example rules is that in semantics, the first
one keeps the result of the evaluation for all possible assignments, while
the second one changes the results for some of the assignments. Formally,
the first rule is "valid" while the second one is not.
With the term "valid" it is now easy to summarize the actual problem:
The inference rule
(FOO || BAR) && (!FOO && !BAR) -> n
is not valid. The proof for this is assigning 1 to FOO and also to BAR.
As we have already seen, for this assignment, the expression evaluates to 1.
In contrast, the expression "n" always evaluates to 0. So, this inference
rule is not valid.
> Perhaps, it helps to use a Kconfig file that visualizes the problem:
>
> mainmenu "Expr Test"
>
> config expr-config
> bool "Expr Config"
> depends on (m || m) && (!m && !m)
> # depends on (m && m) || (!m || !m)
>
> config dummy
> bool "Dummy"
>
> config modules
> bool
> option modules
> default y
>
> Those two depends, according to your calculation and if I understood
> correctly also to Martin's, should evaluate to 'm' and thus the menu
> entry should always be visible, because both depends should evaluate to
> 'm'. But because of expr_eliminate_dups2() it is either invisible (the
> first depends becomes 'n') or always visible (the second depends becomes
> 'y').
This is a good idea. However, I tried to avoid an example that contains
the constant symbol "m". The problem with this is that "m" is treated
specially and can lead to some confusion, although a very short test case is
possible using m:
config expr-config-short
bool "Expr Config Short"
depends on m && !m
When this file is read, each of the two "m" symbols is replaced with
"m && MODULES", so the expression reads:
(m && MODULES) && !(m && MODULES)
then the negation of "!(m && MODULES)" is transformed:
(m && MODULES) && (!m || !MODULES)
(this corresponds to one of the "De Morgan's laws" in other logical systems)
Finally, the bad inference rule applies (although the form of the expression is
slightly different from above) and this expression is replaced with:
n
This is not valid (assigning 2 to MODULES should yield 1 for the whole
expression, but "n" evaluates to 0).
Does this make things clearer?
Regards,
Martin Walch
--