Migrate modified Rust standard libraries to mir-json

RyanGlScott · RyanGlScott · commit 5401898cec0d · 2025-03-27T14:56:28.000-04:00
Now that the `mir-json`-specific versions of the Rust standard libraries have been moved to the `mir-json` repo (in GaloisInc/mir-json#85 and GaloisInc/crucible#1319), this patch adjusts the various references to the standard libraries to ensure that SAW's documentation, CI, and test suite remain up to date.
diff --git a/CHANGES.md b/CHANGES.md
@@ -48,6 +48,12 @@ This release supports [version
   occurred, so this change makes SAW more permissive with respect to
   unsupported LLVM versions.)
 
+* The modified copies of the Rust standard libraries that `mir-json` depends on
+  (and SAW therefore ingests when performing MIR verification) now live in the
+  `mir-json` repo rather than in the `crucible` repo. See the [`mir-json`
+  README](https://github.com/GaloisInc/mir-json/blob/master/README.md) for
+  details.
+
 ## Bug fixes
 
 * An off-by-one error in `listSortDrop` in the SAWCore prelude has
diff --git a/crux-mir-comp/test/Test.hs b/crux-mir-comp/test/Test.hs
@@ -95,7 +95,7 @@ runCrux rustFile outHandle mode = Mir.withMirLogging $ do
                                             _ -> "",
                                         Crux.branchCoverage = (mode == RcmCoverage) } ,
                    Mir.defaultMirOptions { Mir.printResultOnly = (mode == RcmConcrete),
-                                           Mir.defaultRlibsDir = "../deps/crucible/crux-mir/rlibs" })
+                                           Mir.defaultRlibsDir = "../deps/mir-json/rlibs" })
     let ?outputConfig = Crux.mkOutputConfig (outHandle, False) (outHandle, False)
             Mir.mirLoggingToSayWhat (Just $ Crux.outputOptions $ fst options)
     setEnv "CRYPTOLPATH" "."
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good b/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good
@@ -8,11 +8,11 @@ failures:
 [Crux]   test/symb_eval/comp/alias_array_bad.rs:45:14: 45:16: error: in alias_array_bad/<DISAMB>::use_f[0]
 [Crux]   references AllocIndex 0 and AllocIndex 1 must not overlap
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_bad.rs:46:5: 46:37: error: in alias_array_bad/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_bad.rs:46:5: 46:37: error: in alias_array_bad/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_array_bad.rs:46:5:
 [Crux]   	0 < b[0].get()
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_bad.rs:47:5: 47:38: error: in alias_array_bad/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_bad.rs:47:5: 47:38: error: in alias_array_bad/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_array_bad.rs:47:5:
 [Crux]   	b[0].get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good b/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good
@@ -8,7 +8,7 @@ failures:
 [Crux]   test/symb_eval/comp/alias_array_bad2.rs:45:14: 45:16: error: in alias_array_bad2/<DISAMB>::use_f[0]
 [Crux]   references AllocIndex 0 and AllocIndex 1 must not overlap
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_bad2.rs:47:5: 47:38: error: in alias_array_bad2/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_bad2.rs:47:5: 47:38: error: in alias_array_bad2/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_array_bad2.rs:47:5:
 [Crux]   	b[0].get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good b/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good
@@ -5,7 +5,7 @@ failures:
 
 ---- alias_array_ok/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_ok.rs:48:5: 48:38: error: in alias_array_ok/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_ok.rs:48:5: 48:38: error: in alias_array_ok/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_array_ok.rs:48:5:
 [Crux]   	b[0].get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_bad.good b/crux-mir-comp/test/symb_eval/comp/alias_bad.good
@@ -8,11 +8,11 @@ failures:
 [Crux]   test/symb_eval/comp/alias_bad.rs:45:11: 45:13: error: in alias_bad/<DISAMB>::use_f[0]
 [Crux]   references AllocIndex 0 and AllocIndex 1 must not overlap
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_bad.rs:46:5: 46:34: error: in alias_bad/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_bad.rs:46:5: 46:34: error: in alias_bad/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_bad.rs:46:5:
 [Crux]   	0 < b.get()
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_bad.rs:47:5: 47:35: error: in alias_bad/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_bad.rs:47:5: 47:35: error: in alias_bad/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_bad.rs:47:5:
 [Crux]   	b.get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_ok.good b/crux-mir-comp/test/symb_eval/comp/alias_ok.good
