How to pass `target-feature` in cargo-kani?

[zpzigi754]

This symptom would only occur in aarch64 target.

I tried this code:

// src/main.rs

#[cfg(kani)]
mod verification {
    #[kani::proof]
    fn success_example() {
        assert!(true);
    }
}

fn main() {
}

with the below dependency

# Cargo.toml

[package]
name = "hello-half"
version = "0.1.0"
edition = "2021"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
half = { version = "2.4.0", default-features = false}

using the following command line invocation:

cargo kani

with Kani version: the latest one (12768f2)

I expected to see this happen

VERIFICATION:- SUCCESSFUL

Instead, this happened.

...
error: register class `vreg` requires the `neon` target feature
   --> /home/changho/.cargo/registry/src/index.crates.io-6f17d22bba15001f/half-2.4.0/src/binary16/arch/aarch64.rs:171:9
    |
171 |         in(vreg) a,
    |         ^^^^^^^^^^

error: register class `vreg` requires the `neon` target feature
   --> /home/changho/.cargo/registry/src/index.crates.io-6f17d22bba15001f/half-2.4.0/src/binary16/arch/aarch64.rs:172:9
    |
172 |         in(vreg) b,
    |         ^^^^^^^^^^

error: aborting due to 32 previous errors

error: could not compile `half` (lib) due to 33 previous errors
error: Failed to execute cargo (exit status: 101). Found 33 compilation errors.

The above error was caused by not adding neon target feature in the half crate. However, passing target-feature to cargo-kani (e.g., -C target-feature=+neon) doesn't seem to work.

Note that I've added a patch commit in the half crate, but being able to control target-feature would be still useful even after that patch being merged.

[celinval]

Hi @zpzigi754, how did you try to pass the target configuration to Kani? Have you tried setting rustflags in you cargo configuration?

[zpzigi754]

I've tried it in multiple ways including setting RUSTFLAGS environment variable (RUSTFLAGS='-C target-feature=+neon' cargo kani), using .cargo/config.toml, and slightly modifying kani-driver's cargo_config_args() like the below.

> diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
pub fn cargo_config_args() -> Vec<OsString> {
    [
        "--target",
        env!("TARGET"),
        // Propagate `--cfg=kani` to build scripts.
        "-Zhost-config",
        "-Ztarget-applies-to-host",
+       "-Ctarget-feature=+neon",
        "--config=host.rustflags=[\"--cfg=kani\"]",

# in .cargo/config.toml
[build]
rustflags = [
  "-C", "target-feature=+neon",
]

[zhassan-aws]

Can you try using:

RUSTFLAGS='-C target-feature=+v7,+neon' cargo kani

?

[zpzigi754]

Can you try using:

RUSTFLAGS='-C target-feature=+v7,+neon' cargo kani

?

Thank you for the suggestion, @zhassan-aws. I tried the suggestion, yet the symptom is the same: could not compile half (lib) due to 33 previous errors. The command extracted from verbose option is as follows.

/home/changho/zpzigi754/kani/target/kani/bin/kani-compiler --crate-name half --edition=2021 /home/changho/.cargo/registry/src/index.crates.io-6f17d22bba15001f/half-2.4.0/src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=91 --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 -C metadata=b374fed85354eac9 -C extra-filename=-b374fed85354eac9 --out-dir /home/changho/test/kani-test/hello-half-not-work/target/kani/aarch64-unknown-linux-gnu/debug/deps --target aarch64-unknown-linux-gnu -L dependency=/home/changho/test/kani-test/hello-half-not-work/target/kani/aarch64-unknown-linux-gnu/debug/deps -L dependency=/home/changho/test/kani-test/hello-half-not-work/target/kani/debug/deps --extern cfg_if=/home/changho/test/kani-test/hello-half-not-work/target/kani/aarch64-unknown-linux-gnu/debug/deps/libcfg_if-77f5aff8ee49a6b0.rmeta --cap-lints allow -C overflow-checks=on -Z unstable-options -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -Z always-encode-mir --cfg=kani -Z 'crate-attr=feature(register_tool)' -Z 'crate-attr=register_tool(kanitool)' --sysroot /home/changho/zpzigi754/kani/target/kani -L /home/changho/zpzigi754/kani/target/kani/lib --extern kani --extern 'noprelude:std=/home/changho/zpzigi754/kani/target/kani/lib/libstd.rlib' -C target-feature=+v7,+neon -C panic=abort -C symbol-mangling-version=v0 -Z panic_abort_tests=yes --kani-compiler '-Cllvm-args=--check-version=0.47.0 --log-level=info --assertion-reach-checks --goto-c'

I think that passing target-feature to kani-compiler through RUSTFLAGS does not work.

[zhassan-aws]

I see. And does cargo build with the target-feature succeed?

[zpzigi754]

I see. And does cargo build with the target-feature succeed?

In that case (cargo build), build works successfully with the passed target-feature.

[zi0Black]

I think I have a similar issue with --cfg tokio_unstable, tried with RUSTFLAGS and .cargo/config.toml, it builds fine with cargo build but not with cargo kani.