Make kernel log buffer derived from cmake config

This removes the explicit CMake configuration for the kernel log buffer
and replaces it with a #define that is enabled for the required
configurations.

Signed-off-by: Curtis Millar <curtis@curtism.me>

mcs: add MAX_BUDGET_US

We need to bound the time the user provides to configure scheduling
contexts to avoid malicious or erraneous overflows of the scheduling
math. Make the max period/budget 1 hour.

1 hour is sufficiently small that it will fit in a 32-bit error message.

1 week is sufficiently small for 64-bit platforms.

Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>

Enabled IPC debug features under new config

Introduced a new config flag to enable
userError format strings to be written to the IPC buffer.
Another config bool has been introduced to toggle
printing the error out and this can also be set at runtime.

Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>

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.

Create device untypeds at boot for all arches

Currently on x86 device untypeds are generated by passing the entire
address space minus any parts that are reserved by the kernel or that
are "real" memory (e.g. kernel image, physical RAM).

On ARM and RISC-V, device untypeds were generated at compile-time from
a device tree. This patch moves ARM and RISC-V to use the same approach
as x86, and moves the code from x86 into a common location that's
shared between the three architectures.

Co-Authored-By: Anna Lyons <anna@gh.st>

kernel: set maximum user paddr in build system

expose the maximum physical address that can be given to userspace
for use in hardware_gen.py

tools: rewrite hardware_gen.py

This is almost a complete rewrite from the old hardware_gen.py.

It separates the 'parse DT' stage from the 'generate output'
devices more strictly, and is hopefully easier to understand and
easier to extend.

We also no longer generate the 'devices' list (in YAML)
or the dev_p_regs array (in C), as the kernel will implicitly
expose all non-RAM untypeds as devices.

config.cmake: fix typo

Discovered at IEEE SecDev 2019 when someone asked about binary
verification and optimisation levels.

riscv: SMP option

Allow to enable the SMP option for RISCV.

CMake: Mark config options as advanced

This removes them from appearing in the CMake configuration cache and
being confusing.

CMake: Add KernelHardwareDebugAPIUnsupported

There are platforms/archs that don't support the Kernel Hardware Debug
API and they can now advertise that by setting
KernelHardwareDebugAPIUnsupported.

cmake: Only include cmake files for selected arch

This prevents accidental declaration of properties or configurations
that are for the incorrect architecture selected. This was previously
required as the variables KernelWordSize and KernelArch were defined in
each arch specific cmake.config file. Now that they are defined in
advance it is possible to exclude the other imports.

mcs: allow kernel WCET estimate to be scaled

This configuration option allows for building images destined for
simulators, which may not simulate as fast as hardware, to still be
used.

mcs: provide tickless api for arm timers

This does not implement the timers for any platforms, but
provides the generic arm arch, and aarch32/aarch64 infrastructure for
tickless timer drivers.

mcs: tickless scheduler implementation

This changes the budget/remaining fields in scheduling contexts
to contain timer ticks, not number of abstract sel4ticks.

seL4_SchedControl_Configure now takes microseconds, not ticks.

This commit is plat-independant - the platform and arch specific
timer code follows in later commits.

mcs: Add a scheduling context object

This is the first part of the seL4 MCS. This commit:

* adds a scheduling context object. Threads without scheduling
context objects cannot be scheduled.
* replaces tcbTimeSlice with the scheduling context object
* adds seL4_SchedControl caps for each core
* adds seL4_SchedControl_Configure which allows users to configure
amount of ticks a scheduling context has, and set a core for the
scheduling context.
* adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows
a tcb to be bound to a scheduling context.

CMake: Add KernelIsMCS option

This switches between master and mcs configurations.
This also adds a build system variable KernelPlatformSupportsMCS that
can be used to error on platforms that don't support MCS due to
unimplemented functionality.

python2 --> python3

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).

[SMP] Added PPI support for gic_v2

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.

tools: store KernelDTBSize as internal cache var

This is so KernelDTBSize can be consumed by other tools.

CMake: Process platform files in -C config

Allow projects that use the kernel as a subproject to configure the
kernel in -C scripts.

CMake supports providing a script via -C upon first initialisation of a
build directory. This script is expected to populate the configuration
cache for the rest of the build to depend on. This is how standalone
kernel builds are currently configured. However in buildsystems that add
the kernel as a subproject, it was up to the application to modify
configuration properties before or after the kernel was imported. This
lead to circular dependencies where properties were changed by a module
later in the build, but this then invalidated properties that were set
based on the first property's original value. This lead to running CMake
multiple times in order for settings to reach a stable state.

