convert license headers to SPDX

Integrate future induction.

The required checks and search process were added recently.
The ProofNode proof script type now has a SingleRevInduct
proof kind, which captures the reverse-induction at a single
loop point, and the search process emits the relevant proof
scripts.

This required a minor restructure of the searcher.

Tweaks, setup for next feature.

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?

Factor out a common substitution pattern.

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.

Report more on failures, in particular timeouts.

Some more inner loop handling sanity.

This gets us past the 'check' phase of problem setup for functions
with inner loops.

Experiment with side-proving rodata ineqs.

The suspicion was that some slow-down seen lately was because the
rodata-witness value might now have a disjunction of possible
reasons for difference, which might make the solver logic for
understanding that function input are valid more obscure. A possible
fix for that is to pre-test and pre-assert that the witness must be
disjoint from problem pointers on the C side, based just on their PC.
That should simplify the SMT logic, one might think.

Tweaks, mostly diagnostic.

Take more care with scan_mem_calls.

With some asm wrappers and other rare cases, some ASM-side functions
fetch/save the stack and others don't. This leads to confusion about
the number of calls any memory has participated in. Since this case
is rare anyway, just merge the call sets and be pessimistic about
which functions have 'really' been called.

Trace reasons for skipping funcall pairings.

Fix funcall pair optimisation for ro-functions.

The funcall pair optimisation tracks how many function calls have
contributed to any given memory variable. Special care is now taken
for read-only C functions which don't return an updated memory.

Minor bugfixes.

The calls-on-memory optimisation.

Track, for each memory object, the number of calls to various
functions that have gone into it. Well, a range, min-max. Avoid
producing function relations for function call pairs that can't
reasonably be related. This may substantially reduce the problem
complexity for function calls in loops that get unrolled a fair
bit.

Search performance improvements.

Tweaking now, less tracing, more caching, more caution in using the
necessary linear sequence alignment, and a cache to avoid repeatedly
testing similar weakly aligned splits.

Tweak handling of reachability.

Move reachability cache to problem (from rep_graph), use in check
to insist on discovering (0) loop bounds slightly less often.

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.

Adjust handling of unusual restrs in rep_graph.

Address minor issues in previous.

More use of parallel model generation.

Debug & fix some array assertion issues.

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.

Improve some diagnostics.

Parallelise more often.

Better parallel implementation of hyp testing.

WIP: test_hyp_imps via parallel strategies.

Make solver-set configurable per Solver instance.

Performance tweaks.

Bugfixes.

Simplify search_bound, bugfixes.

Import of graph-refine tool.