search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
437 stars 63 forks source link

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

Open weaversa opened 2 months ago

weaversa commented 2 months ago

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 https://github.com/GaloisInc/saw-script/issues/2111#issuecomment-2316528551 for action items.

RyanGlScott commented 2 months ago

This is expected, as we updated the version of the MIR JSON schema that we support in https://github.com/GaloisInc/saw-script/pull/2107. The most direct fix is to compile your Rust code using a version of mir-json that includes the corresponding changes (in https://github.com/GaloisInc/mir-json/pull/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 https://github.com/GaloisInc/mir-json/issues/45.)

Would these improvements help your needs here?

weaversa commented 2 months ago

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 commented 2 months ago

Thanks for confirming! In that case, I will repurpose this issue to track the improvements in https://github.com/GaloisInc/saw-script/issues/2111#issuecomment-2316528551. (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 (https://github.com/GaloisInc/mir-json/issues/45). We should also add mir-json as a submodule. That is being done as part of https://github.com/GaloisInc/saw-script/pull/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 commented 2 months ago

https://github.com/GaloisInc/saw-script/pull/2115 addresses the first check box in https://github.com/GaloisInc/saw-script/issues/2111#issuecomment-2316528551.