Migrate modified Rust standard libraries from `crucible` to `mir-json` #85

RyanGlScott · 2025-03-07T18:42:35Z

This merges the commit history of crucible's crux-mir/lib directory (which contains the modified versions of the Rust standard libraries that mir-json uses) and crux-mir/translate_libs.sh script (which compiles the standard libraries using mir-json) into the mir-json repo. I have rewritten the commit history to locate these at libs/ and translate_libs.sh, respectively. I performed this commit rewrite using the following git-filter-repo invocation:

$ git-filter-repo --path crux-mir/lib --path-rename crux-mir/lib:libs --path crux-mir/translate_libs.sh --path-rename crux-mir/translate_libs.sh:translate_libs.sh --refs refs/heads/filter-source --force

Only the two last commits in this PR updates are of real interest to reviewers (all other commits are churn induced by moving files from crucible over to this repo.):

The second-to-last commit updates the mir-json documentation to describe libs/ and translate_libs.sh.
The last commit updates the CI to call translate_libs.sh and package up the results in the uploaded artifacts.

This is one half of a fix for GaloisInc/crucible#1252.

These have been moved to `mir-json` as part of GaloisInc/mir-json#85. Towards #1252

…gration 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 and CI remain up to date. Towards #1252

spernsteiner · 2025-03-07T20:01:05Z

I'm a little skeptical about this move - I think the patches to the libraries are more closely tied to what crucible-mir can handle than to anything in mir-json. When trying to get a new library feature working in crux-mir, IIRC it was common to do some parts as library patches and some parts as new crucible-mir intrinsics/overrides, but it was very rare to need to change mir-json.

RyanGlScott · 2025-03-07T20:05:30Z

Per GaloisInc/crucible#1252 (comment), I'm not a fan of housing the libraries under crux-mir, as I don't think this location makes sense now that the libraries are used by multiple tools (crux-mir and SAW). Moreover, as noted in GaloisInc/crucible#1252 (comment), putting the libraries in the mir-json repo has the secondary benefit of streamlining installation for users, as mir-json needs to have a standard library installation present in order to be useful. (It also greatly simplifies the CI and Docker stories, although those are less convincing arguments.)

While I could be convinced to house the files somewhere besides mir-json, I really don't think that they should be under crux-mir/lib. Do you have an alternative suggestion?

These have been moved to `mir-json` as part of GaloisInc/mir-json#85. Towards #1252

…rd 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

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.

RyanGlScott · 2025-03-10T22:43:53Z

I spoke to @spernsteiner offline about this, and we came to an agreement to proceed with the plan in this PR. There are tradeoffs regardless of which repo we house these standard libraries in (for instance, housing them in mir-json has the disadvantage of coupling mir-json and crucible-mir development a bit more tightly), but I do think the pros outweigh the cons.

…rd 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

These have been moved to `mir-json` as part of GaloisInc/mir-json#85. Towards #1252

…rd 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

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.

README.md

We don't currently specify what happens if both `CRUX_RUST_LIBRARY_PATH` and `SAW_RUST_LIBRARY_PATH` are defined but set to different values (in reality, `CRUX_RUST_LIBRARY_PATH` always takes precedence), but people might think that they can use different paths for Crux and SAW. So maybe we should just say "one of".

These have been moved to `mir-json` as part of GaloisInc/mir-json#85. Towards #1252

…rd 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

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.

spernsteiner added 30 commits August 8, 2019 17:39

update some overrides + tests to work with crate names

34847af

update symbolic test cases to use external libcrucible

106c318

start adding libstd stubs

a0faf1a

add libcore + stdarch sources from rustc d3f8a0b (nightly-2019-08-04)

624d61b

add #[cfg] attrs to disable nonessential parts of libcore

241f74b

libcore: add fmt_min, a copy of fmt

63cb2c9

remove implementation code from fmt_min

fe1022d

create stripped-down str_min module

7a3fd6c

#[cfg] out a few more bits of libcore

74781ff

replace hash with stripped-down hash_min

c6ebdb0

remove implementation code from core::fmt::float

3b2edc5

libcore: disable Any::downcast_{ref,mut}

13d0d74

add libcompiler_builtins stub

08ad4bc

some progress on running the old scalar test

