From 4334531636da0e813d8b99eba24d6e1ddef02638 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 | 22 ++++++++++++++++++++++
 .gitmodules              |  3 +++
 deps/mir-json            |  1 +
 doc/manual/manual.md     | 14 +++++++++++++-
 5 files changed, 40 insertions(+), 1 deletion(-)
 create mode 160000 deps/mir-json

diff --git a/.github/ci.sh b/.github/ci.sh
index 6d86bb867d..347ac4e615 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/*
 
+  $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
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 57f7d3454d..122bf0abf6 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 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 }}
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..117ec97f97
--- /dev/null
+++ b/deps/mir-json
@@ -0,0 +1 @@
+Subproject commit 117ec97f971171cfac3eea37e5009e1f6bfa9ae8
diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index ff3555b46a..6c809d1356 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