Add a `--form_file <file>` option to the bitfield generator for
printing a `/* generated from <file> */` message in a comment.

Use this option in cmake to provide the original source .bf file before
preprocessing so it's easier to find out where the corresponding
definitions are.

Signed-off-by: Gerwin Klein <[email protected]>

Mention that it can be Ok for regions to overflow. State explicitly
that the end is exclusive.

Signed-off-by: Gerwin Klein <[email protected]>

Document in `create_untypeds_for_region` what makes region overflow for
device untypeds work.

Signed-off-by: Gerwin Klein <[email protected]>

Add compile time checks for conditions on physBase that are necessary
for verification of multikernel builds to succeed -- if these fail, the
proofs will fail.

If these succeed, and nothing else has changed compared to a verified
kernel other than physBase, then the proofs will succeed. This does not
mean that all platform requirements are validated, it just means that
all requirements for the proofs to be consistent are met.

The conditions correspond to those in

    spec/machine/*/Arch_Kernel_Config_Lemmas.thy

in the verification repository.

Signed-off-by: Gerwin Klein <[email protected]>

* boot: sanity checks for provide_untyped_cap

Check arguments for alignment, size, and kernel window (if not device
untyped). This provides sanity checks in case any of the memory region
computations are wrong.

Since this code is not performance critical and can return failure,
these are not assertions, but normal conditions with user feedback.
I.e. they are on in release and verified configurations.

Signed-off-by: Gerwin Klein <[email protected]>

GICD_IROUTERn is at the offset 0x6100 for SPI 32.
SGIs and PPIs do not have a target since they are private to CPUs.
Signed-off-by: JorgeMVP <[email protected]>

Signed-off-by: Axel Heider <[email protected]>

These are the prefixes used by the official Arm GNU Toolchain [1] It
would be convenient if seL4 would recognise it out of the box.

[1] https://developer.arm.com/downloads/-/arm-gnu-toolchain-downloads

Signed-off-by: Mathieu Mirmont <[email protected]>

- "When an address translation instruction is executed,
explicit synchronization is required to guarantee the
result is visible to subsequent direct reads of PAR_EL1."

Signed-off-by: JorgeMVP <[email protected]>

- dmb() no longer works for GICv3, and consequently
a stronger barrier like dsb() has to be used. A weaker
variant of dsb is used to ensure the observability of
complete stores in the same inner-shareable domain.

Signed-off-by: JorgeMVP <[email protected]>

Signed-off-by: Axel Heider <[email protected]>

Improve the documentation to describe about the potential pitfall in SMP
boot and the non-recommended barrier that is used.

Signed-off-by: Axel Heider <[email protected]>

The cache maintenance is needed on AARCH32, so check explicitly for
this architecture instead of doing this everywhere except AARCH64.

Signed-off-by: Axel Heider <[email protected]>

Signed-off-by: Axel Heider <[email protected]>

Include sel4/config.h instead of autoconf.h in the generated code.

Signed-off-by: Axel Heider <[email protected]>

Make sel4/config.h the only file to eventually include autoconf.h

Signed-off-by: Axel Heider <[email protected]>

Including the configuration first ensure consistent behavior.

Signed-off-by: Axel Heider <[email protected]>

Signed-off-by: Kent McLeod <[email protected]>

Add a config option, KernelAArch64UserCacheEnable, that enables user
level access to DC CVAU, DC CIVAC, DC CVAC, and IC IVAU which are cache
maintenance operations for the data caches and instruction caches
underlying Normal memory and also access to the read-only cache-type
register CTR_EL0 that provides cache type information. The ArmV8-A
architecture allows access from EL0 as fast cache maintenance operations
improves DMA performance in user-level device drivers.

These instructions are a subset of the available cache maintenance
instructions as they can only address lines by virtual address (VA).
They also require that the VA provided referrs to a valid mapping
with at least read permissions. This corresponds to lines that the
EL0 could already affect via regular operation and so it's not expected
to break any cache-partitioning scheme.

The config option allows this policy to be selected for a particular
kernel configuration, but it is default enabled as this has been the
existing behavior for current aarch64,hyp configurations and have not
been explicitly disabled in non-hyp configurations.

Signed-off-by: Kent McLeod <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Add a user manual for the bitfield generator that documents syntax,
semantics and basic concepts. Should also be able to serve as main
spec for what the tool is supposed to do.

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

- CNTFRQ is a constant value, and does not work for this case,
while CNT_CT is the one that should be used as 64-bit physical counter.

Signed-off-by: JorgeMVP <[email protected]>

The `--multifile_base` option is unused in the seL4 build and has
comments indicating that it is broken.

Signed-off-by: Gerwin Klein <[email protected]>

* Add help texts for all CLI options.

* Point to the manual in file header.

* Remove obsolete `--multifile_base` and `--c_defs` options. The former
  is unused and the logic for it was removed in the previous commit.
  The latter is not referenced in the code and has no effect. `

* Remove unused `mode` variable.

Signed-off-by: Gerwin Klein <[email protected]>

* describe CLI
* describe pruning
* mention where in seL4 generated code and source are

Signed-off-by: Gerwin Klein <[email protected]>

The verified configs have a typo in the name of the
KernelMaxNumBootinfoUntypedCaps setting, which is then ignored by the
build system and the default is used if not otherwise set.

Remove the instances that have been ignored so far and replace with
the default value if they are not otherwise set. This means there is
no actual config change.

Signed-off-by: Gerwin Klein <[email protected]>

- In non-secure world, group 1 IRQs are used instead of group 0.
Signed-off-by: JorgeMVP <[email protected]>

Avoid redundancy.

Signed-off-by: Axel Heider <[email protected]>

Signed-off-by: Ivan-Velickovic <[email protected]>

Signed-off-by: Ivan-Velickovic <[email protected]>

Signed-off-by: Ivan-Velickovic <[email protected]>

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

Signed-off-by: Ivan-Velickovic <[email protected]>

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 <[email protected]>

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

Signed-off-by: JorgeMVP <[email protected]>

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

Signed-off-by: Gerwin Klein <[email protected]>

__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 <[email protected]>

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 <[email protected]>

Signed-off-by: Ivan-Velickovic <[email protected]>

Make FPU possible for "ARM" verification targets.

Signed-off-by: Rafal Kolanski <[email protected]>

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 <[email protected]>

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 <[email protected]>

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 <[email protected]>

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 <[email protected]>

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

Signed-off-by: Gerwin Klein <[email protected]>

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 <[email protected]>

Signed-off-by: Chris Guikema <[email protected]>

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 <[email protected]>

Removes duplication of the vmlaunch/vmresume code.

Signed-off-by: Jingyao Zhou <[email protected]>

Co-authored-by: Ivan-Velickovic <[email protected]>
Signed-off-by: Axel Heider <[email protected]>

Signed-off-by: Ivan-Velickovic <[email protected]>

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 <[email protected]>

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 <[email protected]>

Signed-off-by: Axel Heider <[email protected]>

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

Signed-off-by: Axel Heider <[email protected]>

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

Signed-off-by: Axel Heider <[email protected]>

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

Signed-off-by: Kent McLeod <[email protected]>

Signed-off-by: Alwin Joshy <[email protected]>

Signed-off-by: Alwin Joshy <[email protected]>

Signed-off-by: Alwin Joshy <[email protected]>