The kernel device IRQs and Frame mappings generated by this script will
only come from nodes specified in the seL4,kernel-devices property of
the chosen node.  Previously these devices were inferred by the script
but this led to false matching and didn't support easily overriding
which devices to match under different configurations or across
different platforms.

Explicitly specifying which devices from the device tree will be used in
the kernel makes it easier to check which devices the kernel is actually
using and makes it easier to change on a per platform or per
configuration basis.

- Device.regions() now just calculates memory regions without splitting
them into user and kernel groups.
- Config.split_regions() now calls Device.regions() and performs the
splitting if the device is a kernel device, otherwise returns the
original regions.
- Config.split_regions() is now only used in a context when dealing with
kernel devices, otherwise Device.regions() can be called to return only
informatioin extracted from the device tree.

- directly return IRQs from Device.get_interrupts(): Previously, these
IRQs were then mutated by Config.get_irqs() based on driver definitions
in hardware.yml. Inverting this order makes get_interrupts more general.
- Config.get_irqs() uses the Device it gets passed to call
get_interrupts() only when it needs to extract interrupts for a device.
- Use Config.get_irqs() for building kernel's IRQ list instead of
calling Device.get_interrupts() due to the new inversion.

Not used and it is unlikely that it will be needed in the near future.

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.