crux-mir: Adjust documentation, CI, and test suite in light of standard library migration

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), this patch adjusts the various
references to the standard libraries to ensure that `crux-mir`'s documentation,
CI, and test suite remain up to date.

Towards #1252

Author: RyanGlScott

.github/Dockerfile-crux-mir

@@ -39,7 +39,9 @@ ENV LANG=C.UTF-8 \
 WORKDIR ${CRUX_BUILD_DIR}/dependencies/mir-json
 RUN curl https://sh.rustup.rs -sSf | bash -s -- -y --profile minimal --default-toolchain ${RUST_TOOLCHAIN}
 RUN rustup component add --toolchain ${RUST_TOOLCHAIN} rustc-dev
-RUN cargo install --locked
+RUN cargo install --locked && \
+    ./translate_libs.sh
+ENV CRUX_RUST_LIBRARY_PATH=$(pwd)/rlibs
 
 RUN mkdir -p /crux-mir/rootfs/usr/local/bin
 WORKDIR /crux-mir/rootfs/usr/local/bin
@@ -59,8 +61,6 @@ RUN mkdir -p /home/crux-mir/.ghcup && \
     ghcup install ghc 9.4.8 && \
     ghcup set ghc 9.4.8
 
-WORKDIR ${CRUX_BUILD_DIR}/crux-mir
-RUN ./translate_libs.sh
 WORKDIR ${CRUX_BUILD_DIR}
 RUN cabal v2-update && \
     cabal v2-build --only-dependencies crux-mir && \
@@ -82,7 +82,7 @@ RUN apt-get update && \
 COPY --from=build /home/crux-mir/.cargo/bin /home/crux-mir/.cargo/bin
 COPY --from=build /home/crux-mir/.rustup /home/crux-mir/.rustup
 COPY --from=build /crux-mir/rootfs /
-COPY --from=build ${CRUX_BUILD_DIR}/crux-mir/rlibs /crux-mir/rlibs
+COPY --from=build ${CRUX_BUILD_DIR}/dependencies/mir-json/rlibs /crux-mir/rlibs
 
 RUN useradd -m crux-mir && chown -R crux-mir:crux-mir /crux-mir /home/crux-mir
 USER crux-mir

.github/workflows/crux-mir-build.yml

