search

GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
628 stars 42 forks source link

`crux-mir`: Support cross-compiling libs to `wasm32` target #1147

Closed qsctr closed 9 months ago

qsctr commented 9 months ago
qsctr commented 9 months ago

Hmm it seems like there is a reference to an apparently now-nonexistent flag --no-model-internal-atomics for translate_libs.sh here. I should do something to prevent people from using it and it getting treated as a target triple by the script, but I'm not sure what is the right thing to do (add the flag back to translate_libs.sh? just delete that part of the docs? something else?)

RyanGlScott commented 9 months ago

Bummer, I completely missed that --no-model-internal-atomics flag when I worked on https://github.com/GaloisInc/crucible/pull/1096. I doubt that it would be a small amount of work to add back to crux-mir, so I have opened https://github.com/GaloisInc/crucible/issues/1148 as a reminder to do this at some point in the future. As such, I don't think we need to block this PR on that front, although it would be worth setting translate_libs.sh up in such a way that we can pass multiple configuration-related arguments to the script. I'm not strongly opinionated on the best way to do this—perhaps via environment variables? getopt? Something else?

qsctr commented 9 months ago

although I would request that you add some additional documentation so that when we next update the rustc toolchain that crux-mir supports, we have some reminders about why dlmalloc needs to be included.

What's the best place to put this? Is the comment in translate_libs.sh enough? I'm not sure I should put it in lib/Patches.md since there are no patches.

qsctr commented 9 months ago

Also, should we test a wasm32-unknown-unknown build in CI?

RyanGlScott commented 9 months ago

What's the best place to put this? Is the comment in translate_libs.sh enough?

Short answer: Yes, I think that is likely good enough for now.

Long answer: The translate_libs.sh script was originally created by using a Python script that @m10f wrote to scrape the dependencies from the standard libraries' Cargo.toml files and generate the necessary calls to mir-json. After creating the initial version of the script, however, we quickly discovered many manual tweaks that were necessary to address various corner cases, make certain test cases work, etc. It got to the point that the final version of translate_libs.sh was quite different from what the script produced.

Ultimately, we never checked in the generator script, but I kind of wish that we did, since that script would be a good place to document things such as the inclusion of dlmalloc. After all, when we upgrade crux-mir to support a new rustc toolchain, it is quite possible that the dependencies will change slightly, at which point we will have to change (or rewrite) translate_libs.sh to accommodate it. Of course, we should make sure to look at the old version of translate_libs.sh to preserve what it did before, but it is easy to overlook things (as evidenced by https://github.com/GaloisInc/crucible/issues/1148). I'd hate to accidentally drop dlmalloc from translate_libs.sh because of such an oversight.

If we had a proper generator script that documented all of these quirks, I think the likelihood of dropping dlmalloc in the future would be greatly reduced. We could also build a cross-compiled version of crux-mir in the CI, which brings me to your other question...

RyanGlScott commented 9 months ago

Also, should we test a wasm32-unknown-unknown build in CI?

Perhaps so, although I wonder how much we should actually do. For instance, have you run the crux-mir test suite using a Wasm version of the Rust standard libraries? Do all the tests pass? If they don't pass, then unless you want to spend the time fixing up all of the test cases, then we wouldn't be able to run everything in CI with a Wasm target triple. In that scenario, we could conceivably do something like making sure that the Rust standard libraries build, but refrain from doing anything else.

qsctr commented 9 months ago

I don't think it's easy to run the test suite with wasm32, since it seems to use the binary output of rustc as an oracle, which would mean we need to run it in a wasm VM. In any case I don't think there is much runtime (rather than compile time) differences in behavior between targets that might be caused by some bug in crux-mir, so I was more thinking of just making sure TARGET=wasm32-unknown-unknown ./translate_libs.sh runs successfully.

RyanGlScott commented 9 months ago

OK. In that case, I agree that a simple CI action that simply runs TARGET=wasm32-unknown-unknown ./translate_libs.sh would be appropriate. Would you be willing to open an issue as a a reminder to do this?