Kconfig: Remove bad inference rules expr_eliminate_dups2()

PATCH Superseded Martin Walch 2 participants 6 messages May 17, 2015 – May 25, 2015

Subsystems (2)

Kbuild Kconfig

lore

Share & tools

lore

Martin Walch

author

2015-05-17 02:14 UTC #0 lore raw

PATCH v3 1/1 Kconfig: Remove bad inference rules expr_eliminate_dups2()

From: Martin Walch <[email protected]>

expr_eliminate_dups2() in scripts/kconfig/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 scripts/kconfig/expr.c

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]>

---
Version 3:
Earlier versions fixed some comments, too. Remove those bits and focus on the logical problem.

 scripts/kconfig/expr.c | 111 -------------------------------------------------
 1 file changed, 111 deletions(-)

scripts/kconfig/expr.c +0 ~~-111~~

index fb0a2a2..0d7364c 100644
@@ -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;

Signature · 1 line

2.0.5

Michal Marek

2015-05-18 07:36 UTC #1 lore raw

Dne 17.5.2015 v 10:14 Martin Walch napsal(a):

Quoted 15 lines

From: Martin Walch <[email protected]>
expr_eliminate_dups2() in scripts/kconfig/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

Quoted 6 lines

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.

Are you able to construct a testcase that triggers this bug? I haven't been successful:

$ cat Kconfig.test
config MODULES
	def_bool y
	option modules

config FOO
def_tristate m

config BAR
def_tristate m

config TEST1

	def_tristate (FOO || BAR) && (!FOO && !BAR)

if TEST1 != m
comment "TEST1 broken"
endif

config TEST2

	def_tristate (FOO && BAR) || (!FOO || !BAR)

if TEST2 != m
comment "TEST2 broken"
endif

$ ./scripts/kconfig/conf Kconfig.test && cat .config
*
* Linux Kernel Configuration
*
#
# configuration written to .config
#
#
# Automatically generated file; DO NOT EDIT.
# Linux Kernel Configuration
#
CONFIG_MODULES=y
CONFIG_FOO=m
CONFIG_BAR=m
CONFIG_TEST1=m
CONFIG_TEST2=m

I'm all for eliminating unneeded code, but if it's meant to fix a bug as well, I'd like to understand the bug.

thanks,
Michal

Martin Walch

author

2015-05-18 09:38 UTC #2 lore raw

Quoted 5 lines · On Monday 18 May 2015 15:36:03 Michal Marek wrote:

Are you able to construct a testcase that triggers this bug? I haven't been successful:
[..]
config TEST1
	def_tristate (FOO || BAR) && (!FOO && !BAR)

This does not trigger the bug, because expr_eliminate_dups is only applied to dependencies, but not to the expressions of default values.

I modified your example a bit, so that the bug becomes apparent:

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

As you can see, I also added a third symbol TEST3 with a line

Quoted 1 line

depends on m && !m

This case is special: m && !m 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.

Regards,
Martin Walch

Michal Marek

2015-05-21 06:39 UTC #3 lore raw

Dne 18.5.2015 v 17:38 Martin Walch napsal(a):

Quoted 11 lines · On Monday 18 May 2015 15:36:03 Michal Marek wrote:

Quoted 5 lines
Are you able to construct a testcase that triggers this bug? I haven't been successful:
[..]
config TEST1
	def_tristate (FOO || BAR) && (!FOO && !BAR)
This does not trigger the bug, because expr_eliminate_dups is only applied to dependencies, but not to the expressions of default values.
I modified your example a bit, so that the bug becomes apparent:

Thanks, now I can reproduce it as well. Would you be so kind add this reproducer to the changelog?

Thanks,
Michal

Martin Walch

author

2015-05-22 11:41 UTC #4 lore raw

PATCH v4 1/1 Kconfig: Remove bad inference rules expr_eliminate_dups2()

From: Martin Walch <[email protected]>

expr_eliminate_dups2() in scripts/kconfig/expr.c applies two invalid inference rules:

(FOO || BAR) && (!FOO && !BAR) -> n
(FOO && BAR) || (!FOO || !BAR) -> y

(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 scripts/kconfig/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 <[email protected]>

---
Version 3:
Earlier versions fixed some comments, too. Remove those bits and focus on the logical problem.

Version 4:
Add test case to commit description.

 scripts/kconfig/expr.c | 111 -------------------------------------------------
 1 file changed, 111 deletions(-)

scripts/kconfig/expr.c +0 ~~-111~~

index fb0a2a2..0d7364c 100644
@@ -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;

Signature · 1 line

2.0.5

Michal Marek

Applied

2015-05-25 08:05 UTC #5 lore raw

Dne 22.5.2015 v 19:41 Martin Walch napsal(a):

Quoted 78 lines

From: Martin Walch <[email protected]>
expr_eliminate_dups2() in scripts/kconfig/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 scripts/kconfig/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.

Quoted 8 lines

Signed-off-by Martin Walch <[email protected]>
---
Version 3:
Earlier versions fixed some comments, too. Remove those bits and focus on the logical problem.
Version 4:
Add test case to commit description.

Thanks, applied now!

Michal