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.

Check reverse single induction, use in search.

The check module now knows how to check a proof of loop equalities
by induction. The loop_bounds module already had this, but now it
is more official. It can also check a predicate by *reverse*
induction. The idea here is to name some predicate, show that it
would be true if some iteration bound is reached (i.e. typically
a very large number), and then show by induction back down that the
predicate was also true in the initial iterations.

This is useful in a special case involving a loop of the form
for (i = 0; i < n; i ++) { } with no function calls. Suppose the
body contains an array index p[i], which implies the array fits in
memory, i * sizeof(*p) < 2 ^ 32. Since the final iteration
i = n - 1 must be reached, the compiler can deduce
that n <= 2 ^ 32 / sizeof(*p), a fact we will prove by reverse
induction.

The search module now contains code to detect cases like this and
discover the best bound we can impose by simple binary search.

Tweaks, setup for next feature.

Update for tweak to the way search works.

More loop_bounds inspection code.

Bugfixes.

Use loop bound extra eqs in split search.

Try this strategy if an induct fails. It seems to get init_irqs to
prove, and it's really easy to implement and usually fast.

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.

Fix for metrics generation.

Add quick query of loop body addrs.

Add facility for checking which loops are complex.

Improve loop_bounds induction; avoid nesteds.

New code for making sure loop_bounds avoids nested loops.

Also, a substantial upgrade to how quickly the inductive search package
discovers the true set of inductive invariants.

Tweak detection of complex loops.

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.

Exclude instruction functions from loop_bounds.

Improve metrics mechanisms.

Note function limits in trace_refute also.

Function limits of zero are a decent way of forbidding access to part of the
system for experimental reasons.

Fix up loop bound metrics, useable.

Bugfix.

Finish work on loop timing estimates.

Or rather, problem metrics that may be correlated with loop timing.

Loop timing estimates.

Retire some old code from loop_bounds.

Slightly more timing information, diagnostic.

Bugfix.

loop_bounds: more principle for preemptionPoint

We've been manually adding bounds for functions which call preemptionPoint, but
that means manually checking that we've found them all, and for larger numbers
of runs I'm starting to make mistakes. Add a mechanism to quickly check this.
Has to be configured to the name of the functions limited. Also allows pruning
functions considered unreachable in this run.

loop_bounds: Recurse more thoroughly for merge.

Merged bounds are computed by considering all possible call sites of a
function. We need to avoid doing this recursively, since the exponentially many
possible contexts would explode us. Previously this was done by avoiding the
context operations inside a merge, which prevents us looking up the stack for
functions with single call sites. This patch adds a little more finesse.

Track timing in LoopBounds.txt

added a flag to convert_loop_bounds.py and get_bound_super_ctxt to only
read cached result and not do any long running calculations (treat those
as failures)

Re-fix loop bound conversion.

The call to the new test_hyp_group was still wrong.

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.

Split load_target and load_target_args.

Add no-C-information mode, tweak solver models.

Robustness adjustments.

Normalise loop ids in get_bound_super_ctxt.

Bugfix.

Don't assume loop heads are canonical.

Instead switch to the canonical loop heads for internal caching.

Cache aborts as None in get_bound_super_ctxt.

Commentate loop bounds better on stdout.

Bugfixes.

Capture un-paired functions in some analyses.

Functions callable from functions tagged 'ASM' should be analysed
in ASM analysis phases also. Tongue twist that.

More bugfixing and diagnostics for loop_bounds.

Yet more of the above.

Pass explicit tags further to fix more bugs.

More caching & bugfixes.

Loop bounds passing for now on seL4.

(It's not actually finding all that many bounds, so we're not done
yet.)

Trivia.

More loop search bugfixes.

Simplify search_bound, bugfixes.

Fix bug in linear series hyp processing.

Further bugfixes for linked problems.

Continue searching on Abort.

minor bugfix

Integrate loop_bounds.py from WCET project.

The new loop_bounds.py is a sibling to trace_refute. It discovers
bounds for binary loops in various ways.

This version takes a previous external version and stitches it into
the local infrastructure. It's still a bit of a mess.