• Martin Walch's avatar
    Kconfig: Remove bad inference rules expr_eliminate_dups2() · e9115030
    Martin Walch authored
    
    
    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.
    Signed-off-by: default avatarMartin Walch <walch.martin@web.de>
    Signed-off-by: default avatarMichal Marek <mmarek@suse.cz>
    e9115030
expr.c 24.1 KB