@@ -168,8 +168,13 @@ jobs:
           with_ghc()  { $NS -c ${@}; }
           (cd crux-mir;      with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
 
-      - shell: bash
-        run: cd dependencies/mir-json && cargo install --locked --force
+      - name: Install mir-json
+        shell: bash
+        working-directory: dependencies/mir-json
+        run: |
+          cargo install --locked --force
+          bash ./translate_libs.sh
+          echo "CRUX_RUST_LIBRARY_PATH=$(pwd)/rlibs" >> $GITHUB_ENV
 
       - shell: bash
         run: .github/ci.sh configure
@@ -185,9 +190,6 @@ jobs:
         name: Haddock
         run: cabal v2-haddock crucible-syntax crucible-concurrency crux-mir
 
-      - shell: bash
-        run: cd crux-mir && bash ./translate_libs.sh
-
       - shell: bash
         run: .github/ci.sh test crux-mir
 

crux-mir/README.md

@@ -15,9 +15,10 @@ functionality.
 
     $ git submodule update --init
 
-Next, navigate to the `crucible/dependencies/mir-json` directory and install
-`mir-json` according to the instructions in [the `mir-json`
-README][mir-json-readme].
+Next, navigate to the `crucible/dependencies/mir-json` directory. Install
+`mir-json`, translate its standard libraries, and define the
+`CRUX_RUST_LIBRARY_PATH` environment variable according to the instructions in
+[the `mir-json` README][mir-json-readme].
 
 Currently, `crux-mir` supports [version
 1](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#1) of
@@ -44,21 +45,6 @@ Use GHC 9.4, 9.6, or 9.8. From the `crux-mir` directory, run:
 
     $ cabal v2-install exe:crux-mir --overwrite-policy=always
 
-Then translate the Rust libraries in `lib/`:
-
-    $ ./translate_libs.sh
-
-If you want to cross-compile for a different target, you can optionally set the
-environment variable `TARGET` to a [target
-triple](https://doc.rust-lang.org/nightly/rustc/platform-support.html) when
-running `./translate_libs.sh`. This is experimental and we have only tested
-`wasm32-unknown-unknown` to work; you might get build errors for other targets.
-
-    $ TARGET=wasm32-unknown-unknown ./translate_libs.sh
-
-When upgrading from a previous version, first install the new `mir-json`
-version, then rerun the `cabal v2-install` and `./translate_libs.sh` commands.
-
 
 ## Usage
 
@@ -71,8 +57,8 @@ compiled by checking for the `crux` configuration predicate using
 `#[cfg_attr(crux, crux::test)]`.
 
 Test cases can create and manipulate symbolic values using the functions in the
-[`crucible`](lib/crucible) Rust crate.  See
-[`example/ffs/lib.rs`](example/ffs/lib.rs) or the files in
+[`crucible`](https://github.com/GaloisInc/mir-json/tree/master/libs/crucible)
+Rust crate.  See [`example/ffs/lib.rs`](example/ffs/lib.rs) or the files in
 [`test/symb_eval/`](test/symb_eval) for examples of creating symbolic values
 and asserting properties about them.
 

crux-mir/test/symb_eval/concretize/assert.good

@@ -4,7 +4,7 @@ failures:
 
 ---- assert/<DISAMB>::crux_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:48:17: 48:82 !test/symb_eval/concretize/assert.rs:10:5: 10:81: error: in assert/<DISAMB>::crux_test[0]
+[Crux]   ./libs/crucible/lib.rs:48:17: 48:82 !test/symb_eval/concretize/assert.rs:10:5: 10:81: error: in assert/<DISAMB>::crux_test[0]
 [Crux]   MIR assertion at test/symb_eval/concretize/assert.rs:10:5:
 [Crux]   	100 + 157 == 1
 

crux-mir/test/symb_eval/crux/early_fail.good

@@ -10,7 +10,7 @@ failures:
 
 ---- early_fail/<DISAMB>::fail2[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/early_fail.rs:17:5: 17:29: error: in early_fail/<DISAMB>::fail2[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/early_fail.rs:17:5: 17:29: error: in early_fail/<DISAMB>::fail2[0]
 [Crux]   MIR assertion at test/symb_eval/crux/early_fail.rs:17:5:
 [Crux]   	x == 0
 

crux-mir/test/symb_eval/crux/fail_return.good

@@ -8,7 +8,7 @@ failures:
 [Crux]   test/symb_eval/crux/fail_return.rs:8:22: 8:27: error: in fail_return/<DISAMB>::fail1[0]
 [Crux]   attempt to compute `move _4 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/fail_return.rs:8:5: 8:32: error: in fail_return/<DISAMB>::fail1[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/fail_return.rs:8:5: 8:32: error: in fail_return/<DISAMB>::fail1[0]
 [Crux]   MIR assertion at test/symb_eval/crux/fail_return.rs:8:5:
 [Crux]   	x + 1 > x
 
@@ -17,7 +17,7 @@ failures:
 [Crux]   test/symb_eval/crux/fail_return.rs:15:22: 15:27: error: in fail_return/<DISAMB>::fail2[0]
 [Crux]   attempt to compute `move _5 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/fail_return.rs:15:5: 15:32: error: in fail_return/<DISAMB>::fail2[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/fail_return.rs:15:5: 15:32: error: in fail_return/<DISAMB>::fail2[0]
 [Crux]   MIR assertion at test/symb_eval/crux/fail_return.rs:15:5:
 [Crux]   	x + 1 > x
 

crux-mir/test/symb_eval/crux/mixed_fail.good

@@ -10,7 +10,7 @@ failures:
 [Crux]   test/symb_eval/crux/mixed_fail.rs:8:22: 8:27: error: in mixed_fail/<DISAMB>::fail1[0]
 [Crux]   attempt to compute `move _5 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/mixed_fail.rs:8:5: 8:32: error: in mixed_fail/<DISAMB>::fail1[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/mixed_fail.rs:8:5: 8:32: error: in mixed_fail/<DISAMB>::fail1[0]
 [Crux]   MIR assertion at test/symb_eval/crux/mixed_fail.rs:8:5:
 [Crux]   	x + 1 > x
 
@@ -19,7 +19,7 @@ failures:
 [Crux]   test/symb_eval/crux/mixed_fail.rs:14:22: 14:27: error: in mixed_fail/<DISAMB>::fail2[0]
 [Crux]   attempt to compute `move _5 + const 2_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/mixed_fail.rs:14:5: 14:32: error: in mixed_fail/<DISAMB>::fail2[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/mixed_fail.rs:14:5: 14:32: error: in mixed_fail/<DISAMB>::fail2[0]
 [Crux]   MIR assertion at test/symb_eval/crux/mixed_fail.rs:14:5:
 [Crux]   	x + 2 > x
 

crux-mir/test/symb_eval/crux/multi.good

@@ -9,7 +9,7 @@ failures:
 [Crux]   test/symb_eval/crux/multi.rs:8:22: 8:27: error: in multi/<DISAMB>::fail1[0]
 [Crux]   attempt to compute `move _5 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/multi.rs:8:5: 8:32: error: in multi/<DISAMB>::fail1[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/multi.rs:8:5: 8:32: error: in multi/<DISAMB>::fail1[0]
 [Crux]   MIR assertion at test/symb_eval/crux/multi.rs:8:5:
 [Crux]   	x + 1 > x
 
@@ -20,7 +20,7 @@ failures:
 
 ---- multi/<DISAMB>::fail3[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/multi.rs:20:5: 20:29: error: in multi/<DISAMB>::assert_zero[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/multi.rs:20:5: 20:29: error: in multi/<DISAMB>::assert_zero[0]
 [Crux]   MIR assertion at test/symb_eval/crux/multi.rs:20:5:
 [Crux]   	x == 0
 

crux-mir/test/symb_eval/crypto/bytes.good

@@ -4,23 +4,23 @@ failures:
 
 ---- bytes/<DISAMB>::f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/<DISAMB>::f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/<DISAMB>::f[0]
 [Crux]   MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 [Crux]   	a[i] == b[i]
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/<DISAMB>::f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/<DISAMB>::f[0]
 [Crux]   MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 [Crux]   	a[i] == b[i]
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/<DISAMB>::f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/<DISAMB>::f[0]
 [Crux]   MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 [Crux]   	a[i] == b[i]
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/<DISAMB>::f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/<DISAMB>::f[0]
 [Crux]   MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 [Crux]   	a[i] == b[i]
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/<DISAMB>::f[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/<DISAMB>::f[0]
 [Crux]   MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 [Crux]   	a[i] == b[i]
 

crux-mir/test/symb_eval/overrides/bad_symb1.good

@@ -4,7 +4,7 @@ failures:
 
 ---- bad_symb1/<DISAMB>::crux_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   lib/crucible/symbolic.rs:24:64: 24:68 !lib/crucible/symbolic.rs:30:1: 36:2: error: in crucible/<DISAMB>::symbolic[0]::{impl#1}[0]::symbolic[0]
+[Crux]   libs/crucible/symbolic.rs:24:64: 24:68 !libs/crucible/symbolic.rs:30:1: 36:2: error: in crucible/<DISAMB>::symbolic[0]::{impl#1}[0]::symbolic[0]
 [Crux]   symbolic variable name must be a concrete string
 
 [Crux] Overall status: Invalid.