From bfff324f69cb661aea0e66670683b5bc5fd94a9a Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 10 May 2023 10:30:38 -0400
Subject: [PATCH] Include MIR JSON files for Rust standard libs in SAW bindists

When distributing SAW binaries, we want users to be able to turn their Rust
code into MIR JSON with relatively minimal effort. To that end, this patch
includes JSON files for the Rust standard libraries in SAW binary distributions
so that users do not have to build this themselves. This mirrors how these
files are included in `crux-mir` binary distributions.

This checks off one box in #1859.
---
 .github/ci.sh            |  1 +
 .github/workflows/ci.yml | 19 +++++++++++++++++++
 .gitmodules              |  3 +++
 deps/mir-json            |  1 +
 doc/manual/manual.md     | 14 +++++++++++++-
 5 files changed, 37 insertions(+), 1 deletion(-)
 create mode 160000 deps/mir-json

diff --git a/.github/ci.sh b/.github/ci.sh
index 6d86bb867d..a258557693 100755
--- a/.github/ci.sh
+++ b/.github/ci.sh
@@ -93,6 +93,7 @@ bundle_files() {
   cp LICENSE README.md dist/
   $IS_WIN || chmod +x dist/bin/*
 
+  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
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 3fd05777f7..481a87fab7 100644
--- a/.github/workflows/ci.yml
+++ b/.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 mir-json version documented in
+  # deps/mir-json/README.md.
+  RUST_TOOLCHAIN_VERSION: "nightly-2020-03-22"
+
   # Solver package snapshot date - also update in the following locations:
   # ./saw/Dockerfile
   # ./saw-remote-api/Dockerfile
@@ -119,6 +123,17 @@ 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
+        with:
+          toolchain: ${{ env.RUST_TOOLCHAIN_VERSION }}
+          override: true
+          components: rustc-dev
+
+      - name: Install mir-json
+        shell: bash
+        run: cd dependencies/mir-json && cargo install --locked --force
+
       - shell: bash
         run: .github/ci.sh install_system_deps
         env:
@@ -146,6 +161,10 @@ jobs:
       - shell: bash
         run: .github/ci.sh build
 
+      - name: Translate Rust standard libraries with mir-json
+        shell: bash
+        run: cd deps/crucible/crux-mir && bash ./translate_libs.sh
+
       - shell: bash
         env:
           RELEASE: ${{ needs.config.outputs.release }}
diff --git a/.gitmodules b/.gitmodules
index 926212c99c..941a80948a 100644
--- a/.gitmodules
+++ b/.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
diff --git a/deps/mir-json b/deps/mir-json
new file mode 160000
index 0000000000..3a621e1023
--- /dev/null
+++ b/deps/mir-json
@@ -0,0 +1 @@
+Subproject commit 3a621e102350582d610dfc726d2cb7263b150bf2
diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index f34ed84e1c..943a00b369 100644
--- a/doc/manual/manual.md
+++ b/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