Welcome to CADOS / VAMOS
Topic of the project is variability of system software evoked by the non-functional properties of operating-system functions, which emerges from (a) different implementations of the same system function to make an appearance of certain non-functional properties and (b) the using level of those implementations in order to compensate for effects of these properties.
With this project, the undertaker, we provide tools to examine and evaluate CPP based source files. See VAMOS or CADOS for more information.
Please send bug reports and feature requests to: cados-dev(at)lists.informatik.uni-erlangen.de. If you find our tools useful, we would be happy to learn about your experiences with them.
For a complete list of local wiki pages, see TitleIndex.
undertaker
The undertaker is an implementation of our preprocessor and configuration analysis approaches. It can check the structure of your preprocessor directives against different configuration models to find blocks than can't be selected or deselected.
Furthermore, the tool provides the functionality to tailor a given Linux kernel to specific use cases (UndertakerTailor).
A new tool, called undertaker-checkpatch (released with v1.6), is able to analyze patch files. This tool will tell you if your patch introduces new defects, fixes old ones or if a defect remains unchanged. Furthermore it provides functionality to help analyze the causes of the defects.
For additional information to the latest release, check here.
Download
- The undertaker is licensed GPLv3 or later. Parts that are imported from the Linux kernel are GPLv2
- Tarball: v1.6.1 (all releases)
- to get the most current (non-release) version, clone from git:
git clone https://i4gerrit.informatik.uni-erlangen.de/undertaker
Requirements
- g++ (4.8.1 or above) with a matching libstdc++ version
- libboost-wave (1.53 or above)
- libboost-regex (1.53 or above)
- libboost-filesystem (1.53 or above)
- libboost-thread (1.53 or above)
- libboost (1.53 or above)
- PUMA (from the http://aspectc.org project, Ubuntu / Debian users may install via apt-get libpuma-dev, others might use 'make localpuma' see 'Building' section)
- pstreams (package libpstreams-dev)
Additional Requirements for undertaker-developers
- check (0.9.6 or above) - testing suite for C
- pylint
- python-unittest2
- spatch / sparse / clang
- limmat/limboole (download sources for 0.2, compile and put the path to limboole into PATH)
- bison
- flex
Requirements for undertaker-checkpatch
- whatthepatch
whatthepatch is installed via 'pip', which is part of the 'python-pip' package (ubuntu). If you have pip, you can install 'whatthepatch' via
pip install whatthepatch
Building
To install the dependencies in Debian or Ubuntu, you paste this in your shell.
apt-get install libboost1.55-dev libboost-filesystem1.55-dev libboost-regex1.55-dev libboost-thread1.55-dev libboost-wave1.55-dev libpuma-dev libpstreams-dev check python-unittest2 clang sparse pylint bison flex
Compiling and installation
$ make
and
$ make install
or $ PREFIX=/path/to/install make install
Compilation can be done in parallel, just add '-jX' to the make command, where X is the number of threads.
$ make -j10
To compile the undertaker-tools statically:
$ STATIC=1 make
Building without libpuma-dev
Some Distributions (*Suse, Gentoo, Fedora, ...) don't have a libpuma-dev package. To be able to compile and run the undertaker on these distributions, it is required to download the pre-woven sources of Puma.
The 'localpuma' target will download the required sources and trigger the compilation.
$ make localpuma
If you already have a local copy of the pre-woven Puma sources, you can specify the LOCALPUMA environment variable with the path to the sources.
$ LOCALPUMA=/path/to/aspectc++/Puma/ make
or use a relative path:
$ LOCALPUMA=../Puma/ make
Workflow (example)
To check a single file (or all files) in the Linux kernel for dead or undead preprocessor blocks, you have to extract the configuration models from the kconfig first. Therefore you just have to execute undertaker-kconfigdump in the root of a Linux tree. This will generate models for each architecture and place them in the subfolder models.
$ ls models alpha.model blackfin.model h8300.model m68k.model mips.model powerpc.model sh.model x86.model arm.model cris.model ia64.model m68knommu.model mn10300.model s390.model sparc.model xtensa.model avr32.model frv.model m32r.model microblaze.model parisc.model score.model tile.model
If you want to examine a single file for dead blocks with checks against the models you can execute
$ undertaker -v -j dead -m models kernel/sched.c I: loaded rsf model for alpha [...] I: loaded rsf model for xtensa I: found 23 rsf models I: Using x86 as primary model I: creating kernel/sched.c.B250.x86.missing.dead I: creating kernel/sched.c.B360.x86.missing.dead I: creating kernel/sched.c.B362.x86.missing.dead I: creating kernel/sched.c.B364.missing.globally.dead I: creating kernel/sched.c.B368.x86.missing.dead I: creating kernel/sched.c.B396.x86.missing.dead I: creating kernel/sched.c.B408.x86.missing.dead I: creating kernel/sched.c.B421.x86.missing.dead I: creating kernel/sched.c.B437.x86.missing.dead I: creating kernel/sched.c.B447.missing.globally.dead I: creating kernel/sched.c.B556.x86.missing.dead
This means in detail:
- -j dead: do a dead analysis
- -m models: load all models from directory models/
- kernel/sched.c: examine this file
- I: Using x86 as primary model": x86 is the default model which the file is checked against (this can be changed with -M <arch>)
- All x86.missing.dead files are just dead on x86, there is at least one architecture this block can be enabled
- missing.globally.dead files are dead on every architecture.
To check all files in the Linux kernel there is the helper script undertaker-linux-tree, which starts the undertaker with the correct list of working files and gives it the correct count of parallel worker processes on your multicore machine.
$ undertaker-linux-tree
Detailed information
- UndertakerModelFiles - syntax and semantic of the kconfig models
- UndertakerDeadAnalysis - finding dead and undead blocks in your code
- UndertakerPreconditions - preconditions for line numbers and symbols
- UndertakerInteractive - interactive mode for the undertaker
- UndertakerTailor - tailor a given Linux kernel to specific use cases
- Flipper - lean trace collection method for UndertakerTailor
- undertaker.el - undertaker mode for emacs
