Migrate modified Rust standard libraries to mir-json

RyanGlScott · RyanGlScott · commit a2bc5dc0f105 · 2025-03-26T12:37:43.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/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/crucible b/deps/crucible
@@ -1 +1 @@
-Subproject commit 278e009659864b907b8144e12b9fe4ec656cd132
+Subproject commit 5bdbe074e5bde207433449753f39f40c9fe9f5f9
diff --git a/deps/mir-json b/deps/mir-json
@@ -1 +1 @@
-Subproject commit 64642a2a09eff6562df4fcc804ad00424deb442a
+Subproject commit b551a32c713739e8087c955b6d46202530b45063
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
