convert license headers to SPDX

graph-refine: print failing function in check_funs

Compress dead-arc/missing-node warnings.

Quieter load messages.

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.

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.

Handle CountTrailingZeroes.

Beginnings of support for 16-bit linear series.

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.

Add definitions for WordReverse.

Simple operator that does the obvious thing, puts the bits of a
word in the opposite order. Can be used to count zeroes at the
other end, which is exactly what GCC does on ARM.

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.

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 fixes.

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.

Minor adjustments.

skip fastpath functions for now

Use ss as expected in Expr.subst.

Oops. Thanks to Brian Campbell for reporting.

Implementation of TokenWords: WordArray variant.

Indexed by Token rather than by a word type. Should be more
convenient to work with for various C ghost data.

Initial implementation of Tokens.

Token is a new type that encodes strings. The only supported
operation is equality. They're actually encoded as unique words at
the SMT level, but we avoid committing to that too early.

No idea what I was thinking last night.

Faster implementation of pseudo compiling.

Make a little more use of subst from syntax.

Introduce expr subst operation.

A bit like visits, allows broad adjustments of exprs. Avoids
duplicating expressions when no substitutions are actually made.

Bugfixes.

First steps toward floating point support.

This gets mostly just passed through to the relevant SMT logics. Since they're
still transitionally supported it's not clear whether to change the QF_ABV
logic or not.

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.

Make function hashes stable.

It turns out hash(None) varies by python implementation. Strings,
ints and tuples thereof have stable hashes. Keeping the hashes
stable allows StackBounds and LoopBounds files to be shared between
machines.

Import of graph-refine tool.