4591a07

libcore: avoid a usize->i32 cast (currently unsupported) in Range::next

ea487f0

fix up overrides for slice::get_unchecked variants

a8957ed

support iterating over slices

7ea609f

add cursor_read test case & get it working

0616df6

add a shell script for translating all the libraries

39f49aa

add byteorder library, v1.3.2 (0582376)

0b3a96f

crucible-friendly implementations of byteorder functions

c33ab04

fix existing io & byteorder tests; add some new ones

2203e96

fix translate_libs.sh

e0c2419

add std::io::Sink; add Vec and Bytes/BytesMut stubs

1bd63db

stubs for more Bytes/BytesMut APIs

cdc7ff1

more stubs and trait impls for Bytes, BytesMut, and Vec

d9f5a2d

more Vec and BufMut stubs

972dfea

Bytes and Vec iterator stubs

8ca5c53

bytes: impl BufMut for &mut T where T: BufMut

094fc7e

full implementation of bytes::Writer

33a3be4

RyanGlScott force-pushed the crucible-T1252-merge-std-libs branch from 181402b to 3f91f8c Compare March 7, 2025 19:17

RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Mar 7, 2025

Remove crux-mir/lib and crux-mir/translate_libs.sh

11b7ec9

These have been moved to `mir-json` as part of GaloisInc/mir-json#85. Towards #1252

RyanGlScott mentioned this pull request Mar 7, 2025

crux-mir: Migrate modified Rust standard libraries to mir-json GaloisInc/crucible#1319

Merged

RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Mar 10, 2025

Remove crux-mir/lib and crux-mir/translate_libs.sh

83071d8

These have been moved to `mir-json` as part of GaloisInc/mir-json#85. Towards #1252

RyanGlScott mentioned this pull request Mar 10, 2025

Migrate modified Rust standard libraries to mir-json GaloisInc/saw-script#2249

Merged

qsctr mentioned this pull request Mar 11, 2025

Require {CRUX,SAW}_RUST_LIBRARY_PATH or MIR_JSON_USE_RUSTC_LIBRARY #86

Merged

RyanGlScott marked this pull request as ready for review March 26, 2025 16:29

Merge branch 'master' into crucible-T1252-merge-std-libs

b551a32

RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Mar 26, 2025

Remove crux-mir/lib and crux-mir/translate_libs.sh

26d4bdf

These have been moved to `mir-json` as part of GaloisInc/mir-json#85. Towards #1252

RyanGlScott requested review from qsctr and spernsteiner March 26, 2025 18:34

qsctr reviewed Mar 26, 2025

View reviewed changes

README.md Outdated Show resolved Hide resolved

qsctr approved these changes Mar 27, 2025

View reviewed changes

RyanGlScott merged commit 5b7cda1 into master Mar 27, 2025
3 checks passed

RyanGlScott deleted the crucible-T1252-merge-std-libs branch March 27, 2025 17:56

RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Mar 27, 2025

Remove crux-mir/lib and crux-mir/translate_libs.sh

c7437a3

These have been moved to `mir-json` as part of GaloisInc/mir-json#85. Towards #1252

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Migrate modified Rust standard libraries from `crucible` to `mir-json` #85

Migrate modified Rust standard libraries from `crucible` to `mir-json` #85

Uh oh!

RyanGlScott commented Mar 7, 2025 •

edited

Loading

Uh oh!

spernsteiner commented Mar 7, 2025

Uh oh!

RyanGlScott commented Mar 7, 2025 •

edited

Loading

Uh oh!

RyanGlScott commented Mar 10, 2025

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

Migrate modified Rust standard libraries from crucible to mir-json #85

Migrate modified Rust standard libraries from crucible to mir-json #85

Uh oh!

Conversation

RyanGlScott commented Mar 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

spernsteiner commented Mar 7, 2025

Uh oh!

RyanGlScott commented Mar 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

RyanGlScott commented Mar 10, 2025

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

Migrate modified Rust standard libraries from `crucible` to `mir-json` #85

Migrate modified Rust standard libraries from `crucible` to `mir-json` #85

RyanGlScott commented Mar 7, 2025 •

edited

Loading

RyanGlScott commented Mar 7, 2025 •

edited

Loading