sysexit requires a 64-bit operand to remain in 64-bit mode when
switching to user level. gcc versions older than 12 encode this as
"REX.W SYSEXIT" while clang encodes this as "SYSEXITQ". Both compilers
don't support the alternate encoding. We instead use ".byte
0x48,0x0F,0x35" which is the actual opcode of the required instruction
which will work with both compilers.

Signed-off-by: Kent McLeod <kent@kry10.com>

Changes compiler options and the linker script to group most small data
objects together in a new .small section, and point __global_pointer$ at
.small so that nearly all objects can be referenced via gp.

Signed-off-by: Stefan O'Rear <sorear@fastmail.com>

Signed-off-by: Stefan O'Rear <sorear2@gmail.com>

For writing/reading/copying TCB registers, the
arch_flags parameter is not used on RISC-V (in
addition to x86 and ARM).

Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>

Various kernel symbols have changed their names; update
the GDB macros to match.  Also remove hard-coded  0xf0000000 for
the address of the kernel window.

Signed-off-by: Peter Chubb <peter.chubb@unsw.edu.au>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

When using the cortex-a9 CPU allow the kernel to be used as a
hypervisor.

Signed-off-by: Kent McLeod <kent@kry10.com>

seL4_UserTop must be defined to be > 0xC0000000 when the kernel is in
hyp mode due to assumptions made by the kernel init code.

Signed-off-by: Kent McLeod <kent@kry10.com>

Accessing the hyp mode SPSR register via the banked instruction syntax
is UNPREDICTABLE if hyp is the current mode. The direct syntax needs to
be used instead. This is documented in the ARMv7 Architecture reference
manual.

Signed-off-by: Kent McLeod <kent@kry10.com>

The value supplied in the maaxboard.dts file provided by
Avnet is too small. It is corrected in the overlay DTS file.
Signed-off-by: Mark Jenkinson <mark.jenkinson@capgemini.com>

Signed-off-by: Mark Jenkinson <mark.jenkinson@capgemini.com>
Co-Authored-By: Stephen Williams <stephen.williams@capgemini.com>

Set Write-through non-transient, No-Write-allocate, Read-allocate
attributes for kernel log buffer.

Signed-off-by: Nataliya Korovkina <malus.brandywine@gmail.com>

CPSR.AIF already presented in HCR_COMMON macro,
And HCR_NATIVE includes HCR_COMMON, then no need
To set CPSR.AIF bit again

Signed-off-by: Cao Jianlong <caojianlong@outlook.com>

The seL4 CMake build currently uses the `stat` utility to determine the
size of the flattened device tree file. The `stat` utilities in macOS
and GNU coreutils have different interfaces, the CMake build needs to
determine which one it's using.

This change supports building on macOS with GNU coreutils in the PATH,
by only using the macOS `stat` interface with `/usr/bin/stat` on a macOS
host, and otherwise assuming GNU coreutils.

In future, we might be able to avoid the `stat` utility altogether, by
using the built-in `file (SIZE ...)` command that became available in
CMake version 3.14. For now, we avoid updating our build dependencies.

Signed-off-by: Matthew Brecknell <matt@kry10.com>

The latest code updates introduced CONFIG_ENABLE_KERNEL_LOG_BUFFER
meanwhile other code and config.cmake keeps using
CONFIG_KERNEL_LOG_BUFFER

Signed-off-by: Nataliya Korovkina <malus.brandywine@gmail.com>

Remove x86 and Arm from heading of the "Re-using address spaces" caveat
because it's also present on RISCV and isn't actually arch specific.

Signed-off-by: Kent McLeod <kent@kry10.com>

Provide the raw timer register values, higher layer may then detect
and handle roll overs.

Signed-off-by: Axel Heider <axelheider@gmx.de>

Signed-off-by: Axel Heider <axelheider@gmx.de>

Signed-off-by: Axel Heider <axelheider@gmx.de>

There is no need to cast twice.

Signed-off-by: Axel Heider <axelheider@gmx.de>

Now that there is no need to reserve page table entries in each VSpace
object, the full architecture specified address space range is usable.

Signed-off-by: Kent McLeod <kent@kry10.com>

Each vspace object has a count of how many SMMUv2 context banks are
bound to it. This attribute is moved out of a reserved page table entry
slot into the asid_map_t structure.

This also reduces the width of the MappedCB field from 12 to 8 bits
which is large enough to hold the maximum number of CBs allowed by the
SMMUv2 spec (128). This conserves otherwise wasted bits.

Signed-off-by: Kent McLeod <kent@kry10.com>

When switching to the new thread, it's VSpace must have a valid ASID
mapping. This means that the ASID in the vspace cap must resolve to the
same vspace object as the vspace cap does. In addition, when the VSpace
object is for a stage 2 translation there must be a currently assigned
hardware VMID for the vspace. Otherwise the slowpath must be taken.

Once these checks are done, the TTBR registers can be directly updated
without needing to perform another ASID translation.

Signed-off-by: Kent McLeod <kent@kry10.com>

This stores the 8-bit vmid in the ASID map rather than in a
slot of the virtual address space root for hypervisor configurations.

Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Kent McLeod <kent@kry10.com>

This uses the asid_map bitfield from x86 for aarch64 to map from ASID to
a given address space.

This will allow for alternate mappings from ASIDs in the future as well
as moving small amounts of metadata into the the ASID table itself.

Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Kent McLeod <kent@kry10.com>

Signed-off-by: Axel Heider <axelheider@gmx.de>

Signed-off-by: matt rice <ratmice@gmail.com>

Signed-off-by: matt rice <ratmice@gmail.com>

Signed-off-by: matt rice <ratmice@gmail.com>

Signed-off-by: matt rice <ratmice@gmail.com>

Signed-off-by: matt rice <ratmice@gmail.com>

Signed-off-by: matt rice <ratmice@gmail.com>

Signed-off-by: matt rice <ratmice@gmail.com>

The condition element currently exists parallel
to the condition attribute.  The condition attribute
should be removed in a subsequent patch.

Signed-off-by: matt rice <ratmice@gmail.com>

Signed-off-by: matt rice <ratmice@gmail.com>

No intended changes to the schema, just change
the schema from dtd to xsd, and update ci to use it.

Signed-off-by: matt rice <ratmice@gmail.com>

- SLOTS cannot be less than MAX_IRQ
- remove helper variable MAX_IRQ

Signed-off-by: Axel Heider <axelheider@gmx.de>

Bring up-to-date with current proof style, make style consistent,
slightly increase proof parallelism.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

A tagged union can now optionally use multiple fields to indicate the
tag. These are called "sliced" tags in the code. The tag fields have to
be at the same position and width in each block of the tagged unions,
and all tag fields have to be within the same word.

When sliced tags are used, tag class masks cannot be used at the same
time for this tagged union.

In the `tagged_union` declaration, the values of such sliced tags
become tuples. For instance, if `x` and `y` are tag fields (declared in
blocks not shown here) with width 1 and 2, we can write:

    tagged_union ex exType(x,y) {
        tag ex1 (0,2)
        tag ex2 (1,3)
    }

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

The conditional else-block with the dummy reference might have been
added once to avoid a compiler warning about unreferenced parameters.
However, 'int_vector' is used in the code now, so this is obsolete.

Signed-off-by: Axel Heider <axelheider@gmx.de>