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

Explicitly check mir-json schema version #2228

Merged
merged 3 commits into from
Feb 20, 2025
Merged

Explicitly check mir-json schema version #2228

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0dbbac3
Regenerate *.linked-mir.json files to include schema versions
RyanGlScott Feb 20, 2025
9c62545
Explicitly check mir-json schema version
RyanGlScott Feb 20, 2025
05d7c89
Document SAW conventions surrounding mir-json schema versions
RyanGlScott Feb 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
# next -- TBA

This release supports [version
1](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#1) of
`mir-json`'s schema.

## New Features

* SAW documentation is now under a single Sphinx umbrella, resulting in a
Expand All @@ -17,6 +21,11 @@
* Add `mir_equal` and `jvm_equal` commands, which mirror the `llvm_equal`
command for the MIR and JVM backends, respectively.

* Explicitly check that the `mir-json` schema version is supported when parsing
a MIR JSON file. If the version is not supported, it will be rejected. This
helps ensure that unsupported `mir-json` files do not cause unintended
results.

## Bug fixes

* The saw executable's usage message now fits into a terminal. (#405)
Expand Down
27 changes: 18 additions & 9 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,15 +98,24 @@ any failure during `llvm_load_module` should be considered a bug.
SAW has experimental support for analyzing Rust programs. To do so, one must
compile Rust code using [`mir-json`](https://github.com/GaloisInc/mir-json), a
tool which compiles Rust code to a machine-readable, JSON-based format.
Note that:

* Each version of SAW understands the JSON output of a particular version of
`mir-json`, so make sure that you build the version `mir-json` that is
included in the `mir-json` submodule (located in `deps/mir-json`).
* Moreover, SAW requires slightly modified versions of the Rust standard
libraries that are suited to verification purposes. SAW consults the value
of the `SAW_RUST_LIBRARY_PATH` environment variable to determine where to
look for these modified standard libraries.

Currently, SAW supports [version
1](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#1) of
`mir-json`'s schema. Note that the schema versions produced by `mir-json` can
change over time as dictated by internal requirements and upstream changes. To
help smooth this over:

* We intend that once SAW introduces support for any given schema version, it
will retain that support across at least two releases.
* An exception to this rule is when `mir-json` updates to support a new Rust
toolchain version. In general, we cannot promise backwards compatibility
across Rust toolchains, as the changes are often significant enough to
impeded any ability to reasonably provide backwards-compatibility guarantees.

Moreover, SAW requires slightly modified versions of the Rust standard
libraries that are suited to verification purposes. SAW consults the value of
the `SAW_RUST_LIBRARY_PATH` environment variable to determine where to look for
these modified standard libraries.

For complete instructions on how to install `mir-json`, the modified Rust
standard libraries, and how to defined the `SAW_RUST_LIBRARY_PATH` environment
Expand Down
2 changes: 1 addition & 1 deletion deps/crucible
Open in desktop
Submodule crucible updated 10 files
+4 −0 crucible-mir/CHANGELOG.md
+17 −14 crucible-mir/src/Mir/GenericOps.hs
+3 −0 crucible-mir/src/Mir/JSON.hs
+2 −0 crucible-mir/src/Mir/Mir.hs
+12 −2 crucible-mir/src/Mir/ParseTranslate.hs
+2 −1 crucible-mir/src/Mir/Trans.hs
+10 −0 crux-mir/CHANGELOG.md
+16 −0 crux-mir/README.md
+2 −2 crux-mir/src/Mir/Language.hs
+1 −1 dependencies/mir-json
2 changes: 1 addition & 1 deletion deps/mir-json
Open in desktop
Submodule mir-json updated 7 files
+15 −0 README.md
+17 −0 SCHEMA_CHANGELOG.md
+2 −0 src/analyz/mod.rs
+1 −0 src/lib.rs
+8 −1 src/lib_util.rs
+20 −0 src/link.rs
+9 −0 src/schema_ver.rs
2 changes: 1 addition & 1 deletion intTests/test1973/test.linked-mir.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::244e86ab7dde68ac"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::244e86ab7dde68ac"}},"pos":"test.rs:5:5: 5:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::244e86ab7dde68ac"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:6:2: 6:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::244e86ab7dde68ac"}]},"name":"test/386aae68::f","return_ty":"ty::Ref::244e86ab7dde68ac","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"test/386aae68::S::_adtb7803c2264daf0ec[0]","orig_def_id":"test/386aae68::S","orig_substs":[],"repr_transparent":true,"size":1,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/386aae68::S::0","ty":"ty::u8"}],"inhabited":true,"name":"test/386aae68::S"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/386aae68::f","kind":"Item","substs":[]},"name":"test/386aae68::f"}],"tys":[{"name":"ty::Adt::fe89a517b102d23b","ty":{"kind":"Adt","name":"test/386aae68::S::_adtb7803c2264daf0ec[0]","orig_def_id":"test/386aae68::S","substs":[]}},{"name":"ty::Ref::244e86ab7dde68ac","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Adt::fe89a517b102d23b"}},{"name":"ty::u8","ty":{"kind":"Uint","uintkind":{"kind":"U8"}}}],"roots":["test/386aae68::f"]}
{"version":1,"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::72fda5b91c47396c"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::72fda5b91c47396c"}},"pos":"test.rs:5:5: 5:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::72fda5b91c47396c"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:6:2: 6:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::72fda5b91c47396c"}]},"name":"test/0d75de25::f","return_ty":"ty::Ref::72fda5b91c47396c","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"test/0d75de25::S::_adtb7803c2264daf0ec[0]","orig_def_id":"test/0d75de25::S","orig_substs":[],"repr_transparent":true,"size":1,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/0d75de25::S::0","ty":"ty::u8"}],"inhabited":true,"name":"test/0d75de25::S"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/0d75de25::f","kind":"Item","substs":[]},"name":"test/0d75de25::f"}],"tys":[{"name":"ty::Adt::a8a1a3466e211b44","ty":{"kind":"Adt","name":"test/0d75de25::S::_adtb7803c2264daf0ec[0]","orig_def_id":"test/0d75de25::S","substs":[]}},{"name":"ty::Ref::72fda5b91c47396c","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Adt::a8a1a3466e211b44"}},{"name":"ty::u8","ty":{"kind":"Uint","uintkind":{"kind":"U8"}}}],"roots":["test/0d75de25::f"]}
2 changes: 1 addition & 1 deletion intTests/test2000/test.linked-mir.json
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion intTests/test2005_mir_lifetime/test.linked-mir.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:6:12: 6:13","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"test.rs:6:5: 6:15"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::e028c0f25e8b6323"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::d14b05c19ee909be"}},"pos":"test.rs:6:5: 6:15","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:7:2: 7:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::d14b05c19ee909be"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/b552c423::f","return_ty":"ty::Adt::d14b05c19ee909be","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"test/b552c423::S::_adtbd21306cbe4f0b9b[0]","orig_def_id":"test/b552c423::S","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/b552c423::S::x","ty":"ty::Ref::e028c0f25e8b6323"}],"inhabited":true,"name":"test/b552c423::S"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/b552c423::f","kind":"Item","substs":[]},"name":"test/b552c423::f"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::Adt::d14b05c19ee909be","ty":{"kind":"Adt","name":"test/b552c423::S::_adtbd21306cbe4f0b9b[0]","orig_def_id":"test/b552c423::S","substs":["nonty::Lifetime"]}}],"roots":["test/b552c423::f"]}
{"version":1,"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:6:12: 6:13","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"test.rs:6:5: 6:15"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::e028c0f25e8b6323"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::188545d5524e10a7"}},"pos":"test.rs:6:5: 6:15","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:7:2: 7:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::188545d5524e10a7"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/c76ff53f::f","return_ty":"ty::Adt::188545d5524e10a7","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"test/c76ff53f::S::_adtbd21306cbe4f0b9b[0]","orig_def_id":"test/c76ff53f::S","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/c76ff53f::S::x","ty":"ty::Ref::e028c0f25e8b6323"}],"inhabited":true,"name":"test/c76ff53f::S"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/c76ff53f::f","kind":"Item","substs":[]},"name":"test/c76ff53f::f"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::Adt::188545d5524e10a7","ty":{"kind":"Adt","name":"test/c76ff53f::S::_adtbd21306cbe4f0b9b[0]","orig_def_id":"test/c76ff53f::S","substs":["nonty::Lifetime"]}}],"roots":["test/c76ff53f::f"]}
Loading
Loading