We currently only support Sv39 on RV64. Sv39 has a cannonical address
range of -2^38 and 2^38-1. This means that bits 63-39 must be equal to
bit 38, or that we sign extend from bit 39 to 63 based on the value of
bit 38. It also means that we only have 39 bits of addressable space,
which limits our max untype size.

These shared objects have different definitions based on the cannonical
address of the virtual memory system.

base 32 implies base of 32 and mask of 32 with no sign extension which
is required for Sv32

Conventionally a newline is used to signify a system word boundary. This
is supposed to improve readability

The assert has an assumption that regions are also ordered in ascending
order.

This change fixes support for instances where we have
multiple kernel devices in the same page, or kernel devices
which aren't at page-aligned addresses.

Also use seL4_UserTop to pick the right address to start
putting the kernel device pages.

Note that the auto-generated kernel_devices will differ slightly from
the ones present in the kernel until now. When devices have
registers that aren't page-aligned we now always set the appropriate
PPTR to be the start address of the device, while previously the PPTR
was sometimes page-aligned.

Specifically, this change to PPTRs affects:
- bcm2837 intc
- bcm2837 uart
- allwinnerA20 timer

KDEV_BASE is the first address that can be used for mapping devices.
This will be used by hardware_gen to auto-generate the kernel_devices
table.

This header is going away and contains nothing of substance. Remove it.

This removes the need for the buses array in the hardware YAML

This moves the kernel back up to 0x60000000 as it was before
the HW headers were autogenerated, as this behaviour is depended on by
some user-level projects.

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.