- add new platforms supported by verification
- remove 32-bit imx8mm with FPU (proof out of date)
- add AArch64 integrity
- add FPU where covered
- remove caveat on lazy FPU and VCPU switching (fixed)
- remove caveat on SMP lock with clang (fixed)
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove debug printing inside handleSpuriousIRQ() to get the
same behaviour as on the other architectures. Spurious IRQ reporting
already happens on the outside of this function.
The IRQ that is printed has to be irqInvalid (= 0 on RISC-V), because
that is when this function is called. RISC-V introduces an additional
case when irq > maxIRQ, which should not be possible (could
theoretically happen during a board port when maxIRQ is set
incorrectly).
The reason this IRQ printing is coming up now is that MCS (incorrectly)
calls preemption point handling when no IRQ has fired, but thread budget
has expired. This registers as spurious IRQ in preemption handling,
since no IRQ happened and getActiveIRQ correctly returns irqInvalid.
Generic spurious IRQ printing was disabled for this case on the outside
of this function (until the MCS behaviour is adjusted), but the special
RISC-V printing was not covered by that measure so far.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
When building for aarch32 only 32-bit physical addressing is supported.
An overlay is needed to clamp memory that extends above 32bit addresses.
Signed-off-by: Kent McLeod <kent@kry10.com>
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>
The proofs are shared between GICv2 and GICv3, which means we want the
term structure to be the same for key functions that are visible to the
proofs (but constants are Ok to change).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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>
On 32-bit x86, when booting under multiboot1 the physical memories
above 4GB are skipped and not included as usable memory regions.
Make sure we also do this when booting under multiboot2.
Signed-off-by: Liu, Chang <cl91tp@gmail.com>
The i.MX8MQ platforms use a clock frequency of 8333333 rather
than the 8000000 value which the -MP and MM platforms do.
This caused booting seL4 on these platforms to always print
Warning: gpt_cntfrq 8333333, expected 8000000
which seems to have actually been a correct warning.
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>
Before this change, options that were hidden from the cmake-gui due to
unsatisfied config_choice conditions were not recorded in
gen_config.{yaml,json,h}. After this change, these hidden options are
recorded as disabled.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
... from the device UT listed by platform_gen. The kernel itself
does not care about this memory, and it is just given as device UT.
We also just remove the reserved array entirely from the return of
`get_physical_memory` since it only seems to be a footgun, it's
only used internally to affect what memory the kernel wants to use.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: julia <git.ts@trainwit.ch>
`align_memory()` in hardware.py both modifies the first normal memory
region to adjust the base of it for alignment, and adds an extra
reserved region to our list of reserved regions. This then feeds
through `get_addrspace_exclude` which inverts the regions given
and turns it into the available "device memory" at user-level.
dev_mem = hardware.utils.memory.get_addrspace_exclude(
list(reserved) + phys_mem + kernel_devs, config)
Anything as an argument to this is not given as "device memory" by
the kernel. (It does not precisely match how the kernel works).
However, since `align_memory()` has adjusted both the phys_mem up
(which *would* have added this region as "device" memory) but also
added it to "reserved" region, which then made it disappear entirely,
as "reserved" regions are not exposed to userspace.
However, this **does not** match the behaviour of the kernel, as it was
not reserved, so this behaviour did not match the untypeds given to
userspace. This commit solves this by removing the extra reserved
region being added for that memory.
PR #1426 worked around this issue by removing the alignment on AArch64.
Whilst this fixed the issue that microkit was seeing, it just masked
the underlying issue. Reverting that PR, then applying this fix,
results in the following platform_gen.yaml:
devices:
- end: 0x1000000
start: 0x0
- end: 0xff800000
start: 0x3b400000
- end: 0xff841000
start: 0xff801000
- end: 0x100000000000
start: 0xff843000
memory:
- end: 0x3b400000
start: 0x1000000
Note especially the device region from 0x0 to 0x1000000; which is the
combination of the 0x0 to 0x1000 reserved region, and the 0x1000 to
0x1000000 reserved by the kernel's alignment requirement. Previously,
the platform_gen.yaml reported only the 0x0 to 0x1000 region,
devices:
- end: 0x1000
start: 0x0
- end: 0xff800000
start: 0x3b400000
- end: 0xff841000
start: 0xff801000
- end: 0x100000000000
start: 0xff843000
memory:
- end: 0x3b400000
start: 0x1000000
I will be following this commit up with a PR to instead make the
alignment-reserved region into a new memory region, since there's not
any reason why userspace can't use this memory.
This has been tested on a few platforms with sel4test and with
microkit on the pi4B.
Signed-off-by: julia <git.ts@trainwit.ch>
The Isabelle side of the binary verification tool chain currently does
not implement proof tactics for the "continue" statement. Use skip
(semicolon) instead for empty loop body.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Wrap NUM_SGIS using wrap_config_set() so that verification automation
does not simplify it away automatically when it is 0.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Make the treatment of spurious IRQs equal between handleInterruptEntry
and preemption handling. The infoflow proof requires that these behave
identically -- this was so far only true for platforms that define
handleSpuriousIRQ to be empty (which is almost all of them).
Adding platforms to the verification that have a non-empty body for
handleSpuriousIRQ requires equalising the calls.
Factor out the code that is common between preemption and interrupt
kernel entry into its own function checkInterrupt to remove duplication.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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>
Fail early with IllegalOperation if IssueSGISignal is not supported at
all for the platform.
This also helps with verification, because the later range check gets
simplified away automatically, leading to divergent code paths.
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>
This was *fine*, because IT_ASID has an ASID_HIGH(IT_ASID) of
0, but the asid_pool_cap_new expects capASIDBase which should
instead be an aligned ASID ID (i.e. asidLowBits all 0).
Signed-off-by: julia <git.ts@trainwit.ch>
