convert license headers to SPDX

Support some more instructions and stack cases.

Firstly, handle some more instruction forms that are showing up
in the source & binary.

Secondly, adjust the way that conditional path comparisons are
handled in stack_logic. This whole calculation is mostly an
over-precise way of trying to work around the presence of
non-returning function calls. Downstream from these we compute
stack offsets which are conditional on the impossible path, which
then need to be simplified. This new formulation seems to handle
the new cases, but may need to be strengthened yet again.

Split inner instructions into pairs.

Create extra functions l_impl'isb, r_impl'isb etc instead of just impl'isb.
This means that rep_graph's function pair mechanism can figure out how to
orient the function pair, which avoids weird bugs.

Support dmb instruction and an accumulator.

For unrolled loops, we may need an accumulator where a value is incremented and
trimmed to 8-bits repeatedly. Bleh.

Miscellaneous updates.

1) Support new instruction'* function naming scheme from the graph decompiler
which includes instruction addresses in the name of the function. This makes
the instruction naming scheme uniform, which is a good thing.
2) Have tokens appear by name in SMT expressions and diagnostic results.
3) Miscellaneous refactor and cleanup

New feature: instruction specs.

Adds bodies for instruction'mcr* and asm_instruction'mcr* etc functions.
Handles mcr and mrc forms already. These bodies just map to impl'mcr_
functions, but the mapping eliminates irrelevant complexity (some synonyms and
also the details of which register holds args/rets). Works for a couple of
functions.