Symbolic build constraints evaluator

[Paul]

Hi all,

I'm new to the list, but am interested in helping out. I'd like to bring attention to a tool that can produce a symbolic Boolean expression describing the constraints of each compilation unit from Kbuild Makefiles. It's a python tool called Kmax and it uses static analysis backed by z3.

I've spent some time making it easier to install and use with python setuptools and the latest version can be found here: https://github.com/paulgazz/kmax/

The complete output from Kmax for Linux v5.3.11 (x86) can be found here: https://drive.google.com/file/d/1q7dDzOvEKWUi7FlZ2YixValV6xlkq1yY/view?usp=sharing There are two files, unit_pc and full_pc. unit_pc contains the symbolic constraints for each .o file and subdirectory, while full_pc combines them to yield the complete symbolic constraint for a given .o file including all of its parent directories.

I'm curious about what the next most useful application of this would be for developers/maintainers. Any opinions on what to tackle next?

While Kmax is not for Kconfig per se, I'm thinking there would be some useful combinations with a SAT-based (or z3-based) Kconfig. I've got a (rough) tool for converting kconfig to dimacs or a z3 model here (along the lines of LVAT or KconfigReader), but it's not quite ready for primetime: https://github.com/paulgazz/kclause

Here is a small example what Kmax produces. This Kbuild Makefile snippet

obj-y := fork.o
ifeq ($(CONFIG_A),y)
BITS := 32
else
BITS := 64
endif
obj-$(CONFIG_B) += probe_$(BITS).o

will produce this output

unit_pc tests/probe_64.o ((! CONFIG_A) && CONFIG_B)
unit_pc tests/probe_32.o (CONFIG_A && CONFIG_B)
unit_pc tests/fork.o 1

Best,
Paul
https://paulgazzillo.com/