diff --git a/CHANGES.md b/CHANGES.md index f3802da85..08ba587dd 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -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 @@ -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) diff --git a/README.md b/README.md index 26282c02b..a5f28126a 100644 --- a/README.md +++ b/README.md @@ -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