Kconfig: Remove bad inference rules expr_eliminate_dups2()

expr_eliminate_dups2() in config/expr.c applies two invalid
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 assigning the value 1 to both, FOO and BAR:

(FOO || BAR) && (!FOO && !BAR)
-> min(max(1, 1), min(2-1, 2-1)) = min(1, 1) = 1

while n evaluates to 0 and

(FOO && BAR) || (!FOO || !BAR)
-> max(min(1, 1), max(2-1, 2-1)) = max(1, 1) = 1

with y evaluating to 2.

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 config/expr.c

Currently the bug is not triggered in mainline, so this patch does not
modify the configuration space there. To observe the bug consider this
example:

config MODULES
        def_bool y
        option modules

config FOO
        def_tristate m

config BAR
        def_tristate m

config TEST1
        def_tristate y
        depends on (FOO || BAR) && (!FOO && !BAR)

if TEST1 = n
comment "TEST1 broken"
endif

config TEST2
        def_tristate y
        depends on (FOO && BAR) || (!FOO || !BAR)

if TEST2 = y
comment "TEST2 broken"
endif

config TEST3
        def_tristate y
        depends on m && !m

if TEST3 = n
comment "TEST3 broken"
endif

TEST1, TEST2 and TEST3 should all evaluate to m, but without the patch,
none of them does. It is probably not obvious that TEST3 is the same bug,
but it becomes clear when considering what happens internally to the
expression
m && !m":
First it expands to
(m && MODULES) && !(m && MODULES),
then it is transformed into
(m && MODULES) && (!m || !MODULES),
and finally due to the bug it is replaced with n.

As a side effect, this patch reduces code size in expr.c by roughly 10%
and slightly improves startup time for all configuration frontends.

Signed-off-by: Martin Walch <walch.martin@web.de>
Signed-off-by: Michal Marek <mmarek@suse.cz>
Signed-off-by: Christian Lamparter <chunkeey@googlemail.com>

diff --git a/config/expr.c b/config/expr.c
index fb0a2a286dca6a8b0cc0c74deb5d23096be096c3..0d7364ce9132f2c67f489203867b9d623c1148e2 100644 (file)
--- a/config/expr.c
+++ b/config/expr.c
@@ -13,9 +13,6 @@
 
 static int expr_eq(struct expr *e1, struct expr *e2);
 static struct expr *expr_eliminate_yn(struct expr *e);
