The CAmkES VM wants these. These definitions are incomplete, but
are enough that the kernel will pass the appropriate memory regions
through to userspace.

Merge overlapping regions to ensure that we don't expose
the same paddr more than once.

If one region is conditional and another isn't, we shouldn't merge them.
This fixes a problem where some regions wouldn't be exposed to
userspace when they were merged with a conditional region which would
cause userspace apps to fail in unexpected ways.

Argparse supports file arguments, use this for all files.

This commit stops using FdtNodes as dict keys, as those aren't hashable
with python3. It also opens the DTB in binary mode to prevent decoding
errors under python3.

doRemoteOp1Arg data1 and cpu arguments were switched,
which triggered a conditional statement preventing
the VM from exiting and handling a bound notification.

Change-Id: I019faeaf0c7d51ef7f6b2a2ffa83bea1cf76f811

This is due to the new dependency, pyfdt

This removes the big tables of interrupt numbers from each platform.

This adds support for extracting interrupt numbers from DTS
to the hardware header file generator, so that the majority
of the per-platform interrupt listings can be removed.

This changes all ARM platforms over to using the device tree found in
the kernel to generate memory region information.

This change adds infrastructure to automatically generate the
physBase macro, the avail_p_regs array, and the dev_p_regs array
based on a device tree. Platforms can opt-in to using this
by adding DTS files to the KernelDTSList variable.

The Python script uses the hardware.yml file to determine which
devices in the device tree are of interest to the kernel and should
be hidden from userspace and instead mapped into the kernel. Note that
currently the kernel mappings are not (yet) generated, however most
of the infrastructure needed to make that happen is present.

This will be used to validate the kernel's hardware configuration file
against a schema.

Move PHYS_BASE 16MiB into RAM to match the /memreserve/ in the DTS.

Adjust PHYS_BASE to the start of RAM to match the DTS.

These contain various fixes that the Linux DTSs need
to generate usable output for seL4.

Move DTS to the kernel in preparation for using them to autogenerate
hardware headers.

This includes DTS that we didn't have previously, extracted from the
Linux kernel. Everything except TX2 comes from Linux v4.20, extracted
with the following commands:

checkout https://github.com/torvalds/linux.git v4.20
./update-dts.sh /path/to/linux/checkout

The TX2 dts is identical to the one that was found in seL4_tools.

* Use cleanByVA_PoU since we are only cleaning a single word each iteration of the loop.
* invalidateTranslationSingle takes a virtual address, not a physical address

* Also document the reason why the particular address for KS_LOG_PPTR was chosen.

This patch adds a pointer to the PD entry that sets the benchmark log frame.

vcpu_switch gets preprocessed away on non hyp configurations, but
arch/object/vcpu.h needs to be included for this.

Use correct values and document them.

Previously the kernel did not call vcpu_switch on the fastpath since the fastpath avoids
calling setVMRoot, so when sending an IPC message from a guest thread to a native thread,
if the IPC was small enough to go on the fastpath the kernel would fail to disable the
HYP traps and would treat the native thread like a guest thread.

This results in the correct defaults being defined in the cache.

Latin Modern is a vectorised version of the default Computer Modern.

When deleting `ASID`s the `HWASID` would be deleted before it was used to
invalidate the TLB entries. Rearranging the order of `invalidateTLBByASID`
and `invalidateASIDEntry` should correctly invalide the entries.

aarch64 hyp mode only has support for 8 bit hardware ASIDs. We use the
same strategy used in aarch32 for hardware asids where we maintain a
pool of hwasids that seL4 ASIDs are allocated. The allocation is stored
in the last entry of top level paging structure. This commit
encapsulates this into the bitfield specification in the same way as
aarch32.

MAX_IRQ was used on several platforms. Remote it. This is a layer of indirection which adds no value.