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>
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>
- Make assignments an atom, the compiler can handle the details.
- Define variables when they are needed.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Moving the type checks avoid the need for conditional compilation. This
also allows simplifying some include file dependencies.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- 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>
Previously, the case where there was no memory region large enough for
the root server objects was unhandled. The loop termination condition
(i>=0) was trivially true for all values of the loop variable. This
commit fixes the issue by making the loop variable signed, and adding a
failure case.
It also:
- adds a check for underflow in the calculation of the address to begin
allocating root server objects,
- removes two redundant checks that were guaranteed to be true, and
- adds some clarifying comments.
Co-authored-by: Axel Heider <axelheider@gmx.de>
Signed-off-by: Matthew Brecknell <matthew@brecknell.net>
The function plic_init_hart() is part of the internal kernel API, so
every SOC's PLIC implementation has to provide it, even if it is
empty.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- Use SMP_TERNARY() macro.
- Rename get_hart_id() to plic_get_current_hart_id(), as this is just a
helper function for the other PLIC code in this file.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.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>
Both Ariane and Rocketchip are experimental platforms that support
accessing peripherals, but the status of support for external interrupts
via a PLIC is unclear and my differ depending on the version that is
synthesized. Using the dummy PLIC driver seems the better option for now
to avoid confusion or even crashes.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- describe PLIC behavior and corner cases.
- provide a common header file for the API.
- add a dummy PLIC driver for spike.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- Move CSR SIE access wrappers to generic code.
- Move CSR SIE/SIP bit constants to header file.
- Rename CSR SIE/SIP bit constants to use the names from the RISC-V
specification.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
INTERRUPT_CORE_TIMER is just an alias for KERNEL_TIMER_IRQ. There is
no need for this indirection, KERNEL_TIMER_IRQ can be used directly.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
