The K Framework LLVM backend implements fast concrete execution for languages written in K. It does so by compiling K definitions to specialized, native-code interpreters via LLVM IR. This document is intended as a technical reference for developers of the LLVM backend, rather than for end users of K. If you are a K user looking for technical advice, please open an issue on the main K repository.
The LLVM backend documentation is split into two main sections: technical documentation for the internal implementation details of the backend, and a developer guide with best practices and conventions for working on the repository.
An incomplete, high-level overview of the backend's main structure and features is given in the remainder of this document. Full details are given in the technical documentation.
The backend does not operate on K definitions directly. Rather, it operates on KORE, a de-sugared, simplified internal representation of K with a formal basis in Matching Logic. A KORE definition can be compiled into a native interpreter binary that efficiently implements the rewrite system specified by that definition; these interpreters transform KORE terms into other KORE terms by rewriting.
The backend performs compilation in two main steps. First, the set of rewrite rules in the definition are used to generate a decision tree structure; these trees describe an efficient way to destructure a KORE term to determine whether a rewrite rule applies to it. Full details of this procedure are given here.
Then, information from the definition and the compiled decision trees are used to emit LLVM IR that implements an interpreter for the definition's rewrite system.
The interpreters generated by the backend load a KORE term as input, then parse it to generate a space-efficient internal term structure. Rewrite rules are applied to the term until no more can apply (i.e. rewriting finishes), and the result is un-parsed to a KORE term for output.
