convert license headers to SPDX

Adjusted hypothesis kind, Eq assuming PC.

This is a fairly big change, I guess. The 'future' proof I need to
do requires a hypothesis kind in which an equality is gated by
whether the relevant addresses are visited. Perhaps all equalities
could be phrased this way anyway?

More debug tricks.

Fix symbol printing in debug memory traces.

Looks like it got broken a while back when some formatting
was consolidated.

Factor out some patterns and more debug code.

Adds some new helpers mk_n_implies and smt_num_t to factor out some
common use patterns. Also adds yet more debug tracing.

Silliest of bugfixes in handling ctz.

Need to reverse first, then clz. Not the other way around. Seriously.

Debug tweaks.

Debug tweak.

Debug tweaks.

Tweak a debug tracing mechanism.

Tweaks, mostly diagnostic.

Two major tweaks to var cycle analysis.

Firstly, var cycle analysis is now generally much better at handling
masking problems, e.g. when a linear variable is repeatedly masked off
or cast up and down, interspersed with other arithmetic.

Secondly, var cycle analysis detects dead paths within loops with some
vague approximation of const-propagation, which in particular allows an
offset value pageBitsForSize (SectionBits) in map_kernel_window to be
recognised as a constant offset.

Debug tweaks.

Tweak debug again.

Handle case splits in previous debug wrapper.

OK, returning the case split isn't so useful, it's better to keep
probing instead.

Add debug wrapper for funcall matching search.

The previous facility can speed up some otherwise lengthy searches
down to a likely match (and a likely inductive failure). The new
debug wrapper makes this easier to do.

Tweak era matching in debug script.

Improve debug script funcall matching.

Adjust approach to splittables.

Generate splittable information lazily and store in cached_analysis
of problem. Also check for complex loops at a slightly different
point.

Also replace an experimental better split point detector in logic
with another experimental one which also doesn't work perfectly yet.

Add 'strncmp' optimisation to search algorithm.

The search algorithm performed poorly in functions such as strncmp
where the only values changing in the loop are linear sequences.
(The approach is to relate these linear sequences to the initial
values rather than any matching values in the other loop.)

The optimisation is to first scan for any memory access addresses or
function call arguments that form linear progressions, and try to
match them. In particular, if doing so requires a case split, it's a
fast way to find it. In general we also narrow down to a smaller
collection of possible loop matching sequences.

Debug & fix some array assertion issues.

Hacky support for 8-bit reads in loops.

The (heuristic) stack variable estimation now sort-of supports reads of 8-bit
words inside loops, by just taking a slice of another word.

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.

Adjust for API change in check_hyp_group.

Somewhere in the parallelisation change, the change of return type
of this function didn't get propagated.

Debug support: trace mem address symbol names.

This makes some debug traces much easier to read.

Import of graph-refine tool.