cargo bolero test --engine kani <test> fails to match harness

[robo9k]

There is some issue in selecting the proper integration test for Kani:

$ cargo bolero --version
cargo-bolero 0.8.0

$ cargo kani --version
cargo-kani 0.23.0

$ cargo new project

$ cargo bolero new verify

$ cargo bolero test --engine kani verify
error: no harnesses matched the harness filter: `verify`

$ cat tests/verify/main.rs
#[cfg_attr(kani, kani::proof)]
fn main() {
    bolero::check!().for_each(|v| {
        let _ = todo!();
    });
}

The following works, but executes all test targets:

$ cargo kani --tests

The following works, but isn't very useful:

$ cargo kani --tests --harness main

The following works, but doesn't use Kani:

$ cargo bolero test verify

Is this a problem with cargo kani rather than cargo bolero?

P.S: actual setup is within a cargo workspace

[adpaco-aws]

Hi @robo9k , have you tried this?

cargo bolero test main --engine kani

It seems you were using Kani in the command

cargo bolero test --engine kani verify
error: no harnesses matched the harness filter: `verify`

verify isn't a harness in your example, but main is.

[robo9k]

Maybe I'm not using the "harness" terminology correctly, but cargo bolero test doesn't use it at all:

$ cargo bolero test --help
cargo-bolero-test 0.8.0
Run an engine for a target

USAGE:
    cargo-bolero test [FLAGS] [OPTIONS] <test>

FLAGS:
        --all-features           Activate all available features
        --build-std              Build the standard library with the provided configuration
    -h, --help                   Prints help information
        --no-default-features    Do not activate the `default` feature
        --rustc-bootstrap        Fake using a nightly toolchain while using the default toolchain by using
                                 RUSTC_BOOTSTRAP
    -V, --version                Prints version information

OPTIONS:
        --corpus-dir <corpus-dir>                User-defined location for the corpus folder
        --crashes-dir <crashes-dir>              User-defined location for the crashes folder
    -e, --engine <engine>                        Run the test with a specific engine [default: libfuzzer]
    -E, --engine-args <engine-args>...           Additional arguments to pass to the selected engine
        --features <features>                    Space-separated list of features to activate
    -j, --jobs <jobs>                            Number of parallel jobs
        --manifest-path <manifest-path>          Path to Cargo.toml
    -l, --max-input-length <max-input-length>    Limit the size of inputs to a specific length
    -p, --package <package>                      Package to run tests for
        --release <release>                      Build artifacts in release mode, with optimizations [default: true]
    -r, --runs <runs>
            Run the engine for a specified number of runs. If unspecified it will continue until manually stopped

    -s, --sanitizer <sanitizer>...               Build with the sanitizer enabled [default: address]
    -S <seed>                                    Run the engine with an initial seed
        --target <target>                        Build for the target triple [default: x86_64-unknown-linux-gnu]
        --target-dir <target-dir>                Directory for all generated artifacts
    -T <time>
            Run the engine for a specified duration. If unspecified it will continue until manually stopped

    -t, --timeout <timeout>
            Maximum amount of time to run a test target before failing [default: 10s]

        --toolchain <toolchain>                  Use a rustup toolchain to execute cargo build

ARGS:
    <test>    Name of the test target

To me this reads like <test> is a [[test]] from my Cargo.toml.

Ignoring terminology for a moment, if I were to create a second test creatively named cargo bolero new verify2, I would end up with a tests/verify2/main.rs which contains yet another fn main().
How would I execute only the "verify2" test using cargo bolero test?

[adpaco-aws]

Hey @robo9k , sorry for the late reply. In my previous answer, I wasn't aware that Bolero and Kani decide the test targets following different procedures.

I'm quite sure that this problem comes from Kani, but I'd need to investigate how we handle integration tests in there. It's likely that the solution requires either tweaking how we interface with Kani from Bolero, or extending how Kani chooses test targets (maybe even both).

Note: "harness" is the term we commonly use for Kani tests (more details here).