Kmax

Version 2.3 includes a number of bug-fixes, documentation improvements, additional scripting, polished support for Linux experiments, support in klocalizer for verification of Kconfig files, and results from bug reporting and patching to Linux.

Version 2.2 adds support in kextractor for prior versions of Kconfig, selectable on the command-line. It also improves how the --version flag is handled and adds a quiet mode for klocalizer and kclause.

Version 2.1 ports kmaxtools to python 3 and retains support for python 2. There are also improvements to the documentation with a simpler "getting started" section, and detailed information has been moved to the docs/ directory.

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.

This release improves the constraints, adds sampling, fixes bugs, and improves usability
- Added additional constraints in klocalizer that disable configuration options used in a compilation unit's constraints but are not declared in the given architecture.
- Fixed issue in kbuild file processing where src and srctree variables are needed
- Fixed scalability issue with hoisting in kmax by trimming infeasible paths
- Support generating multiple satisfying configurations, i.e., a sample, using a random seed.
- Various improvements to the README.md
- klocalizer will now use the type of the configuration option to generate appropriate settings in the .config file, in particular non-Boolean types
- Added build instructions for kconfig_extractor, needed for kclause
- More test cases are now supported, specifically those where the .config has non-Booleans
- Added link to cached formulas to tool usage instructions
- Added more experimental results and documentation

Kmax now extracts top-level architecture-specific directories.
Previously, all top-level directories were assumed to be always
included, but some architcture-specific directories, e.g., with
core-y, are configurable. So this version also collects
subdirectories from these other Kbuild variables and adds them to the
Kmax formulas.