Add rewriting step for moving execute clauses into auxiliary functions

For example, generates an auxiliary function execute_ADD (rs, rt, rd) for the
clause execute (ADD (rs,rt,rd)) = ...

Without this rewriting, the execute function easily becomes too large to be
handled by Isabelle (e.g., for CHERI-MIPS; for MIPS alone, it seems to be just
about small enough).

This used to be implemented in the pretty-printer, but that code was commented
out recently in order to support a recursive execute function for RISC-V
compressed instructions.

0 files changed, 0 insertions, 0 deletions