From 07a8263a9d5ccaafca9f94be1d3539a0cd3f9127 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 1 May 2023 12:10:10 +1000 Subject: [PATCH] bitfield_gen: add CLI to manual * describe CLI * describe pruning * mention where in seL4 generated code and source are Signed-off-by: Gerwin Klein --- tools/bitfield_gen.md | 136 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 130 insertions(+), 6 deletions(-) diff --git a/tools/bitfield_gen.md b/tools/bitfield_gen.md index 2add6aac1..6c587772e 100644 --- a/tools/bitfield_gen.md +++ b/tools/bitfield_gen.md @@ -22,6 +22,10 @@ - [Restrictions](#restrictions) - [Correctness](#correctness) - [Limitations](#limitations) +- [Command Line](#command-line) + - [Usage](#usage) + - [Options](#options) + - [seL4 build](#sel4-build) ## Introduction @@ -679,14 +683,134 @@ access functions for variants, but it does support all those that are used in seL4. If proof support for new combinations is needed, the tool could be extended relatively easily. +## Command Line + +### Usage + +The tool can be invoked from the command line as follows + +```sh +bitfield_gen.py [options] +``` + +where `` is a bitfield specification file as described in this manual. +If no file is given, the tool reads from `stdin`, and if no output file is given, +the tool prints to `stdout`. + +By default, the output is generated C code. See options below for how to +additionally produce Isabelle/HOL theory files for specifications and proofs. + +### Options + +`-h, --help`:\ + Show help message and exit. + +`--environment={seL4,libseL4}`:\ + Whether to produce code for the `seL4` or `libseL4` environment. This + influences which header files are included, what statement to use for + `assert`, what type names `uint32` etc have, and how a function is declared + inline. The values are determined by the `INCLUDES`, `ASSERTS`, `INLINE`, + and `TYPES` dictionaries in the generator source. + +`--hol_defs`:\ + Produce Isabelle/HOL theory files with specifications and definitions. + +`--hol_proofs`:\ + Produce Isabelle/HOL theory files with proofs, assuming specification + and definition files exist. Requires the `--umm_types` option. + +`--sorry_lemmas`:\ + When producing proofs, only state lemmas, but do not prove them. This + requires explicitly setting `quick_and_dirty` in Isabelle and + is useful for reducing processing time during other proof development. + +`--prune=`:\ + Append `` to the list of files with pruning information, which contain + the names of bitfield functions that are used in the client code base. The + option can be used multiple times. If this option is used, the generator + will only produce the functions that are listed in one of these files. This + is useful to reduce code size, processing time, and especially proof + processing time drastically. It does make it harder to discover which + functions are generated by the tool, so if that is important, consider + leaving this option off until proofs are needed. + +`--toplevel=`:\ + Append Isabelle/HOL `` name to the list of top-level heap types. The + proofs will generate appropriate frame conditions for all of these top-level + heap types. The option can be used multiple times. + +`--umm_types=`:\ + Path to the file `umm_types.txt` which contains dependency information + between the top-level heap types (e.g. which structs contain which other + structs or type fields). The file can be generated using + `spec/cspec/mk_umm_types.py` in the [l4v] repository. (UMM = unified memory + model). + +`--cspec-dir=`:\ + Location of the `cspec` directory containing the theory file + `KernelState_C`. This is specific to the seL4 proof setup. + +`--thy-output-path=`:\ + Where to put the generated theory files. + +`--skip_modifies`:\ + Do not emit "modifies" proofs. These proofs state and show which global + state is modified by each generated function. They are weaker versions + of the full specifications and may not be needed if the full specifications + are always used instead. + +`--showclasses`:\ + Print the parsed classes and fields. + +`--debug`:\ + Print debug information during code and proof generation. + +`--from_file=`:\ + Original source file before preprocessing. Use this to produce a + `Generated from FROM_FILE` comment in the output. + +[l4v]: https://github.com/seL4/l4v + +### seL4 build + +In the seL4 build system, `.bf` files are usually first passed through the C +preprocessor to process `#include` and `#ifdef` statements, as well as perform +macro expansion, which are currently not part of the bitfield specification +language. + +The source files containing C preprocessor macros and includes are called `.bf`. +There are the following main files in seL4: + +- `include/structures_32.bf` and `include/structures_64.bf` contain generic + kernel objects and capabilities for 32 and 64 bit systems +- `include/arch/**/object/structures.bf` contain architecture dependent object + and capability definitions. +- some `plat/**` directories contain `hardware.bf` files for hardware structures. +- `libseL4` contains some bitfield definitions that are shared with the kernel in + `libsel4/sel4_arch_include/*/sel4/sel4_arch/types.bf`, + `libsel4/arch_include/*/sel4/arch/shared_types.bf`, and + `libsel4/mode_include/*32*/sel4/shared_types.bf`. + +The generated C code contains a comment which `.bf` include hierarchy the +definitions are coming from. + +The generated code can be found in a build directory under the `generated` +directory, where e.g. `structures_gen.h` will have been generated from +`structures.bf.pbf`, which in turn is the preprocessed source of +`structures.bf`. + +Note that the seL4 build uses the `--prune` option, which means that the +generator will only produce functions that are mentioned in the rest of the seL4 +sources. To generate a function that is not yet mentioned, simply use a +supported function name pattern in the source (e.g. `_get_`) and +the generator will supply it. To discover which functions can be generated, +either use the name template descriptions in this manual or consider temporarily +removing the `--prune` option in the `cmake` build to look at the generated +sources. This should only be done when no proofs are required, because it will +drastically increase proof processing time. +