vtd: Add seL4_PageBits when testing address bits

The total bits should include the page bit and index bits.

The commit is based on PR #185 by laokz.

Co-authored-by: laokz <laokz@foxmail.com>

Signed-off-by: Yanyan Shen <yshen@cog.systems>

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.

boot: refactor allocation of rootserver objects

Prior to this change, the boot process would dynamically allocate
memory for root server objects based on the order of initialisation.
Allocation was a best-fit algorithm.

This change preallocates all memory for root server objects to an
aligned untyped just after the user image. By allocating the objects in
order of size, allocation is greatly simplified and the ability to
reproduce the allocation offline based on the kernel and user image
sizes is increased.

trivial: remove unneccessary void cast

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.

intel-vtd: Improve DMA fault error helpfulness

The error will now split the source up into bus,dev,func components.

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

Share linker.h between architectures

Removed unused static function supports_passthrough

The last call to supports_passthrough was removed in commit
8e15c42921e42be2b80b2645f750fce7238fe231

[STYLE_FIX]

Avoid using bitfield generated *_ptr_new functions

These functions can cause slow down during verification C parsing and do not currently
have any proofs about them. More importantly there is no performance impact from just
calling the regular *_new functions instead

[STYLE_FIX]

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-556: Rationalize BITS vs INDEX_BITS

s/VTD_PT_BITS/VTD_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

x86: Use IO page table size defined in libsel4

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: Port some of the IOMMU changes on the experimental branch

This changes the IOMMU from using passthrough devices and instead
directly mapping in the reserved regions that are needed for each
device.

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

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

Rationalize standard types

This commit aims to rationalize how we represent different types
for compatiblity between ARM and x86, as well as between 32 and
64 bit code. The choices being made here is to declare that a
uint32_t has a type of 'int', this allows uint32_t to be declared
consistently across 32 and 64 bit (at least in GCC).
The word_t type is declared using a 'long' (not a uint32_t or uint64_t) to
allow for a word_t to be backed by the same type on both 32 and 64 bit
All other types that want to be declared as the size of a native word
get declared in terms of a word_t

and one last format string

Fix IOMMU part of x86 build

Release snapshot