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.

Treat optimize attribute as gcc specific

Clang doesn't provide support for __attribute__((optimize ...)). There
are alternatives to provide the same functionality but due to how rarely
the kernel is compiled without optimisations, this can be added on
demand.

ARM/v7-a: Force -O2 compilation of idle thread

This fixes a problem with -O0 SMP builds on ARM visible as kernel
data aborts whenever the idle thread executes.

The idle thread receives no stack pointer. At -O2, this is fine
as the wfi() call is inlined and stack operations in idle_thread
are optimized out. At -O0, the stack operations remain and wfi()
is not inlined, resulting in stack accesses in the idle thread
that cause data aborts.

Forcing -O2 behaviour was deemed the simplest solution for now.
Giving the idle thread a stack would have had larger verification
ramifications for what is now a fairly uncommon use case.

trivial: print kernel entry reason on halt

It is generally useful to know what operation was occuring
when the kernel halted, as this is usually called from assert.

Mark halt as no-inline and no-return.

This actually leads to better code. Copies of the halt loop inlined
in various places will instead be single instructions 'bl halt'. It's
also important for the translation validation to avoid having
pointless loops everywhere, especially inside the bodies of other
loops.

Remove many DONT_TRANSLATE markers.

The vast majority of the DONT_TRANSLATE markers in the kernel are used
to hide __asm__ statements and builtin functions
(e.g. __builtin_unreachable ()) from the C-to-Isabelle parser.

The parser now supports underscore identifiers and many __asm__ statements,
and the builtin functions are prototyped, meaning the vast majority of the
DONT_TRANSLATE markers can be dropped. The remaining markers cover functions
that must be treated specially.

[STYLE_FIX]

SELFOUR-614: calling halt() on the hikey platform results in infinite data abort
SELFOUR-408: halt does not halt

Remove assembly files for halt and idle thread and add wfi in armv.