The KMIR team at Runtime Verification Inc. is responsible for defining the operational semantics of Rust’s Middle Intermediate Representation (MIR) in K to bring Rust into the K Framework ecosystem! We would like to give an update on the current status of the project, and what we are working on next. The past many weeks we have tackled serialisation of Stable MIR, development of a driver program to extract the JSON serialised representation of Stable MIR from Rust programs, definition of the Stable MIR syntax and semantics in K, and parsing serialised Stable MIR into a K Abstract Syntax Tree (AST).
Stable MIR Serialisation
KMIR (and other projects) require a portable and stable representation of MIR for our tools to access. In order to benefit the broader community, we have worked on serialisation of Stable MIR and have upstreamed an initial version into the Rust Compiler! Read more about this in our recent blog post.
smir_pretty Driver
The serialisation of Stable MIR is accessed through interrupting the compiler through Ccallbacks and initiating the serialisation in the after_analysis function. We built our own driver framework in our smir_pretty repository to allow for easy serialisation of Rust programs to JSON. This driver currently has to link to a custom branch of the Rust compiler where we work on the development of Stable MIR serialisation, however once we have a final version of serialisation upstreamed we will be able to work with the main branch of the Rust compiler.
Defining Stable MIR Syntax and Semantics in K
Our work to define the syntax of Stable MIR in K is largely completed, and now we have moved on to developing the semantics of Stable MIR. This is an ongoing iterative process as we iron out the syntax in a way to allow the semantics to work efficiently and intuitively. Defining the syntax and semantics of MIR in K is a large project, and we want to make sure to get it right, so we’re spending a lot of time up-front designing the semantics to ensure the smoothest possible operation of KMIR in the long term.
Parsing Serialised Stable MIR into K
With the serialisation of Stable MIR available to us in JSON format, we need to develop a parser to bring that JSON into K. We have chosen a new approach for a schema driven parser written in python. We believe a schema driven parser is the best approach as our AST of Stable MIR in K is essentially a 1 - 1 representation of it as it is in the Rust compiler. This approach allows us to easily identify how symbolic execution using KMIR corresponds to the original Stable MIR source, and also allows us to quickly update the entire toolchain as Stable MIR evolves (as nascent technology is bound to do).
Future Work
Many parts have to be developed and connected to complete the KMIR project, but each is underway and steady progress is being made. We aim to keep iterating on the above components and improve them until they are completed and have easy to use user interfaces. We will also begin development of Koat, the property testing framework for Rust that will use KMIR as its semantics backend.
