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.

Sign up for GitHub

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

Jump to bottom

Better synchronize SAW with the mir-json version it depends on #2111

Open
weaversa opened this issue Aug 28, 2024 · 4 comments
Open

Better synchronize SAW with the mir-json version it depends on #2111

weaversa opened this issue Aug 28, 2024 · 4 comments
Assignees
@RyanGlScott @mccleeary-galois
Labels
priority High-priority issues subproject Issues involving one of the various subprojects SAW depends on subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json type: bug Issues reporting bugs or unexpected/unwanted behavior

Comments

@weaversa
Copy link
Contributor

weaversa commented Aug 28, 2024 •
edited by RyanGlScott
Loading

I have a Rust verification script that has been working until today. Neither the script nor the Rust implementation have changed, so I am guessing some new version of either saw or rust are causing the issue. Any help would be appreciated.

$ saw ...
...
saw_client.exceptions.VerificationError: error: Stack trace:
JSON Decoding of linked-mir.json failed: Error in $.fns[2].body.blocks[2].block.data[4].rhs.usevar.data.rendered: parseJSON - bad rendered constant kind: Just (String "bstr")

EDIT: See the checklist in #2111 (comment) for action items.
@andrew-bivin andrew-bivin added type: bug Issues reporting bugs or unexpected/unwanted behavior priority High-priority issues labels Aug 29, 2024
@RyanGlScott
Copy link
Contributor

RyanGlScott commented Aug 29, 2024 •
edited
Loading

This is expected, as we updated the version of the MIR JSON schema that we support in #2107. The most direct fix is to compile your Rust code using a version of mir-json that includes the corresponding changes (in GaloisInc/mir-json#73).

Obviously, it's not ideal that existing code fails with such an inscrutable error message, of course. I see two ways that we could do better:

  1. We should more clearly communicate that SAW needs to ingest Rust code that is compiled with a particular mir-json version. In crux-mir, we achieve this by (1) pinning mir-json as a submodule, and (2) instructing users (via the documentation) to compile the version of mir-json that is included as a submodule. We could just as well adopt a similar mir-json submodule approach in SAW as well.
  2. The error message above is confusing, but it's really a result of attempting to load a MIR JSON file that is using an older version of the schema that SAW no longer supports. Ideally, SAW would detect this and say as much in the error message. (We propose doing this as part of Add a schema version to JSON mir-json#45.)

Would these improvements help your needs here?

@weaversa
Copy link
Contributor Author

Thank you. I hadn't realized the tools I was using were out of sync. I updated as suggested and things are working again.

I agree with you suggestions for improvements!

@RyanGlScott
Copy link
Contributor

Thanks for confirming! In that case, I will repurpose this issue to track the improvements in #2111 (comment). (I've also re-titled the issue accordingly—I hope that's alright with you.)

As noted above, checking for old MIR JSON schemas will first need to start at the mir-json level (GaloisInc/mir-json#45). We should also add mir-json as a submodule. That is being done as part of #1868, but that PR is being blocked on other tasks. I propose that we factor out the mir-json submodule part of that patch (without anything else) into its own PR.

@RyanGlScott RyanGlScott changed the title parseJSON - bad rendered constant kind: Just (String "bstr") Better synchronize SAW with the mir-json version it depends on Aug 29, 2024
@RyanGlScott RyanGlScott added subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json upstream labels Aug 29, 2024
RyanGlScott added a commit that referenced this issue Sep 4, 2024
@RyanGlScott
Explicitly pin the mir-json version that SAW requires
04ee593 
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 mentioned this issue Sep 4, 2024
Merged
@RyanGlScott
Copy link
Contributor

#2115 addresses the first check box in #2111 (comment).

RyanGlScott added a commit that referenced this issue Sep 9, 2024
@RyanGlScott
Explicitly pin the mir-json version that SAW requires
a66f178 
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 mentioned this issue Sep 9, 2024
Open
RyanGlScott added a commit that referenced this issue Sep 10, 2024
@RyanGlScott
Explicitly pin the mir-json version that SAW requires (#2115)
2684385 
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.
@sauclovian-g sauclovian-g added subproject Issues involving one of the various subprojects SAW depends on and removed upstream labels Oct 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RyanGlScott RyanGlScott

@mccleeary-galois mccleeary-galois

Labels
priority High-priority issues subproject Issues involving one of the various subprojects SAW depends on subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
5 participants
@RyanGlScott @weaversa @andrew-bivin @sauclovian-g @mccleeary-galois