Check if QEMU_OUTPUT_MESSAGE is empty before the STRIP
If no error in the previous qemu test command, the output
message is empty (QEMU_OUTPUT_MESSAGE), then the STRIP
will fail on empty input. Then, if it is empty do not
run STRIP.
Signed-off-by: Juan Pablo Ruiz <juanpablo@ssrc.tii.ae>
Add KernelCustomDTSOverlay option to append user provided DTS overlay
files. This way users do not need to modify the seL4 kernel sources
just because they use a hardware module differently. Also useful for
defining VM memory regions.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.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>
32-bit architectures have to share a small 4GiB address space between
privileged and non-privileged modes. Picking the address to split the
address space at affects how much virtual memory userlevel can use, and
how much physical memory the kernel can turn into untypeds. This is
something that should be configurable policy as different divisions make
sense for different applications. For now we only add the config
option to qemu-arm-virt to try it out before potentially adding it to
all 32-bit platforms.
Signed-off-by: Kent McLeod <kent@kry10.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>
When KernelIsMCS is set a different timer device is used by the kernel
which is selected by an MCS specific device tree overlay. This overlay
now sets the correct serial device for the nitrogen6sx board.
Signed-off-by: Kent McLeod <kent@kry10.com>
Mutate cannot be used to badge endpoints (many years ago, before the
first public release, this was possible, but was removed).
Also explain why Mutate is not always replaceable with Mint+Delete.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The concept of untyped object was confusing the description here, esp
when it comes to the CDT and what is derived from what. Also explain
when memory is actually zeroed, because that is important for where you
want to make sure that no confidential data remains in memory, for
instance.
This commit only affects the retype/revoke explanation and does not
attempt to clear up the concept of untyped object more generally.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add error conditions for the lazy bind of SchedContexts to
notifications or TCBs (introduced in e18e32e28e).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Some of the Github actions in this repository require secrets for
access to hardware test or other compute infrastructure, or for
deployment. When these are run in a fork on GitHub they are safe,
but generate annoying error messages.
This commit adds tests in the relevant actions whether they are run
from the seL4 org or not, and skips the action when they are run
outside. This should make the remaining actions more useful on forks.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- seL4_FailedLookup in X86IOPageTableMap
- seL4_FailedLookup in ARM page invalidation operations
- seL4_FailedLookup in ARMASIDPoolAssign
Signed-off-by: Jimmy Brush <code@jimmah.com>
Extra spaces are inserted after texttt tags when generating doxygen
comments in order to ensure that xmlonly tags are readable by doxygen.
The extra spaces cause a description like this:
```
Testing <texttt text="1"/>, 2, 3
```
To be rendered like this:
```
Testing 1 , 2, 3
```
This change identifies text runs that start with extra spaces and either
a period or a comma and removes the extra spaces, allowing at least
common punctuation to be rendered correctly.
Signed-off-by: Jimmy Brush <code@jimmah.com>
- pass DTB as paddr/len and check location
- Fail boot if DTB region is invalid. Logging error messages requires
reordering the code.
- Do not copy the whole DTB region, but only the actual DTB data to
bootinfo.
- Align the ARM and RISC-V implementations.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- Pass on the DTB as paddr/len.
- Fail boot if DTB region is invalid. Logging error messages requires
reordering the code.
- Do not copy the whole DTB region, but only the actual DTB data to
bootinfo.
- Align the ARM and RISC-V implementations.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
When the kernel is built the build system is responsible for finding
a suitable physical memory location where the kernel can be put on
the given target platform.
This is recorded into the kernel.elf file and read by the elfloader
program when it loads the kernel to that memory address.
In order to find memory blocks to avoid, the build system looks for
the /reserved-memory node in the target platform's device tree dts,
along with other device memory blocks.
The bcm2837 / Raspberry Pi 3 bootloader uses the first memory page
at address 0x0 to load a so called armstub which is used to set up
the ARM processor's initial state. It is also used to "park" the
secondary cores by putting them in a spin loop located within the
armstub from which the boot core can release them when ready.
The rpi3.dts already contains a /memreserve/ node reserving this
page, however as the build system only looks for the standardized
reserved-memory node it promptly disregards it and allow the kernel
to be loaded at physical address 0x0, overwriting the armstub.
A side effect of this is that the spinloop code also is overwritten,
potentially releasing the secondary cores to execute whatever kernel
code is written in the place of their spinloops, causing all kinds
of undefined behavior dependent on both race conditions and kernel
elf layout. It also implies that the kernel SMP boot code would not
be able to release the cores if implemented for the platform.
This patch adds the /reserved-memory node to the overlay-rpi3.dts
file and a child node reserving the memory region for the first
memory page. This in effect causes the kernel to instead be loaded
to 0x1000000 (aligned to a supersection).
Co-authored-by: Axel Heider <axelheider@gmx.de>
Signed-off-by: Viktor Sannum <sannum.viktor@gmail.com>
The bitfield generated accessor would only return an error if the region
being turned into an untyped was seriously wrong and would have already
been caught by earlier error checking in the region setup code.
Signed-off-by: Kent McLeod <kent@kry10.com>
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>
reserve_region() adds a region to a reserved list so that it doesn't get
turned into device untypeds. init_freemem() also takes a reserved region
list for regions that aren't supposed to be turned into regular untyped
or device untyped. If the ui_p_reg region is > PADDR_TOP then it is
outside of the region of memory that can be turned into regular untyped
and doesn't need to be added to this reserved list, but it still needs
to be added to the device untyped reserved list so that it doesn't show
up as device untyped. (It is already given to user level as frame
objects and so shouldn't also be reachable via different UT objects).
Signed-off-by: Kent McLeod <kent@kry10.com>
It's incorrect to add a region in boot_state.mem_p_regs to the reserved
region list. The reserved region list's purpose is for restricting the
creation of any untyped objects. This error was being masked by a second
call to reserve_region with a partially overlapping region that caused
the memory region to get actually turned into regular untypeds, but the
other reserved region to still get turned into device untypeds.
Now the range [0x0, 0x100000] isn't being added to a reserved region and
will still be turned into device untypeds.
This change shouldn't change the untypeds given to userlevel.
Signed-off-by: Kent McLeod <kent@kry10.com>
The KernelArmExportPTMRUser and KernelArmExportVTMRUser options for
enabling user access to the generic timer were previously only supported
on aarch64 but are now supported on aarch32 also.
Signed-off-by: Kent McLeod <kent@kry10.com>
The function Arch_finaliseInterrupt() is empty now and can be removed as
it serves no purpose any longer. There has never been a guarantee that
it gets only called due to kernel entry caused by an interrupt. Instead,
getActiveIRQ() is called in various places of the kernel to check if
there is a pending interrupt. There is a guarantee that the generic
kernel code calls ackInterrupt() within the same kernel entry call
path eventually, when it has finished processing this interrupt. Any
architecture or platform specific cleanup can be done there is this is
necessary.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
PC99 is the only platform that uses Arch_finaliseInterrupt() instead of
ackInterrupt(). There seem no reason for this, thus the code is moved
from Arch_finaliseInterrupt() to ackInterrupt() now.
Arch_finaliseInterrupt() is empty now, but still kept, because it is
part of the proofs and provides a hook that might be useful one day.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
On aarch64 in EL2, there aren't any addresses after 2^48 and so the
any kernel device untypeds that have very large physical addresses could
potentially move into an invalid address range when translated to a
Kernel window PPTR address when being stored in a cap slot. The kernel
in EL2 doesn't need to share its address space with user level and so we
can make the kernel window start low enough that we can't get overflows.
We start from the second entry in the top level page table so that we
don't conflict with any setup code running in the lowest 512GiB of
virtual addresses.
Signed-off-by: Kent McLeod <kent@kry10.com>
CONFIG_DEBUG_BUILD and CONFIG_PRINTING are different config options that
can be used independently from each other. CONFIG_PRINTING controls the
backend of kernel print functions while CONFIG_DEBUG_BUILD controls
other kernel debug features.
Note that CONFIG_VERIFICATION_BUILD is the config option that controls
whether any of these options can be used.
Signed-off-by: Kent McLeod <kent@kry10.com>
- resolve mix of service mechanism, abstraction
- update verification explanation + references
- remove reference to ARM11 which is slated to be discontinued
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- KernelGlobalsFrame caused the definition of seL4_GlobalsFrame which
was a reservation at the top of the user address space on ARMv6
platforms.
- KernelDangerousCodeInjectionOnUndefInstr was used to implement calling
user code in kernel mode won ARMv6.
Signed-off-by: Kent McLeod <kent@kry10.com>
Remove all support for ARMv6 architectures now that all platforms and
CPUs that use this architecture have been removed.
Signed-off-by: Kent McLeod <kent@kry10.com>
