Offline Partial Eval

[ncough]

Wrapper around existing online partial evaluation work to perform offline partial evaluation. Rather than producing the semantics for a single instruction opcode, this approach produces a lifter for some subset of the architecture.

The process looks roughly like the following:

1. Convert the decoder & instruction encoding structures into ASL functions
2. Identify all of the reachable functions from this initial set up to a configurable frontier
3. Simplify these functions to remove annoying/unsupported features
4. Transform each function such that loop bounds and bitvector widths are always known
5. Run the existing online partial evaluation over each instruction encoding function
6. Do some cleanup and pruning based on the results of the partial evaluation
7. Run a taint analysis over the evaluated instruction encoding functions to identify what is known at lifttime vs runtime
8. Transform all runtime influenced statements and expressions into IR generating operations against an assumed interface
9. Print the result as an OCaml program with the IR interface instantiated as ASL IR

The above works for a significant portion of AArch64 matching the existing lifters coverage for all but aarch64_memory_vector_single_post_inc, aarch64_memory_vector_single_no_wb, aarch64_memory_vector_multiple_post_inc, aarch64_memory_vector_multiple_no_wb. However, the resulting OCaml program is ~200k lines long and takes ~5min to build. This can mostly be attributed to some aggressive specialisation in stage 4 and the resulting unrolling transforms introduced by stage 5.

There are still a decent number of things to do:

• Improvements to AArch64 coverage:
  • LExpr BitTuple support
• Improvements to compile time / size:
  • Break the produced OCaml program into a series of files, rather than one
  • Support symbolic for loops throughout the pipeline, to reduce unrolling and specialisation
  • Simplify based on branch conditions (e.g. if X = '1' then c should replace X with '1' in c)
• 'Quality' of resulting program:
  • Comparison of online & offline lifter results
  • Implement a form of copy prop over the IR generating operations produced in stage 8
  • Implement some trivial identities within the IR interface

Given the compile time issues, this PR includes a generate lifter that supports no instructions. A new lifter can be generated using echo ':gen A64 aarch64.+' | dune exec asli from the project directory. A subsequent dune build will compile the new lifter. There are two entry points to the lifter:

• asloff-sem OPCODE will dump the semantics of OPCODE
• asloff-coverage PAT will run the coverage test for all instruction encodings matching PAT

[ncough]

Apologies, made a few improvements. After splitting the OCaml program across multiple files, build times are now down to ~1min. Also managed to get the copy prop pass implemented. Will merge once the tests pass.