Tweaks, setup for next feature.

Factor out a common substitution pattern.

Setup for doing some more loop linear analysis.

There's always more to be done, apparently.

Retire 'ret_inner' in logic.linear_series_exprs

The flag adjusted the return type, but apparently the old version
no longer worked anyway.

More debug tricks.

Probable solution to the map_kernel_window saga.

The key monster here is a function with three loops, each of a known
iteration count, where the count in the second loop is 16 and it is
unrolled. That doesn't get caught by any of our existing detectors.

The linear sequence mechanism can be used to detect what's happened. The
interesting elements of loop 2 in the C side are matched by elements outside
all loops on the binary side. That can be used to trigger a loop bound check.

Bugfixes.

Bugfix linear expr adjustments.

Refactor of get_necessary_split_opts.

Also, oops. The function I was wanting to apply this to doesn't generate any.

Bugfix for unmatched functions in linear loops.

Change side for rodata proofs.

Of course, it's much easier to prove the C output memory is unchanged,
since the pvalid arguments directly relate the C memory access addresses
to the reserved .rodata addresses. I think the reason it was done
differently before is that there must always be an input asm-side memory,
whereas the C one may be missing, and we still need to know rodata.

New version: do everything on C side if possible. If only ASM side exists,
assume rodata holds. So sometimes read-only functions will happen after
ASM updates and the solvers will have to work hard to figure out that the
updates (on the ASM side) were protected (on the C side). But most of the
time rodata will prove quickly because it's easy to see the updates aren't
touching the witness address.

Find interesting linear series saved to memory.

At the moment we've only been tracking memory access pointer
sequences, but it makes some sense to save a linear sequence to
some address then call some function on it, and something like
that comes up with a memory-mapped hardware register in -O2.

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.

Beginnings of support for 16-bit linear series.

Workaround for oddity in UXTH decompile.

The decompiler sometimes emits code that bitmasks to e.g. the bottom 16 bits
before casting to that sized word, which breaks the linear series analysis for
the relevant values. Triggered by the UXTH instruction at the moment.

Still only half fixed.

Fix bug in shiftl offset logic.

This one was a howler, but there might be more subtle offset problems
around.

Frustratingly, the obvious way to test the offset logic won't work.
Any stack access, particularly around a function call, requires a
serious correctness argument to line up the way the analysis sees it
with what might happen in the general case.

Fix a bug with stack pointers in var analysis.

To do loop var analysis on stack slots, we 'virtualise' some nodes
to what they would be if stack slots were variables. Along the way,
the stack pointers themselves disappear, which is a problem if a
stack-relative address has been saved into a register other than the
stack pointer. To fix this we insert some redundant lvals in our
fake nodes.

Slight tweak to loop analysis.

In particular, handle the case where a constant value is repeatedly
computed and stored somewhere, e.g. a constant stack value being
retrieved into a register.

Expand loop example, fix logic.py bugs, solve.

A new version of the loop-example also includes a loop with a
function call. Some tweaking in logic.py is necessary to detect
the key linear sequences, but the problems all solve pretty quickly
now, which is a huge improvement on their original times.

Better linear split logic.

Instead of trying to unroll everything far enough to see the sequences
line up, pay attention to the sequence offsets and do the linear
calculations locally.

Tweak necessary split mechanism.

Now works for arguments to function calls that are not necessarily
encountered in every loop iteration. It also fails faster.

Get function limit bounds working.

Resolution:
- the previous hack for general splittable points was restored.
- the loop bound function limit code was rewritten to not require
this anyway.

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.

Initial switch-optimisation implementation.

Partly working. Has detection for switch-like problems that can probably
be best addressed with an initial case split. New search feature discovers
matching path pairs from within the case split set. Hook for building proofs
based on this not currently working.

Bugfixes, also report times in reports.

Major refactor of search, should fail faster.

- knowledge is now a class, SearchKnowledge.
- CaseSplit is no longer a last resort.
+ failed searches (at any depth) have follow-up searches which specialise
to a single case (if possible)
+ the follow-up search keeps some of the previous knowledge
+ a CaseSplit is built if the single-case follow-up search succeeds.

Doing the additional follow-up searches may slow down some successful runs that
need to iterate up to a high depth. However loops that cannot be split will
fail in roughly the usual time rather than trying every possible case split
for an eternity, which should more than compensate.

Debug & fix some array assertion issues.

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.

Allow unspecified padding in stack returns.

When returning a struct containing shorter words, the compiler is permitted to
save to only the relevant part of the target word. This is different to the
usual in-register behaviour.

Minor fixes.

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.

Make a little more use of subst from syntax.

Don't trace constant vars in loop analysis.

Support 64-bit loads and stores.

Bugfix: size-0 types are possible now.

A type with a size of 0 used to be nonsensical, but the array types
in principle can have it (in odd irrelevant expressions) and some assertions
have to be tweaked to make sense.

Add PArrayValid support.

Not fully tested yet, but this is the rough shape of support for array
size assertions, including dynamic array size assertions.

Performance tweaks.

Code for finding a loop-splitting point.

So far we've been assuming the entry point to a loop will be a
splitting point. With this code we would be able to handle this case, but I'll
have to review other code to figure out what will break if I just turn it on.

Fix a couple of bugs exposed by 'example'.

One is a regression in the old-style pairing setup, caused by
exclusively using the 'CPU' style in more recent problems.

The other is an interesting bug in conditional_cond_simps caused
by a conditional both of whose branches point to the same node. This
causes a double update where data is lost. Also not seen recently
because such nodes aren't produced by current graph generators.

Import of graph-refine tool.