We now assume that most shared system configuration occurs in initial -C
settings evaluation. seL4Config.cmake is a configuration module that the
kernel exports that allows a configuration script to set kernel platform
and architecture settings in a way that doesn't introduce circular
dependencies.

seL4Config can be imported into other configuration files. This should
make it easier for a full system configuration script to query and
configure kernel configuration values without introducing circular
dependencies on configuration properties.

Add syscall for setting the current TLS register.

Some platforms and configurations do not allow user code to change the
value of the register used for TLS. On these architectures a syscall can
be used to allow the kernel to update the register on their behalf.

This does not immediately update the value in the user context on many
configurations as the values are only stored in the user context on a
context switch.

CMake: Invert plat config.cmake processing order

Instead of processing each platform CMake file during the arch's
config.cmake file, we process all of the platform CMake files first.
This is primarily motivated by wanting to move platform configuration
into a config file that is processed via a -C argument to the initial
build initialisation command.

Now a platform config is responsible for setting the kernel architecture
and it's own platform/arch specific config settings. Where previously a
platform was chosen in an arch specific way via either setting
KernelARMPlatform or KernelX86Sel4Arch or KernelRiscVPlatform, a
platform can now be set by KernelPlatform. In cases where a platform may
further parameterise its configuration it is free to choose its own
config options to query. Platforms that support multiple seL4
architectures should use KernelSel4Arch to query this. Platforms that
provide sub platforms such as exynos5 and subplatforms exynos5250,
exynos5410 and exynos5422 can be selected by specifying
KernelPlatform=exynos5, KernelARMPlatform=exynos5410 for example.

RISCV: Add Hifive unleashed platform

This change adds support for Hifive unleashed board. It also removes the
outdated hifive suport from the spike platform.

CMake: Generate device headers from DTS for spike

The DTS compilation was arm platforms only. Moving it to the top level
config file, making it available to RISCV platforms. The generated files
are almost identical with minor differences. A new argument(--arch) is
added to the hardware_gen.py for the differences.

config: make root cnode size 4k minimum

The previous minimum (4) was actually too small to fit more than 1
capability, which would not allow the kernel to boot. A 4K minimum means
on 32-bit, an 8 size is the minimum (256 slots) and on 64-bit, 7 (128
slots).

In addition to being a more practical minimum, this also allows for
simplification of the boot code for future commits.

CMake: Add -O0 option for kernel compilation

-O0 is a valid optimisation level. Results in faster compilation, but
noticably slower kernel execution when running applications such as seL4
test.

style: use consistent styling for all cmake files

Add .cmake-format.yaml which defines custom functions with kwargs to
style nicely

cmake: make pde_C an optional top-level type.

RISCV has its own model of page tables that doesn't have a distinguished
'directory' level.

riscv: Guard against setting max num nodes

SMP is not currently supported on riscv, this prevents a user accidentally trying to
use it.

RISC-V: Add CMake build files

x64: SKIM window to mitigate Meltdown (CVE-2017-5754) on x86-64

Introduces a kernel option that, when enabled, reduces the kernel window in a user address
space to just be Static Kernel Image and Microstate (SKIM), instead of the full kernel
address space. This isolates the important kernel data from the user preventing a
Meltdown style attack being able to violate secrecy. The kernel text and read only data,
i.e. anything that is static from boot, is not secret and can be allowed in the SKIM window
and potentially read by the user. Additionally to switch to and from the actual kernel
address space a small amount of state needs to also be in the SKIM window.

This is only an implementation for x86-64, although the same design is applicable to ia32

Hikey: disable DANGEROUS_CODE_INJECTION

DANGEROUS_CODE_INJECTION does not work on the Hikey due to the current
state of the vspace implementation.

cmake: TOPLEVELTYPES declared as target property

TOPLEVELTYPES is not intended to be configurable by the user, rather is a reflection
on the types defined by the source. This changes the TOPLEVELTYPES argument to be
a property, allowing it to be constructed as a generator expression when generating
BF files. By being a property, and not something like a global property, it removes
the need to ensure that additions to TOPLEVELTYPES are done prior to any bitfield
target definitions.

cmake: Custom target for holding properties

Defines an empty custom target whose purpose is to hold properties and configuration
data that can be retrieved using generator expressions in the build phase.

proof: Do not override proof variables

Using the `INTERNAL` attribute implied `FORCE` overriding any value the user may have set
for these. This was not the intention, and they should merely set a `CACHE` value if one
does not already exist.

proof: Do not check for KernelState_C.thy in CSPEC_DIR path

Add config option for CONFIG_RESET_CHUNK_BITS

The config variable is used in the kernel but no setting was provided
prio to this commit.

Add a CMake based build system

This commit adds an alternate build system using CMake that operates indepenently of
the existing Kconfig+Kbuild+make based build system