-static struct expr *expr_extract_eq_and(struct expr **ep1, struct expr **ep2);
-static struct expr *expr_extract_eq_or(struct expr **ep1, struct expr **ep2);
-static void expr_extract_eq(enum expr_type type, struct expr **ep, struct expr **ep1, struct expr **ep2);
 
 struct expr *expr_alloc_symbol(struct symbol *sym)
 {
@@ -559,62 +556,6 @@ static void expr_eliminate_dups1(enum expr_type type, struct expr **ep1, struct
 #undef e2
 }
 
-static void expr_eliminate_dups2(enum expr_type type, struct expr **ep1, struct expr **ep2)
-{
-#define e1 (*ep1)
-#define e2 (*ep2)
-       struct expr *tmp, *tmp1, *tmp2;
-
-       if (e1->type == type) {
-               expr_eliminate_dups2(type, &e1->left.expr, &e2);
-               expr_eliminate_dups2(type, &e1->right.expr, &e2);
-               return;
-       }
-       if (e2->type == type) {
-               expr_eliminate_dups2(type, &e1, &e2->left.expr);
-               expr_eliminate_dups2(type, &e1, &e2->right.expr);
-       }
-       if (e1 == e2)
-               return;
-
-       switch (e1->type) {
-       case E_OR:
-               expr_eliminate_dups2(e1->type, &e1, &e1);
-               // (FOO || BAR) && (!FOO && !BAR) -> n
-               tmp1 = expr_transform(expr_alloc_one(E_NOT, expr_copy(e1)));
-               tmp2 = expr_copy(e2);
-               tmp = expr_extract_eq_and(&tmp1, &tmp2);
-               if (expr_is_yes(tmp1)) {
-                       expr_free(e1);
-                       e1 = expr_alloc_symbol(&symbol_no);
-                       trans_count++;
-               }
-               expr_free(tmp2);
-               expr_free(tmp1);
-               expr_free(tmp);
-               break;
-       case E_AND:
-               expr_eliminate_dups2(e1->type, &e1, &e1);
-               // (FOO && BAR) || (!FOO || !BAR) -> y
-               tmp1 = expr_transform(expr_alloc_one(E_NOT, expr_copy(e1)));
-               tmp2 = expr_copy(e2);
-               tmp = expr_extract_eq_or(&tmp1, &tmp2);
-               if (expr_is_no(tmp1)) {
-                       expr_free(e1);
-                       e1 = expr_alloc_symbol(&symbol_yes);
-                       trans_count++;
-               }
-               expr_free(tmp2);
-               expr_free(tmp1);
-               expr_free(tmp);
-               break;
-       default:
-               ;
-       }
-#undef e1
-#undef e2
-}
-
 struct expr *expr_eliminate_dups(struct expr *e)
 {
        int oldcount;
@@ -627,7 +568,6 @@ struct expr *expr_eliminate_dups(struct expr *e)
                switch (e->type) {
                case E_OR: case E_AND:
                        expr_eliminate_dups1(e->type, &e, &e);
-                       expr_eliminate_dups2(e->type, &e, &e);
                default:
                        ;
                }
@@ -829,57 +769,6 @@ bool expr_depends_symbol(struct expr *dep, struct symbol *sym)
        return false;
 }
 
-static struct expr *expr_extract_eq_and(struct expr **ep1, struct expr **ep2)
-{
-       struct expr *tmp = NULL;
-       expr_extract_eq(E_AND, &tmp, ep1, ep2);
-       if (tmp) {
-               *ep1 = expr_eliminate_yn(*ep1);
-               *ep2 = expr_eliminate_yn(*ep2);
-       }
-       return tmp;
-}
-
-static struct expr *expr_extract_eq_or(struct expr **ep1, struct expr **ep2)
-{
-       struct expr *tmp = NULL;
-       expr_extract_eq(E_OR, &tmp, ep1, ep2);
-       if (tmp) {
-               *ep1 = expr_eliminate_yn(*ep1);
-               *ep2 = expr_eliminate_yn(*ep2);
-       }
-       return tmp;
-}
-
-static void expr_extract_eq(enum expr_type type, struct expr **ep, struct expr **ep1, struct expr **ep2)
-{
-#define e1 (*ep1)
-#define e2 (*ep2)
-       if (e1->type == type) {
-               expr_extract_eq(type, ep, &e1->left.expr, &e2);
-               expr_extract_eq(type, ep, &e1->right.expr, &e2);
-               return;
-       }
-       if (e2->type == type) {
-               expr_extract_eq(type, ep, ep1, &e2->left.expr);
-               expr_extract_eq(type, ep, ep1, &e2->right.expr);
-               return;
-       }
-       if (expr_eq(e1, e2)) {
-               *ep = *ep ? expr_alloc_two(type, *ep, e1) : e1;
-               expr_free(e2);
-               if (type == E_AND) {
-                       e1 = expr_alloc_symbol(&symbol_yes);
-                       e2 = expr_alloc_symbol(&symbol_yes);
-               } else if (type == E_OR) {
-                       e1 = expr_alloc_symbol(&symbol_no);
-                       e2 = expr_alloc_symbol(&symbol_no);
-               }
-       }
-#undef e1
-#undef e2
-}
-
 struct expr *expr_trans_compare(struct expr *e, enum expr_type type, struct symbol *sym)
 {
        struct expr *e1, *e2;