GaloisInc / mir-json

Plugin for rustc to dump MIR in JSON format
Apache License 2.0
9 stars 2 forks source link

Add `cargo run-saw` command #59

Open RyanGlScott opened 11 months ago

RyanGlScott commented 11 months ago

Currently, the process of going from a Rust project to a SAW file is somewhat clunky. You must undergo the following steps:

  1. Compile your project with cargo saw-build.
  2. During the build, pay close attention to the output to find the line that says something like linking <N> mir files into example.linked-mir.json.
  3. Copy the example.linked-mir.json file name from the build output.
  4. Create a .saw file containing mir_load_module "example.linked-mir.json".

This is all doable, but a bit tiresome. It would be convenient to have a cargo run-saw command that automates the process. That is, starting from a Rust project, cargo run-saw would build the code, grab the name of the resulting MIR JSON file, and then emit a .saw template that already contains the appropriate call to mir_load_module. From there, users can build upon the .saw template further, and if they need to rebuild their Rust code, they can use cargo saw-build instead of run-saw.

This idea is similar in spirit to cargo crux-test's ability to generate a separate test script involving the compiled MIR JSON file, except that run-saw's functionality would be separate from saw-build.

spernsteiner commented 11 months ago

A related issue is that the name of the JSON file includes a cargo-generated hash that changes sometimes, such as when adding a library dependency, so we may need saw-build to copy the file to a more predictable path.

Another option would be to have cargo saw-run foo.saw actually invoke saw foo.saw, but with an additional variable in the initial scope that gives the path to the JSON file. This might require adding a SAW command-line option along the lines of gcc/clang's -D NAME=VALUE.

qsctr commented 11 months ago

Is there always only a single .linked-mir.json file in the target/<target>/<profile>/deps directory?

RyanGlScott commented 11 months ago

That's right. mir-json takes all of the intermediate build artifacts and links them together into a single .json file at the end.

qsctr commented 11 months ago

This is an awful hack but it seems to work

json_path <- exec "find" ["target/<target>/<profile>/deps", "-name", "<crate>*.linked-mir.json", "-printf", "%p"] "";
m <- mir_load_module json_path;

It's probably a better idea just to have mir-json output it to a fixed path like <crate>.linked-mir.json or something though.

spernsteiner commented 11 months ago

Is there always only a single .linked-mir.json file in the target/<target>/<profile>/deps directory?

On a clean build, there will be only one. But the filename includes a hash of crate metadata, so if you build, add/remove a dependency, and build again, you might end up with two different .linked-mir.json files.