INTERNAL implies FORCE but in some versions of CMake if a config option
has been passed in via a -D option the INTERNAL set doesn't override the
value when it should.
See: https://gitlab.kitware.com/cmake/cmake/issues/19015
INTERNAL does not imply FORCE for CACHE
The DTS compilation was arm platforms only. Moving it to the top level
config file, making it available to RISCV platforms. The generated files
are almost identical with minor differences. A new argument(--arch) is
added to the hardware_gen.py for the differences.
We need other tools to be able to gather information about the kernel
memory reservation areas and device memory regions. Add mandatory
parameter --yaml for specifying the name of the output file to receive
this information. Write it.
Committed by G. Branden Robinson <Branden.Robinson@data61.csiro.au>.
Move module imports that are not absolutely required into a function
instead of at the top level so that we don't spew the diagnostic message
in scenarios like `--help` or usage errors.
- Minimise calls to external_process as this is more expensive than
using built-in CMake file operations.
- Update check_outfile_stale to also save the list of files it checks
for stale checks so if a config changes the list of files then the
output file will still be stale even if the input list of files are
older than it.
should_parse_regions performs a lot of repeated recursive calls on
immutable inputs. Memoizing it to cache previous calls leads
to a noticible reduction in execution time.
Our upcoming cmake styling tool requires any custom functions you want
styled nicely to be lower case. We only need to style these two nicely,
as they have kwargs we would like aligned.
This reduces chances of other parts of the script printing to stdout and
allows the compatibility strings file to be inspected or manually
changed for debugging purposes.
Updated YAML validation error message to use logging.warning,
forwarding the output to stderr. This would otherwise end up
in the CMake dts compatibility string.
Modify hardware_gen script to only include chosen
serial path. Added newlines to serial drivers to fix
concat issues when compiling. Move cmake macro RegisterDriver
up a level to support timer refactor. Modify arm cmake to reflect
this.
Have added a drivers/serial folder to kernel, where all serial drivers
will be kept. The point is to have the the dts parsed and generate cmake
to include the right uart.c file prefixed with the compatibility.
Have removed all io.c from plat and includes from plat/config.cmake and
updated CHANGES file.
This change fixes support for instances where we have
multiple kernel devices in the same page, or kernel devices
which aren't at page-aligned addresses.
Also use seL4_UserTop to pick the right address to start
putting the kernel device pages.
If one region is conditional and another isn't, we shouldn't merge them.
This fixes a problem where some regions wouldn't be exposed to
userspace when they were merged with a conditional region which would
cause userspace apps to fail in unexpected ways.
This commit stops using FdtNodes as dict keys, as those aren't hashable
with python3. It also opens the DTB in binary mode to prevent decoding
errors under python3.
This adds support for extracting interrupt numbers from DTS
to the hardware header file generator, so that the majority
of the per-platform interrupt listings can be removed.
This change adds infrastructure to automatically generate the
physBase macro, the avail_p_regs array, and the dev_p_regs array
based on a device tree. Platforms can opt-in to using this
by adding DTS files to the KernelDTSList variable.
The Python script uses the hardware.yml file to determine which
devices in the device tree are of interest to the kernel and should
be hidden from userspace and instead mapped into the kernel. Note that
currently the kernel mappings are not (yet) generated, however most
of the infrastructure needed to make that happen is present.
Move DTS to the kernel in preparation for using them to autogenerate
hardware headers.
This includes DTS that we didn't have previously, extracted from the
Linux kernel. Everything except TX2 comes from Linux v4.20, extracted
with the following commands:
checkout https://github.com/torvalds/linux.git v4.20
./update-dts.sh /path/to/linux/checkout
The TX2 dts is identical to the one that was found in seL4_tools.
Add kernel_platforms_string and kernel_platforms_list to tools/helpers.cmake.
kernel_platforms_string: concatenates all platform strings together into a
newline separated string.
kernel_platforms_list: returns a list of all kernel platforms.
Modified the behaviour of the EXACT_INPUT option within the
CPPFile helper function. Now named EXACT_NAME, the option
copies the input file to a temporary file. The name of the
temporary file is also passed in by the caller. This
step in necessary in getting the CPP step to correctly
depend on the targets given by the caller
(through EXTRA_DEPS). Also updated the CPP generation of the
kernel_all.i file to reflect the change.
Added an "ignore" argument to the circular_includes script. This
allows the caller to specify files for the script to ignore when
it parses the source file. Rather than creating a special
ignore case for "kernel_all.c" in the script itself, the user
parses the file as an argument (plus others if needed). Updated
the kernels cmake file to reflect the change.
Added small bash scripts to run astyle, pylint and xmllint
checks over the kernel source. These style checks were ported
from the old Make build system.
REALPATH was unnecessary and results in resolving symlinks in the target, although
the working directory will not have its symlink resolved. This results in very strange
paths from the base directory (which is the working directory) to the target.
This is a new version of GenCPPCommand that uses an OBJECT library intermediate to get
cmake to do 'arbitrary' compilation (by adding the -E flag) where the result does not
need to be linkable. The advantage of this over the GenCPPCommand version is there is
no need for trying to manually invoke GCC with all the correct arguments lists.
As a macro this helper would not operate as expected if output and input were defined
as the same variable. Making a function and explicitly writing into the PARENT_SCOPE
fixes this and also makes the code simpler
This change makes values take on more intuitive and expected defaults when gradually
configuring the kernel, either programatically or through the graphic interfaces
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.
TOPLEVELTYPES is not intended to be configurable by the user, rather is a reflection
on the types defined by the source. This changes the TOPLEVELTYPES argument to be
a property, allowing it to be constructed as a generator expression when generating
BF files. By being a property, and not something like a global property, it removes
the need to ensure that additions to TOPLEVELTYPES are done prior to any bitfield
target definitions.
Uses the COMMAND_EXPAND_LISTS flag to allow for generator expressions in parameters
to GenBFCommand. As lists are now being expanded the 'args' variable must also be
quoted.
Previously if a variable had unmet dependencies and had been hidden, by being made
an internal variable, it would not have been unhidden by the use of `option`. This
emulates the behaviour of `option` that we were wanting, but additionally using `FORCE`
to override the `INTERNAL` setting
Uses file(GENERATE) to directly create the contents of generated configuration files instead of
awkwardly using custom commands to echo the contents of multi line strings into files.
Newer versions of cmake provide a COMMAND_EXPAND_LISTS option that allows a quoted string,
such as "a;b" to be given to a COMMAND parameter and have it expand into multiple arguments.
Using this we can much more nicely generate some of our COMMAND invocations, at the cost of
requiring a more recent cmake version
The config_option helper was previously using cmake_dependent_option, which supposedly took
a value to set the option to in the case where it was disabled. However, this only sets
the value in the current function context, and not the cache. I do not understand why this
is the case and it seems to make that functionality completely useless. This commit simply
does the dependency checking itself and correctly sets the disabled value.
Instead of explicitly depending on Kernel_C.thy prior to generating proofs, this removes
the dependency check and leaves isabelle to check the dependency upon import.
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.
Dependencies can now be downloaded with:
pip install sel4-deps
Dependencies can be changed by modifying the setup.py script.
Information on how to update the package is in the setup.py script.
JIRA: SELFOUR-909
The lxml module relies on native libraries. When linting, pylint will
not load native libraries for security reasons. Thus, it can't find some
symbols exported by lxml, causing linting to fail. Whitelisting lxml
prevents this.
If `seL4_arch_invocations` is an empty list, this will cause `nSeL4ArchInvocationLabels`
to be declared as 0, rather than `nInvocationLabels` as intented. This change correctly
respects the behaviour of the 'first' variable, and does an explicit assignment to
`nSeL4ArchInvocationLabels` should it be the first (and only) member of the enum.
Closes#53
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.
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
