If invocations are hidden behind config guards the count of how
many invocations there are will be wrong. The C compiler will
correctly assign the value with enum auto numbering, so there's
no need to override that here
Placing a config condition on the first define
in sel4arch.xml will fail as currently the first define
must start at the last define + 1 of the previous
invocation enum.
If this is ever required, autoconf.h will need to be passed
to the script so it can check config variables itself.
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.
This module seems to be extracted from a larger package that expects
some structure to be in place that isn't here. Patch up the check
slightly to work here, and also maybe elsewhere?
There are now separate libs for benchmark, assert, printf, putchar
start/stop:
libs/libsel4benchmark
libs/libsel4assert
libs/libsel4printf
libs/libsel4putchar
libs/libsel4startstop
The primary changes are introducing sel4/sel4.h and removing std* types
plus porting assert and IO code from the kernel to libsel4assert,
libsel4printf, libsel4putchar.
This means the code within libsel4 and the newlibs do not overload any
typical libc entities. Instead the libraries use types like
seL4_Uint32 ... instead of uint32_t. And printf is now seL4_Printf and
assert is seL4_Assert ....
Finally, the only file modified that effects kernel code is
kernel/tools/bitfield_gen.py. It needed to be modified as it generates
files for both kernel and user space. And for user space the generated code
(types_gen.h) needed to use the new types and asserts. The changes should
not change what is generated for the kernel and I did a comparison of
kernel_final.{c|s} before and after my change and the only differences
were time stamps.
Bug: #15 Streamline kernel/libsel4 and remove its libc dependencies
This commit adds a two new output targets for the bitfield generator,
--autocorres-defs and --autocorres-proofs. These produce, respectively,
abstract definitions of the generated C functions suitable for use in
AutoCorres proofs and WP/simp lemmas suitable for use within AutoCorres proofs
of functions that call the generated C functions. Existing behaviour and
functionality should be unaffected.
The bitfield generator constructs tags as enums. The compiler is free to back
these by any type big enough to cover the enum. The generator emits code that
uses these tag values in mask and shift operations where the target type is
typically a uint32_t. As a result, it can produce code involving undefined
shifts like:
(seL4_CapData_Badge & 0x1) << 31
This commit casts the tag value to the unsigned target type before masking to
ensure everything is done on an appropriate sized unsigned type.
JIRA: SELFOUR-193
