arm: give away FPU on thread delete

The ownership of FPU would only be updated when a thread causes FPU
exception. If the thread being deleted owns the FPU, the ownership needs
to be given away proactively to avoid memory corruption.

Reported-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Signed-off-by: Siwei Zhuang <siwei.zhuang@data61.csiro.au>

Make kernel log buffer derived from cmake config

This removes the explicit CMake configuration for the kernel log buffer
and replaces it with a #define that is enabled for the required
configurations.

Signed-off-by: Curtis Millar <curtis@curtism.me>

SMMU: basic driver for init and probing

Introducing the driver in kernel for detecting SMMU features
and initialise the hardware.

Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

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.

style: set min-conditional-indent to 0

Given we use braces all the time conditional indents do not make code
cleaner.

style: consistently attach return type

Add attach-return-type to astyle

style: correct parenthesis padding

Use astyle's unpad-paren to unpad all parentheses that are not included
by pad-header, pad-oper, and pad-comma.

Allow Arch_finaliseCap to return cleanup information

Changes Arch_finaliseCap and Mode_finaliseCap to return the same finaliseCap_ret_t type
as finaliseCap. This allows the Arch and Mode specific functions to define cleanup
information of its capabilities if necessary, just like the generic capabilities can
in finaliseCap.

SELFOUR-748: ARM - Support local/remote TLB invalidation operations

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: update AUXUPD for ARM_HYPERVISOR_SUPPORT

arm: Remove redundant memzero

Zeroing of memory was previously removed from being done on creation of each
object, to doing initial zeroing of whole untyped. The VCPU and IOPageTable
objects were evidently missed in the original change.

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.

SELFOUR-567: use seL4_CapRights_t from libsel4

This change

* changes seL4_CapRights from the kernel to be seL4_CapRights_t in
libsel4
* deprecates the duplicated seL4_CapRights in libsel4, which is
now the bitfield generated type seL4_CapRights_t.
* fixes all usages in kernel and libsel4

Impact: for verification, this will require the type to change name
from cap_rights to seL4_CapRights_t.
This is a breaking libsel4 API change, although most code uses
seL4_AllRights or similar constants, which will not break
at a source level as these constants have been updated.

Remove recycle

Removes the recycle operation and adds an operation
to cancel any badged sends on and endpoint. Calling
Revoke + CancelBadgedSend is equivalent to Recycle
on a badged endpoint

SELFOUR-444: Preemptible zeroing for retype.

Change to the order of operations and timing behaviour of
invokeUntyped_Retype. The Retype operation now zeroes the
entire range of the Untyped cap (if it is being used for
the first time) before installing any objects. This avoids
the need for long-running initialisation of large objects,
whose initial contents are always zero. The initial zeroing
phase is preemptible, and may take multiple timeslices to
complete.

[STYLE_FIX]

SELFOUR-421: minor changes for c-refine

SELFOUR-421: fix up boolean equality in Arch_sameObjectAs

SELFOUR-421: added device check to sameObjectAs

SELFOUR-421: Arch_createObject changed to use new user_data_device in ghostupdates for device pages

SELFOUR-421 Introduce explicit device frames and untypeds

Kernel objects cannot be created from device untypeds, with the
exception of frames, which do not get zeroed and cannot be used
as an IPC buffer. Device untypeds additionally cannot be used
in the construction of ASID pools.

This then changes the API to the rootserver (i.e. bootinfo) to
send device untypeds instead of device frames. On ARM these
device untypeds are the same as the previously exported device
frame regions. On x86 PCI scanning is removed and all physical
memory addresses (that are not important for kernel integrity)
are released to the user.

In order to have bits in the frame and untyped caps on ARM the
number of software ASIDs had to be reduced from 2^18 to 2^17,
and the maximum untyped size reduced from 2^31 to 2^30

SELFOUR-556: Rationalize BITS vs INDEX_BITS

s/PD_BITS/PD_INDEX_BITS
Current convention is to say that X_BITS is the log base 2
size of an object, not the log base 2 number of indices

SELFOUR-556: Rationalize BITS vs INDEX_BITS

s/PT_BITS/PT_INDEX_BITS
Current convention is to say that X_BITS is the log base 2
size of an object, not the log base 2 number of indices

SELFOUR-518: User-level log buffer

Remove global ksLog and use KS_LOG_PPTR instead

Benchmark - Log buffer: use global page table

SELFOUR-551: Standardize VCPU capitalization

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

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

astyle: Make comments compatible with both 2.03 and 2.04 astyle versions

SELFOUR-557: s/isIOSpaceFrame/isIOSpaceFrameCap/

trivial: style

arm-hyp: Hide more definitions

arm-hyp: Hide calls to isIOSpaceFrame

arm-hyp: Pander to the C parser

The C parser will not accept a switch statement that just has a
default case. This change adds some more pre-processor gymnastics
to hide the 'switch' if it would result in this case.

arm-hyp: Hide iospace caps being #ifdef

These cap type existing, even if unused, break the original verification

arm-hyp: Minor cleanups

Cleanup some small licensing, whitespace and configuration details

arm-hyp/tk1: address review comments.

arm-hyp/tk1: address review comments.

arm-hyp/tk1: make style

arm-hyp/tk1: fix bugs found during testing

arm-hyp/tk1: add the missing return

arm/tk1: connect objects with SMMU invocations

arm/tk1: a checkpoint for SMMU implementation

trivial: make style with astyle 2.03

trivial: make style commit

SELFOUR-399: object sizes and globals frame addr should come from the same source

Rearranging sources for aarch32 to 32/*