<!-- START doctoc generated TOC please keep comment here to allow auto update -->
<!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
- [The kmax tool suite](#the-kmax-tool-suite)
- [Getting started](#getting-started)
- [Installing the kmax tool suite](#installing-the-kmax-tool-suite)
- [Kicking the tires](#kicking-the-tires)
- [Using `klocalizer --repair` on patches](#using-klocalizer---repair-on-patches)
- [Using `koverage`](#using-koverage)
- [Using `kismet`](#using-kismet)
- [Additional documentation](#additional-documentation)
- [Bugs found](#bugs-found)
- [Credits](#credits)
<!-- END doctoc generated TOC please keep comment here to allow auto update -->
# The kmax tool suite
## Getting started
### Installing the kmax tool suite
Install using pipx.
sudo apt install -y pipx
pipx install kmax
Instructions to install from source can be found in the [advanced documentation](https://github.com/paulgazz/kmax/blob/master/docs/advanced.md).
#### Installing SuperC (recommended)
[SuperC](https://github.com/appleseedlab/superc) allows `klocalizer` to find `#ifdef` constraints.
# install superc
sudo apt-get install -y libz3-java libjson-java sat4j unzip flex bison bc libssl-dev libelf-dev xz-utils lftp
wget -O - https://raw.githubusercontent.com/appleseedlab/superc/master/scripts/install.sh | bash
# setup environment
export COMPILER_INSTALL_PATH=$HOME/0day
export CLASSPATH=/usr/share/java/org.sat4j.core.jar:/usr/share/java/json-lib.jar:${HOME}/.local/share/superc/z3-4.8.12-x64-glibc-2.31/bin/com.microsoft.z3.jar:${HOME}/.local/share/superc/JavaBDD/javabdd-1.0b2.jar:${HOME}/.local/share/superc/xtc.jar:${HOME}/.local/share/superc/superc.jar:${CLASSPATH}
export PATH=${HOME}/.local/bin/:${PATH}
Add the environment variables to your `.bash_profile` to make them permanent.
### Kicking the tires
Install Linux kernel compilation dependencies:
sudo apt install -y flex bison bc libssl-dev libelf-dev
Get the Linux kernel source:
cd ~/
wget https://cdn.kernel.org/pub/linux/kernel/v5.x/linux-5.16.tar.xz
tar -xvf linux-5.16.tar.xz
cd ~/linux-5.16/
Test `klocalizer` by automatically repair `allnoconfig` to build `drivers/usb/storage/alauda.o`, which would normally be omitted by `allnoconfig`.
# create allnoconfig
make ARCH=x86_64 allnoconfig
# run klocalizer to repair allnoconfig to build alauda.c
klocalizer --repair .config -o allnoconfig_repaired --include drivers/usb/storage/alauda.o
# clean and build the kernel with the repair config file
KCONFIG_CONFIG=allnoconfig_repaired make ARCH=x86_64 olddefconfig clean drivers/usb/storage/alauda.o
You should see `CC drivers/usb/storage/alauda.o` at the end of the build.
## Using `klocalizer --repair` on patches
`klocalizer` will take config file that fails to build lines of a patch and repairs it to build the whole patch. This requires installing [SuperC](https://github.com/appleseedlab/superc) as described above.
Let's first get an example patch from the Linux kernel's mainline repository:
cd ~/
git clone git://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
cd ~/linux/
git checkout 6fc88c354f3af
git show > 6fc88c354f3af.diff
Next, let's repair allnoconfig, which does not build all lines from the patch.
# create allnoconfig
make ARCH=x86_64 allnoconfig
# run klocalizer to repair allnoconfig to include the patch
klocalizer --repair .config -a x86_64 --include-mutex 6fc88c354f3af.diff
# clean and build the files modified by the patch (optionally build the whole kernel)
KCONFIG_CONFIG=0-x86_64.config make ARCH=x86_64 olddefconfig clean kernel/bpf/cgroup.o net/ipv4/af_inet.o net/ipv4/udp.o net/ipv6/af_inet6.o net/ipv6/udp.o
We can use `koverage` to check how much of patch is covered by a given config file:
koverage --config 0-x86_64.config --arch x86_64 --check-patch 6fc88c354f3af.diff -o coverage_results.json
cat coverage_results.json
In contrast, we can see that `allnoconfig` omits coverage of the patch:
make ARCH=x86_64 allnoconfig
koverage -f --config .config --arch x86_64 --check-patch 6fc88c354f3af.diff -o allnoconfig_coverage_results.json
cat allnoconfig_coverage_results.json
Notes:
- While repair usually covers all lines of a patch, some lines may still be omitted, for instance if they are dead code or in header files.
- If a patch modifies both arms of an `#ifdef`, multiple config files are needed to cover all lines. These are exported as `NUM-ARCH.config`.
## Using `klocalizer --save-dimacs` and `klocalizer --save-smt`
This tool extracts a DIMACS or a SMT formula.
Therefore, execute the following commands in the root directory of your Linux kernel:
klocalizer -a x86_64 --save-dimacs <Path>
klocalizer -a x86_64 --save-smt <Path>
Note that `<Path>` should be replaced by the absolute path to the file, the formulae should be written to.
If you intend to use a Docker container, feel free to use the Dockerfile provided in [Advanced Usage](https://github.com/paulgazz/kmax/blob/master/docs/advanced.md).
## Using `koverage`
`koverage` checks whether a Linux configuration file includes a set of source file:line pairs for compilation. This following checks whether lines 256 and 261 of `kernel/fork.c` are included for compilation by Linux v5.16 allyesconfig.
cd ~/linux-5.16/
make.cross ARCH=x86_64 allyesconfig
koverage --config .config --arch x86_64 --check kernel/fork.c:[259,261] -o coverage_results.json
make allnoconfig; klocalizer -v --repair .config --include kernel/fork.c:[259]; rm -rf koverage_files/; koverage -v -a x86_64 --config .config --check kernel/fork.c:[259] -o coverage.out
The coverage results are in `coverage_results.json`, which indicate that line 259 is included while 261 is excluded by allyesconfig, because the lines are under mutually-exclusive `#ifdef` branches.
Use `--check-patch file.patch` to check coverage of all source lines affected by a given patch.
## Using `kismet`
This tool will check for unmet dependency bugs in [Kconfig specifications](https://www.kernel.org/doc/html/latest/kbuild/kconfig-language.html#menu-attributes) due to reverse dependencies overriding direct dependencies.
Run `kismet` on the root of the Linux source tree.
kismet --linux-ksrc="${HOME}/linux-5.16/" -a=x86_64
Once finished (it can take about an hour on a commodity desktop), kismet will produce three outputs:
1. A summary of the results in `kismet_summary_x86_64.txt`
2. A list of results for each `select` construct in `kismet_summary_x86_64.csv` (`UNMET_ALARM` denotes the buggy ones)
3. A list of `.config` files meant to exercise each bug in `kismet-test-cases/`
Technical details can be found in in the [kismet documentation](https://github.com/paulgazz/kmax/blob/master/docs/advanced.md#kismet) and the [publication](https://paulgazzillo.com/papers/esecfse21.pdf) on `kclause` and `kismet`. The experiment [replication script](https://github.com/paulgazz/kmax/blob/master/scripts/kismet_evaluation/kismet_experiments_replication.sh) can be used to run kismet on all architectures' Kconfig specifications.
## Additional documentation
[Advanced Usage](https://github.com/paulgazz/kmax/blob/master/docs/advanced.md)
## Bugs found
[Bugs Found](https://github.com/paulgazz/kmax/blob/master/docs/bugs_found.md) by our tools
## Credits
The main developers of this project have been [Paul Gazzillo](https://paulgazzillo.com) (`kextract`, `kclause`, `kmax`, `klocalizer`), [Necip Yildiran](http://www.necipyildiran.com/) (`kismet`, `krepair`, `koverage`), [Jeho Oh](https://www.linkedin.com/in/jeho-oh-110a2092/) (`kclause`), and [Julian Braha](https://julianbraha.com/) (`koverage`). [Julia Lawall](https://pages.lip6.fr/Julia.Lawall/) has posed new applications and provided invaluable advice, feedback, and support. Thanks to all the users who have contributed code and issues. Special thanks to the [Intel 0-day](https://01.org/lkp) team for working to [include `kismet` into the kernel test robot](https://lore.kernel.org/all/d13eec5d-ee87-2207-05a4-1c7732bca4cd@intel.com/) and for their valuable feedback. This work is funded in part by the National Science Foundation under awards [CCF-1840934](https://nsf.gov/awardsearch/showAward?AWD_ID=1840934) and [CCF-1941816](https://nsf.gov/awardsearch/showAward?AWD_ID=1941816).
Raw data
{
"_id": null,
"home_page": "https://github.com/paulgazz/kmax",
"name": "kmax",
"maintainer": null,
"docs_url": null,
"requires_python": null,
"maintainer_email": null,
"keywords": "makefile kconfig kbuild configurations kmax kclause klocalizer",
"author": "Paul Gazzillo",
"author_email": "paul@pgazz.com",
"download_url": "https://files.pythonhosted.org/packages/6c/b1/f39776f8bfcc7d0e9c0d06599754ce8c69fd1d606bf870f7f03c0e6755fb/kmax-4.5.3.tar.gz",
"platform": null,
"description": "<!-- START doctoc generated TOC please keep comment here to allow auto update -->\n<!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->\n\n- [The kmax tool suite](#the-kmax-tool-suite)\n - [Getting started](#getting-started)\n - [Installing the kmax tool suite](#installing-the-kmax-tool-suite)\n - [Kicking the tires](#kicking-the-tires)\n - [Using `klocalizer --repair` on patches](#using-klocalizer---repair-on-patches)\n - [Using `koverage`](#using-koverage)\n - [Using `kismet`](#using-kismet)\n - [Additional documentation](#additional-documentation)\n - [Bugs found](#bugs-found)\n - [Credits](#credits)\n\n<!-- END doctoc generated TOC please keep comment here to allow auto update -->\n\n\n# The kmax tool suite\n\n## Getting started\n\n### Installing the kmax tool suite\n\nInstall using pipx.\n\n sudo apt install -y pipx\n pipx install kmax\n\nInstructions to install from source can be found in the [advanced documentation](https://github.com/paulgazz/kmax/blob/master/docs/advanced.md).\n\n#### Installing SuperC (recommended)\n\n[SuperC](https://github.com/appleseedlab/superc) allows `klocalizer` to find `#ifdef` constraints.\n\n # install superc\n sudo apt-get install -y libz3-java libjson-java sat4j unzip flex bison bc libssl-dev libelf-dev xz-utils lftp\n wget -O - https://raw.githubusercontent.com/appleseedlab/superc/master/scripts/install.sh | bash\n \n # setup environment\n export COMPILER_INSTALL_PATH=$HOME/0day\n export CLASSPATH=/usr/share/java/org.sat4j.core.jar:/usr/share/java/json-lib.jar:${HOME}/.local/share/superc/z3-4.8.12-x64-glibc-2.31/bin/com.microsoft.z3.jar:${HOME}/.local/share/superc/JavaBDD/javabdd-1.0b2.jar:${HOME}/.local/share/superc/xtc.jar:${HOME}/.local/share/superc/superc.jar:${CLASSPATH}\n export PATH=${HOME}/.local/bin/:${PATH}\n\nAdd the environment variables to your `.bash_profile` to make them permanent.\n\n### Kicking the tires\n\nInstall Linux kernel compilation dependencies:\n\n sudo apt install -y flex bison bc libssl-dev libelf-dev\n \nGet the Linux kernel source:\n\n cd ~/\n wget https://cdn.kernel.org/pub/linux/kernel/v5.x/linux-5.16.tar.xz\n tar -xvf linux-5.16.tar.xz\n cd ~/linux-5.16/\n\nTest `klocalizer` by automatically repair `allnoconfig` to build `drivers/usb/storage/alauda.o`, which would normally be omitted by `allnoconfig`.\n\n # create allnoconfig\n make ARCH=x86_64 allnoconfig\n # run klocalizer to repair allnoconfig to build alauda.c\n klocalizer --repair .config -o allnoconfig_repaired --include drivers/usb/storage/alauda.o\n # clean and build the kernel with the repair config file\n KCONFIG_CONFIG=allnoconfig_repaired make ARCH=x86_64 olddefconfig clean drivers/usb/storage/alauda.o\n \nYou should see `CC drivers/usb/storage/alauda.o` at the end of the build.\n\n\n## Using `klocalizer --repair` on patches\n\n`klocalizer` will take config file that fails to build lines of a patch and repairs it to build the whole patch. This requires installing [SuperC](https://github.com/appleseedlab/superc) as described above.\n\nLet's first get an example patch from the Linux kernel's mainline repository:\n\n cd ~/\n git clone git://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git\n cd ~/linux/\n git checkout 6fc88c354f3af\n git show > 6fc88c354f3af.diff\n\nNext, let's repair allnoconfig, which does not build all lines from the patch.\n\n # create allnoconfig\n make ARCH=x86_64 allnoconfig\n # run klocalizer to repair allnoconfig to include the patch\n klocalizer --repair .config -a x86_64 --include-mutex 6fc88c354f3af.diff\n # clean and build the files modified by the patch (optionally build the whole kernel)\n KCONFIG_CONFIG=0-x86_64.config make ARCH=x86_64 olddefconfig clean kernel/bpf/cgroup.o net/ipv4/af_inet.o net/ipv4/udp.o net/ipv6/af_inet6.o net/ipv6/udp.o\n\nWe can use `koverage` to check how much of patch is covered by a given config file:\n\n koverage --config 0-x86_64.config --arch x86_64 --check-patch 6fc88c354f3af.diff -o coverage_results.json\n cat coverage_results.json\n\nIn contrast, we can see that `allnoconfig` omits coverage of the patch:\n\n make ARCH=x86_64 allnoconfig\n koverage -f --config .config --arch x86_64 --check-patch 6fc88c354f3af.diff -o allnoconfig_coverage_results.json\n cat allnoconfig_coverage_results.json\n\nNotes:\n\n- While repair usually covers all lines of a patch, some lines may still be omitted, for instance if they are dead code or in header files.\n- If a patch modifies both arms of an `#ifdef`, multiple config files are needed to cover all lines. These are exported as `NUM-ARCH.config`.\n\n## Using `klocalizer --save-dimacs` and `klocalizer --save-smt`\n\nThis tool extracts a DIMACS or a SMT formula.\nTherefore, execute the following commands in the root directory of your Linux kernel:\n\n klocalizer -a x86_64 --save-dimacs <Path>\n klocalizer -a x86_64 --save-smt <Path>\n\nNote that `<Path>` should be replaced by the absolute path to the file, the formulae should be written to.\nIf you intend to use a Docker container, feel free to use the Dockerfile provided in [Advanced Usage](https://github.com/paulgazz/kmax/blob/master/docs/advanced.md).\n\n## Using `koverage`\n\n`koverage` checks whether a Linux configuration file includes a set of source file:line pairs for compilation. This following checks whether lines 256 and 261 of `kernel/fork.c` are included for compilation by Linux v5.16 allyesconfig.\n\n cd ~/linux-5.16/\n make.cross ARCH=x86_64 allyesconfig\n koverage --config .config --arch x86_64 --check kernel/fork.c:[259,261] -o coverage_results.json\n make allnoconfig; klocalizer -v --repair .config --include kernel/fork.c:[259]; rm -rf koverage_files/; koverage -v -a x86_64 --config .config --check kernel/fork.c:[259] -o coverage.out\n\nThe coverage results are in `coverage_results.json`, which indicate that line 259 is included while 261 is excluded by allyesconfig, because the lines are under mutually-exclusive `#ifdef` branches.\n\nUse `--check-patch file.patch` to check coverage of all source lines affected by a given patch.\n\n## Using `kismet`\n\nThis tool will check for unmet dependency bugs in [Kconfig specifications](https://www.kernel.org/doc/html/latest/kbuild/kconfig-language.html#menu-attributes) due to reverse dependencies overriding direct dependencies.\n\nRun `kismet` on the root of the Linux source tree.\n\n kismet --linux-ksrc=\"${HOME}/linux-5.16/\" -a=x86_64\n\nOnce finished (it can take about an hour on a commodity desktop), kismet will produce three outputs:\n\n 1. A summary of the results in `kismet_summary_x86_64.txt`\n 2. A list of results for each `select` construct in `kismet_summary_x86_64.csv` (`UNMET_ALARM` denotes the buggy ones)\n 3. A list of `.config` files meant to exercise each bug in `kismet-test-cases/`\n\nTechnical details can be found in in the [kismet documentation](https://github.com/paulgazz/kmax/blob/master/docs/advanced.md#kismet) and the [publication](https://paulgazzillo.com/papers/esecfse21.pdf) on `kclause` and `kismet`. The experiment [replication script](https://github.com/paulgazz/kmax/blob/master/scripts/kismet_evaluation/kismet_experiments_replication.sh) can be used to run kismet on all architectures' Kconfig specifications.\n\n## Additional documentation\n\n[Advanced Usage](https://github.com/paulgazz/kmax/blob/master/docs/advanced.md)\n\n\n## Bugs found\n\n[Bugs Found](https://github.com/paulgazz/kmax/blob/master/docs/bugs_found.md) by our tools\n\n\n## Credits\n\nThe main developers of this project have been [Paul Gazzillo](https://paulgazzillo.com) (`kextract`, `kclause`, `kmax`, `klocalizer`), [Necip Yildiran](http://www.necipyildiran.com/) (`kismet`, `krepair`, `koverage`), [Jeho Oh](https://www.linkedin.com/in/jeho-oh-110a2092/) (`kclause`), and [Julian Braha](https://julianbraha.com/) (`koverage`). [Julia Lawall](https://pages.lip6.fr/Julia.Lawall/) has posed new applications and provided invaluable advice, feedback, and support. Thanks to all the users who have contributed code and issues. Special thanks to the [Intel 0-day](https://01.org/lkp) team for working to [include `kismet` into the kernel test robot](https://lore.kernel.org/all/d13eec5d-ee87-2207-05a4-1c7732bca4cd@intel.com/) and for their valuable feedback. This work is funded in part by the National Science Foundation under awards [CCF-1840934](https://nsf.gov/awardsearch/showAward?AWD_ID=1840934) and [CCF-1941816](https://nsf.gov/awardsearch/showAward?AWD_ID=1941816).\n",
"bugtrack_url": null,
"license": "GPLv2+",
"summary": "Tools for working with symbolic constraints from Kbuild Makefile.",
"version": "4.5.3",
"project_urls": {
"Homepage": "https://github.com/paulgazz/kmax"
},
"split_keywords": [
"makefile",
"kconfig",
"kbuild",
"configurations",
"kmax",
"kclause",
"klocalizer"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "6cb1f39776f8bfcc7d0e9c0d06599754ce8c69fd1d606bf870f7f03c0e6755fb",
"md5": "73c861f49855f02ee77a662249746ec4",
"sha256": "c5d944102f83f96622fcc4352d108aab777565f44ddad097f585fa3f70d68075"
},
"downloads": -1,
"filename": "kmax-4.5.3.tar.gz",
"has_sig": false,
"md5_digest": "73c861f49855f02ee77a662249746ec4",
"packagetype": "sdist",
"python_version": "source",
"requires_python": null,
"size": 671149,
"upload_time": "2024-04-23T15:12:31",
"upload_time_iso_8601": "2024-04-23T15:12:31.996860Z",
"url": "https://files.pythonhosted.org/packages/6c/b1/f39776f8bfcc7d0e9c0d06599754ce8c69fd1d606bf870f7f03c0e6755fb/kmax-4.5.3.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-04-23 15:12:31",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "paulgazz",
"github_project": "kmax",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "kmax"
}
JSON
