This commit introduces `addressTranslateS1` to be used on Arm platforms
with hypervisor enabled for stage 1 (vaddr to IPA) translation. On
AArch32 this is a rename from `addressTranslateS1CPR`, and on AArch64 it
wraps `ats1e1r`. This changes the ABI on AArch64 to report faulting
address as IPA.

Reasoning:

With hypervisor enabled, AArch64 defined `addressTranslateS1CPR` to do
nothing, while AArch32 defined it to do stage 1 translation. This
delivered VM faults to the user with the faulting address being either
an IPA or a vaddr depending on mode. This inconsistency is undesireable.

This commit proposes adjusting the inconsistency to match AArch32
behaviour, as it is one of the verified platforms.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

There are cases that reasonably require non-ASCII characters in the
source code, hence tools/bitfield_gen.py must be able to handle them
correctly. This commit makes sure the bitfield generator consistently
opens all files with UTF-8 encoding.

Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Bin Meng <bmeng.cn@gmail.com>

Generated from maaxboard-dcss-hdmi.dts (Avnet/linux-imx) for more
comprehensive device support. Updated overlay to align.
Signed-off-by: Mark Jenkinson <mark.jenkinson@capgemini.com>

Sometimes device trees may have differences between vanilla Linux
and SoC vendor, and the changes can be tedious to override with a
device tree overlay.

This change allows overriding the platform default dts and overlays
with a custom dts.

Signed-off-by: Markku Ahvenjärvi <markkux@ssrc.tii.ae>

Some inter-procedural optimisations can produce cloned or partial
functions in the binary. Since binary verification is incompatible with
cloned and partial functions, we add a config option to disable these
optimisations.

This does not change any defaults, so to avoid cloned and partial
functions for a binary verification build, it is necessary to explicitly
configure this, e.g. using `-DKernelBinaryVerificationBuild=ON`.

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

For ARM currently TIMER_PRECISION exists, but that is in microseconds
and not fine-grained enough.

This is needed to make periodic tasks synchronous with the system clock.
If this value is zero every period will be extended with the overhead of
taking an interrupt and reading the system clock. To avoid this drift,
the configured value should be set to at least the average overhead.

See also issue #844.

Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>

sc_sporadic() already calls sc_active.

Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>

The MCS-related macros were causing the build to fail when configured to
use the sysenter instruction. Additionally, some message registers
weren't explicitly being passed to the assembly block for
seL4_NBSendRecv in this configuration.

Signed-off-by: Jimmy Brush <code@jimmah.com>

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

Use kernel's config.h

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

Avoid redundant code.

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

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>