The default value is zero anyway.

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

This insertion is not required, as the slot has just been cleared by
cteDelete. Avoiding the insertion simplifies verification.

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

This changes it to be a pure function, which eases verification

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

The assert() condition is checked two lines above

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

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

Move the ksCurTime assertions out of setDeadline, because they are not
necessarily true there. Assert ksCurTime in setNextInterrupt instead.

We only know that the deadline being set is at least ksCurTime -
getTimerPrecision(), which can be slightly in the past (ksCurTime is
already slightly in the past, at kernel entry).

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

Make sure the invariant "sc_sporadic implies sc_active" is preserved by
invalid SchedContexts as well.

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

Change the statement ordering such that the "sc_sporadic implies
sc_active" invariant is not violated. In the previous code order, the
scSporadic flag is set while the scheduling context is still
potentially inactive. Setting the flag later avoids temporarily
breaking the invariant.

Move the badge setting together with the flag to keep these heap
updates together.

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

Follow Arm's code where it tries to place traps and vector
code adjacently in a 4KiB page to optimise performance
(through spatial cache locality).

Closes #1091

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

This commit fixes a linking error when using LLVM's lld.

llvm-as doesn't assume or assign section flags for input section if
not specified. This will make the section non-allocatable and put
into a none segment and trigger relocation linking errors against
symbols in non-allocatble sections.

For example, when building with LLVM/lld for AArch64, the following
error occurs:
(traps.S.obj:(function arm_vector_table: .vectors+0x0): has non-ABS
relocation R_AARCH64_JUMP26 against symbol 'invalid_vector_entry')
This does not happen with ld.bfd (GNU's linker) as it seems to allow
relocations against symbols in non-allocatable sections.

The GNU's assembler documentation states that:
"If no flags are specified, the default flags depend upon the
section name. If the section name is not recognized, the default
will be for the section to have none of the above flags: it will
not be allocated in memory, nor writable, nor executable.
The section will contain data. [1]"

This commit explicitly sets .section flags in assembly to avoid
this error and for better intentionality (and good practice)
without relying on toolchains handling flags and linkage differently.

[1] https://sourceware.org/binutils/docs/as/Section.html



Sponsored by: DARPA.

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

The vspace (top level PT) cap had non-standard names which were a bit
confusing to reason about. The name conflict with capPTBasePtr also
spits out fully-qualified names in verification.
This commit updates all the field names of vspace_cap to start with
"capVS" and updates all the call sites.

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

Verification sees macros as the preprocessed C code. On other arches, we
have checkVPAlignment, but on AArch64 we had IS_PAGE_ALIGNED only. Since
this was the only use, this commit also removes IS_PAGE_ALIGNED in
favour of checkVPAlignment.

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

For verification purposes, don't go through `_ptr_set_` from the
bitfield generator (same as RISC-V).

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

Report the vspace cap (1) as invalid, instead of the frame cap (0) in
decodeARMFrameInvocation to stay consistent with the other
architectures.

See also #1075

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

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

(it makes PTEs, not pages)

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

`makeUserPage` was a bit confusing to understand, and went around the
bitfield-generator's back by modifying the tag bits. As a result, it did
not set bit 58 for 4k pages, meaning a 4k page could not be identified
from an encoded PTE. This version addresses that, and hopefully improves
the repetition.

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

This change was missing from the rename of the pgd cap
to vspace cap on aarch64. Allows vm fault fastpath enabled
configs to build.

Signed-off-by: Dan Shea <danshea00@gmail.com>

- Describe the SMP lock variable mechanism detail.
- Add checks that the lock state is valid, this will catch potential
  kernel loader problems.

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

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

Enable badged SMC capabilities to be revokable so that dynamic systems
can revoke badged capabilities that are handed out.

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

Make a few changes to follow the syscall message passing convention:
- Confirm with a static assert that NUM_SMC_REGS >= n_msgRegisters.
- Require the input length to be >= NUM_SMC_REGS. This ensures that any
  accesses to the IPC buffer memory is safe (if the IPC buffer isn't
  present then the message length will be truncated to n_msgRegisters).
- If the call parameter isn't set then the kernel isn't supposed to
  reply to the invoking thread. This means no updates to it's registers.
- Set the ThreadState to ThreadState_Running so that the default empty
  success message isn't applied at kernel exit (which overwrites
  msgInfoRegister)

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

The exec spec typically requires that invocations have a decode phase
that can fail followed by an invoke phase that can not fail.
A switch block is not required when there is only a single valid
invocation label.

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

Drivers may need to use SMC calls to configure hardware resources

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

Signed-off-by: Alex Pavey <Alex.Pavey@dornerworks.com>

See PR at https://github.com/seL4/seL4/pull/701



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

Use seL4_BootInfoFrameSizeBits directly.

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

Provide seL4_BootInfoFrameSize (and seL4_BootInfoFrameBits) for
userland, to there is no longer a need to hard-code the 4 KiByte
assumption.

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

C parser and verification don't handle taking addresses of local
variables. Use direct `_cap_set_*` and pass by value instead of
pointer-based `_cap_ptr_set_*`.

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

Latest AArch64 only uses pte_C which is already declared in common
setup, so pde_C only needs to be declared on AArch32.
Affects bitfield generator and verification.

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

- print period and budget with units
- print tick value also
- use proper format specifiers and avoid casting

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

These operations should be possible on seL4 with and without hypervisor
mode.

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

Add helper functions to get kernel image location. This removes any
dependencies from the rest of the code on symbols and defines. It
also avoid passing a parameter though various functions.

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

Currently getting the timestamp for RISC-V platforms uses the
`rdtime` pseudo-instruction which ends up invoking OpenSBI
and then accessing the CLINT memory-mapped `mtime` register.
This patch eliminates the use of `rdtime` in favour of
directly getting the timestamp for performance.

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

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>

vaddr argument is 0th argument, not 2nd.

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>