Consolidate kernel virtual memory regions

Each architecture now only needs to describe the bounds of the three
memory regions: the 1:1 mapped physical memory region, the kernel ELF
region (which may or may not overlap the physical memory region) and the
device / kernel page table region.

The physical base address of the 1:1 mapped physcial memory region and
the kernel ELF region must also be specified.

The top of user addressable memory (where in the same virtual address
space as the kernel) is defined by USER_TOP.

The physic memory virtual mapping is described by PPTR_BASE and
PPTR_TOP. The base physical memory address is PADDR_BASE and is the
physical address used to map PPTR_BASE.

Don't use kernelBase when referring to the base of the 1:1 mapped
physical memory window.

The kernel ELF virtual address region is described by KERNEL_ELF_BASE
and extends until the virtual address of the symbol `ki_end` which is
created by the linker. KERNEL_ELF_PADDR_BASE is the base address of
the physical memory region used to map the kernel and is the address to
which KERNEL_ELF_BASE maps.

KERNEL_ELF_BASE and KERNEL_ELF_PADDR_BASE do not need to be aligned to a
page size boundary as they are approriately truncated during boot by the
`map_kernel_window` function.

KDEV_BASE describes the base virtual address of the kernel device region
and the region is assumed to extend to the end of virtual memory.

Note: The offset between PPTR_BASE and PADDR_BASE is used to translate
the virtual address of all untyped objects to physical addresses. This
includes device untyped objects or frame objects where the virtual
address does not fall within the 1:1 mapped physical memory region.

Signed-off-by: Curtis Millar <curtis.millar@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.

rename KDEV_PPTR/PPTR_KDEV to KDEV_BASE

This is the virtual address for the start of the kernel device mapping
region.

x86: always invalidate TLB during unmapPage

On SMP configurations, the VSpace may be in use on other cores and so a
TLB shoot down has to be performed unconditionally.

Create device untypeds at boot for all arches

Currently on x86 device untypeds are generated by passing the entire
address space minus any parts that are reserved by the kernel or that
are "real" memory (e.g. kernel image, physical RAM).

On ARM and RISC-V, device untypeds were generated at compile-time from
a device tree. This patch moves ARM and RISC-V to use the same approach
as x86, and moves the code from x86 into a common location that's
shared between the three architectures.

Co-Authored-By: Anna Lyons <anna@gh.st>

SELFOUR-161: Merge Page_Remap with Page_Map

- Remove Remap function from seL4 API for arm, x86, riscv and the
respective invocation implementation.
- Update Map as replacement for Remap
- Update manual

This allows a change of rights if the frame being mapped is already
mapped in at the given vaddr. To map a page to a different address,
unmap it first.

Co-authored-by: Hesham Almatary <hesham.almatary@data61.csiro.au>
Co-authored-by: Anna Lyons <Anna.Lyons@data61.csiro.au>
Co-authored-by: Victor Phan <Victor.Phan@data61.csiro.au>
Co-authored-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>

x86: avoid -Waddress-of-packed-member

It's safe to take the address of this member, since it's the
first thing in a cacheline-aligned struct.

style: set code width to 120

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: consistently align pointer with name

Run astyle with align-pointer=name

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.

x86: Explicit check against PPTR_USER_TOP instead of mask

The previous mask approach relied on the user region being a power of 2 size, which is not
true on ia32. This change supports arbitrary PPTR_USER_TOP.

x86: extract createSafeMappingEntries_* into separate functions for ease of verification

x86: Unify page map/remap logic with existing verified ARM behaviour

x86: All page unmap paths perform an invocation

This takes the current logic in the decode function for unmap that decides which perform
function to call and considers that logic to be part of the perform step, and places it
in a wrapping perform function. As a result the case where we do not call any detailed
perform function will still result in calling a perform step from decode, instead of doing
nothing.

x86: Consistently order remap invocation errors

This reordering brings this invocation inline with other invocations where we first check
the message length, and then the capability.

x86: Consistently compare against PPTR_USER_TOP

PPTR_USER_TOP is the last valid user address and so any address greater than it
should not be used. Due to pages being at least 4K aligned it is also correct
to do a >= comparison, but it is clearer and more consistent with verification
to perform just >.

x86: Move hwASIDInvalidate inside condition in deleteASID

We shouldn't be invalidating the ASID unless we know that the ASID is
actually mapped to a corresponding VSpace.

x86: Check ASID instead of mapping type

This is a simpler check for verification

x86: Guard call to unmapPage

This `if` is not strictly necessary as unmapPage will immediately return after failing to
look up the asid but this makes verification easier.

x86: modeUnmapPage returns whether or not tlb needs invalidation

Whilst it is always correct to invalidate the TLB even if no page was unampped this
provides a small optimization and makes the modeUnmapPage behaviour mirror the general
arch behaviour

x86: Define per node arch global state

Global state in this context is state/datastructures that need to be available at all times,
both in user and kernel mode, by the hardware for correct operation. The purpose of creating
a separate per-node structure for it is so that there is the option of treating it specially
in the future from other per node state

x86: declare pageBits to be word_t in lookupIPCBuffer

