Include MIR JSON files for Rust standard libs in SAW bindists

.github/ci.sh

@@ -93,6 +93,7 @@ bundle_files() {
   cp LICENSE README.md dist/
   $IS_WIN || chmod +x dist/bin/*
 
+  $IS_WIN || cp -r deps/crucible/crux-mir/rlibs dist/lib
   (cd deps/cryptol-specs && git archive --prefix=cryptol-specs/ --format=tar HEAD) | (cd dist/deps && tar x)
   cp doc/extcore.md dist/doc
   cp doc/tutorial/sawScriptTutorial.pdf dist/doc/tutorial.pdf

.github/workflows/ci.yml

@@ -19,6 +19,10 @@ env:
   CACHE_VERSION: 1
   DISABLED_TESTS: "test0000 test_FNV_a1_rev test0010_jss_cnf_exp test0039_rust test_boilerplate test_external_abc"
 
+  # Keep this in sync with the Rust nightly documented in
+  # deps/mir-json/README.md.
+  RUST_TOOLCHAIN: "nightly-2023-01-23"
+
   # Solver package snapshot date - also update in the following locations:
   # ./saw/Dockerfile
   # ./saw-remote-api/Dockerfile
@@ -108,6 +112,19 @@ jobs:
           cabal user-config update -a "extra-include-dirs: \"\""
           cabal user-config update -a "extra-lib-dirs: \"\""
 
+      - name: Install Rust toolchain
+        uses: actions-rs/toolchain@v1
+        if: runner.os != 'Windows'
+        with:
+          toolchain: ${{ env.RUST_TOOLCHAIN }}
+          override: true
+          components: rustc-dev
+
+      - name: Install mir-json
+        shell: bash
+        if: runner.os != 'Windows'
+        run: cd deps/mir-json && cargo install --locked --force
+
       - shell: bash
         run: .github/ci.sh install_system_deps
         env:
@@ -135,6 +152,11 @@ jobs:
       - shell: bash
         run: .github/ci.sh build
 
+      - name: Translate Rust standard libraries with mir-json
+        shell: bash
+        if: runner.os != 'Windows'
+        run: cd deps/crucible/crux-mir && bash ./translate_libs.sh
+
       - shell: bash
         env:
           RELEASE: ${{ needs.config.outputs.release }}

.gitmodules

@@ -46,3 +46,6 @@
 [submodule "deps/language-sally"]
 	path = deps/language-sally
 	url = https://github.com/GaloisInc/language-sally
+[submodule "deps/mir-json"]
+	path = deps/mir-json
+	url = https://github.com/GaloisInc/mir-json

doc/manual/manual.md

@@ -1715,7 +1715,19 @@ Note that:
   the `.linked-mir.json` file that appears after `linking X mir files into`, as
   that is the JSON file that must be loaded with SAW.
 * `SAW_RUST_LIBRARY_PATH` should point to the the MIR JSON files for the Rust
-  standard library.
+  standard libraries.
+
+  SAW binary distributions include these MIR JSON files, so if you are using a
+  SAW binary distribution, it suffices to define
+  `SAW_RUST_LIBRARY_PATH=<saw-directory>/lib/rlibs`. If you are building SAW
+  from source, you must also build the MIR JSON files for the Rust standard
+  libraries from source. To do so, run the following commands:
+
+  ```
+  $ cd deps/crucible/crux-mir
+  $ ./translate_libs.sh
+  $ export SAW_RUST_LIBRARY_PATH=$(pwd)/rlibs
+  ```
 
 `mir-json` also supports compiling individual `.rs` files through `mir-json`'s
 `saw-rustc` command. As the name suggests, it accepts all of the flags that