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>
* 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 user manual for the bitfield generator that documents syntax,
semantics and basic concepts. Should also be able to serve as main
spec for what the tool is supposed to do.
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>
For verification flexible w.r.t kernel placement in physical memory, we
need to relate physBase as a named constant to its abstract equivalent.
Unfortunately, apart from enums, the C programming language does not
have real constants. The C parser follows the C standard and requires
enums constants to be storable as int, meaning without major overhaul
enums are not sufficient for storing word_t-sized memory addresses.
Since the linker scripts can't deal with static inline functions
in the constants they need (KERNEL_ELF_BASE and KERNEL_ELF_PADDR_BASE),
we provide the following preprocessor definitions for the linker
specifically:
* PHYS_BASE_RAW (the numerical value returned by physBase())
* KERNEL_ELF_BASE_RAW
* KERNEL_ELF_PADDR_BASE_RAW
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
gen_config.json provides a language-independent means of accessing the
kernel configuration. Before, gen_config.h was generated directly in
CMake. Now, gen_config.yaml is generated directly in CMake, and
gen_config.h and gen_config.json are derived from gen_config.yaml.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
