Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cargo saw-build/saw-rustc: Don't generate crux-mir-related test script #84

Open
RyanGlScott opened this issue Feb 28, 2025 · 2 comments
Labels

Comments

@RyanGlScott
Copy link
Contributor

Currently, if you compile code with the cargo saw-build or saw-rustc commands, then it will generate a test script with the following contents:

#!/bin/sh
exec "${CRUX_MIR:-crux-mir}" --assert-false-on-error --cargo-test-file "$(dirname "$0")"/'$CRATE_NAME.linked-mir.json' "$@"

This is silly to do in the context of cargo saw-build/saw-rustc, however, as these commands aren't meant to be used in conjunction with crux-mir. We should suppress generating this script when using these commands.

@spernsteiner
Copy link
Collaborator

Does saw-rustc always emit this, or only when run with saw-rustc --test? My vague recollection of the way it was supposed to work for crux was that cargo crux-test runs RUSTC_WRAPPER=... cargo test, and the final build step invokes rustc (actually mir-json) with the --test flag, which causes mir-json to emit the test script. So I would expect saw-rustc to emit the script only when passed --test.

As for cargo saw-build, if it's currently using cargo test (like cargo crux-test does), it might be better to switch it to cargo build.

@RyanGlScott
Copy link
Contributor Author

saw-rustc always emits this, as saw-rustc always passes --test to the underlying rustc invocation. In fact, if you try to run saw-rustc --test, it fails:

$ SAW_RUST_LIBRARY_PATH=$(pwd)/../../Haskell/crucible/crux-mir/rlibs saw-rustc --test hello_world.rs
test build - extract output path - ["rustc", "--test", "hello_world.rs", "--test", "--target", "x86_64-unknown-linux-gnu", "--cfg", "crux", "-L", "/home/ryanscott/Documents/Hacking/Rust/hello-world/../../Haskell/crucible/crux-mir/rlibs", "--sysroot", "/home/ryanscott/Documents/Hacking/Rust/hello-world/../../Haskell/crucible/crux-mir/rlibs"]
error: Option 'test' given more than once

And indeed, cargo saw-build uses cargo test currently, just like cargo crux-test.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants