Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Explicitly pin the mir-json version that SAW requires #2115

Merged
merged 1 commit into from
Sep 10, 2024

Conversation

RyanGlScott
Copy link
Contributor

SAW's MIR backend requires a particular MIR JSON schema, but it is not entirely obvious which version of the JSON schema to use (#2111). This patch is one step towards addressing this concern. It:

  • Adds mir-json as a submodule. At present, nothing in the repo (CI or otherwise) actually builds this submodule. Its presence is purely to communicate which version of mir-json must be used to compile Rust code to JSON that SAW can ingest.

  • Documents this in the README.

In the future, we will want to actually build and use mir-json in the CI (see #1868 for an in-progress attempt at this), but in the meantime, this is a decent first step. Until we actually start building mir-json in the CI and using it, we will need to remember to bump the mir-json submodule each time that SAW's JSON schema requirement changes.

Addresses one part of #2111.

@RyanGlScott RyanGlScott added the subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json label Sep 4, 2024

For more information on how to install `mir-json`, follow the instructions
[here](https://github.com/GaloisInc/mir-json#installation-instructions).

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I feel like this section ought to say something about translate-libs and $SAW_RUST_LIBRARY_PATH, but maybe that belongs in a separate branch.

Otherwise, LGTM.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a good point, although I wonder if the README is the best place to list instructions at this level of depth. Let me know if you feel differently, but I am more inclined to describe translate-libs, SAW_RUST_LIBRARY_PATH, and other topics related to mir-json in the SAW manual, and then include a forward reference to the SAW manual in this part of the README.

That being said, I just checked the relevant part of the SAW manual, and it is unfortunately somewhat scarce on details of how one actually installs mir-json. I definitely think we should rectify that, and since this PR is mostly a documentation-related change, I would be fine with adding such details to this PR.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess there's two aspects to this: (1) the translate-libs process should be documented somewhere, but also (2) all the critical pieces of the complete setup process for doing MIR verification should be mentioned in the same places, especially as long as things fail in a non-obvious way if you forget parts of it. So I think if we're going to mention setting up mir-json in the README, it should also mention the translate-libs process, even if just as a reference into the manual.

(I actually think it's probably good to have the complete setup process in the README, but I'm not totally committed to this given that the whole thing is experimental and hopefully by the time it isn't it'll all be less complicated and less fragile)

So... carry on I guess :-)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've pushed a new version of the PR that expands the discussion in the README somewhat, mentioning both the need for a specific mir-json version and the need for custom Rust standard libraries. I've also fleshed out the relevant section in the SAW manual to mention the mir-json submodule, translate_libs.sh, and the SAW_RUST_LIBRARY_PATH environment variable. I think this should be much better than it was before—PTAL.

The manual currently assumes that you are starting from a saw-script repo checkout. This is not ideal, since many SAW users download a binary distribution instead. In order to do better here, however, I think we need to first explicitly version mir-json's schema. I've started work on that in GaloisInc/mir-json#75.

@RyanGlScott RyanGlScott added the documentation Issues involving documentation label Sep 5, 2024
SAW's MIR backend requires a particular MIR JSON schema, but it is not entirely
obvious which version of the JSON schema to use (#2111). This patch is one step
towards addressing this concern. It:

* Adds `mir-json` as a submodule. At present, nothing in the repo (CI or
  otherwise) actually _builds_ this submodule. Its presence is purely to
  communicate which version of `mir-json` must be used to compile Rust code to
  JSON that SAW can ingest.

* Documents this in the `README`.

In the future, we will want to actually build and use `mir-json` in the CI
(see #1868 for an in-progress attempt at this), but in the meantime, this is a
decent first step. Until we actually start building `mir-json` in the CI and
using it, we will need to remember to bump the `mir-json` submodule each time
that SAW's JSON schema requirement changes.

Addresses one part of #2111.
@RyanGlScott RyanGlScott merged commit 2684385 into master Sep 10, 2024
34 checks passed
@RyanGlScott RyanGlScott deleted the T2111-mir-json-submodule branch September 10, 2024 18:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Issues involving documentation subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants