Kmax Tool Suite v4.1-rc2

This update adds the new kextract version's source files to MANIFEST.in, which is necessary for creating a working distribution for pypi.

Kmax Tool Suite v4.1-rc1

This version introduces a new tool, koverage, which measures how much
a configuration file covers a given patch file. It also includes
support for the build system code cache for kismet. The automatic
selection of the kextractor version been improved and a version of
kextractor for another older version of the Kconfig parser has been
added as well.

Kmax Tool Suite v4.0

Version 4.0 introduces a new tool, called krepair, that is integrated into the klocalizer tool. Used with klocalizer --repair .config --include-mutex patch.diff, krepair will take an existing .config file and modify it to build the changes in the given patch file, typically with relatively few changes to the .config file (100-200 on average). klocalizer can also take some additional constraints: see klocalizer -h for --include-mutex, --include, and --exclude for more information, as well as docs/advanced.md for an example.

This version also fixes some bugs in the kmax Makefile analyzer and greatly improves the klocalizer driver. klocalizer integrates the use of SuperC to gather per-line file constraints. Additionally, The documentation for installing and using klocalizer, krepair, and kismet tool (introduced in version 3.0) are greatly improved, with relatively few steps to get the tool suite and its dependencies, including SuperC, installed and ready for use.

Kmax Tool Suite v4.0-rc1

This version includes krepair and updated documentation.

Kmax Tool Suite v3.0

Version 3.0 version introduces a new tool, kismet, as well as several updates, fixes, and features. Here is an overview of the changes/additions:

• The kismet tool and documentation. kismet finds unmet dependency bugs in Kconfig files using static analysis based on kclause's logical model of Kconfig files.

• There is a listing of Kconfig unmet dependency bugs found by kismet so far as well as a replication script for experiments with it.

• There are several fixes to the kclause tool, including support for the handling of non-Boolean option visibility which greatly improved kismet precision when generating configuration files.

• klocalizer now has the ability to check for and download already-generated kclause formula caches to quickly boostrap configuration localization.

• klocalizer can now take arbitrary z3 constraints, which used by kismet for proving verification conditions.

• There is new kextractor python module for more recent version of the Kconfig parser.

• The repository now supports using python 3.8.

• The tooling has been refactored and has common Kconfig and Linux source handling code in libraries.

Kmax Tool Suite v2.3

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.

Kmax Tool Suite v2.2

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.

Kmax Tool Suite v2.1

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.

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.

Kmax Tool Suite v2.0-rc19

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