Kmax Tool Suite v2.0-rc12

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.

Kmax Tool Suite v2.0-rc11

Add the klocalizer tool for creating a configuration for a given compilation unit. This version merges kmax, kclause, and klocalizer into a single installable project. The version has a number of improvements to the formulas generated by kmax and kclause and adds support for multiple architectures to klocalizer.

Kmax v2.0-rc5

This version adds back in BDD support, dramatically improving performance. Linux 5.3.11 takes 6 minutes instead of 4 hours. Z3 is still used, because it is faster to write out the resulting formulas, since it avoids exhaustive enumeration of the solutions.

Kmax v2.0-rc3

This version removes the dependency of pycudd, relying entirely on z3.

Kmax v2.0-rc2

This version of Kmax converts the repository into a stand-alone python project. Removed are the Kconfig analyses and experiments, which can be found in older versions of Kmax.

Kmax v2.0-rc1

This version of Kmax includes several new features and improvements:

• Integration with z3 instead of BDDs. This enables Kmax to more efficiently work with Boolean expressions and use better simplification tactics. Special thanks to ThanhVu Nguyen for helping integrate z3 into Kmax.
• A new tool called Kclause, which translates Kconfig specifications to Boolean expressions. This has both BDD and z3 backends. Special thanks to Jeho Oh for spending time to work on Kconfig's semantics.
• There are many more test cases for both Kmax and Kclause in tests/
• Documentation is somewhat improved in README.md to make it easier to run Kmax on the whole Linux kernel.

Kmax v1.1

Kmax's Kconfig parser has been updated with the one found in Linux v4.12.8.

There are also improvements to the installation instructions.

Kmax v1.0

This is the first version of Kmax and the one used for evaluation in the ESEC/FSE '17 paper.