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>
Presumably, this was copied from the common_arm.lds linker script,
but it was a particular implementation detail of the arm32 code,
and is unneeded on RISC-V.
Signed-off-by: julia <git.ts@trainwit.ch>
These are never supposed to happen.
Note, that this will still use the kernel stack to save the registers
and so if page tables are corrupted, it will continually fault near the
trap_entry. But this is reasonably easy to tell from a debugger.
Not all traps will be handled via the s-mode trap handler; it depends on
the value of the `medeleg` register. This appears to default to 0xf0b509
(in QEMU) and so we can catch page faults.
Without this, traps in the kernel will be attributed to a trap of the
current running thread.
Previously, some kernel modifications that corrupted memory caused:
```
Caught cap fault in send phase at address 0
while trying to handle:
vm fault on data at address 0 with status ��7
in thread ��ffffffff8401bc00 "idle_thread" at address 0
With stack:
Invalid vspace
```
Now, the kernel prints out:
```
KERNEL ABORT (exception within s-mode)!
scause: 0xf, stval: 0x0
halting...
Kernel entry via Syscall, number: 1, Call
Cap type: 2, Invocation tag: 1
```
Signed-off-by: julia <git.ts@trainwit.ch>
On aarch64, clang interprets the compile option -mgeneral-regs-only
as disabling all FPU-related registers and instructions, which not
only include those generated by the compiler (which is how gcc would
interpret this option), but also those in (inline) assemblies written
explicitly by the programmer, which gcc does not forbid with this
option. This commit enables FPU-related registers and instruction
explicitly in the FPU-context switching code, so the kernel will build
under clang-18 on aarch64. The commit that changed the behaviour
between clang-17 and clang-18 is eabffc7 of the LLVM project.
Signed-off-by: Liu, Chang <cl91tp@gmail.com>
Presumably intended to be something like
typedef enum IRQConstants { ... } platform_interrupt_t;
this instead declares a symbol that is exported and kept in the
binary, but is never used. Remove it.
Spotted as my kernel.elf binary contained a strange symbol:
ffffffff8401b7f0 g O .bss 0000000000000004 platform_interrupt_t
Signed-off-by: julia <git.ts@trainwit.ch>
The previous commit 05858be didn't actually add it to both instances
of the if/else statement, and so doesn't actually work in all cases
(e.g. with `../init-build.sh`).
Signed-off-by: julia <git.ts@trainwit.ch>
This refactors refill_budget_check and schedule_used to
ease verification by limiting heap access via refill_head
and refill_tail, and providing (inlined) named functions
for both the condition and bodies of the loops.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
The settings KernelArmVtimerUpdateVOffset and
KernelArmDisableWFIWFETraps should be project settings, not platform
settings, and the values set here are not required for the platform to
work -- they just provide a different default.
Setting these in platform configs could lead to inconsistent project
builds when switching between platforms.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The default python version changes on ubuntu-24, which breaks the
version of cmake-format we are currently using.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Current TCB_PTR_CTE_PTR assumes that thread blocks are aligned at
BIT(seL4_TCBBits). However the idle thread blocks are aligned
differently at BIT(TCB_SIZE_BITS), thus TCB_PTR_CTE_PTR cannot be
used for idle threads.
This changes idle thread alignment to be consistent with standard
TCBs. Even though macros like TCB_PTR_CTE_PTR should not be used
for idle thread, verification assumes consistent alignment for all
TCBs.
Signed-off-by: Yanfeng Liu <yfliu2008@qq.com>
Multiple versions of GCC were unable to determine that these variables
in decodeX86PortInvocation are initialized in all cases.
Oddly, this compilation failure was only observed with -O1. Compilation
with -O2 was not failing.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
The increment and reserve here is not an issue, but to keep
consistency with the change made in 291af86 we should remove it.
See PR #1317 for more info
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
In cases where the kernel is passed a very fragmented map of
available memory (specifically when booting from GRUB on x86),
it is possible for multiple available regions to overlap with
a single reserved region.
Currently, if there is an overlap
(where avail_reg[a].start >= reserved[r].start), the available
region is trimmed and the region index is incremented. This causes
any other overlapping regions to be handled as if they are
non-overlapping, since it's now looking at the next reserved region.
This eventually leads to reserved memory being passed to the root
task and can cause corruption issues if it is used.
It is fine to skip this index increment, since the available region
is now either empty or non-overlapping, and both cases are already
trivially handled.
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
This adds `seL4_CapSMC` to table 9.1 and updates section 9.1 so
that to be in line with latest upstream code.
Signed-off-by: Yanfeng Liu <yfliu2008@qq.com>
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>
Do not perform cache flushing in clearMemory. Instead flush the cache
only for those object types where it is necessary, and only when the
object is retyped, not when the untyped cap is reset.
This reduces overall need for flushing and delays it to the point of
use. This should speed up boot time significantly, but may impact WCET,
because the largest flush is now the largest page size (e.g. 24) instead
of CONFIG_RESET_CHUNK_BITS (8). The user could already request a flush
of the largest page size before, though, so it this may not actually
impact WCET. Remains to be investigated.
Why this is safe:
- Flushing is only necessary for objects that are seen by other parts of
the system, not for kernel-internal object. These objects are
non-device frames (including IOMMU pages) and page tables. All other
objects are only read/written by the kernel. Frames need to be flushed
to RAM (as clearMemory did), because they could be seen uncached by
devices. Page tables only to PoU for the page table walker.
- Before createNewObject in retype, these objects do not exist and
cannot be seen by any part of the system. createNewObject is the point
where new objects can become visible to the user.
- Theoretically, we could defer flushing further to the point where
frames or page tables are mapped, but it is more complex to track
whether a flush has already happened when they are mapped multiple
times, whereas at retype the object cannot have been flushed already.
- The original implementation, before clearing memory was moved into
reset untyped, also flushed at the same points.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This factors out code from cancelAllIPC and cancelBadgedSends
by introducing the inline function restart_thread_if_no_fault
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Make str_to_long more defensive against malformed content, since this
function runs on user (cmd line) input on x86. The input is from boot
time, i.e. trusted, but the function should still be memory safe.
This change does not fix overflow issues which may still lead to
undefined behaviour.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
getKernelStack() is never called, and readHTPIDRO() was only called in
getKernelStack(). readTPIDRPRW() is only used in hyp configurations.
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>
This configuration is not in CI (hence why it lead to
a build error in the first place) so I just tested
it locally via sel4test with:
```
../init-build.sh -DPLATFORM=qemu-riscv-virt \
-DMCS=1 -DKernelRiscvExtD=1 \
-DKernelRiscvExtF=1 -DRISCV32=1
```
and it passed.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Print virtual address already mapped in user error
Co-authored-by: Axel Heider <axel-h@users.noreply.github.com>
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This eases verification by using a local variable
which remains unchanged during execution of the
function.
This preserves semantics since tcbSchedDequeue
will not modify the scTcb field of the given sc.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
On aarch32, single stepping is configured by setting an instruction
breakpoint to mismatch mode. The way that it is checked whether a
given breakpoint is being used as a normal breakpoint or for
single-stepping is by checking if it has been configured to mismatch.
This works because the HW debug API does not currently provide a way
to otherwise configure mismatch breakpoints, but seems like an
unsatisfactory solution. Whether single-stepping is enabled, and
the breakpoint that is being used for it is already stored in the
TCB of a thread, and this commit changes checks related to
single-stepping to use this information instead.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
Changing the debug register fields to what they are referred to
as in the ARMv7 and ARMv8 manuals. Mostly a cosmetic change,
but improves clarity.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
