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 this change, options that were hidden from the cmake-gui due to
unsatisfied config_choice conditions were not recorded in
gen_config.{yaml,json,h}. After this change, these hidden options are
recorded as disabled.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
... from the device UT listed by platform_gen. The kernel itself
does not care about this memory, and it is just given as device UT.
We also just remove the reserved array entirely from the return of
`get_physical_memory` since it only seems to be a footgun, it's
only used internally to affect what memory the kernel wants to use.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: julia <git.ts@trainwit.ch>
`align_memory()` in hardware.py both modifies the first normal memory
region to adjust the base of it for alignment, and adds an extra
reserved region to our list of reserved regions. This then feeds
through `get_addrspace_exclude` which inverts the regions given
and turns it into the available "device memory" at user-level.
dev_mem = hardware.utils.memory.get_addrspace_exclude(
list(reserved) + phys_mem + kernel_devs, config)
Anything as an argument to this is not given as "device memory" by
the kernel. (It does not precisely match how the kernel works).
However, since `align_memory()` has adjusted both the phys_mem up
(which *would* have added this region as "device" memory) but also
added it to "reserved" region, which then made it disappear entirely,
as "reserved" regions are not exposed to userspace.
However, this **does not** match the behaviour of the kernel, as it was
not reserved, so this behaviour did not match the untypeds given to
userspace. This commit solves this by removing the extra reserved
region being added for that memory.
PR #1426 worked around this issue by removing the alignment on AArch64.
Whilst this fixed the issue that microkit was seeing, it just masked
the underlying issue. Reverting that PR, then applying this fix,
results in the following platform_gen.yaml:
devices:
- end: 0x1000000
start: 0x0
- end: 0xff800000
start: 0x3b400000
- end: 0xff841000
start: 0xff801000
- end: 0x100000000000
start: 0xff843000
memory:
- end: 0x3b400000
start: 0x1000000
Note especially the device region from 0x0 to 0x1000000; which is the
combination of the 0x0 to 0x1000 reserved region, and the 0x1000 to
0x1000000 reserved by the kernel's alignment requirement. Previously,
the platform_gen.yaml reported only the 0x0 to 0x1000 region,
devices:
- end: 0x1000
start: 0x0
- end: 0xff800000
start: 0x3b400000
- end: 0xff841000
start: 0xff801000
- end: 0x100000000000
start: 0xff843000
memory:
- end: 0x3b400000
start: 0x1000000
I will be following this commit up with a PR to instead make the
alignment-reserved region into a new memory region, since there's not
any reason why userspace can't use this memory.
This has been tested on a few platforms with sel4test and with
microkit on the pi4B.
Signed-off-by: julia <git.ts@trainwit.ch>
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>
As decided at the most recent TSC meeting, bump cmake format to the
latest version. This will change/break style in many of the existing
cmake files, but pinning pyyaml to < 6 is not a long-term option.
Also bump patch version of autopep8, which should not lead to style
changes.
Bump overall sel4-deps version because the cmake-format change is
incompatible. Version 0.6.0 was not published because of the pyyaml
pinning/downgrade.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove manual table of contents for rendering on the docsite, which will
provide an automatic TOC.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Take advantage of the new --skip-unchanged option added to the
config_gen.py header generator to skip regenerating unchanged header
files which forced a rebuild of the entire project whenever CMake was
reconfigured.
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
Currently, whenever CMake is reconfigured, config_gen.py will always
regenerate the output config header and json, forcing a timestamp
update and a rebuild. This change adds a --skip-unchanged option which
skips writing to the output file if the write would not change the
file's contents. The default is off to avoid breaking builds that rely
on the existing behavior of always overwriting.
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
Previously, config_gen.py required the generated header and json to be
either written to a file or sent to stdout. This meant that there was
no way to avoid writing to a file, as the header and json data would be
merged into the same stdout stream. This change makes it so that the
header or json generation can be suppressed entirely by omitting the
corresponding --write-c or --write-json options.
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
The SiFive Premier P550 [1] is a new development board from SiFive
that is based on the ESWIN EIC7700X SoC.
The platform is interesting to the seL4 community as it implements
the RISC-V hypervisor extension meaning we now have real hardware to
evaluate RISC-V hypervisor changes to seL4. It also implements the
Sscofpmf extension and so we'll be able to get more experiment with
proper profiling on RISC-V.
Unfortunately, it seems we still do not have proper ASID suppor
according to [2].
The board comes in two configurations, 16GB and 32GB of memory.
This adds support for the 16GB model.
The DTS comes from SiFive's fork of Linux [3].
No modifications were made, any extra things are in the overlay.
[1]: https://www.sifive.com/boards/hifive-premier-p550
[2]: https://forums.sifive.com/t/asid-vmid-support-in-p550-eic7700x/6887
[3]: https://github.com/sifive/riscv-linux/tree/dev/kernel/hifive-premier-p550
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Instead of special handling for the SBI region in the kernel, which can
be platform specific, treat it as a reserved memory region in the device
tree which is sufficient to prevent the kernel from turning the reserved
region into kernel untyped caps.
Signed-off-by: Kent McLeod <kent@kry10.com>
Compatibility with versions <3.10 is going away.
As it happens, we're not using any CMake features that have changed
between 3.7 and 3.16, so bump the lowest version to 3.16.
Also remove the minimum version statement from the platform config
files --- they're all very simple files that are version independent;
and the version is checked elsewhere anyway.
Also, Fix style issue
A commit to fix style to make the PR go through.
Signed-off-by: Peter Chubb <Peter.Chubb@unsw.edu.au>
Right now the `platform_gen.json` and `platform_gen.yaml` files contain
regions that are not actually used by the kernel. This is fine for
`platform_gen.h` because they are guarded by #ifdefs with kernel config
defines but the same approach does not work for YAML and JSON.
So, this patch changes the Python scripts that generate this files so
that they only generate the regions that actually end up being used.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
With recent proof improvements the proofs now apply to further platforms
in the ARM and AARCH64 configurations.
Refactor the verified configs to build on one include file per major
architecture which is then used for each platform with potentially
modified settings. Add path argument to `cmake_script_build_kernel`
macro to accommodate inclusion from different locations in the file
system.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
We relied on str.removeprefix(), which is only available in
python >= 3.9. To make this script more portable, we add our
own implementation.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
The version bump should be stable in code layout and fixes crashes on
more recent python code.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Before, some object API XML files conflicted when the include,
arch_include, and sel4_arch_include directories were combined:
- include/interfaces/sel4.xml
- arch_include/*/interfaces/sel4arch.xml
- sel4_arch_include/*/interfaces/sel4arch.xml
This commit renames them to:
- include/interfaces/object-api.xml
- arch_include/*/interfaces/object-api-arch.xml
- sel4_arch_include/*/interfaces/object-api-sel4-arch.xml
Now, when the include, arch_include, and sel4_arch_include directories
are combined, we are left with:
- interfaces/object-api.xml
- interfaces/object-api-arch.xml
- interfaces/object-api-sel4-arch.xml
Signed-off-by: Nick Spinale <nick@nickspinale.com>
The ELF loader may well be satisfied with a smaller alignment, but the
compile time assert in the kernel requires super section alignment for
physBase.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This new platform is NXP Semiconductor's Evaluation Kit for the i.MX 8M
Plus Applications Processor. It's from the i.MX 8M family of processors
and is largely similar to the existing i.MX 8M Quad and i.MX 8M Mini
platforms.
Signed-off-by: Damon Lee <damon@kry10.com>
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>
This should not have been added in commit ad4ea6cd. And since
commit c642a398 this is handled by a python script anyway.
Signed-off-by: Axel Heider <axel.heider@codasip.com>
The Odroid-C4 is supposed to have 4GB of DDR memory.
According to the SoC manual (S905X3 Revision 02) the
DDR region goes from 0x0 to 0xF57FFFFF in Table 7-1.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Commit 6d439a4646, which added JSON configuration output, caused the
configuration headers to be generated at build-time instead of
configure-time. This broke CAmkES build systems which depend on
configuration headers in CAmkES files at configure-time.
This commit makes the configuration headers available at configure-time.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Without this patch, user-level programs have the ability to
map in the core-local interrupt controller on RISC-V platforms
which contains the memory-mapped registers for the core-local
timer the kernel uses. This is a level of privilege that
user-level programs should not have. Writing to the `mtime`
register is possible which can then affect the timer interrupts
are delivered to the kernel.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
