Move some lockTLB magic into C.

This patch moves the 'outer' chunk of lockTLBEntry into C rather
than handwritten assembly. The outer chunk accesses a global
counter and does arithmetic. The inner chunk (lockTLBEntryCritical)
writes to the registers, must be specially aligned, and is generally
special.

The change reduces unnecessary handwritten assembly, and also avoids
a special case that was problematic for binary verification.

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.

ARM: Add 32 bit directory for armv8-a

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.

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.

Release snapshot