@@ -5,7 +5,7 @@ failures:
 
 ---- alias_ok/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_ok.rs:49:5: 49:35: error: in alias_ok/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_ok.rs:49:5: 49:35: error: in alias_ok/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_ok.rs:49:5:
 [Crux]   	b.get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/override_test_indep.good b/crux-mir-comp/test/symb_eval/comp/override_test_indep.good
@@ -7,7 +7,7 @@ failures:
 
 ---- override_test_indep/<DISAMB>::use_f2[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/override_test_indep.rs:57:5: 57:29: error: in override_test_indep/<DISAMB>::use_f2[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/override_test_indep.rs:57:5: 57:29: error: in override_test_indep/<DISAMB>::use_f2[0]
 [Crux]   MIR assertion at test/symb_eval/comp/override_test_indep.rs:57:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/ptr_offset.good b/crux-mir-comp/test/symb_eval/comp/ptr_offset.good
@@ -5,7 +5,7 @@ failures:
 
 ---- ptr_offset/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/ptr_offset.rs:64:5: 64:30: error: in ptr_offset/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/ptr_offset.rs:64:5: 64:30: error: in ptr_offset/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/ptr_offset.rs:64:5:
 [Crux]   	b2 < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good b/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good
@@ -5,7 +5,7 @@ failures:
 
 ---- ptr_offset_rev/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/ptr_offset_rev.rs:64:5: 64:30: error: in ptr_offset_rev/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/ptr_offset_rev.rs:64:5: 64:30: error: in ptr_offset_rev/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/ptr_offset_rev.rs:64:5:
 [Crux]   	b2 < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_array.good b/crux-mir-comp/test/symb_eval/comp/spec_array.good
@@ -5,7 +5,7 @@ failures:
 
 ---- spec_array/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_array.rs:43:5: 43:29: error: in spec_array/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_array.rs:43:5: 43:29: error: in spec_array/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_array.rs:43:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_box.good b/crux-mir-comp/test/symb_eval/comp/spec_box.good
@@ -5,7 +5,7 @@ failures:
 
 ---- spec_box/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_box.rs:58:5: 58:29: error: in spec_box/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_box.rs:58:5: 58:29: error: in spec_box/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_box.rs:58:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good b/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good
@@ -5,7 +5,7 @@ failures:
 
 ---- spec_immut_cell/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_immut_cell.rs:68:5: 68:35: error: in spec_immut_cell/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_immut_cell.rs:68:5: 68:35: error: in spec_immut_cell/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_immut_cell.rs:68:5:
 [Crux]   	d.get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut.good b/crux-mir-comp/test/symb_eval/comp/spec_mut.good
@@ -5,7 +5,7 @@ failures:
 
 ---- spec_mut/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_mut.rs:61:5: 61:29: error: in spec_mut/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_mut.rs:61:5: 61:29: error: in spec_mut/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_mut.rs:61:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good
@@ -5,7 +5,7 @@ failures:
 
 ---- spec_mut_slice/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_mut_slice.rs:48:5: 48:29: error: in spec_mut_slice/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_mut_slice.rs:48:5: 48:29: error: in spec_mut_slice/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_mut_slice.rs:48:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_struct.good b/crux-mir-comp/test/symb_eval/comp/spec_struct.good
@@ -5,7 +5,7 @@ failures:
 
 ---- spec_struct/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_struct.rs:51:5: 51:29: error: in spec_struct/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_struct.rs:51:5: 51:29: error: in spec_struct/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_struct.rs:51:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_tuple.good b/crux-mir-comp/test/symb_eval/comp/spec_tuple.good
@@ -5,7 +5,7 @@ failures:
 
 ---- spec_tuple/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_tuple.rs:55:5: 55:29: error: in spec_tuple/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_tuple.rs:55:5: 55:29: error: in spec_tuple/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_tuple.rs:55:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/subst_output.good b/crux-mir-comp/test/symb_eval/comp/subst_output.good
@@ -4,7 +4,7 @@ failures:
 
 ---- subst_output/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/subst_output.rs:32:5: 32:30: error: in subst_output/<DISAMB>::use_f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/subst_output.rs:32:5: 32:30: error: in subst_output/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/subst_output.rs:32:5:
 [Crux]   	b0 == a
 
diff --git a/deps/mir-json b/deps/mir-json
@@ -1 +1 @@
-Subproject commit 64642a2a09eff6562df4fcc804ad00424deb442a
+Subproject commit 5b7cda1939637c6ea6e892a7301f5f94fb5010cd
diff --git a/doc/pdfs/rust-verification-with-saw.pdf b/doc/pdfs/rust-verification-with-saw.pdf
diff --git a/doc/pdfs/saw-user-manual.pdf b/doc/pdfs/saw-user-manual.pdf
diff --git a/doc/rust-verification-with-saw/about-mir-json.md b/doc/rust-verification-with-saw/about-mir-json.md
@@ -92,19 +92,16 @@ it is worthwhile to teach SAW the location of the custom libraries now.
 At present, the best way to obtain the custom version of the Rust standard
 libraries is to perform the following steps:
 
-1. Clone the [`crucible`](https://github.com/GaloisInc/crucible) repo like so:
+1. Clone the [`mir-json`](https://github.com/GaloisInc/mir-json) repo like so:
 
    :::{code-block} console
-   $ git clone https://github.com/GaloisInc/crucible
+   $ git clone https://github.com/GaloisInc/mir-json
+   $ cd mir-json
    :::
 
-2. Navigate to the
-   [`crux-mir`](https://github.com/GaloisInc/crucible/tree/master/crux-mir)
-   subdirectory of the `crucible` checkout:
-
-   :::{code-block} console
-   $ cd crucible/crux-mir/
-   :::
+2. 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`.
 
 3. Run the `translate_libs.sh` script:
 
@@ -119,7 +116,7 @@ libraries is to perform the following steps:
    to the newly created `rlibs` subdirectory:
 
    :::{code-block} console
-   $ export SAW_RUST_LIBRARY_PATH=<...>/crucible/crux-mir/rlibs
+   $ export SAW_RUST_LIBRARY_PATH=<...>/mir-json/rlibs
    :::
 
 An upcoming release of SAW will include these custom libraries pre-built, which
diff --git a/doc/saw-user-manual/loading-code.md b/doc/saw-user-manual/loading-code.md
@@ -154,15 +154,7 @@ following steps:
    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:
-
-   :::{code-block} console
-   $ cd ../crucible/crux-mir/
-   :::
-
-5. Run the `translate_libs.sh` script:
+4. Run the `translate_libs.sh` script in the `mir-json` submodule:
 
    :::{code-block} console
    $ ./translate_libs.sh
@@ -171,11 +163,11 @@ following steps:
    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
+5. Finally, define a `SAW_RUST_LIBRARY_PATH` environment variable that points
    to the newly created `rlibs` subdirectory:
 
    :::{code-block} console
-   $ export SAW_RUST_LIBRARY_PATH=<...>/crucible/crux-mir/rlibs
+   $ export SAW_RUST_LIBRARY_PATH=<...>/mir-json/rlibs
    :::
 
 For `cargo`-based projects, `mir-json` provides a `cargo` subcommand called
diff --git a/doc/scripts/epoch.mk b/doc/scripts/epoch.mk
@@ -24,6 +24,6 @@
 #    - the devel version can then be bumped to the current day if needed
 #
 
-# BSD/Linux: date +%s -d "04/03/2025 00:00:00 GMT"
-# OSX: date -j -f "%m/%d/%Y %H:%M:%S %Z" "4/3/2025 00:00:00 GMT" +%s
-SOURCE_DATE_EPOCH=1743638400
+# BSD/Linux: date +%s -d "04/04/2025 00:00:00 GMT"
+# OSX: date -j -f "%m/%d/%Y %H:%M:%S %Z" "4/4/2025 00:00:00 GMT" +%s
+SOURCE_DATE_EPOCH=1743724800
