forked from Imagelibrary/seL4
bitfield_gen: add CLI to manual
* describe CLI * describe pruning * mention where in seL4 generated code and source are Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
@@ -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] <input.bf> <outfile>
|
||||
```
|
||||
|
||||
where `<input.bf>` 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=<file>`:\
|
||||
Append `<file>` 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=<type>`:\
|
||||
Append Isabelle/HOL `<type>` 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=<file>`:\
|
||||
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=<dir>`:\
|
||||
Location of the `cspec` directory containing the theory file
|
||||
`KernelState_C`. This is specific to the seL4 proof setup.
|
||||
|
||||
`--thy-output-path=<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=<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. `<block>_get_<field>`) 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.
|
||||
|
||||
<!--
|
||||
TODO:
|
||||
|
||||
- semantics (Isabelle?)
|
||||
- pruning
|
||||
- command line options
|
||||
- preprocessing used in seL4
|
||||
- file extension .bf
|
||||
- where can I find the generated code
|
||||
- where can I find the bitfield definitions in seL4
|
||||
-->
|
||||
|
||||
Reference in New Issue
Block a user