This is useful for all x86 IOMMU work, which otherwise has
to duplicate the definitions of VTD_PT_INDEX_BITS in userspace
code. Follow the same pattern as many other existing code in
the libsel4 headers where the kernel depends on it.
Note we can't define seL4_IOPageTableBits in terms of Index + Entry
because the capDL tool does the c-preprocessor to make a YAML file
containing the constant, and it won't do evaluation.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Previously, this would just print a 'halting via unknown'
in debug mode when an SError occurred and SError ignore was
not turned on. This changes the trap code so that we print
out the known cause of the trap.
KERNEL INVALID VECTOR ENTRY!
Vector: 0x580 (SError 64-bit EL0/EL1)
Fault attributed to program counter: 0x221dc0
ESR: 0xbf000000 FAR: 0x2881c98000824100
halting...
Kernel entry via Unknown (0)
This was encountered after some rust-seL4 changes to the
initialiser for Microkit related to untyped mappings broke
boot: https://github.com/seL4/microkit/issues/541
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Make the function validFaultHandler available to the assert in
sendFaultIPC in faulthandler.c.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
User context already has a kernelSP, which is used.
Also, the 64-bit also doesn't has this, so probably a leftover.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Apply the changes from commit 771c9e43ce to the signal fast path,
which was missed there.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- Introduce functions to append and dequeue to/from endpoint and
notification queues, in order to make verification feasible. Handle
linked list manipulations with the same functions that were
previously used for the ready and release queues, together with a new
function that allows for a new item to be inserted into the queue
after another item that is already in the queue.
- Remove tcbEPNext and tcbEPPrev pointers from the MCS version, and
instead use tcbSchedNext and tcbSchedPrev pointers, given that no
thread can be simultaneously in any two of the endpoint,
notification, ready, or release queues.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Currently, the kernel permits userspace VMMs to enable and use the
VMX-preemption timer by allowing writes to the following VMCS fields:
- VMX_GUEST_PREEMPTION_TIMER_VALUE (count)
- VMX_CONTROL_PIN_EXECUTION_CONTROLS (timer enable bit)
- VMX_CONTROL_EXIT_CONTROLS (save current count on context switch bit)
It also forwards the timer expiry event as a VM exit.
But it does not tell userspace how fast the timer will count down,
making it impossible to use. This commit exposes the timer's scale
via `seL4_X86_VCPU_ReadMSR`.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Allow CR0.PE and CR0.PG to be cleared if "Unrestricted Guest" mode is
supported by the host CPU. This mode allows guest software to run in
unpaged protected mode or in real-address mode. From [1] with Indan's
feedback applied.
[1] https://github.com/seL4/seL4/pull/1438
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Co-authored-by: Heyang Zhou <hello@su3.io>
Only call the command on CMake files that may be the first file
evaluated from the project. Remove from all other files.
Signed-off-by: Kent McLeod <kent@kry10.com>
The AArch64 FPU trap helpers were modifying both CPTR_EL2.TFP and
CPTR_EL2.TCPAC when enabling or disabling FPU trapping. However, only
TFP controls trapping of FP/SIMD instructions from EL0/EL1 to EL2.
TCPAC traps accesses to CPACR_EL1 and is unrelated to FPU instruction
execution. Trapping CPACR_EL1 is unnecessary for seL4’s FPU handling
and can interfere with other architectural features that are
controlled via CPACR_EL1.
In particular, CPACR_EL1 is an Architectural Feature Access Control
Register and is not limited to FP/SIMD. For example, Morello uses
CPACR_EL1.CEN to enable CHERI instructions. Trapping CPACR_EL1 via
TCPAC would therefore require special handling or could break guests
that legitimately modify CPACR_EL1 for non-FPU features.
Since seL4 only needs to trap FP/SIMD instructions if FPU is disabled
per TCB/VM, it is sufficient to control CPTR_EL2.TFP alone. Remove the
modification of TCPAC from enableTrapFpu()/disableTrapFpu() and leave
CPACR_EL1 accesses untrapped.
This aligns the implementation with the architectural intent of the
AArch64 FP/SIMD trapping model and avoids assuming that CPACR_EL1 is
used solely for FPU control.
See Issue #1601 for more context and discussion.
Signed-off-by: Hesham Almatary <hesham.almatary@cl.cam.ac.uk>
- Factor out the inline assembly from invokeSMCCall so that it can be
made a separate machine operation in the specification. This part of
the change should produce the same binary as before.
- Parse IPC buffer arguments in decode, not in invoke. This eliminates
the "buffer" argument to the invoke function and keeps argument
processing in decode.
- Use setMR instead of replicating its functionality.
- Reduce decode argument list to the ones that are used.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
No change to behaviour, the commit just makes sure all cases are
explicitly listed instead of falling through to default.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This in particular introduces the function
schedContext_unbindReply, which is used within
finaliseCap, as well as invokeSchedContext_Unbind.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Try detect if we are running as a guest based on the CPUID
and skip clock_sync_test if we are.
Similar as previous patches for skipping QEMU on ARM/RISC-V
but at run-time instead of build-time.
Tested with qemu-system-x86_64 using `-smp 4`, the test is now
skipped with regular QEMU as well as `-accel kvm`.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
White space change only:
- left-align sizes within each block declaration
- min 2 spaces to separate field name from size
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Eliminate #ifdefs for BF_CANONICAL_RANGE in bitfield specifications,
using the new field_ptr command. Use word_size expressions for some of
the padding fields to make clearer where the sizes come from.
The transformations in this commit are written to produce exactly
identical output for code and proofs. In some rare cases, padding
could in the future be rearranged to make more use of field_ptr, but
these edits would create code differences and are left for later.
It may now also be to share more blocks between generic 32 and 64
definitions if they only reference word_size. This is also left for
later to reduce noise.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Doing an ISB is very expensive, about ~30 cycles on some CPUs,
so try to avoid them if possible.
For the writes to (most) system registers to be observed, a
'Context Synchronization event' needs to occur (see ARM DDI 0487
M.a §D24.1.2.2 / pD24-8367).
The kernel is not doing any FPU operations after disabling the FPU,
so there is never a need for an ISB there. Returning to user space
counts as a 'Context Synchronization event' and ensures the FPU enable
or disable has completed when user space starts executing.
An ISB after enabling the FPU is only needed in case the FPU was
disabled for the kernel and the kernel wants to do FPU operations
like saving or restoring the FPU state. The ISB ensures that the
FPU enable system register write is finished before FPU using
instructions are executed.
For Aarch64 non-HYP it is possible to disable the FPU for user space
(EL0), but keep it enabled for the kernel (EL1). This is done by
setting CPACR_EL1.FPEN to 1, which the code actually already did.
Aarch64 with virtualisation enabled is more complicated and needs
higher level changes to achieve the same, which aren't done here,
the change is limited to removing the ISB in disableFpu().
This partially fixes issue #1569.
Signed-off-by: Indan Zupancic <indan@nul.nu>
This will sometimes fail when using QEMU RISC-V virt
with multiple cores, make the behaviour consistent as
QEMU ARM virt.
Given that QEMU is not intended to be a cycle accurate
simulator, I imagine that is why this does not reliably
succeed.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Otherwise it is not possible to send SGIs to all cores on platforms
with non-contiguous Affinity values or more than 16 cores.
16 is the limit of the target list, which is only relevant when
sending an SGI to multiple targets at once.
Update the API documentation to reflect what's actually happening.
Signed-off-by: Indan Zupancic <indan@nul.nu>
The compile error for exposing vcpu_t could be easily fixed, the real
issue is the functions not existing when HYP is disabled.
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This reverts https://github.com/seL4/seL4/pull/1490 as the
change that was made in that PR was reading the wrong part
of the GIC specification, because ARM decided that the
register layouts are different in non-secure vs secure mode.
Fixes (again) https://github.com/seL4/seL4/issues/1489
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
These diagrams were really unclear and confusing to me,
especially as I always needed to convert from "2^64 - 2^39"
form to "0x0000008000000000" form many times in my head.
They were also out of date and wrong, containing graphics of the
PDPT (from x86) as well as TLB bitmaps.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Move setIRQTrigger from <arch>/hardware.h into interrupt.h together
with the rest of the IRQ interface, because it is now a visible
interface even for platforms and architectures that do not provide the
functionality.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Provide a default dummy implementation for setIRQTrigger even for
non-GIC platforms where this operation is not supported. Otherwise,
the function is declared in the header, but has no implementation.
Implementing it as UNREACHABLE() means verification will show that the
function is not called.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Adding a spec with precondition False means verification has to show
that the function is not called.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Provide an implementation of the header function plat_SGITargetValid
even for non-GIC platforms. This function will not be called, but
verification has a general lemma about it, and the default
implementation makes that lemma true without adding special cases.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
There's a few cases in the kernel where the ksKernelEntry tracking
is not perfect, such as in SError reporting, and (I believe) a few
other places which I haven't tracked down to a cause - but some of
e.g. the RISC-V trap code where the first entry faults and the 2nd
proceeds can report stale information.
In these cases, the kernel says that the entry was via a certain
syscall or interrupt (etc), even though that was clearly not the
case because we know the kernel exited. Now we will print out this:
halting...
Kernel entry via Unknown (0)
The changes:
- When exiting the kernel, via `c_exit_hook()`, reset
`ksKernelEntry.path` to "Unknown".
An alternative here would have been add a global "valid" boolean
to the kernel state, but this requires modifying every site where
we set the ksKernelEntry.path to also set valid = true, which is
ugly.
- Remove Entry_UnimplementedDevice from entry_type_t as it is never
used, to leave enough room to add Entry_Unknown.
- Switch out the CONFIG_DEBUG_BUILD || BENCHMARK TRACK ENTRIES #if
in the x86 breakpoint code with the more concise
`TRACK_KERNEL_ENTRIES` define used elsewhere.
Signed-off-by: julia <git.ts@trainwit.ch>
Similar to #510 but for all other platforms. The idle_thread runs
without a stack and so cannot handle the stack prologue. This should
hopefully make the kernel rely less on FORCE_INLINE for this as well.
We create idle.S assembly files for each platform, as GCC does not
support `__attribute__((naked))` on AArch64 (GCC 13.2.0) and bails out.
Signed-off-by: julia <git.ts@trainwit.ch>
Helps the C compiler to recognise irqInvalid as a constant. This in
turn helps with binary verification, because irqInvalid is already
parsed as a constant in Isabelle since it is never written to.
See also the discussion in #1349 and #1324
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The GIC platforms use irq_t for irqInvalid -- bring remaining AArch32
platforms in line with that.
irq_t is an unsigned type (when it is an integer) and enum constants are
signed. For the proofs to treat these platforms uniformly, they need to
be the same kind. They can't all be enums, because irq_t can be a more
complex type for SMP platforms.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Also, change the definition of ASID_HIGH from
((a >> asidLowBits) & MASK(asidHighBits))
to
((a) >> asidLowBits)
because the mask is an unnecessary operation (this is handled by the
proofs). It is unnecessary because these (SW) ASIDs are kernel-only
and are never exposed to users, so they will never set bits asid from
the asidLow and asidHigh bits.
Signed-off-by: julia <git.ts@trainwit.ch>
According to Arm documentation, the exception-handling routine
needs to zero the following bits in FPEXC:
DEX, IDF, IXF, UFF, OFF, DZF and IOF
In seL4, the user space fault handler should do this, as the kernel
doesn't know when user space is done handling the FPU trap.
In case of virtualisation, the guest kernel should clear these bits.
Now that the seL4 kernel doesn't handle FPU traps itself any more,
user space can handle asynchronous traps if it wants to.
Signed-off-by: Indan Zupancic <indan@nul.nu>
On 32-bit ARM the fpexc system register is set by loadFpuState,
which includes the FPU enable/disable bit FPEXC_EN_BIT. This
register is part of the usercontext and needs to be initialised
correctly, otherwise the FPU will be disabled by loadFpuState.
Before, this bug was hidden because the FPU was enabled lazily
after a trap. This bug just caused one extra FPU trap at first
FPU use for each task: The first handleFPUFault would fail to
enable the FPU, causing another FPU trap when user space gets
restarted.
On the second FPU fault, switchLocalFpuOwner calls enableFpu first
and then calls saveFpuState because ksActiveFPUState is set to the
current task's FPU state. Then it gets saved with FPEXC_EN_BIT set
and the task can continue with the FPU actually enabled.
This also means that with the old code, the initial FPEXC state
of each task was equal to the previous active FPU task's.
Signed-off-by: Indan Zupancic <indan@nul.nu>
