convert license headers to SPDX

graph-refine: fix bitrot

Removes 'def_p_regs', a symbol that doesn't exist.

Blacklists 'arm_swi_syscall', a function defined in assembly that isn't
called by any C function, but which calls 'c_handle_syscall', another
blacklisted function.

Renames the special pointer return variable from 'r0_input' to
'ret_addr_input', to match upstream HOL.

Factor out a common substitution pattern.

Support some more instructions and stack cases.

Firstly, handle some more instruction forms that are showing up
in the source & binary.

Secondly, adjust the way that conditional path comparisons are
handled in stack_logic. This whole calculation is mostly an
over-precise way of trying to work around the presence of
non-returning function calls. Downstream from these we compute
stack offsets which are conditional on the impossible path, which
then need to be simplified. This new formulation seems to handle
the new cases, but may need to be strengthened yet again.

squash

stack analysis: more diagnostic information.

Add some more information to the default channel when doing
stack analysis. It's silly to go digging through the various
debug mechanisms only to discover an extra function inlined
in a funny place.

Tweaks for loop_bounds variants in stack_logic.

More diagnostic info.

Helper for finding problematic clones.

Fix problem with stack analysis, inst funs.

Apparently stack analysis of some functions was being blocked by
the presence of instruction functions, leading to dumb errors down
the line.

Fix a stack_logic issue, problem not solved.

Of course, the real issue here is that we don't have stack
preservation across these clone function calls, so we don't
know what to expect on the far side.

Very odd bugfix.

Handle conditionals better in stack offs analysis.

Start trying to address clones in stack anaysis.

More descriptive assertion on stack calc.

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.

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

Minor bugfixes.

Allow stack virtualisation failures.

Todo, recurse on these to learn more, eliminate these failures
and thus approximate Magnus' solution to the problem.

Assume functions with symbols respect the stack.

This supports some functions whose symbols and bodies are defined
directly in assembly, the current such culprit being lockTLBEntryCritical.

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.

Fix previous; include a compatibility workaround.

Fixes a bug in previous.

Also adds a hook whereby a target can request a previous level of
compatibility with functions that contain ASM statements and other
non-calling-convention compatible functions that may dangerously
adjust the stack pointer.

(The previous level of compatibility is actually unsound, because
it assumed that e.g. the fastpath restore assembly block did not
do what it did.)

Experimental: ignore unmatched ASM functions.

This may allow an (unreliable) WCET estimate of some code which
we haven't properly made sense of yet.

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.

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

Activate inst_logic for seL4-example, fixups.

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.

Improve some diagnostics.

Support 64-bit loads and stores.

Recognise new instruction'mcr function types.

Bugfix.

Bugfixes.

Addendum to previous in stack_logic.

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 caching & bugfixes.

Handle un-paired functions for stack analysis.

Further bugfixes for linked problems.

Improve documentation and output.

Import of graph-refine tool.