Add the new block command
field_ptr(align) name size
as an abbreviation for
padding size - canonical + align
field_high name canonical - align
The (align) part is optional. If left out, align is 0.
This is useful for removing #ifdefs for pointer storage that are trying
to achieve constant size over different canonical bit representations.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Allow arithmetic integer expressions in all places where previously
only integer literals were allowed.
The operators +, -, *, / and % are supported. Additionally, in field,
field_high, and padding specifications, the constants "word_size" and
"canonical" are available.
This enables more readable bitfield specifications without changing
any of the code and proof generation. Produces identical output to
before.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Before:
static inline uint64_t PURE
pte_pte_table_ptr_get_pt_base_address(pte_t *pte_ptr) {
uint64_t ret;
assert(((pte_ptr->words[0] >> 0) & 0x400000000000003) ==
0x3ull);
After:
static inline uint64_t PURE
pte_pte_table_ptr_get_pt_base_address(pte_t *pte_ptr) {
uint64_t ret;
/* fail if union does not have the expected tag */
assert(((pte_ptr->words[0] >> 0) & 0x400000000000003) ==
0x3ull /* sliced tag pte_pte_table */);
Signed-off-by: julia <git.ts@trainwit.ch>
Replace "\<"" in strings with "\\<". Until recently python did not
complain about this illegal escape sequence, but now it warns.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Depedencies on Python2/3 cross support (such as six, past and future)
are removed as only Python3 is supported at this point. Fewer
external deps is a good thing.
Signed-off-by: Ben Leslie <benno@brkawy.com>
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
* Add help texts for all CLI options.
* Point to the manual in file header.
* Remove obsolete `--multifile_base` and `--c_defs` options. The former
is unused and the logic for it was removed in the previous commit.
The latter is not referenced in the code and has no effect. `
* Remove unused `mode` variable.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The `--multifile_base` option is unused in the seL4 build and has
comments indicating that it is broken.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add a `--form_file <file>` option to the bitfield generator for
printing a `/* generated from <file> */` message in a comment.
Use this option in cmake to provide the original source .bf file before
preprocessing so it's easier to find out where the corresponding
definitions are.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
There are cases that reasonably require non-ASCII characters in the
source code, hence tools/bitfield_gen.py must be able to handle them
correctly. This commit makes sure the bitfield generator consistently
opens all files with UTF-8 encoding.
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Bin Meng <bmeng.cn@gmail.com>
Bring up-to-date with current proof style, make style consistent,
slightly increase proof parallelism.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
A tagged union can now optionally use multiple fields to indicate the
tag. These are called "sliced" tags in the code. The tag fields have to
be at the same position and width in each block of the tagged unions,
and all tag fields have to be within the same word.
When sliced tags are used, tag class masks cannot be used at the same
time for this tagged union.
In the `tagged_union` declaration, the values of such sliced tags
become tuples. For instance, if `x` and `y` are tag fields (declared in
blocks not shown here) with width 1 and 2, we can write:
tagged_union ex exType(x,y) {
tag ex1 (0,2)
tag ex2 (1,3)
}
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Isabelle2021 sometimes gets further with mask_simps, so this commit
makes them optional. Also removes a duplicate simp-rule warning.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Changes the 'size suffix map' to be useful in more places. In general,
when we use the 'short name' of a variable in these generated proofs, we
run the risk of a change in variable declaration order breaking the
resulting proofs (since declaration order is how the C parser chooses
which variables get the short name). Best practice is to use the long
names whenever possible.
Uses the suffix map for some generated proofs.
Removes an unnecessary simp step.
Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.
In Python 3, dict value iterators aren't deterministic between runs,
which causes nondeterministic definition output order. Some L4V proofs
are sensitive to this order.
Use sorted keys to guarantee order when iterating over values.
Update all scripts and build system to call python3, given python2's
upcoming doom. Use sys.maxsize instead of sys.maxint in one script
(maxint does not exist in python3).
For bitfields requiring sign extension, the generated specs are nicer to
work with in proofs. The proofs also support an updated `sign_extend`
specification (in the l4v repository) which has nicer properties.
This change also speeds up some bitfield proofs.
For blocks and unions, generate only one write for each word, rather
than an update for each bitfield.
For verification, this speeds up some automatically generated proofs.
CONFIG_LIB_SEL4_PUBLIC_SYMBOLS=y will disable inlining for external
interfaces (except deprecated functions), thereby providing public
symbols for easy linkage with other languages.
This is a technical change to the proof mode of the bitfield
generator included in the seL4 source.
The postconditions of the generated specifications of the
*_ptr_set and *_ptr_new functions now describe the entire new
heap via (new_heap = hrs_mem_update (...) old_heap).
Previously they described the contents of various projections
of the heap, which is less precise.
This reverts commit 5ee3971563. This backend was
previously used in an experiment towards libsel4 verification. That project has
since adopted a different strategy and this backend is now unused. Meanwhile
the backend has lagged behind breaking changes to AutoCorres. This commit
removes the backend to avoid confusion from users who believe it to be
functional.
The plan here is to move some of the proof script complexity embedded
in the text of the bitfield_gen utility into generic proof helpers in the
l4v repository that bitfield_gen can use more modularly. This is a simple
first step.
