aarch32: tune vcpu struct padding for verification

Verification requires packed C structures for reasoning. The C parser
assumes uint64_t (unsigned long long) has 8-byte alignment, thus size of
struct vcpu should be a multiple of 8. As this was not the case, we add
an extra word_t (4 bytes) for padding.

This type of manual padding is naturally fragile and will break as soon
as any field of struct vcpu changes in size by < 8 bytes.

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

replacing all ifndef with pargma once

All the kernel header files now use pargma once rather than the ifndef,
as the pre-processed C files do not change while header files
are protected with pargma once. This will also solve any naming issues
caused by ifndef.

Convert license tags to SPDX identifiers

This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.

arm: remote IPI call support for VIRQS

Added support for injecting remote IPI calls towards given VCPU's
on SMP configured systems. This introudcing a new type of
IpiRemoteCall and handlers for updating the vgic state on
incoming/outgoing IPI's.

Co-authored-by: Yanyan Shen <yanyan.shen@data61.csiro.au>

arm_hyp: Save and restore vtimer state on switches

Added support for reading and writing additional virtual timer
registers for vcpu hw read and write accesses. These include the
compare value register (CNTV_CVAL) and offset register (CNTV_OFF),
each represented as two 32 bit (high and low) registers on aarch32 and
as single 64 bit registers on aarch64.

Added support for explicitly saving and restoring the virtual
timer registers when the vcpu is enabled and disabled. This
ensures when the vcpu is switched in and out, the virtual timer
registers are restored to a state that is consistent to when
it was last run.

By default the CNTVOFF register will be updated by the kernel to
accumulate the time the VCPU is not running. From the guest this will
result in the VCNT register not increasing when the VCPU is suspended.
This behavior can be turned off by disabling the
KernelArmVtimerUpdateVOffset config option.

arm: New virtual PPI event fault type

This commit introduces a new fault type, seL4_Fault_VPPIEvent.

This change means the kernel can reserve PPI interrupts and virtualise
them via delivering the irq to the active vcpu through a
specific fault. This enables multiplexing PPI IRQs across multiple VCPUS
which requires correctly masking and unmasking the IRQ depending on
which VCPU is running.

A new VCPU invocation, seL4_ARM_VCPU_AckVPPI is also added for
acknowledging the handling of the IRQ. This takes an IRQ as a parameter
but will only accept IRQ numbers that are sent as VPPIEvent faults.

Co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Co-authored-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>

arm_hyp: Refactor code into arch headers

Move vcpu functions that are specific to a particular Arm architecture
version into the relevant header files. Also move some generic functions
into the generic vcpu header file for use by arch specific headers.

style: consistently align pointer with name

Run astyle with align-pointer=name

arm/hyp: refactor VCPU states

Use an array and constants to replace register names in the VCPU.

arm/hyp: add support for running multiple ARM VMs

This commit saves/restores various control registers that can be
modified by guest VM kernels, so seL4 can execute multiple ARM
32-bit VMs multiplexing a single physical core.

When the CONFIG_HAVE_FPU option is selected, the commit allows
the VMs to use FPU registers and enables lazily saving/restoring
FPU registers for the VMs.

armv8/hyp: Add aarch64 HCR fields

arm/hyp: uint32_t -> word_t

arm/hyp: Move common HCR macros to vcpu.h

armv8: Use array regs in vcpu for aarch64

Share linker.h between architectures

arm: Pass 'call' down to invokeVCPUReadReg

invokeVCPUReadReg should not be setting message registers for the return message unless
the user performed a call. In doing so we must refactor the call to readVCPUReg to
outside the introduced `if` condition since, as it performs machine operations, it
should always happen

arm hyp: make invokeVCPUInjectIRQ index arg unsigned long

Argument passed to it comes directly from a word_t so it shouldn't be
signed. Also, verification.

rename arch_tcb.vcpu -> arch_tcb.tcbVCPU, vcpu.tcb -> vcpu.vcpuTCB

struct vcpu { struct tcb* tcb; ...
struct arch_tcb { struct vcpu* vcpu; ...
and
struct tcb { struct arch_tcb tcbArch; ...

These conspire to generate a type error on verification side due to
assumptions about non-colliding names.

arm: save/restore banked registers in VCPUs

Adds space in the vcpu_t struct for the registers from the different operating modes
and saves/restores these registers as part of saving and restoring the VCPU

Remove unneeded usages of `VISIBLE`

Using `VISIBLE` where it is not needed limits the ability for the
compiler to optimize, especially when using whole program optimizations

SELFOUR-609: Introduce virq type in bitfield

Introduces a bitfield defined virq type that is then used to replace
manual bit packing of virtual irqs in the vcpu/vgic LR registers

SELFOUR-551: Prevent vcpu_boot_init appearing to verification

When hypervisor extensions are not enabled the boot code cannot
actually call vcpu_boot_init as the symbol names do not even
exist. This is fixed be defining macros that expand to nothing

SELFOUR-551: Remove direct accesses to machine data structures

This commit wraps accesses to the vgic in functions that are marked as
DONT_TRANSLATE and uses a global constant (that is determined at boot time)
for the number of LR registers to prevent loops that have undefined bounds

SELFOUR-551: Standardize VCPU capitalization

For acronyms seL4 other does CAPS or caps, this changes some functions
that were doing Caps

SELFOUR-551: Remove unused arguments from decodeVCPUSetTCB

SELFOUR-551: Swap argument order of [di|a]ssociateVcpuTcb

Attempts to create some consistently across other functions that have
VCPU first in the name and also VCPU first in the argument list

Minor fixes for other ARM platforms

arm-hyp: Minor cleanups

Cleanup some small licensing, whitespace and configuration details

arm-hyp/tk1: make style

arm_hyp: rm ARM_HYP ifdefs; func inline assembly

vcpu.c:
encapsulate inline assembly into inline functions that added to
device_pl2.h file.

other files:
replace #ifdef ARM_HYP with config_set(ARM_HYP)

arm_hyp: add file to contain hyp mode inline funcs

machine_pl2.h:
new place for hyp mode inline functions.

boot.c:
replace #ifdef ARM_HYP with config_set(ARM_HYP).

vcpu.h, machine_pl2.h:
add empty functions when ARM_HYP is not defined to
pass compilation.

arm_hyp: rm ARM_HYP ifdefs; func inline assembly

vcpu.c:
encapsulate inline assembly into inline functions that added to
device_pl2.h file.

other files:
replace #ifdef ARM_HYP with config_set(ARM_HYP)

arm_hyp: add file to contain hyp mode inline funcs

machine_pl2.h:
new place for hyp mode inline functions.

boot.c:
replace #ifdef ARM_HYP with config_set(ARM_HYP).

vcpu.h, machine_pl2.h:
add empty functions when ARM_HYP is not defined to
pass compilation.

ARM HYP: Trap SMC

Recommit of arm_hyp branch on release snapshot