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>
On e.g. FreeBSD, Bash lives at /usr/local/bin/bash. This change
makes the script find Bash wherever it may be hiding.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
These files are derived from the output of the device tree compiler in
the Linux kernel. The licenses of the input files do all have to be
compatible with at least GPL-2.0-only to be part of Linux.
Invocation and syscall headers are generated and provided under
BSD-2-Clause for user code and GPL-2.0-only for kernel code. To
facilitate people other than the copyright holder performing this
operation, the master files are provided under both (BSD or GPL, free
to choose).
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.
Added support for reading and writing additional virtual timer
registers for vcpu hw read and write accesses. These include the
compare value register (CNTV_CVAL) and offset register (CNTV_OFF),
each represented as two 32 bit (high and low) registers on aarch32 and
as single 64 bit registers on aarch64.
Added support for explicitly saving and restoring the virtual
timer registers when the vcpu is enabled and disabled. This
ensures when the vcpu is switched in and out, the virtual timer
registers are restored to a state that is consistent to when
it was last run.
By default the CNTVOFF register will be updated by the kernel to
accumulate the time the VCPU is not running. From the guest this will
result in the VCNT register not increasing when the VCPU is suspended.
This behavior can be turned off by disabling the
KernelArmVtimerUpdateVOffset config option.
This sets the first UART as the stdout-path dts setting in the
"chosen" node in the HiFive device tree.
Change-Id: Icb6b9abf999bdd8a278df5a2ba73ad492af06a24
The elfloader is going to start using devices based on the device tree.
Add an output method for hardware_gen.py that generates header files
that the elfloader can use. Currently they contain an array of
"devices", where each device has a compatiblity string and a series of
regions (represented simply as the physical address of the region).
For now, the elfloader only uses the serial device specified by the
stdout-path property in the DTB.
Currently on x86 device untypeds are generated by passing the entire
address space minus any parts that are reserved by the kernel or that
are "real" memory (e.g. kernel image, physical RAM).
On ARM and RISC-V, device untypeds were generated at compile-time from
a device tree. This patch moves ARM and RISC-V to use the same approach
as x86, and moves the code from x86 into a common location that's
shared between the three architectures.
Co-Authored-By: Anna Lyons <anna@gh.st>
- we're going to switch to mapping the whole address space, excluding
parts used by the kernel, to userspace. We trust the root server anyway,
so giving it extra (possibly invalid) MMIO space just simplifies stuff
on the kernel end.
- drop the hacky true/false/null 'user' flag in favour of a saner
true/false one.
- remove support for 'default' regions. By default we will pass unused
regions through to userspace.
This is almost a complete rewrite from the old hardware_gen.py.
It separates the 'parse DT' stage from the 'generate output'
devices more strictly, and is hopefully easier to understand and
easier to extend.
We also no longer generate the 'devices' list (in YAML)
or the dev_p_regs array (in C), as the kernel will implicitly
expose all non-RAM untypeds as devices.
This directory-scoped varible is now used by config_option,
config_choice and config_string to set a created CMake cache variable as
advanced or not. An advanced variable is hidden by default in the CMake
configuration editors. Setting SEL4_CONFIG_DEFAULT_ADVANCED to ON will
cause variables to be advanced and not show up in the cache. Projects
can set this to limit the amount of options presented in the
config editor. Any cache variable can have this overridden by calling
mark_as_advanced(CLEAR config_name)
This leverages #!/usr/bin/env -S cmake -P to invoke a cmake
configuration file as a script that configures and builds a kernel in
the current directory with the configuration that was invoked. It is a
quick way for producing a kernel.elf or kernel_all_pp.c input file to
verification for a particular config.
In the pip namespace, 'pyaml' is "pretty-yaml", a YAML generator (but
not a YAML parser); 'pyyaml' (accessed with "import yaml"), a.k.a.
"PyYAML", is the YAML serialiser and reader we actually use.
Bump the minor version number per semantic versioning rules. (One could
argue that we are "removing" pyaml (pretty-yaml) from our interface and
therefore a major version bump is required, but we weren't _actually_
using that module so I would argue that the introduction of 'pyyaml' is
the visible change.)
Thanks to Japheth Lim for identifying this issue.
The `shoehorn` tool in tools/seL4 (the sel4_tools repository) requires
this.
Bump minor version number per semantic versioning rules (interface
extension). (0.3.1 instead of 0.3.0 because 0.3.0 saw the light of day
with an incorrect dependency on `libarchive` instead of `libarchive-c`.)
This reverts commit a14264336c.
There are (at least) 3 namespaces relevant to Python module names:
Debian package names, PyPI module names, and the name of a module used
by actual Python language imports. That's one more than my brain could
handle. I wanted "libarchive-c" in setup.py instead of "libarchive".
The `shoehorn` tool in the tools/seL4 (the sel4_tools repository) will
require this in a future commit.
Bump minor version number per semantic versioning rules (interface
extension).
- use gpt, so we can have overflow and compare interrupts at the same
time (epit only allows compare)
- set the gpt to use the ipg_highfreq timer, as the standard ipg is too
low and breaks the timer calculations
In commit 24131333ac ("trivial: disable
YAML loading warning"), an assumption was made that the version of pyaml
present was 5.1 or later; see https://msg.pyyaml.org/load .
Version the dependency.
- remove add_build_rules() and replace with shorter inline impl.
- Remove nested for looping from Config.get_irqs() and .split_regions()
as we already know that a rule exists and have a reference to it via the
kernel device.
- Don't allow multiple rules for a single compatibility string. There
currently aren't multiple rules for a single string without any
motivating examples it is unclear whether this should be supported.
The kernel device IRQs and Frame mappings generated by this script will
only come from nodes specified in the seL4,kernel-devices property of
the chosen node. Previously these devices were inferred by the script
but this led to false matching and didn't support easily overriding
which devices to match under different configurations or across
different platforms.
Explicitly specifying which devices from the device tree will be used in
the kernel makes it easier to check which devices the kernel is actually
using and makes it easier to change on a per platform or per
configuration basis.
- Device.regions() now just calculates memory regions without splitting
them into user and kernel groups.
- Config.split_regions() now calls Device.regions() and performs the
splitting if the device is a kernel device, otherwise returns the
original regions.
- Config.split_regions() is now only used in a context when dealing with
kernel devices, otherwise Device.regions() can be called to return only
informatioin extracted from the device tree.
- directly return IRQs from Device.get_interrupts(): Previously, these
IRQs were then mutated by Config.get_irqs() based on driver definitions
in hardware.yml. Inverting this order makes get_interrupts more general.
- Config.get_irqs() uses the Device it gets passed to call
get_interrupts() only when it needs to extract interrupts for a device.
- Use Config.get_irqs() for building kernel's IRQ list instead of
calling Device.get_interrupts() due to the new inversion.
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).
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
