Skip to content

Commit

Permalink
Document SAW conventions surrounding mir-json schema versions
Browse files Browse the repository at this point in the history
This documents the expectations surrounding SAW's requirements for `mir-json`
schema versions in the `README`. It also advertises the fact that we check for
schema versions in the changelog.
  • Loading branch information
RyanGlScott committed Feb 20, 2025
1 parent 9c62545 commit 05d7c89
Show file tree
Hide file tree
Showing 2 changed files with 27 additions and 9 deletions.
9 changes: 9 additions & 0 deletions CHANGES.md
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
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

0 comments on commit 05d7c89

Please sign in to comment.