diff --git a/simulator/run-miri.sh b/simulator/run-miri.sh new file mode 100755 index 000000000..e065f3c68 --- /dev/null +++ b/simulator/run-miri.sh @@ -0,0 +1,31 @@ +#!/bin/bash + +ARGS=("$@") + +# Intercept the seed if it's passed +while [[ $# -gt 0 ]]; do + case $1 in + -s=*|--seed=*) + seed="${1#*=}" + shift + ;; + -s|--seed) + seed="$2" + shift 2 + ;; + *) + shift + ;; + esac +done +# Otherwise make one up +if [ -z "$seed" ]; then + # Dump 8 bytes of /dev/random as decimal u64 + seed=$(od -An -N8 -tu8 /dev/random | tr -d ' ') + ARGS+=("--seed" "${seed}") + echo "Generated seed for Miri and simulator: ${seed}" +else + echo "Intercepted simulator seed to pass to Miri: ${seed}" +fi + +MIRIFLAGS="-Zmiri-disable-isolation -Zmiri-disable-stacked-borrows -Zmiri-seed=${seed}" cargo +nightly miri run --bin limbo_sim -- "${ARGS[@]}" diff --git a/simulator/runner/cli.rs b/simulator/runner/cli.rs index 8a941dde1..97062dd2d 100644 --- a/simulator/runner/cli.rs +++ b/simulator/runner/cli.rs @@ -30,7 +30,7 @@ pub struct SimulatorCLI { short = 'n', long, help = "change the maximum size of the randomly generated sequence of interactions", - default_value_t = 5000, + default_value_t = normal_or_miri(5000, 50), value_parser = clap::value_parser!(u32).range(1..) )] pub maximum_tests: u32, @@ -38,7 +38,7 @@ pub struct SimulatorCLI { short = 'k', long, help = "change the minimum size of the randomly generated sequence of interactions", - default_value_t = 1000, + default_value_t = normal_or_miri(1000, 10), value_parser = clap::value_parser!(u32).range(1..) )] pub minimum_tests: u32, @@ -149,7 +149,8 @@ pub struct SimulatorCLI { pub keep_files: bool, #[clap( long, - help = "Disable the SQLite integrity check at the end of a simulation" + help = "Disable the SQLite integrity check at the end of a simulation", + default_value_t = normal_or_miri(false, true) )] pub disable_integrity_check: bool, #[clap( @@ -279,3 +280,7 @@ impl ValueParserFactory for ProfileType { ProfileTypeParser } } + +const fn normal_or_miri(normal_val: T, miri_val: T) -> T { + if cfg!(miri) { miri_val } else { normal_val } +} diff --git a/stress/opts.rs b/stress/opts.rs index 796f85847..aac93f67d 100644 --- a/stress/opts.rs +++ b/stress/opts.rs @@ -21,7 +21,7 @@ pub struct Opts { short = 'i', long, help = "the number of iterations", - default_value_t = 100000 + default_value_t = normal_or_miri(100_000, 1000) )] pub nr_iterations: usize, @@ -75,3 +75,11 @@ pub struct Opts { )] pub busy_timeout: u64, } + +const fn normal_or_miri(normal_val: T, miri_val: T) -> T { + if cfg!(miri) { + miri_val + } else { + normal_val + } +} diff --git a/stress/run-miri.sh b/stress/run-miri.sh new file mode 100755 index 000000000..2de0069e5 --- /dev/null +++ b/stress/run-miri.sh @@ -0,0 +1,4 @@ +#!/bin/bash + + +MIRIFLAGS="-Zmiri-disable-isolation -Zmiri-disable-stacked-borrows" cargo +nightly miri run -p turso_stress -- "$@"