convert license headers to SPDX

More parallel model search in solver.

The existing implementation spawned parallel solvers to search for
a model, but waited for a single solver to test each result. This
implementation makes it all part of a single parallel cycle.
Somewhat tested.

Quiet solver stderr channel.

One of my default solvers is a bit noisy on stderr. We can't handle
its memory exceptions, so just quiet them.

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.

More diagnostic info.

Bugfixes.

Silliest of bugfixes in handling ctz.

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

Handle CountTrailingZeroes.

Fix solv.close () issue.

Problem was, solvers were being counted more than once in the active_solvers
list if they were repeatedly started up. This eventually leads to a solver
killing itself from time to time. Easily fixed.

Slightly more debugging to track down closes.

Erm, correct output problems from previous.

Diagnostic information was being sent to the main channel, and
there was leftover excessive debug tracing. Oops.

Slightly reduce output in previous.

Bugfix parallel solver closing.

Traced down to a foolish 'self.close' when falling back to the slow solver
somewhere. Also trace what's happening to the solvers that are cut off.

Tweaks to support Yices2.

Stronger restrictions again on malformed models.

Handle bad solver responses in parallel.

Running a flaky Z3 variant here that sometimes crashes and spams
the response buffer with things that might or might not parse.
Simple solution in parallel, drop that solver, and hope another
sorts things out.

Fix c_rodata optimisation idea.

Report more on failures, in particular timeouts.

Bugfix: handle None case for rodata_ptrs.

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.

Try to close parallel solvers on interrupts.

Change the way the .rodata section is handled.

The new version allows multiple things to be read-only data. This
allows handling the .boot.rodata pseudo-section from seL4, for
instance.

Mention the absence of psutil in timing msgs.

Miniscule tweak to timing.

Better timing messages, especially with psutil.

Fix solver self-test.

Two problems to fix, firstly that model updates led to a problem in
the check model wrapper, secondly that the self-test failed trivially
because the solver may include a result for the '.rodata_witness'
variable in the model, which makes it more complex than expected.

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.

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.

Much better output for parallel solvers.

Previously the verbose mode for spawning parallel solvers was
*way* too verbose.

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 a parallel word8-rep solver.

Allow model generation in parallel solvers.

This allows the 'slow' solvers to be used in parallel mode to find models,
which rather than picking a single best solver to try to use.

Report timeouts correctly in parallel.

The case where a parallel solver timed out or failed needs to be handled
carefully, permitting the other solvers to possibly solve the problem.

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

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.

Unlink solver input files.

They've been cluttering up /tmp/ directories until now. They aren't needed
once the solver has opened them, and can be unlinked by default. There are
better ways to export them than leaving them lying around on the disk.

fixed another typo

fixed a typo

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.

fixed "import signal" error in solver.py

Support 64-bit loads and stores.

Compatibility adjustment.

Relevant to some versions of python, apparently.

Adding graph-to-graph

added a missing import sys

Parallelise more often.

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.

Close parallel solvers on solver inst shutdown.

Bugfix.

Explain .solverlist strategies.

Better parallel implementation of hyp testing.

WIP: test_hyp_imps via parallel strategies.

Make solver-set configurable per Solver instance.

Do setsid on starting up forked solvers.

Add PArrayValid support.

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

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

Robustness adjustments.

Performance tweaks.

New toplevel result for solver timeout/error.

Until now we've been conflating proof failure caused by solver failure
and proof failure caused by logical incorrectness (sat when unsat was
required). Hopefully clarified.

Better document SMT/.solverlist issues.

Raf found a couple of common misunderstandings, so I've been a lot
more explicit about which solvers are needed/useful and what to expect.

Self-test both slow and fast solver.

Distinguish quiet and regular test.

Add self-test mode for solver.py.

Import of graph-refine tool.