Explicitly pin the mir-json version that SAW requires (#2115)

SAW's MIR backend requires a particular MIR JSON schema, but it is not entirely
obvious which version of the JSON schema to use (#2111). This patch is one step
towards addressing this concern. It:

* Adds `mir-json` as a submodule. At present, nothing in the repo (CI or
  otherwise) actually _builds_ this submodule. Its presence is purely to
  communicate which version of `mir-json` must be used to compile Rust code to
  JSON that SAW can ingest.

* Documents this in the `README`.

In the future, we will want to actually build and use `mir-json` in the CI
(see #1868 for an in-progress attempt at this), but in the meantime, this is a
decent first step. Until we actually start building `mir-json` in the CI and
using it, we will need to remember to bump the `mir-json` submodule each time
that SAW's JSON schema requirement changes.

Addresses one part of #2111.

.gitmodules

@@ -49,3 +49,6 @@
 [submodule "deps/lmdb"]
 	path = deps/lmdb
 	url = https://github.com/GaloisInc/lmdb.git
+[submodule "deps/mir-json"]
+	path = deps/mir-json
+	url = https://github.com/GaloisInc/mir-json.git

README.md

@@ -88,6 +88,26 @@ will be possible for all language constructs. There are various
 instructions that are not supported during verification. However,
 any failure during `llvm_load_module` should be considered a bug.
 
+## Notes on Rust
+
+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.
+
+For complete instructions on how to install `mir-json`, the modified Rust
+standard libraries, and how to defined the `SAW_RUST_LIBRARY_PATH` environment
+variable, follow the instructions
+[here](https://github.com/GaloisInc/mir-json#installation-instructions).
+
 ## Notes on Windows
 
 If you have trouble loading the SAW REPL on Windows, try invoking it

doc/manual/manual.md

@@ -1812,15 +1812,62 @@ In order to verify Rust code, SAW analyzes Rust's MIR (mid-level intermediate
 representation) language. In particular, SAW analyzes a particular form of MIR
 that the [`mir-json`](https://github.com/GaloisInc/mir-json) tool produces. You
 will need to intall `mir-json` and run it on Rust code in order to produce MIR
-JSON files that SAW can load (see [this section](#loading-mir)).
+JSON files that SAW can load (see [this section](#loading-mir)). You will also
+need to use `mir-json` to build custom versions of the Rust standard libraries
+that are more suited to verification purposes.
+
+If you are working from a checkout of the `saw-script` repo, you can install
+the `mir-json` tool and the custom Rust standard libraries by performing the
+following steps:
+
+1. Clone the [`crucible`](https://github.com/GaloisInc/crucible) and `mir-json`
+   submodules like so:
+
+   ```
+   $ git submodule update deps/crucible deps/mir-json
+   ```
+
+2. Navigate to the `mir-json` submodule:
+
+   ```
+   $ cd deps/mir-json
+   ```
+
+3. Follow the instructions laid out in the [`mir-json` installation
+   instructions](https://github.com/GaloisInc/mir-json#installation-instructions)
+   in order to install `mir-json`.
+
+4. Navigate to the
+   [`crux-mir`](https://github.com/GaloisInc/crucible/tree/master/crux-mir)
+   subdirectory of the `crucible` submodule:
+
+   ```
+   $ cd ../crucible/crux-mir/
+   ```
+
+5. Run the `translate_libs.sh` script:
+
+   ```
+   $ ./translate_libs.sh
+   ```
+
+   This will compile the custom versions of the Rust standard libraries using
+   `mir-json`, placing the results under the `rlibs` subdirectory.
+
+6. Finally, define a `SAW_RUST_LIBRARY_PATH` environment variable that points
+   to the newly created `rlibs` subdirectory:
+
+   ```
+   $ export SAW_RUST_LIBRARY_PATH=<...>/crucible/crux-mir/rlibs
+   ```
 
 For `cargo`-based projects, `mir-json` provides a `cargo` subcommand called
 `cargo saw-build` that builds a JSON file suitable for use with SAW. `cargo
 saw-build` integrates directly with `cargo`, so you can pass flags to it like
 any other `cargo` subcommand. For example:
 
 ```
-$ export SAW_RUST_LIBRARY_PATH=<...>
+# Make sure that SAW_RUST_LIBRARY_PATH is defined, as described above
 $ cargo saw-build <other cargo flags>
 <snip>
 linking 11 mir files into <...>/example-364cf2df365c7055.linked-mir.json
@@ -1840,7 +1887,7 @@ Note that:
 `rustc` accepts. For example:
 
 ```
-$ export SAW_RUST_LIBRARY_PATH=<...>
+# Make sure that SAW_RUST_LIBRARY_PATH is defined, as described above
 $ saw-rustc example.rs <other rustc flags>
 <snip>
 linking 11 mir files into <...>/example.linked-mir.json