Returns an array of interrupt affinities corresponding to an array of
interrupts for a Device.

- Use correct timer header file
- Use correct name for FVP target.

This name is case sensitive

Use the specific executable name "python2" to distinguish it from
"python" on distributions that install Python 3 as "python".

In Python 3, dict value iterators aren't deterministic between runs,
which causes nondeterministic definition output order. Some L4V proofs
are sensitive to this order.

Use sorted keys to guarantee order when iterating over values.

Update all scripts and build system to call python3, given python2's
upcoming doom. Use sys.maxsize instead of sys.maxint in one script
(maxint does not exist in python3).

Introduce a variable to hold a long expression to prevent the code
styler from line-wrapping the declare_platform() statement.  We want to
keep that on one line so the `griddle` tool (or humans) can easily
`grep` a list of supported platforms.  As of 2019-08-07, this platform
is the only one requiring this workaround.

This allows MCS and non-MCS versions of the kernel to go through the L4V
build process.

This dep is required by the elfloader for loading Arm and RISC-V
platforms.

This allows SMP support for the imx8m.

This allows SPIs to be routed to different cores.

This function enables ipis to be sent between cores.

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

This commit updates the gic_v3 driver to translate virtual irqs to
hardware irq numbers, which enables PPI support for SMP.

This commit brings the gic_v3 is_sgi and is_ppi checks in line with
gicv2 making the code more consistent.

It also removes unneccessary conditionals in the checks, as is_sgi is
always called before is_ppi so the lower bounds checks are not required.

This removes a redundant constant to use one from the gic_common header.

In order to support gic_v3 SMP, move helpers from gic_v2.h to
gic_common.h

Move common definitions from gic_v2.h and gic_v3.h into gic_common.h

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

Move definition of L1_CACHE_LINE_SIZE_BITS to cmake where it is set
according to the arm processor family.

This removes duplication in the hardware.h header files and makes adding
a new processor family require less lines changed.

This also adds a check that translating a core + irq doesn't result in
an index that is irqInvalid.

Under SMP configurations, getActiveIRQ doesn't directly return an IRQ
ID, but an encoding of the ID and core due to the existance of per core
interrupts. This fixes some remaining locations where the result is
still interpreted as an IRQ.

Setting the IRQState to IRQTimer for each per core timer prevents the
interrupts from getting masked the first time that they are received.

Need to explicitly set these to either ON or OFF rather than simply
setting them.

This is possible now that the kernel supports 40 bit PAs.

This commit adds support for using a 40-bit physical addresses in
aarch64-hyp mode.

40-bit PA support is implemented by using a 3-stage translation, with a
13 bit page upper directory as the vspace root. PageGlobalDirectories
are not used in this configuration.

To use 40-bit PAs, platforms should set KernelArmPASizeBits40 to ON.

Co-authored-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Co-authored-by: Chris Guikema <chris.guikema@dornerworks.com>

Depending on the physical address range the top level translation table
may be a page upper directory or a page global directory. Rename in
libsel4 the invocations on top level structures to be on an
seL4_ARM_VSpace rather than an seL4_ARM_PageGlobalDirectory.

On aarch64-hyp the virtual address translation structure can differ
depending on the physical address range. This commit prepares to support
more than a single physical address range by removing the assumption
that the top-level structure in a vspace is a PGD, replacing it with the
concept of a vspace_root.

Specifically:
    - add and use macros to refer to vtable bitfield generator functions
    - use the existing vspace_root_t type rather than pgde_t
    - pull performASIDPoolInvocation into header
    - add and use VSPACE_PTR rather than PGDE_PTR
    - rename decodeARMVPageGlobalDirectoryInvocation to refer to VSpace
    - update comments/error messages
    - rename variables

The physical address range supported by each aarch64 platform is defined
by which Arm CPUs it has. We therefore configure KernelArmPASizeBits*
based on which CPU is selected.

Check that the configured physical address range is supported by the
processor and that the granule size (4KiB) is supported.

Correctly defined the macros to translate between virtual and hardware
IRQs such that PPIs can be properly handled on gic_v2. It is now
possible to create a per-core handler for PPIs on platforms using this
GIC.

irq_t is now a "virtual" interrupt type that encapsulates the
information of the core in case of a private interrupt. There is a
couple of macros that need to be defined on the interrupt controller
level to translate between virtual and hardware IRQs.

Added a new IPI on ARM to unmask a remote private interrupt.

Created a new syscall, seL4_DebugSendIPI for ARM to send arbitrary SGIs
(software generated interrupts) to arbitrary cores. As SGIs are
specifically PPIs (private interrupts), this syscall effectively allows
to trigger PPIs on arbitrary cores, for debug/testing purposes.

This adds support for the 64-bit i.MX8M Mini evaluation kit.
Currently only AArch64 EL1 is supported.