convert license headers to SPDX

Another fix for 'use reverse induction less often'

Despite refactors, key code paths were blocked by an erroneous
return value. Should be fixed now.

Fix for 'use reverse induction less often'

It seems that this adjustment wasn't tested well enough.

Use reverse induction less often.

Candidate reverse induction proofs can be generated in many problems.
To save time, use them only in cases where the resulting hypothesis
overturns a loop unroll or induction failure judgement.

bugfix: use same large values.

The discrepancy between 2^32 - 3 and 2^32 - 10 can matter. Not very
much, but enough to create unusual failures.

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.

Supply path assumption in linear seq check.

Simple addition of a path hypothesis when necessary_split_opts
is testing a linear sequence match. Sometimes overflow information
isn't available unless the path to the first element of the
sequence is actually taken.

More debug tricks.

Handle case of negative differences better.

Some stats for split discovery.

Hopefully I'll get a useful graph out of these yet ... depends on
-O2 coming through.

Silliest of bugfixes in handling ctz.

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

Fix strange issue left behind in refactor.

More careful in r_side_unroll.

Turns out some of the extra "interesting" expressions are pretty dumb. Pay
attention only to word-type, matched ones.

Drop debugging output.

Tweak find_split_limit to find a precise limit.

Previously it might be out by a few, now it closes in on a precise
limit. This is relevant if the cached limit is re-fetched.

Bugfix.

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.

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.

Final tweaks to linear series adjustments.

I think it's all working fine but the point of the change is moot.
It's tricky to use the data like I want and I've found an easier
way.

Refactor of get_necessary_split_opts.

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

Whoops.

Search in report mode mentions search context.

Add a trace mechanism for inductive failures.

Fix a serious issue in loop offset.

This is turning into a saga, and it's pretty simple after all. The
previous implementation focused on splittables, so it didn't work
for conditionally visited nodes, which may still be important for
lining up linear series in e.g. strncmp. Fix by inverting, then it's
a simple graph-flood calculation.

Bugfix loop-offset code.

Bugfix get_splittables_after, actually works now.

Take more care with loop offsets in multi-entry.

Normally the head point is splittable and the first node of the loop
to be visited, but in the multi-entry case, the head point may not be
the first point visited in one of the cases. This may create an off-by-1
issue in the generated proof script, and needs to be handled a little
more carefully.

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.

Some test code for linear series.

Obvious solution, only apply it to the C code, which doesn't have
stack issues etc.

There's still some risks associated with e.g. 8-bit linear series
stored within 32-bit variables for which we'll see false negatives.
Oh well.

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.

Add debug facility for narrowing search to nodes.

e.g. in case I'm currently debugging, the nodes after calls to
'provide_cap' are expected to be matchable.

New model repair strategy.

It's a bit smarter. Also, in the parallel phase, it allows the
remaining parallel solvers to continue, so there's a chance that
a clean model will be generated while a partly erroneous model is
being repaired.

Minor bugfixes.

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.

Performance tweak necessary splits.

Guess of how many iterations to unfold is adjusted to the minimum
for functions with calls in them, since this was taking a while.

Tweak necessary split mechanism.

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

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.

Tweak previous tweak to linear split candidates.

The previous change dropped a little too much of the new information.
Revert to the previous idea, but with a bit more padding.

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.

Don't assert progress during replay.

This is a bit silly, but it's possible that we're asking the solver
redundant questions when rechecking cached splits.

Performance tweaks and cleanup in loop search.

+ assert progress is being made
+ use the zero-variable properly for loops with no other vars
(less induct failures, hopefully).
+ don't cache working splits unless the induct check passes.

Bugfix.

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.

Tweak report output.

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.

Minor fixes.

Have search say a little more in quiet mode.

More bugfixes.

Minor bugfix.

Minor bugfix.

Address minor issues in previous.

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.

Cache, reuse some loop search results.

This is a warmup to a bigger adjustment to the way loop searches which require
case splits are handled.

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

Minor updates.

Bugfixes.

Better implementation of find_case_split.

1) notices case splits that lead to alternative entry points to loop.
2) ignores case splits that are viable but can't lead to the loop
(this appears in a bit of gcc code using conditional ops to set
up return stuff when the condition that ensures the loop is not
visited has already been seen.)

Definitely an improvement, not sure if sufficient.

Pass explicit tags further to fix more bugs.

Loop bounds passing for now on seL4.

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

Slight adjustment to runtime when a check fails.

Restore the 0-check in split search.

I found out that it had been dropped by adding an example loop problem. This
could potentially lead to insane splits being discovered for loops with no live
variables at some points. (The only useful such loops are linear searches,
where the 'live' variable is treated as a function of the loop count.) It
remains to be seen whether this breaks any existing searches.

Import of graph-refine tool.