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>
- Initialize all elements active_irq during PLIC init and done't assume
implicitly that irqInvalid is zero.
- make active_irq hold elements of the type irq_t and not uint32_t.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
MODE_RESERVED is unused on RISC-V, so remove it from the code base. It
can be brought back when needed based on the state of the ARM
implementation, which has been clean up to remove global dependencies.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- define NUM_RESERVED_REGIONS to align ARM and RSIC-V code
- add runtime checks to catch errors. These checks can't be static or
use assert(), as the parameters are passed by a kernel loader. They
must be considered dynamic and can potentially change any time out
of the kernel's control.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Low version QEMU dump dts not have intc location information
and make subsequent generate dtb failed.
Error information:
Reference to non-existent node or label "/intc@8000000"
So when the QEMU version does not meet the requirements there
should be FATAL_ERROR to notice user early and immediately exit
Signed-off-by: Qiao Yongchang <qiaoyongchang@gmail.com>
In x86/boot_sys.c, we output a warning when `multiboot_mmap_length`
exceed limit. So we should correct its value after the `printf`.
close: #177
Signed-off-by: laokz <laokz@foxmail.com>
Print the available physical memory regions before printing the reserved
virtual memory regions, because as this order is more intuitive. For the
checks the order does not make any difference. Factor out the checks
into separate function to improve code readability.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
python2 is not used in the kernel build anymore so the tool
definition is unnecessary.
python2 is also end-of-line so there is no reason to think
we would ever depend on it again.
Signed-off-by: Ben Leslie <benno@brkawy.com>
Check the return value from execute_process calls and fail
with an appropriate message.
This makes debugging of cmake failures much easier.
Signed-off-by: Ben Leslie <benno@brkawy.com>
Ensure the primary core grabs the BKL once the generic kernel init is
done and the secondary cores are running. Improve the comments to
clarify that this is done to play safe.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
