Implement mir_load_module
#1863
Conversation
doc/manual/manual.md
Outdated
| * `CRUX_RUST_LIBRARY_PATH` should point to the the MIR files for the Rust | ||
| standard library. TODO RGS: Describe how to produce this |
There was a problem hiding this comment.
The name "CRUX_RUST_LIBRARY_PATH" is somewhat unfortunate here, as SAW is a completely separate tool from Crux. This needn't be a blocker for this patch, but we should consider renaming CRUX_RUST_LIBRARY_PATH to something else going forward. I have opened GaloisInc/mir-json#43 to track this.
There was a problem hiding this comment.
GaloisInc/mir-json#46 introduces SAW_RUST_LIBRARY_PATH as an alias for CRUX_RUST_LIBRARY_PATH, and I've updated the SAW manual to reference the former. The explanation for how to know where to point SAW_RUST_LIBRARY_PATH is still somewhat unsatisfactory, but I think may need to include a copy of the MIR-ified Rust standard library in SAW bindists before we can provide better documentation. I've added a reminder to do this as a checkbox in #1859.
RyanGlScott
force-pushed
the
T1859-mir_load_module
branch
from
fbc988a to
6583923
Compare
RyanGlScott
added
the
PR: ready to merge
This implements an experimental `mir_load_module` command, the first SAW command dedicated to MIR (Rust) code. I have added a basic test case to kick the tires and ensure that everything works as you would expect. You can't do much with the resulting MIR module yet (besides printing it in the SAW REPL), but more functionality for verifying the MIR code will come in future patches. Note that in order to produce a MIR JSON file suitable for SAW's needs, you must build your Rust code with one of the two `mir-json` tools added in GaloisInc/mir-json#41. This checks off one box in #1859.
RyanGlScott
force-pushed
the
T1859-mir_load_module
branch
from
6583923 to
7bb990f
Compare
RyanGlScott
added
the
subsystem: crucible-mir
This implements an experimental
mir_load_modulecommand, the first SAW command dedicated to MIR (Rust) code. I have added a basic test case to kick the tires and ensure that everything works as you would expect. You can't do much with the resulting MIR module yet (besides printing it in the SAW REPL), but more functionality for verifying the MIR code will come in future patches.Note that in order to produce a MIR JSON file suitable for SAW's needs, you must build your Rust code with one of the two
mir-jsontools added in GaloisInc/mir-json#41.This checks off one box in #1859.