search

GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
683 stars 44 forks source link

Maintain modified Rust standard libraries and `translate_libs.sh` in a separate repo #1252

Open RyanGlScott opened 2 months ago

RyanGlScott commented 2 months ago

Currently, we vendor in our modified copies of the Rust standard libraries (as well as the associated translate_libs.sh script, which runs mir-json on these modified standard libraries to compile them) as a subdirectory in crux-mir. Historically, this made sense, as crux-mir was the sole consumer of these files. It is unclear if this arrangement makes as much sense nowadays, however, for the following reasons:

  1. Both crux-mir and SAW (the latter of which now has a MIR backend) need to make use of translate_libs.sh. Telling SAW users to download crux-mir for the sole purpose of running translate_libs.sh doesn't make much sense, given that crux-mir is otherwise unrelated to SAW.
  2. The vendored-in copies of the Rust standard libraries are actually quite large (on the order of several megabytes), which substantially increases the amount of time it takes to clone the crucible repo. This is a bit of a shame, considering that many crucible developers aren't going to be using the MIR-related parts.

To address both of these concerns, I propose that we factor out the modified Rust standard libraries (and translate_libs.sh) into a separate repo. I'll tentatively call this repo "mir-json-libs" until I can think of something better. That way, mir-json-libs development can live outside of crucible (thereby avoiding further bloating of the crucible repo), and there is now a central location for further standard library modifications needed to support crux-mir and SAW.

sauclovian-g commented 2 months ago

Won't it still need to be a submodule of crucible (or at least want to be, for the same reasons we just added mir-json in saw)? That kind of defeats point 2. Not that this matters, since point 1 is ample reason to do this :-)

RyanGlScott commented 2 months ago

Won't it still need to be a submodule of crucible (or at least want to be, for the same reasons we just added mir-json in saw)? That kind of defeats point 2.

Yes, that is fair. Let me revise point (2), then: one disadvantage of versioning the crux-mir standard libraries in the same repo as crucible is that the git history for the crux-mir standard libraries is very large and messy, and it would be better to keep it as separate as possible. (For an example of what I'm taking about, check out the sheer number of commits from the last time we updated these standard libraries: https://github.com/GaloisInc/mir-json/pull/49)

sauclovian-g commented 2 months ago

Oof. point taken 😀