Support kconfirm-smt

[julianbraha]

Closes #7

[ekuiter]

Hi Julian,

thanks a lot for your contribution! I am intrigued and have lots of thoughts on this, so bear with me :)

Regarding kconfirm and KConfig parsing:

• If I understand correctly, kconfirm uses Mcdostone/nom-kconfig for KConfig parsing. Does this parser attempt to always target the latest Linux kernel version? Or does it retroactively support older versions? The README states:

  This parser has been tested on the Linux kernel repository from 2.6.11 to 6.4.9 (3733 versions).

  So I assume that it does not target the latest version (although according to your patch series on LKML you seem to be working on the latest version)? I ask because the parser has changed a lot over time, with several incompatible changes (see the Bachelor thesis of my student Taylan Karakaya, which was one of the major challenges I address with torte).

• Also, do you have any experience or plans to in the future apply kconfirm on systems other than Linux (I see that you made some hacks regarding Linux in https://github.com/julianbraha/kconfirm/tree/main/kconfirm-linux)? According to the README of nom-kconfig it even supports KConfigLib:

  There are cargo features for glob-wildcard (used by coreboot, for example) and kconfiglib compatibility.

  Another student of mine, Ljubica Ðorđević, studied the extensions KConfiglib makes and how to rephrase them in LKC's KConfig dialect. It would be great if we could skip all this in the future, and just use a parser that directly accepts KConfigLib syntax.

As for kconfirm-smt:

It's a great idea. A better integration of automated reasoning techniques with KConfig (ideally actively maintained in the kernel tree) is sorely needed, and something that we as the product line research community would love to see (and potentially willing to contribute to, if you're familiar with the kconfig-sat project), because it would reduce a lot of the existing friction in evaluating novel bug-finding approaches etc. I have a few questions:

• What were the results of your "differential tests" noted in your README file (so how accurate is your tool)? My student Nawar Baddour did something similar in his Bachelor thesis (not published yet) for SAT/Kismet with mixed results (mostly missing information due to non-Boolean/SMT level information).
• What was your motivation to integrate kconfirm-smt with torte, do you use it for any specific purpose?
• Did you test your integration of kconfirm-smt in torte? (I currently have no time to test/review your pull request in depth, but will probably have some time in September to do that.) The whole tool is currently structured around SAT-based tooling, so I guess it is currently mostly useful to batch-automate extraction of .smt2 files for many Linux versions.

Regarding the integration of kconfirm[-smt] in the kernel:

I see on LKML that you are currently pretty actively working on KConfig.

• Do you know what the status of your RFC/patch is? Is the goal still to merge kconfirm[-smt] into the kernel? I ask because over the years, there were multiple attempts to merge SAT assistance for KConfig into the kernel (never SMT-based though). So far, none of them were successful, unfortunately, but never say never.
• Was there a specific motivation why you used Rust instead of using the existing LKC parser written in C?
• Finally, what are your experiences with the performance of SMT/Z3? After all, this is one of the main concerns why the product line research community tends to focus on SAT. Especially for model counting/#SAT-based analyses, I imagine that SMT will perform relatively poorly, but simple consistency checks would already be a great benefit.

Regarding KConfig's future in general:

I also saw you mentioning that you want to build more tooling around KConfig, that you plan to give a talk at LPC, and your involvement in the work of J. Oh and Philipp Schubert (and possibly Paul as your supervisor?). Especially your talk abstract very closely aligns to some things I have been working on (together with the students mentioned above).

• Are you aware of my datasets on KConfig (https://elias-kuiter.de/torte-research/)? Or do you have your own data for the LPC talk? I would be very interested in collaborating on this. In particular, what we are looking for is a somewhat complete list of KConfig implementations and consumers/systems (which is what I'm trying to build with torte-research), and then work on tooling which can handle all are most different dialects to analyze various consumers. torte is already a move in that direction, for retroactive analysis - but as you can probably see, it is all a bit messy and needs some strategic alignment in the future.
• Do you happen to know UVL (the Universal Variability Language)? If not, this is a language proposed by my research institute (among others) to model configuration options and their dependencies. UVL has been quite successful among researchers and some practitioners. While I do not imagine the Linux kernel moving away from KConfig soon, having a somewhat reliable way to translate KConfig into UVL (and then apply all the helpful analyses research proposed over the last ~20 years) would be valuable both to researchers and kernel developers. UVL supports different language levels which roughly map to SAT and SMT as reasoning backends underneath.

So as you can see, I have lots of potential discussion points. :-)
Feel free to answer here or via email, I am fine with both public and private discussion.
If you're interested, we could also meet up online.
In the meantime, I will have a look at the pull request itself.

Best, Elias

[julianbraha]

Hi Elias,

kconfirm (as in the main branch) is a heuristics-based static checker. It does not yet use any feature model. This is (close to) the version that would be upstreamed into Linux, if accepted.
The patch-set is currently on v4, now using the in-tree parser, and no longer an RFC:
https://lore.kernel.org/all/20260727001623.2794156-1-julianbraha@gmail.com/

In the future, I plan to integrate kconfirm's checks with my kconfirm-smt model.

The version in the main branch still uses the nom-kconfig parser, and it supports coreboot, u-boot, busybox, and others (the Linux-specific hacks are only used when running it with Linux). I haven't yet tested that with the kconfiglib extension. My motivation for using nom-kconfig was for its support of multiple different Kconfig dialects.

Also, yes the nom-kconfig parser always attempts to support the latest version of Linux; I think the README is outdated.

The differential tests on kconfirm-smt have reported success for about 10,000 runs in each direction. However, that's not really a representative sample of all configurations...

I'll contact you privately :)