Investigate Architecture for Symbolic Executor

[wu-benjamin]

We should begin by figuring out where to put code for the symbolic executor.

Note that we prefer to work with the MIR (middle intermediate representation) of the source code for symbolic execution as it is simple enough to process and analyze (like LLVM byte-code) but maintains some helpful borrow semantics. Moreover, it is helpful that the MIR is in the form of a control flow graph which is how symbolic execution is often described over.

The following options should be considered:

• write a separate plug-in (for MIR) that can be attached to the current official Rust compiler ❌
  • this is not viable as the Rust compiler no longer supports registering a pass for MIR
  • moreover, registering a pass for LLVM is also not supported
• follow what the state-of-the-art symbolic execution engine does (i.e. optionally mark symbolic variables in source code, compile code to LLVM byte-code altered by KLEE processing via compiler intrinsic functions, and analyzing the byte-code with symbolic execution) ❌
  • we will revisit this after considering the next option of forking the official Rust compiler to add a symbolic execution pass as we prefer to work with the MIR (rather than LLVM byte-code) and because this multi-step process is poor user experience
• fork the official Rust compiler and add in a symbolic execution pass there (symbolic variables are marked with Rust attributes and run symbolic execution through the nodes of the MIR) ✅
  • currently being investigated