This avoids an implicit cast from word_t (the return value of
pageBitsForSize) to the original unsigned int, for ease of
verification.

x86: Re-validate ipc buffer is not device frame

This should be redundant, but is required for verification to go through

Declare and check IPC buffer size

Adds a named constant of the IPC buffer size bits that can be used when checking the
size/alignment of an IPC buffer. This constant has a compile time assertion to ensure
it corresponds to the actual IPC buffer

x86: Have single makeUserPDEInvalid function

makeUserPDEPageTableInvalid and makeUserPDELargePageInvalid were both just creating the same
kind of thing, an invalid mapping, which really should be thought of as the third type of
PDE entry type.

x86: Use full word_t for fault addresses

Addresses are not always a uint32_t, and this was resulting in fault addresses being
truncated on x86_64.

x86: Explict enum for fault types

This creates a similar structure as ARM, where an `enum` is created with the `#define` values
from libsel4. Having these values as enum types provides a 'real' C symbol for verification.

x86: Rationalize names of paging structures

Changes the name of paging structure entries to more clearly indicate the kind of object
they map to. Generally this is changing a `pde_small` to `pde_pt` to indicate that this
mapping refers to a page table, removing an inconsistency where `pde_large` indicated that
the mapping was for a large page. For the same reason the `ept_pde_4k` type is changed to
`ept_pde_pt` type to reflect what is present in the actual entry.

`pde_large` is left as 'large' and not explicitly given a size as code common between
ia32 and x86-64 manipulates these entities and 'large' is already a used abstraction
over the two potential page sizes so there is need to introduce a formal abstraction layer
and make the names in the structures more specific.

SELFOUR-1062: Hide all IOMMU related code behind #ifdef guards

The IOMMU implementation is not going to be verified at the moment, and so the code for
it needs to be hidden from verification, which we do by #ifdef'ing it out if the IOMMU
is not enabled. As a result the IOMMU configuration depends on a non verification target

SELFOUR-881: add ghost state updates for x86-64

x86: Avoid taking reference to local variable in init_pat_msr

x86: define L1_CACHE_LINE_SIZE_BITS as with ARM

x86: Invalidating HW ASIDs when deleting ASID pool

x86: Remap frames from correct vspace

Changes the check on a frames ASID to ensure that it is from the virtual
address space that is going to be modified. Without this the frame could
stay mapped into a different vspace, yet have the kernel book keeping
only think it is now mapped into the new one.

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.

SELFOUR-413: refactor libsel4 fault API

This is a *breaking API change*

This commit:

* makes seL4_Fault_tag_t common between the kernel and libsel4
* deprecates the existing functions from sel4/messages.h includes
* introduces a new fault API in sel4/faults.h and
* sel4/sel4_arch/faults.h
* deprecates seL4_GetTag(), as the function did not work without
the user calling seL4_SetTag() first (seL4_MessageInfo is passed
in registers and not set in the IPC buffer)
* removes previously deprecated functions (deprecated prior to 3.0.0)
* updates the seL4 manual to reflect the changes

x86: Pass address space when invalidating ASID

For efficient TLB coherency on x86-64 it will be useful to know
the address space that the ASID being invalidated was last assigned to

x86: Refactor tlb_bitmap to be mode generic

Refactors the TLB bitmap code to be generic across ia32 and x86-64.

x86: Refactor generic x86 pte/pde manipulation

Previously generic functions for manipulating page table and page
directory entries were placed in mode/structures.h. These are moved
to a mode/vspace.h instead so that they can use existing functions
defined in arch/vspace.h.

The x86_make_pde_mapping function is dropped in this move as it is
not used. Instead it is replaced with a function for creating an
empty mapping for whatever is the vspace root.

SELFOUR-634: support for TLB and cache management

SELFOUR-287: 32-bit vt-x implementation

This is an implementation of vt-x for x86 kernels running in
ia32 mode.

x64: Add x86_64 support

SELFOUR-632: implement cores non-architecture dependent structres

x86: Fixup IOMMU implementation

Adds a mapping type to frame caps that tracks
what kind of hierarchy the cap is mapped into;
an MMU, IOMMU and in the future an EPT structure.

Additionally the IOMMU code is updated to
have correct functionality and be verification
friendly.

SELFOUR-630:preliminary booting application processors
- update core detection code and Kconfig file
- update kernel stack managment so that BSP does not use boot stack before IPI APs
- move arch dependant data to a single structure
- add cache line size to Kconfig
- add cpu indexing and apic id mapping
- boot APs to halting state
- add guard for kernel stack if there is only one core

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

Revert "Merge pull request #358 in SEL4/sel4 from ~AZARRABI/sel4:multicore to master"

This reverts commit ce2f666bb811c5e4c779829fcb09d5a189ebcdbb, reversing
changes made to dc183f96b81f2344d7d0d910fc430f924eaae940.

Revert "[STYLE_FIX]"

This reverts commit d29f743bbcc3acff2f61b40dedb4fe0839db38b8.

[STYLE_FIX]

