mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

make miri-seed a regular integer, and also set layout-seed in many-seeds

Browse Source
This commit is contained in:
Ralf Jung 2022-11-20 09:38:02 +01:00
parent 0a9e5e8e81
commit 772d521616
4 changed files with 8 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/tools/miri/README.md
View File

@ -195,7 +195,7 @@ randomness that is used to determine allocation base addresses. The following
snippet calls Miri in a loop with different values for the seed: snippet calls Miri in a loop with different values for the seed:
``` ```
for SEED in $({ echo obase=16; seq 0 255; } | bc); do for SEED in $(seq 0 255); do
echo "Trying seed: $SEED" echo "Trying seed: $SEED"
MIRIFLAGS=-Zmiri-seed=$SEED cargo miri test || { echo "Failing seed: $SEED"; break; }; MIRIFLAGS=-Zmiri-seed=$SEED cargo miri test || { echo "Failing seed: $SEED"; break; };
done done
@ -303,7 +303,7 @@ environment variable. We first document the most relevant and most commonly used
tell what it is doing when a program just keeps running. You can customize how frequently the tell what it is doing when a program just keeps running. You can customize how frequently the
report is printed via `-Zmiri-report-progress=<blocks>`, which prints the report every N basic report is printed via `-Zmiri-report-progress=<blocks>`, which prints the report every N basic
blocks. blocks.
* `-Zmiri-seed=<hex>` configures the seed of the RNG that Miri uses to resolve non-determinism. This * `-Zmiri-seed=<num>` configures the seed of the RNG that Miri uses to resolve non-determinism. This
RNG is used to pick base addresses for allocations, to determine preemption and failure of RNG is used to pick base addresses for allocations, to determine preemption and failure of
`compare_exchange_weak`, and to control store buffering for weak memory emulation. When isolation `compare_exchange_weak`, and to control store buffering for weak memory emulation. When isolation
is enabled (the default), this is also used to emulate system entropy. The default seed is 0. You is enabled (the default), this is also used to emulate system entropy. The default seed is 0. You

4
src/tools/miri/miri
View File

@ -174,9 +174,9 @@ rustc-push)
fi fi
;; ;;
many-seeds) many-seeds)
for SEED in $({ echo obase=16; seq 0 255; } | bc); do for SEED in $(seq 0 255); do
echo "Trying seed: $SEED" echo "Trying seed: $SEED"
MIRIFLAGS="$MIRIFLAGS -Zmiri-seed=$SEED" $@ || { echo "Failing seed: $SEED"; break; } MIRIFLAGS="$MIRIFLAGS -Zlayout-seed=$SEED -Zmiri-seed=$SEED" $@ || { echo "Failing seed: $SEED"; break; }
done done
exit 0 exit 0
;; ;;

7
src/tools/miri/src/bin/miri.rs
View File

@ -394,10 +394,9 @@ fn main() {
if miri_config.seed.is_some() { if miri_config.seed.is_some() {
show_error!("Cannot specify -Zmiri-seed multiple times!"); show_error!("Cannot specify -Zmiri-seed multiple times!");
} }
let seed = u64::from_str_radix(param, 16) let seed = param.parse::<u64>().unwrap_or_else(|_| {
.unwrap_or_else(|_| show_error!( show_error!("-Zmiri-seed must be an integer that fits into u64")
"-Zmiri-seed should only contain valid hex digits [0-9a-fA-F] and must fit into a u64 (max 16 characters)" });
));
miri_config.seed = Some(seed); miri_config.seed = Some(seed);
} else if let Some(_param) = arg.strip_prefix("-Zmiri-env-exclude=") { } else if let Some(_param) = arg.strip_prefix("-Zmiri-env-exclude=") {
show_error!( show_error!(

2
src/tools/miri/test-cargo-miri/run-test.py
View File

@ -133,7 +133,7 @@ def test_cargo_miri_test():
test("`cargo miri test`", test("`cargo miri test`",
cargo_miri("test"), cargo_miri("test"),
default_ref, "test.stderr-empty.ref", default_ref, "test.stderr-empty.ref",
env={'MIRIFLAGS': "-Zmiri-permissive-provenance -Zmiri-seed=feed"}, env={'MIRIFLAGS': "-Zmiri-permissive-provenance -Zmiri-seed=4242"},
) )
test("`cargo miri test` (no isolation, no doctests)", test("`cargo miri test` (no isolation, no doctests)",
cargo_miri("test") + ["--bins", "--tests"], # no `--lib`, we disabled that in `Cargo.toml` cargo_miri("test") + ["--bins", "--tests"], # no `--lib`, we disabled that in `Cargo.toml`