Configuration model files
undertaker uses extracted configuration informations to check the code against them. The format of the model files is simple:
CONFIG_DOES_NOT_IMPLY_ANYTHING CONFIG_21285_WATCHDOG "(CONFIG_WATCHDOG && CONFIG_FOOTBRIDGE) && !CONFIG_21285_WATCHDOG_MODULE"
It's a column format where every column is enclosed in double quotes, with the exception that fields without spaces don't need to be quoted. The model format describes the semantic
COLUMN → COLUMN
|, !, (, ). It must be read as: If the symbol on the left is true, we can deduce, that the expression on the right must evaluate to true. If there is no second column it means, that we can't deduce anything from the symbol.|
In our example we can read: "If CONFIG_21285_WATCHDOG is true, we can deduce that CONFIG_WATCHDOG and CONFIG_FOOTBRIDGE is true and CONFIG_21285_WATCHDOG_MODULE is false"
Metainformations about a model
There are two kinds of specialities to the format: Lines with I: in the first column are comments. And lines with the magic symbol UNDERTAKER_SET set meta informations about the model. It assigns a value to an meta variable.
Each element of ALWAYS_ON is always set to true. This isn't exactly implemented in all parts of the undertaker right now, but will be used soon.
UNDERTAKER_SET ALWAYS_ON "CONFIG_ARCH_HAS_CACHE_LINE_SIZE" "CONFIG_ARCH_HAS_CPU_IDLE_WAIT" "CONFIG_ARCH_HAS_CPU_RELAX"
If this flag is set no referential check is done. Concrete an incomplete model doesn't mention all items, that are defined by the configuration space. For example when you have only a model for the SCSI-Subsystem but also other symbols are used in the code you set this flag, and you won't get referential (missing) defects.
All symbols that match this regex are considered to be in the configuration space. This means they should be defined in the configuration tool. For Linux all CONFIG_ symbols are in the configuration space.
UNDERTAKER_SET CONFIGURATION_SPACE_REGEX "^(ENABLE_|CONFIG_)[^ ]*$"
Configuration models for the Linux kernel
Configuration models for the Linux kernel are generated by the helper script undertaker-kconfigdump, which has to be called inside an linux tree. It will generate models for all architectures in the subfolder models.
Internally it will call first dumpconf, a modified version of menuconfig, that will print out the information about the kconfig into a intermediate format. This format is then transformed with rsf2model into the model files, where all symbols, etc. are evaluated. rsf2model is the point where the kconfig semantic is converted in the above simple model of symbols and implications.