How to run proptest within MIRI?

[jorgecarleitao]

For context, I would like the tests ran in proptest to run under MIRI, but MIRI does not accept getcwd in isolation mode (which we require in our tests).

Running results in

error: unsupported operation: getcwd not available when isolation is enabled

Full log here.

[matthew-russo]

Thanks for reporting this. This is due to proptest's failure persistence which tries to load a failure persistence file to detect seeds of previous failed runs. proptest does allow you disable this, after which proptest will run under MIRI without issue.

There are a few options for disabling proptest which I'll show using the example from the book:

fn add(a: i32, b: i32) -> i32 {
    a + b
}

#[cfg(test)]
mod test {
    use super::*;
    use proptest::prelude::*;

    proptest! {
        #[test]
        fn test_add(a in 0..1000i32, b in 0..1000i32) {
            let sum = add(a, b);
            assert!(sum >= a);
            assert!(sum >= b);
        }
    }
}

which running

$ cargo miri test

results in

test test::test_add ... error: unsupported operation: `getcwd` not available when isolation is enabled
   --> /Users/matthewrusso/.rustup/toolchains/nightly-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/unix/os.rs:148:17
    |
148 |             if !libc::getcwd(ptr, buf.capacity()).is_null() {
    |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `getcwd` not available when isolation is enabled

...

error: aborting due to previous error

error: test failed, to rerun pass `--bin proptest-playground`

Caused by:
  process didn't exit successfully: `/Users/matthewrusso/.rustup/toolchains/nightly-aarch64-apple-darwin/bin/cargo-miri runner /Users/matthewrusso/projects/user/proptest-playground/target/miri/aarch64-apple-darwin/debug/deps/proptest_playground-f0560a7e7d9f061c` (exit status: 1)

---

The first option, which is the only that maintains MIRI isolation is through explicit proptest config:

#[cfg(test)]
mod test {
    use super::*;
    use proptest::prelude::*;

    proptest! {
        #![proptest_config(proptest::test_runner::Config {
            failure_persistence: None,
            ..Default::default()
        })]
        #[test]
        fn test_add(a in 0..1000i32, b in 0..1000i32) {
            let sum = add(a, b);
            assert!(sum >= a);
            assert!(sum >= b);
        }
    }
}

which after running

$ cargo miri test

Preparing a sysroot for Miri (target: aarch64-apple-darwin)... done
    Finished test [unoptimized + debuginfo] target(s) in 0.01s
     Running unittests src/main.rs (target/miri/aarch64-apple-darwin/debug/deps/proptest_playground-f0560a7e7d9f061c)

running 1 test
test test::test_add ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out

The obvious downside is that there is no failure persistence, even when not running in MIRI.

---

The next few options all affect MIRI's isolation.

Just running the original example with the following flags works, and is what MIRI actually suggests in the error message

test test::test_add ... error: unsupported operation: `getcwd` not available when isolation is enabled
   --> /Users/matthewrusso/.rustup/toolchains/nightly-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/unix/os.rs:148:17
    |
148 |             if !libc::getcwd(ptr, buf.capacity()).is_null() {
    |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `getcwd` not available when isolation is enabled
    |
    = help: pass the flag `-Zmiri-disable-isolation` to disable isolation;
    = help: or pass `-Zmiri-isolation-error=warn` to configure Miri to return an error code from isolated operations (if supported for that operation) and continue with a warning
    = note: BACKTRACE:

$ MIRIFLAGS='-Zmiri-disable-isolation' cargo miri test

Preparing a sysroot for Miri (target: aarch64-apple-darwin)... done
    Finished test [unoptimized + debuginfo] target(s) in 0.02s
     Running unittests src/main.rs (target/miri/aarch64-apple-darwin/debug/deps/proptest_playground-c461ce41deb29a64)

running 1 test
test test::test_add ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out

$  MIRIFLAGS='-Zmiri-isolation-error=warn' cargo miri test

running 1 test
test test::test_add ... warning: operation rejected by isolation
   --> /Users/matthewrusso/.rustup/toolchains/nightly-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/unix/os.rs:148:17
    |
148 |             if !libc::getcwd(ptr, buf.capacity()).is_null() {
    |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `getcwd` was made to return an error due to isolation
    |
    = note: inside `std::sys::unix::os::getcwd` at /Users/matthewrusso/.rustup/toolchains/nightly-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/unix/os.rs:148:17: 148:50

...

ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out

both result in passing tests, but the behaviors are different. The first one does load the persistence file and runs any detected seeds, the second one fails to load the persistence file and continues with arbitrary test cases.

---

Lastly, since v1.1, you can disable failure persistence with an env var: PROPTEST_DISABLE_FAILURE_PERSISTENCE

Unfortunately you still need to pass the -Zmiri-disable-isolation flag to disable isolation because by default MIRI blocks env vars

$ PROPTEST_DISABLE_FAILURE_PERSISTENCE=true  MIRIFLAGS='-Zmiri-disable-isolation' cargo miri test

Preparing a sysroot for Miri (target: aarch64-apple-darwin)... done
    Finished test [unoptimized + debuginfo] target(s) in 0.02s
     Running unittests src/main.rs (target/miri/aarch64-apple-darwin/debug/deps/proptest_playground-c461ce41deb29a64)

running 1 test
test test::test_add ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out

---

Hope this helps and sorry for the delay in getting to this issue!

[TomFryersMidsummer]

You can also do this.

PROPTEST_DISABLE_FAILURE_PERSISTENCE=true MIRIFLAGS='-Zmiri-env-forward=PROPTEST_DISABLE_FAILURE_PERSISTENCE' cargo miri test