SELFOUR-630:preliminary booting application processors
- update core detection code and Kconfig file
- update kernel stack managment so that BSP does not use boot stack before IPI APs
- move arch dependant data to a single structure
- add cache line size to Kconfig
- add cpu indexing and apic id mapping
- boot APs to halting state
- add guard for kernel stack if there is only one core

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-617: one source of memory object sizes

Adds the following constants to libsel4
and uses them in the kernel.

seL4_SectionSize (arm)
seL4_SuperSectionSize (arm)
seL4_HugePageSize (x86 - pae)
seL4_LargePageSize (arm)
seL4_DataFault
seL4_InstructionFault

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

SELFOUR-558: Consistently name Unmap instead of UnMap

SELFOUR-557: s/isIOSpaceFrame/isIOSpaceFrameCap/

x86: Improve translation invalidation

x86_64 (with PCIDs enabled) supports a more fine grained invalidation
approach for the TLB and Page Structure Cache. This change expands
the number and kinds of information passed for certain invalidations,
and provides an implementation of this for ia32.

trivial: make style with astyle 2.03

trivial: make style commit

x86: Refactor vspace code to have verification friendly invocations

x86: More portable user mode IO port restriction

For x86-64, to disable IO instructions in user mode requires a
IO permission map being set up properly in TSS. Setting the
IO map base field of TSS larger than the TSS works for 32-bit, but
not 64-bit. This commit sets up a IO permission map usable for both
32-bit and 64-bit kernel and changes the TSS to use the mapping.
The IO permission bitmap is appened to the bitfield generated tss_t,
resulting the tss_io_t structure.

x86: Rename ia32->x86

This is a stylistic commit to make names of variables/constants and
functions in the kernel more consistent. That is, things that are
not IA32 specific, but are generic x86, get renamed to having an
x86 name

x86/libsel4: Rename ia32->x86

Rename all functions, constants and types in libsel4 that are in the
general x86 architecture to have an X86 name instead of an IA32 name.
As libsel4 and the kernel share names this requires changing those
in the kernel as well.

All the original IA32 names can still be used for the moment, but are
marked as deprecated.

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

trivial: style

x86: Add missing checks when mapping and unmapping paging objects

x86: When creating an ASID pool mark the untyped object as used

x86: Introduce mode specific unmap and remap operations

x86: Use typedef for vspace roots instead of void*

x86: Move invalidateTLBEntry in unmapPage

invalidateTLBEntry is currently called twice in unmapPage
Once behind a guard that only performs the invalidate if
the active vspace is the same as the one that contains the
mapping, and then a second time at the end of unmapPage
without any guard at all.

This commit removes the unguarded version and replaces it
with the guarded one from earlier in the function.

x86: Mark map_kernel_window as boot_code

x86: Do not implicitly mask virtual address when mapping frames

This mask made the checkVPAlignment call completely redundant. By
removing this mask and relying on the check we bring the x86 in line
with the ARM behaviour

SELFOUR-114: remove duplication of seL4_MessageInfo_t, adjust naming to avoid cparser mangling

x86: Extract 32-bit specific vspace functions in mode/vspace.c

x86: With multi-kernel support removed make the kernel PDs etc global instead of passing them around

x86: Do not conditionally compile IOMMU code, use build/run time checks

Guarding code with #ifdef's makes even cursor testing of 'does this code compile'
difficult due to code being hidden by the pre-processor. Using config_set in
regular C if statements is performant as the compiler can trivially detect
dead code at compile time, and at -O1 and above will not even link in symbols
referenced by dead code in these blocks, so this will not bloat image size

x86: Do not conditionally compile IRQ controller code, use build/run time checks

Guarding code with #ifdef's makes even cursor testing of 'does this code compile'
difficult due to code being hidden by the pre-processor. Using config_set in
regular C if statements is performant as the compiler can trivially detect
dead code at compile time, and at -O1 and above will not even link in symbols
referenced by dead code in these blocks, so this will not bloat image size

x86: Make some vspace code and definitions non-static that get used by the PAE vspace code

x86: Strip multi kernel support from the x86 kernel. This is not used and is conflicting with planned future features

x86: Rename constants and functions to have X86 prefix instead of IA32 prefix

x86: Make parts of what have become 32-bit specific headers common

The reason these were not made common to begin with is so that there
was a commit that was just a rename of these files to make any merges
with other branches that might exist easier

Change additional int->word_t due to interraction with the C parser to ease verification

unsigned int -> word_t

Trivial: style (again)

Trivial: style

Removed CONFIG_BENCHMARK config option. All checks for '#ifdef CONFIG_BENCHMARK' replaced with '#if CONFIG_MAX_NUM_TRACE_POINTS > 0'.

Added support for using multiple tracepoints at the same time.

ia32: Disable the I/O permission map in the TSS

The I/O bitmap base address needs to be set higher than the
TSS segment limit in order to disable the bitmap completely.
We want the bitmap disabled as this prevents any user I/O
port access. Currently the few ports from 0 to sizeof(tss_t)
are usable.

trivial: fix style

Fix style and unused variable warnings.

x86: Make x86 the name of the architecture instead of IA32

IA32 is 32bit version of the x86 architecture. Whilst only IA32
is supported, much of the code is generic x86. Using a generic
x86 architecture will aid in future 64bit support