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>
This adds support for the Pine64 Quartz64 and other devices based on
the Rockchip RK3566. The platform support is adapted from the
Rockpro64 code, except that the RK356x has A55 cores, and adjusting
for the fact that the ARM Generic Timer is the only on-chip timer
available.
Signed-off-by: Peter S. Housel <housel@acm.org>
Remove redundant (and incorrect) reserved memory
definition for VideoCore memory. The reserved
memory area is defined in 'overlay-rpi4.dts'.
Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>
Signed-off-by: Hannu Lyytinen <hannu.lyytinen@unikie.com>
kernel,bcm2711: Fix RPI4 address mapping
Fix build error and warnings by removing GPIO mapping
from overlay. Also as a note, don't add 'serial1' or 'ethernet'
here, because 'serial1' is already mapped to sel4 kernel by
'chosen' block in 'overlay-rpi4.dts', and the translation for
the 'ethernet' is done with 'ranges' property.
Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>
kernel,bcm2711: Fix memory area overlay DTS
First fix is to change the memory area reserved for
the VideoCore from 64 -> 76 MB, as this is the default
value on RPi4. Using other values would require configuration
of the first stage bootloader with 'config.txt' file.
Second fix is separating the disjunct memory areas
to separate nodes, as the generator Python scripts
in 'kernel/tools/' etc discarded the first area below
1GB limit if all areas were defined in the same node.
The effect of different variations can be observed
during kernel build in the generated
'kernel/gen_headers/plat/machine/devices_gen.h' header.
Third fix is adding the reserved memory area for the
VideoCore memory to avoid any collisions.
Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>
There are cases that reasonably require non-ASCII characters in the
source code, hence tools/bitfield_gen.py must be able to handle them
correctly. This commit makes sure the bitfield generator consistently
opens all files with UTF-8 encoding.
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Bin Meng <bmeng.cn@gmail.com>
Generated from maaxboard-dcss-hdmi.dts (Avnet/linux-imx) for more
comprehensive device support. Updated overlay to align.
Signed-off-by: Mark Jenkinson <mark.jenkinson@capgemini.com>
Bring up-to-date with current proof style, make style consistent,
slightly increase proof parallelism.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
A tagged union can now optionally use multiple fields to indicate the
tag. These are called "sliced" tags in the code. The tag fields have to
be at the same position and width in each block of the tagged unions,
and all tag fields have to be within the same word.
When sliced tags are used, tag class masks cannot be used at the same
time for this tagged union.
In the `tagged_union` declaration, the values of such sliced tags
become tuples. For instance, if `x` and `y` are tag fields (declared in
blocks not shown here) with width 1 and 2, we can write:
tagged_union ex exType(x,y) {
tag ex1 (0,2)
tag ex2 (1,3)
}
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
this allows the template to be parsed with minijinja
which doesn't support namespaces or set (at this time).
Signed-off-by: matt rice <ratmice@gmail.com>
This commit adds a new device tree for the ultra96v2, adding
additional devices to give to userspace.
Signed-off-by: Robbie VanVossen <robert.vanvossen@dornerworks.com>
The memory mapping for the timer only uses 1K on AllwinnerA20, but
the minimum device mapping is 4K in seL4. Other devices within this
4K page (CCU and PIO) cannot be accessed in the userland.
Replace the kernel timer with the ARM generic timer on AllwinnerA20,
and remove the implementation for AllwinnerA20 specific timer in the
kernel. So we should have user access to those devices now.
Signed-off-by: Luca (Wei) Chen <wei@cvluca.com>
Makes it easeier to eyeball the difference between the beaglebone's spec
and (say) the beaglebone-black's spec.
Changed with `sed -re 's/<(.*)>/< \1 >/`
Signed-off-by: Stephen Sherratt <stephen@sherra.tt>
Generated by:
- clone linux from https://github.com/torvalds/linux.git
- checkout v4.20
- run update-dts.sh script
Signed-off-by: Stephen Sherratt <stephen@sherra.tt>
At the end of the physical address range, the last address isn't turned
into an UT object. The scripts generating the memory regions
unnecessarily round down to a small page size when they could instead
round down to the smallest UT size and this memory could be used for
smaller kernel objects.
Signed-off-by: Kent McLeod <kent@kry10.com>
The platform was the original verification target of seL4 over 10 years
ago and by now there doesn't appear to be any ways to obtain new
hardware.
Currently, the KZM platform is the only ARMv6 platform and supporting it
requires a few work-arounds for emulating mechanisms that newer hardware
supports. Removing this platform also implies removing armv6 support
soon.
Signed-off-by: Kent McLeod <kent@kry10.com>
- Provide a nicer string for debugging purposes.
- improve comments about the purpose of __repr__() and __str__()
Signed-off-by: Axel Heider <axelheider@gmx.de>
- A region can't be created from an invalid range
- A region might be too small to support the change. There is no trivial
way to fix this.
Signed-off-by: Axel Heider <axelheider@gmx.de>
RISC-V defines the concept of a PLIC, but leaves the details open. The
driver is for the PLIC of the SiFive U54/U74 SOC, which is used on
the HiFive Unleashed/Unmatched and Polarfire board.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
Merge memory regions before checking for reserved areas
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Bertrand Virfollet <bvirfollet@silicom.fr>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
TQ Group produces a system-on-module family called TQMa8Xx.
The user manual for this SoM is available here:
https://www.tq-group.com/filedownloads/files/products/embedded/manuals/arm/embedded-modul/TQ-Socket/TQMa8Xx/TQMa8Xx.UM.0104.pdf
This SoM comes in a number of different configurations.
The specific NXP SoC used, and the amount of memory are both
configurable.
The TQMa8XQP is the part number for the TQMa8Xx family configured with
the i.MX 8QuadXPlus SoC.
The datasheet for the SoC is available here:
https://www.nxp.com/docs/en/data-sheet/IMX8QXPAEC.pdf
In addition to the SoC being configurable the amount of SDRAM
on the SoM is also configurable.
The support provided in this PR is specifically for the TQMa8XQP
configured for 1GiB of memory. Note: Actual usable memory available
to the ARM application processor is 1022MiB.
System-on-modules rely on an appropriate carrier board.
Testing of this PR has been done on the MBa8Xx carrier board
that is available from TQ Group as part of their starter kit.
To the best of my knowledge there is nothing in this PR
that depends on the carrier board itself; all code is SoM
specific and should support any carrier board.
Note: This support is very specifically for the TQMa8XQP configured
with 1GiB of memory.
This may be a starting point for supporting other boards that
also have the NXP i.MX 8QuadXPlus SoC (as well as the i.MX 8DXP
and possibly other SoC in the i.MX 8 family).
Support is limited to the specific SoM due to the way in which
platform support currently works for seL4. Building a kernel
currently relies on the information from the DTS file (which is
SoM + RAM configuration specific). It would be preferable to
allow more generic support but SoC families but that is beyond
the scope of this PR.
Signed-off-by: Ben Leslie <benno@brkawy.com>
The structure actually describes kernel frames and not kernel devices.
In most of the cases a peripherals will fit into one page, but some can
need more pages. On some platform there are no kernel devices at all.
Provides the macro NUM_KERNEL_DEVICE_FRAMES as simple way to find out if
there are mapping that hides the corner cases. This eventually allows
implementing a generic handling even on RISC-V without much overhead, so
the hack for HiFive/Spike can be removed.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Using explicit field name in the assignment states more clearly what the
generated code does. It is also more robust and allows the compiler to
catch potential inconsistencies in case the structure details change.
Signed-off-by: Axel Heider <axelheider@gmx.de>
This implements GitHub PR #115 on the current repo state. /usr/bin/env
is already used for other (cmake/python/etc) invocations, and this PR
brings bash/sh into line with that for slightly improved portability.
Co-authored-by: Douglas Wilson <douglas.wilson@gmail.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Co-authored-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Co-authored-by: Axel Heider <axel-h@users.noreply.github.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Memoization is not worth it here, the runtime of the entire program
is tiny. Removing the comment to curb temptations in the future.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Avoid the warning 'WARNING:root:Not sure how to parse interrupts for
"/cpus/cpu@0/interrupt-controller"' when building for platform hifive.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
CMake treats any text output that is generated by tools during the
configuration phase as important if it isn't part of a message(STATUS)
command. Output generated by hardware_gen.py often shows up as warnings
about device tree properties that are usually uninformative. Resolving
some of the warning conditions removes these messages for most
platforms.
- Setting kernel_size in hardware.yml to 0x1000 to handle cases where
the kernel only needs the first page of a device that has a
device-tree definition larger than that.
- Remove status print about each Interrupt processed as it's usually not
useful information.
- Only process IRQs for a selected kernel device if the rule for that
device has any interrupt queries. This prevents warnings for IRQ
controllers that the script doesn't know how to process when it
doesn't need to.
Signed-off-by: Kent McLeod <kent@kry10.com>
This adds support for the ODroidC4. The ODroidC4 is just a beefier
ODroidC2 with some bits moved around. The devices we care about here are
all essentially the same except the cores are A55s instead of A53s.
Signed-off-by: Curtis Millar <curtis@curtism.me>
Add support the i.MX low-power UART. This is available on
chipsets such as i.MX8QXP.
Note: This is a preliminary patch in advance of providing
full support for the i.MX8QXP platform.
Note: getchar is not implemented (current) for this platform.
Signed-off-by: Ben Leslie <benno@brkawy.com>
The max IRQ and devicetree definitions are slightly outdated. This
commit updates these definitions.
Signed-off-by: Damon Lee <Damon.Lee@data61.csiro.au>
Isabelle2021 sometimes gets further with mask_simps, so this commit
makes them optional. Also removes a duplicate simp-rule warning.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
There are duplicate interrupts in some of the devices in the devicetree.
This commit removes these duplicate interrupt entries to avoid errors
with some of our tools (CAmkES, etc).
Signed-off-by: Damon Lee <Damon.Lee@data61.csiro.au>
For 64-bit, this adds a 2nd-level page table for mapping devices using
2MiB frames instead of 1GiB frames.
The boot mapping and hardware header generator have also been fixed to
correctly report the number of large frames needed for devices rather
than only reporting the first. The frame size is also specified
correctly (rather than assuming mapping with 4KiB frames).
This likely fixes an issue whereby only the first 4KiB frame of a device
was reserved but the remaining region of that kernel device could be
mapped at user level.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Fix tk1 smmu cmake config variables.
Fix platforn_gen for tk1.
Add separate hardware.yml for tk1.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
"const TYPE *ptr" creates a non-const pointer to const data; for the
pointer itself to be rodata requires "TYPE *const ptr".
Taking the size of the pointer is caught by -Werror by default; suppress
that.
Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
