Add target-feature neon

[thanhnguyen-aws]

This PR enables target-feature neon
(NOT WORKING YET)
Resolves #3059 #3878

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[remi-delmas-3000]

@thanhnguyen-aws do you think this is relevant to our problem ?

Some findings:

• neon is activated as a default feature for aarch64-unknown-linux-gnu (as per the 2025-03-03 stable/nighly)

➜  ~ rustc +stable --target aarch64-unknown-linux-gnu --print cfg
debug_assertions
panic="unwind"
target_abi=""
target_arch="aarch64"
target_endian="little"
target_env="gnu"
target_family="unix"
target_feature="neon"
target_has_atomic="128"
target_has_atomic="16"
target_has_atomic="32"
target_has_atomic="64"
target_has_atomic="8"
target_has_atomic="ptr"
target_os="linux"
target_pointer_width="64"
target_vendor="unknown"
unix

➜  ~ rustc +nightly --target aarch64-unknown-linux-gnu --print cfg
debug_assertions
fmt_debug="full"
overflow_checks
panic="unwind"
relocation_model="pic"
target_abi=""
target_arch="aarch64"
target_endian="little"
target_env="gnu"
target_family="unix"
target_feature="neon"
target_has_atomic
target_has_atomic="128"
target_has_atomic="16"
target_has_atomic="32"
target_has_atomic="64"
target_has_atomic="8"
target_has_atomic="ptr"
target_has_atomic_equal_alignment="128"
target_has_atomic_equal_alignment="16"
target_has_atomic_equal_alignment="32"
target_has_atomic_equal_alignment="64"
target_has_atomic_equal_alignment="8"
target_has_atomic_equal_alignment="ptr"
target_has_atomic_load_store
target_has_atomic_load_store="128"
target_has_atomic_load_store="16"
target_has_atomic_load_store="32"
target_has_atomic_load_store="64"
target_has_atomic_load_store="8"
target_has_atomic_load_store="ptr"
target_os="linux"
target_pointer_width="64"
target_thread_local
target_vendor="unknown"
ub_checks
unix

• Forcing +neon or -neon is unsound in some cases The (stable) neon aarch64 target feature is unsound: it changes the float ABI rust-lang/rust#131058, work is being done to have rustic reject +/-neon in specific cases. If we force it all the time we will cause errors.
• Forcing +neon on unsupported targets will fail (that's what we see in the PR checks)
• Shouldn't Kani just propagate whatever target feature set is defined by the crate's configuration ?
  • considering the defaults above, if neon in missing some cases it would be because
    • the crate's config actively disabled it ?
    • Kani mistakenly overrides the target architecture or the default config ?
• there's a lot of open soundnes issues regarding neon https://github.com/rust-lang/rust/issues?q=is%3Aissue%20state%3Aopen%20neon. There's a good chance that code using neon is broken, verification results could be unsound because the code that eventually gets executed will not behave like we think it does.

[remi-delmas-3000]

wrote a script to map out the neon feature

NEON Feature Support:
Target                                   Toolchain  Available    Default
--------------------------------------------------------------------------------
aarch64-apple-darwin (installed)         nightly    Yes          No
aarch64-apple-darwin (installed)         stable     Yes          No
aarch64-apple-ios                        nightly    Yes          Yes
aarch64-apple-ios                        stable     Yes          Yes
aarch64-apple-ios-macabi                 nightly    Yes          Yes
aarch64-apple-ios-macabi                 stable     Yes          Yes
aarch64-apple-ios-sim                    nightly    Yes          Yes
aarch64-apple-ios-sim                    stable     Yes          Yes
aarch64-linux-android                    nightly    Yes          Yes
aarch64-linux-android                    stable     Yes          Yes
aarch64-pc-windows-gnullvm               nightly    Yes          Yes
aarch64-pc-windows-gnullvm               stable     Yes          Yes
aarch64-pc-windows-msvc                  nightly    Yes          Yes
aarch64-pc-windows-msvc                  stable     Yes          Yes
aarch64-unknown-fuchsia                  nightly    Yes          Yes
aarch64-unknown-fuchsia                  stable     Yes          Yes
aarch64-unknown-linux-gnu                nightly    Yes          Yes
aarch64-unknown-linux-gnu (installed)    stable     Yes          No
aarch64-unknown-linux-musl               nightly    Yes          Yes
aarch64-unknown-linux-musl               stable     Yes          Yes
aarch64-unknown-linux-ohos               nightly    Yes          Yes
aarch64-unknown-linux-ohos               stable     Yes          Yes
aarch64-unknown-none                     nightly    Yes          Yes
aarch64-unknown-none                     stable     Yes          Yes
aarch64-unknown-none-softfloat           nightly    Yes          No
aarch64-unknown-none-softfloat           stable     Yes          No
aarch64-unknown-uefi                     nightly    Yes          Yes
aarch64-unknown-uefi                     stable     Yes          Yes
arm64ec-pc-windows-msvc                  nightly    No           Yes
arm64ec-pc-windows-msvc                  stable     No           Yes

[remi-delmas-3000]

After digging around it seems like this commit rust-lang/rust@93ee180 introduced the warning in the upstream rustc. The check that produces the warning is done at the level of the compiler session.
When building Kani we get that type of warning when building the kani library and the std-lib using kani-compiler.
I could confirm that kani-compiler does not pick up the -C target-feature=+neon given directly on the command line.
So something must be off with the way sessions are set up in kani-compiler.

[remi-delmas-3000]

Update:

• in rustc the target features are obtained via CodegenBackend::target_features_cfg which is implemented for each backend as seen here https://github.com/search?q=repo%3Arust-lang%2Frust+target_features_cfg%28&type=code
• In Kani we implement the trait CodegenBackend for GotocCodegenBackend but we don't define target_features_cfg as a method. So I wonder if rustc ends up using this default implementation for CodegenBackend::target_features_cfg that returns an empty target feature set https://github.com/rust-lang/rust/blob/fa58ce343ad498196d799a7381869e79938e952a/compiler/rustc_codegen_ssa/src/traits/backend.rs#L54

The llvm backend is massaging the target feature set here https://github.com/rust-lang/rust/blob/fa58ce343ad498196d799a7381869e79938e952a/compiler/rustc_codegen_llvm/src/llvm_util.rs#L305

[zhassan-aws]

In the latest toolchain upgrade, this became a hard error when some language features are used:
https://github.com/model-checking/kani/actions/runs/14655944020/job/41130910124#step:4:955

[thanhnguyen-aws]

Thanks @remi-delmas-3000 for the suggestion. I fixed this issue in #4059, so I will close this PR.