ConfigFix extracts unsatisfiable formulas on recent versions

[ekuiter]

Hi!

I have recently integrated ConfigFix into my tool torte, so I can compare it to KConfigReader and KClause and possibly adapt it to other systems/versions.

Unfortunately ConfigFix is not applicable to the most recent Linux versions anymore. Starting with Linux v6.16, the extracted formula is not satisfiable. I tested with multiple CNF transformations (including the one integrated in ConfigFix) and SAT solvers: 6.17.zip

I reduced the formula to the unsatisfiable core, finding that the following is not satisfiable:

c transform-to-dimacs-with-kconfigreader/extract-kconfig-models-with-configfix/linux/v6.17[x86].dimacs
c 1 ARCH_FORCE_MAX_ORDER_NPC
c 2 ARCH_FORCE_MAX_ORDER_0
c 3 PAGE_BLOCK_MAX_ORDER_n
c 4 PAGE_BLOCK_MAX_ORDER_0
c 5 PAGE_BLOCK_MAX_ORDER_1
c 6 PAGE_BLOCK_MAX_ORDER_10
p cnf 75888 308209
1 0
-2 -1 0
-3 0
2 -4 0
2 -5 0
2 -6 0
3 4 5 6 0

The relevant KConfig code is here: https://elixir.bootlin.com/linux/v6.17/source/mm/Kconfig#L1007

I am no expert when it comes to how ConfigFix encodes prompt/visibility conditions and non-Boolean feature values. Can you tell me what is going on here? It seems that this is either a bug in ConfigFix that wasn't triggered in earlier versions, or that the semantics of KConfig have had a breaking change since Linux 6.15.

Looking forward to your feedback!