Kmax Tool Suite v2.0

Version 2.0 includes a suite of tools for processing Kconfig and Kbuild files, including the original kmax tool for Kbuild Makefiles as well kextract and kclause for Kconfig files and klocalizer for localizing Makefile configurations.

Here is a summary of additions and changes:

• kmaxtools is now a stand-alone python program with easy installation via setuptools. kmaxtools is also hosted on PyPi and can be installed via pip.

• Z3 is used for processing Boolean formulas in addition to BDDs in kmax. Z3 provides better heuristics for simplifying formulas as well as fast and human-readable representations for reading and writing formulas. BDD provides faster satisfiability checking for kmax. BDD support uses a python library dd, instead of pycudd, which required users to download compile the C library.

• kmax analyzes Kbuild Makefiles to determine the Boolean constraints of configuration options required to build each compilation unit. There have been various improvements, including the inclusion of architecture-specific directories specified in the top-level Makefiles in the arch/ directories.

• kextract extracts Kconfig specifications and kclause interprets the specifications as Boolean formulas, supporting both Z3 and DIMACS backends. There have been various incremental improvements to the formula extraction and modeling in this version.

• klocalizer combines kmax and kclause formulas to model the valid configurations under which compilation units are built by Kbuild. Various features have been added to klocalizer, such as generating a sample of configurations and approximating existing configurations.

• There are instructions for all tools with several examples of usage.

• There are new test cases for kmax and kclause.

• There are scripts that run kmax, kclause, and klocalizer on the Linux kernel source code.