Any plan to support non-linux-kernel projects?

[FirstLoveLife]

Hi,

There are many projects like buildroot, which use kbuild.

Currently, kmax only supports linux kernel, any plan to support other projects?

[ChristianKaltenecker]

Hey :-)

I am currently also working on extracting models from other projects using kmax.
I may have figured out a way to do so by following the documentation in the Advanced Section.
First, use kextract and kclause to extract the model (as described in the advanced section).
Afterwards, you can use klocalizer via:
klocalizer --kextract <kextractFile> --kclause-formulas <kclauseFile> --save-smt busybox.smt
Note that you have to replace and by the path to the files that you have extracted previously using kextract and kclause.

I'm not sure if this is exactly what you want.

Moreover, I'm not sure if this is the intended way to use it.
Maybe @paulgazz can tell us more about that.

I'll test this setup also on other projects like buildroot.

Edit: It also works for buildroot. Just make sure that you set the BASE_DIR environment variable to output by executing export BASE_DIR=output on Linux.

[paulgazz]

Thanks @ChristianKaltenecker for looking into to buildroot! I had not tried it yet, but as you point out the individual CLI tools can (at least in principle) be used together to process other systems. @FirstLoveLife, check out @ChristianKaltenecker tips on buildroot and see the Advanced Section though these are around BusyBox. The high-level tools, like klocalizer call out to kextract, kclause, and kmax to process the kconfig and kbuild files (kmax is the one for kbuild), though klocalizer has built-in knowledge about Linux' directory structure, architectures, etc. and also handle the I/O between the pipeline of tools, which makes it easier to use.

Do @ChristianKaltenecker's instructions help solve your issue? If no, please say more about what projects (any others besides buildroot) and what you hoping to get as output specifically. Are you looking to get the formulas, do configuration localization, generate config file, something else? While we have been focused on Linux, it would be good to ultimately make the tools more robust and easy-to-use for other Kconfig/Kbuild projects as well, so your input will help guide that.

[FirstLoveLife]

@ChristianKaltenecker @paulgazz Thank you for your response! My apologies for the delayed reply. I will follow your suggestions, conduct some tests on my end, and provide an update on this issue later.

[FirstLoveLife]

With the guidance of @ChristianKaltenecker's instructions, I have successfully obtained buildroot.smt and busybox.smt.

Could you please advise me on how to use kismet with these projects? I would like to identify all unmet dependencies.

Another beginner question: What can be done with the xxx-project.smt files?

[paulgazz]

Great to hear! It should be possible to put the kextract and kclause output in a specific directory tree format to get ksimet to use it. This isn't a nice interface though (you can see it in the kismet code). Let me look into this more and see if I can improve the kismet interface to avoid having to do this.

The .smt files can be used with Z3 or other SMT solvers. kclause produces a model of valid configurations: when the formula is true, the configuration is valid (according to the kconfig specification). We use this in kismet by adding verification conditions that model in logic whether any two configurations options can be used to cause an unmet dependency. There are other applications, e.g., generating valid configurations (the klocalizer tool can do this). You could also check other behavior if you can model it with verification conditions.

[ekuiter]

Regarding the extraction and transformation of feature-model formulas, I have done a lot of work over at https://github.com/ekuiter/tseitin-or-not-tseitin to extract projects other than Linux (see https://github.com/ekuiter/tseitin-or-not-tseitin/blob/main/input/extract_ase22.sh), although this project is mostly specific to our ASE'22 paper.

I am currently working on a more generalized tool (https://github.com/ekuiter/torte) for feature-model extraction/transformation. It also supports kmax for a variety of projects (by adapting kextractor.c). For example, you can run

curl -sS https://raw.githubusercontent.com/ekuiter/torte/main/experiments/splc-2022-benchmark.sh > experiment.sh && bash experiment.sh

to extract feature-model histories for both Linux <= 4.17 and busybox.

Maybe this can help :)