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.

Document internal machine/interrupt.h interface

Every platform has to implement a standard set of interrupt interfaces
that the kernel uses to interract with a machine's interrupt controller.
Providing a single header file for each of these functions provides a
single location to document their behavior.

style: consistently attach return type

Add attach-return-type to astyle

rpi3/aarch64: use generic word sizes in interrupt controller

Fix licenses (the rest)

ARM/IRQ: add a function to initialise local IRQ controller for CPUs

Similar to initIRQController(), cpu_initLocalIRQController() has to
be implemented for each platform. For those that are gonna support
SMP, it should be implemented proprely (if required), otherwise
it can be stubbed for single core implementations.

s/D61/DATA61/ in license headers for consistency

Remove many MODIFIES annotations.

These are redundant for any function which the C-to-Isabelle parser
actually analyses, which is now the vast majority of functions.

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.

SELFOUR-537: Support for raspberry pi3