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

Additional header files may now be included in non-C contexts and so we
need to guard some C definitions with the __ASSEMBLER__ guards
convention.

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

Using branch instructions only allows -+4 KiB offseting range
from the current PC. If the C code is placed (depending on
linkers and address layout) far more than -+4 KiB, linking
will fail (e.g., R_RISCV_BRANCH out of range: 4735 is not in
[-2048, 2047]; references c_handle_fastpath_call.

This commit accounts for this case and uses jumps when jumping
to C code that should give enough offset range (-+ 1 MiB) and
make the assembly code more portable.

Signed-off-by: Hesham Almatary <hesham.almatary@cl.cam.ac.uk>

Some slot positions in the rootnode would depend on configuration.
However that makes it difficult to add new root caps, especially if
multiple caps only exist based on configuration. Make all caps always
there, but null if not configured.

Signed-off-by: Robbie VanVossen <robert.vanvossen@dornerworks.com>

vaddr argument is 0th argument, not 2nd.

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

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

Now the vspace_cap is used for all vspace roots and all other page
tables are referred to by page table caps.

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

This is already what's presented at userlevel. Now the underlying kernel
cap reflects the same name.

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

The page_table cap is used in it's place.

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

Finish combining different page table types into a single type.

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

Next step is to merge pude_t type.

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

Remove the pde_t type and replace all usages with pte_t.
This doesn't remove the page directory cap type yet. Now the page
directory cap refers to a table of pte_t entries and is treated the same
as the object that a page table cap refers to.

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

This first commit only handles 4k pages.
4k pages are mapped using level 3 descriptor formats which annoyingly
have an opposite type definition (bit[1]) from all other levels. At all
other levels, a bit value of 0 is page and 1 is table. At level 3, a bit
value of 1 is page (and there is no bit value for a table).

This prevents us from using a single tagged-union type definition for
all page table descriptor definitions. For now we treat 4k pages as
special and try and push on ahead with the single type definition
anyway.

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

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

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

#1065 introduces a compilation error from refactoring.
Also apply some missed feedback from #1065 

Signed-off-by: Kent McLeod <kent-mcleod@users.noreply.github.com>

It does the same on all architectures, so the contents can be moved
into the generic code.

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

Commit f4c41f39 removed a check that dereferenced tcbSchedContext. It
should have removed this assert() also then.

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

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

Without this patch, user-level programs have the ability to
map in the core-local interrupt controller on RISC-V platforms
which contains the memory-mapped registers for the core-local
timer the kernel uses. This is a level of privilege that
user-level programs should not have. Writing to the `mtime`
register is possible which can then affect the timer interrupts
are delivered to the kernel.

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

These are only called when CONFIG_DEBUG_BUILD is on, which *usually*
means that CONIFG_PRINTING is also enabled, but, it's not necessarily
the case.

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

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

Co-authored-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Signed-off-by: Axel Heider <axelheider@gmx.de>

Removes duplication of the vmlaunch/vmresume code.

Signed-off-by: Jingyao Zhou <jingyao.zhou@unsw.edu.au>

Guard the new implementation of 64-bit x86 guests behind a config
option. This is done so that existing projects that use x86_64 hosts
with ia32-bit guests can continue to be supported until either the old
feature is preferred to be deprecated, or support can be added to
support both simmultaneously.

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

Signed-off-by: Chris Guikema <chris.guikema@dornerworks.com>

This commit combines a number of smaller commits which do the following:

    * Enter IA-32e mode when running a 64-bit host
    * Handle additional general purpose registers in 64-bit mode
    * Handle 64-bit specific MSR events
    * Properly save and restore FS, GS, and Shadow GS registers

CCDC-GVSC DISTRIBUTION A.  Approved for public release; distribution
unlimited. OPSEC#4481.

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

CCDC-GVSC DISTRIBUTION A.  Approved for public release; distribution
unlimited. OPSEC#4481.

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

The verification C parser is failing to translate this function, but it
does not actually need to since this is behind the machine interface
anyway. Mark the function as dont-translate to avoid the problem.

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

Use `ARM_HYP_verified.cmake` from branch exynos5-ver as
`ARM_HYP_exynos5_verified.cmake` on master, so both can be used by
verification CI without switching branches.

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

Use `ARM_verified.cmake` from branch imx8-fpu-ver as
`ARM_imx8mm_verified.cmake` on master, so both can be used by
verification CI without switching branches.

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

Turn FPU off by default for the verification builds we have so far.
Only the imx8mm branch currently supports FPU for AArch32.

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

Make FPU possible for "ARM" verification targets.

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>

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

There are multiple variants of the RPi4B SBC with different sizes of
RAM. There exists 1GB, 2GB, 4GB, and 8GB models. This patch adds the
`RPI4_MEMORY` CMake configuration option in order to be able to specify
the RAM size when building the kernel. Based on the RAM size provided,
an appropriate device tree overlay is selected.

The default memory size of 8GB remains the same as to not introduce
breaking changes.

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

__builtin_offsetof is not part of the verification C subset -- avoid
accidental use by not declaring a macro for it and filter out the
single use by explicitly marking it as invisible to verification.

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

Prefer compile_assert over _Static_assert. The latter is only available
in C11, and the verification demands C99.

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

Enable the timer only at initialization and since it is always
enabled. It is not needed to be re-enabled.

Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>

Generic Timer IRQs are level-sensitive, when the CNT_TVAL
is updated the trigger condition is de-asserted and the
change is propagated to the GIC in a finite time to clear
the pending state.

However, we have to make sure the timer deasserts before
EOIR/DIR, otherwise the interrupt happens again. Therefore,
we need an isb() to cause the timer to de-assert before EOIR/DIR.

There is also a chance of spurious IRQ. A spurious IRQ can be
generated, in the case we have a level-sensitive IRQ, and its
pending state is cleared at device-level but not yet propagated
to the GIC. In between the IRQ deactivation and IRQ ack of the
new interrupt if the requested change from the timer gets propagated
then it causes a spurious IRQ.

Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>

In the interest of stability and not breaking
things, the value of VMReadOnly remains the same.

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