Explicitly version the JSON schema

We now include a `"version": <N>` entry in the top-level JSON map that gets
generated for each MIR JSON file, where `<N>` represents the version of the
JSON schema that is used to generate the file. Going forward, any changes to
the JSON schema will be accompanied by a corresponding schema version bump. I
have also included some logic in `link_crates` to ensure that all of the crates
being linked together use the same schema version.

Fixes #45.

README.md

@@ -36,5 +36,20 @@ book](https://doc.rust-lang.org/book/2018-edition/ch01-01-installation.html)).
 
 See the [crux-mir][crux-mir-repo] README for usage instructions.
 
+## JSON schema
+
+`mir-json` and related tools produce MIR JSON files as output, which the
+contain the intermediate MIR code from the compiled program in a
+machine-readable format. Downstream tools are sensitive to the particular
+schema that a MIR JSON file uses, so we explicitly record the version of the
+JSON schema in each MIR JSON file (in the `"version"` field).
+
+Any time that `mir-json` is updated such that the JSON schema must also be
+changed, we will also update the schema version number. The version number is
+represented as a single integer. Any changes to the schema are assumed to be
+backwards-incompatible with previous versions of the schema, so all version
+bumps should be treated as major version bumps. Each change to the schema is
+described in the [`SCHEMA_VERSIONING.md`](SCHEMA_VERSIONING.md) file.
+
 
 [crux-mir-repo]: https://github.com/GaloisInc/crucible/tree/master/crux-mir

SCHEMA_CHANGELOG.md

@@ -0,0 +1,8 @@
+The following document describes the changes to the JSON schema that
+`mir-json`–produced files adhere to. (This document should not be interpreted
+as a changelog for the code in the `mir-json` tools themselves, which are
+versioned separately.)
+
+## 1
+
+Initial schema version.

src/analyz/mod.rs

@@ -32,6 +32,7 @@ mod ty_json;
 use analyz::to_json::*;
 use analyz::ty_json::*;
 use lib_util::{self, JsonOutput, EntryKind};
+use schema_ver::SCHEMA_VER;
 
 basic_json_enum_impl!(mir::BinOp);
 
@@ -1168,6 +1169,7 @@ pub fn analyze_nonstreaming<'tcx>(
     let total_items = out.fns.len() + out.adts.len() + out.statics.len() + out.vtables.len() +
         out.traits.len() + out.intrinsics.len();
     let j = json!({
+        "version": SCHEMA_VER,
         "fns": out.fns,
         "adts": out.adts,
         "statics": out.statics,

src/lib.rs

@@ -24,5 +24,6 @@ extern crate rustc_target;
 pub mod analyz;
 pub mod lib_util;
 pub mod link;
+pub mod schema_ver;
 
 mod tar_stream;

src/lib_util.rs

@@ -28,6 +28,7 @@ use serde_cbor;
 use serde_json;
 use tar;
 
+use crate::schema_ver::SCHEMA_VER;
 use crate::tar_stream::{TarStream, TarEntryStream};
 
 #[derive(Debug, Default, Serialize, Deserialize)]
@@ -39,6 +40,9 @@ pub struct CrateIndex {
     pub items: HashMap<StringId, ItemData>,
 
     pub roots: Vec<StringId>,
+
+    /// The schema version in use. (See also `SCHEMA_VER`.)
+    pub version: u64,
 }
 
 /// Metadata about a single item.
@@ -245,7 +249,9 @@ impl EmitterState {
         let mut roots = self.roots.into_iter().collect::<Vec<_>>();
         roots.sort();
 
-        CrateIndex { names, items, roots }
+        let version = SCHEMA_VER;
+
+        CrateIndex { names, items, roots, version }
     }
 }
 
@@ -296,6 +302,7 @@ impl<W: Write> Emitter<W> {
 
     pub fn emit_crate(&mut self, j: &JsonValue) -> io::Result<()> {
         write!(self.writer, "{{")?;
+        write!(self.writer, "\"version\":{:?},", SCHEMA_VER)?;
         self.emit_table_from(EntryKind::Fn, j)?;
         write!(self.writer, ",")?;
         self.emit_table_from(EntryKind::Adt, j)?;

src/link.rs

@@ -62,13 +62,41 @@ fn collect_roots(
     roots
 }
 
+/// Ensure that all `CrateIndex`es have consistent schema versions. If all
+/// indexes have the same schema version, return the version number. Otherwise,
+/// return an error.
+///
+/// Precondition: there must be at least one `CrateIndex`. If this precondition
+/// is not met, this function will panic.
+fn check_equal_versions(
+    indexes: &[CrateIndex],
+) -> serde_cbor::Result<u64> {
+    match indexes.split_first() {
+        Some((first_index, last_indexes)) => {
+            let version = first_index.version;
+            for index in last_indexes {
+                if version != index.version {
+                    return Err(serde::ser::Error::custom(format!(
+                        "Mismatched schema version numbers ({:?} and {:?})",
+                        version,
+                        index.version,
+                    )));
+                }
+            }
+            Ok(version)
+        },
+        None =>
+            panic!("check_equal_versions: Empty list of crate indexes"),
+    }
+}
 
 /// Combine the contents of `ocs`, producing a combined JSON crate data object as the result.
 pub fn link_crates<R, W>(inputs: &mut [R], mut output: W) -> serde_cbor::Result<()>
 where R: Read + Seek, W: Write {
     let (indexes, json_offsets) = read_crates(inputs)?;
     let (it, defs, translate) = assign_global_ids(&indexes);
     let roots = collect_roots(&indexes, &translate);
+    let version = check_equal_versions(&indexes)?;
 
 
     let mut seen_names = HashSet::new();
@@ -117,6 +145,7 @@ where R: Read + Seek, W: Write {
 
     // Write tables to the output, copying the serialized content of each entry.
     write!(output, "{{")?;
+    write!(output, "\"version\":{:?},", version)?;
     for (i, kind) in EntryKind::each().enumerate() {
         if i > 0 {
             write!(output, ",")?;

src/schema_ver.rs

@@ -0,0 +1,9 @@
+/// The version of the JSON schema that `mir-json` follows. This is intended for
+/// use by downstream tools to quickly determine if they are ingesting a MIR
+/// JSON file that is compatible with the version of the schema that they are
+/// expecting.
+///
+/// Each version of the schema is assumed to be backwards-incompatible with
+/// previous versions of the schema. As such, any time this version number is
+/// bumped, it should be treated as a major version bump.
+pub const SCHEMA_VER: u64 = 1;