Verify contracts/stubs for generic types with multiple inherent implementations #3829

carolynzech · 2025-01-13T21:43:15Z

Extends Kani's contracts/stubbing logic to handle simple paths with generic arguments. I'll explain the changes commit-by-commit:

Commit `690ba97`: Error for multiple implementations

Prior to this PR, given the code from #3773:

struct NonZero<T>(T);

impl NonZero<u32> {
    #[kani::requires(true)]
    fn unchecked_mul(self, x: u32) {}
}

impl NonZero<i32> {
    #[kani::requires(true)]
    fn unchecked_mul(self, x: i32) {}
}

#[kani::proof_for_contract(NonZero::unchecked_mul)]
fn verify_unchecked_mul() {
    let x: NonZero<i32> = NonZero(-1);
    x.unchecked_mul(-2);
}

When resolving the target, Kani would return the first unchecked_mul implementation that it found for NonZero. If that happens to be the u32 implementation, then we get an error later that the target NonZero::unchecked_mul isn't reachable from the harness, which is confusing because the harness does call unchecked_mul.

The real problem is that the target needs to specify which implementation it wants to verify, so now we throw this error:

Failed to resolve checking function NonZero::unchecked_mul because there are multiple implementations of unchecked_mul in struct `NonZero`. Found:
       NonZero::<u32>::unchecked_mul
       NonZero::<i32>::unchecked_mul
 |
 | #[kani::proof_for_contract(NonZero::unchecked_mul)]
 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 |
   = help: Replace NonZero::unchecked_mul with a specific implementation.

Commit `62b66de`: Path resolution for simple paths with generic arguments

If the user took our suggestion and changed their proof for contract to be NonZero::<i32>::unchecked_mul, they would still get the same error. The syn::Path is this:

Path {
    leading_colon: None,
    segments: [
        PathSegment {
            ident: Ident(
                NonZero,
            ),
            arguments: PathArguments::AngleBracketed {
                colon2_token: Some(
                    PathSep,
                ),
                lt_token: Lt,
                args: [
                    GenericArgument::Type(
                        Type::Path {
                            qself: None,
                            path: Path {
                                leading_colon: None,
                                segments: [
                                    PathSegment {
                                        ident: Ident(
                                            i32,
                                        ),
                                        arguments: PathArguments::None,
                                    },
                                ],
                            },
                        },
                    ),
                ],
                gt_token: Gt,
            },
        },
        PathSep,
        PathSegment {
            ident: Ident(
                unchecked_mul,
            ),
            arguments: PathArguments::None,
        },
    ],

Kani's path resolution would skip over the PathArguments for the base type NonZero, so it would still try to find NonZero::unchecked_mul and run into the same problem. So, this commit adds a base_path_args field to our Path representation to store these arguments, which we use to select the specified implementation.

Resolves #3773

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

… impls Add a base_path_args field to the Path struct so that we can use the generic arguments to choose the appropriate implementation

zhassan-aws

Nice, thanks!

@carolynzech

Github generated release notes: ## What's Changed * Automatic toolchain upgrade to nightly-2025-01-08 by @github-actions in #3821 * Automatic cargo update to 2025-01-13 by @github-actions in #3824 * Automatic toolchain upgrade to nightly-2025-01-09 by @github-actions in #3825 * Bump ncipollo/release-action from 1.14.0 to 1.15.0 by @dependabot in #3826 * Bump tests/perf/s2n-quic from `ac52a48` to `adc7ba9` by @dependabot in #3827 * Automatic toolchain upgrade to nightly-2025-01-10 by @github-actions in #3828 * Automatic toolchain upgrade to nightly-2025-01-11 by @github-actions in #3830 * Verify contracts/stubs for generic types with multiple inherent implementations by @carolynzech in #3829 * Update Charon submodule by @thanhnguyen-aws in #3823 * Automatic toolchain upgrade to nightly-2025-01-12 by @github-actions in #3831 * Automatic toolchain upgrade to nightly-2025-01-13 by @github-actions in #3833 * Upgrade toolchain to 2025-01-15 by @tautschnig in #3835 * Automatic toolchain upgrade to nightly-2025-01-16 by @github-actions in #3836 * Add a regression test for `no_std` feature by @carolynzech in #3837 * Use fully-qualified name for size_of by @zhassan-aws in #3838 * Automatic cargo update to 2025-01-20 by @github-actions in #3842 * Bump tests/perf/s2n-quic from `adc7ba9` to `f0649f9` by @dependabot in #3844 * Upgrade toolchain to nightly-2025-01-22 by @tautschnig in #3843 * Remove `DefKind::Ctor` from filtering crate items by @carolynzech in #3845 * Enable valid_ptr post_condition harnesses by @tautschnig in #3847 * Update build command in docs to use release mode by @zhassan-aws in #3846 * Automatic toolchain upgrade to nightly-2025-01-23 by @github-actions in #3848 * Automatic toolchain upgrade to nightly-2025-01-24 by @github-actions in #3850 * Remove the openssl-devel package from dependencies by @zhassan-aws in #3852 * Fix validity checks for `char` by @celinval in #3853 * Bump tests/perf/s2n-quic from `f0649f9` to `4500593` by @dependabot in #3857 * Automatic cargo update to 2025-01-27 by @github-actions in #3856 * Deprecate `--enable-unstable` and `--restrict-vtable` by @celinval in #3859 * Stub linker to avoid missing symbols errors by @celinval in #3858 * Toolchain upgrade to nightly-2025-01-28 by @feliperodri in #3855 * Allow multiple annotations, but check for duplicate targets. by @remi-delmas-3000 in #3808 * Move documentation of kani_core modules to right places by @qinheping in #3851 * Fix missing function declaration issue by @celinval in #3862 * Fix transmute codegen when sizes are different by @celinval in #3861 * Remove symtab2gb from bundle by @zhassan-aws in #3865 * Update the rustc hack for CLion / RustRover by @celinval in #3868 * Bump tests/perf/s2n-quic from `4500593` to `82dd0b5` by @dependabot in #3872 * Automatic cargo update to 2025-02-03 by @github-actions in #3869 * Add reference for loop contracts by @qinheping in #3849 * remove flag float-overflow-check by @rajath-mk in #3873 ## New Contributors * @rajath-mk made their first contribution in #3873 **Full Changelog**: kani-0.58.0...kani-0.59.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

… args path for equality (#4051) #3829 fixed an issue where we couldn't verify contracts or stubs for types with multiple inherent impls. However, the logic to check for path equality incorrectly assumed that there would only be one element in the path before the generic argument, when in fact the path can be arbitrarily long if there are modules involved. Change the logic to just look at the last two elements, since we can expect those will be the generic argument and the method name. Before this PR, the new test would fail with this error: ``` error: Failed to resolve checking function NegativeNumber::<i32>::unchecked_mul because the generic arguments ::<i32> are invalid. The available implementations are: num::negative::NegativeNumber::<i32>::unchecked_mul num::negative::NegativeNumber::<i16>::unchecked_mul --> /Users/cmzech/kani/tests/kani/FunctionContracts/multiple_inherent_impls.rs:57:5 | 57 | #[kani::proof_for_contract(NegativeNumber::<i32>::unchecked_mul)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info) ``` because we'd try to compare `::negative::NegativeNumber::<i32>::unchecked_mul` to `::<i32>::unchecked_mul` and find they weren't equal. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Carolyn Zech added 2 commits January 10, 2025 15:01

issue 3773: error for multiple implementations

690ba97

Verify contracts on methods where the base type has multiple inherent…

62b66de

… impls Add a base_path_args field to the Path struct so that we can use the generic arguments to choose the appropriate implementation

carolynzech requested a review from a team as a code owner January 13, 2025 21:43

github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jan 13, 2025

zhassan-aws approved these changes Jan 14, 2025

View reviewed changes

fix expected file name

d79e6cb

carolynzech enabled auto-merge January 14, 2025 14:40

carolynzech added this pull request to the merge queue Jan 14, 2025

Merged via the queue into model-checking:main with commit 5efd8b6 Jan 14, 2025
27 of 28 checks passed

carolynzech deleted the issue-3773 branch January 14, 2025 17:15

carolynzech mentioned this pull request Feb 5, 2025

Bump Kani version to 0.59.0 #3876

Merged

carolynzech mentioned this pull request Apr 30, 2025

Contracts/Stubs for multiple inherent impls: fix checking the generic args path for equality #4051

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Verify contracts/stubs for generic types with multiple inherent implementations #3829

Verify contracts/stubs for generic types with multiple inherent implementations #3829

Uh oh!

carolynzech commented Jan 13, 2025

Uh oh!

zhassan-aws left a comment

Uh oh!

Uh oh!

Uh oh!

Verify contracts/stubs for generic types with multiple inherent implementations #3829

Verify contracts/stubs for generic types with multiple inherent implementations #3829

Uh oh!

Conversation

carolynzech commented Jan 13, 2025

Commit 690ba97: Error for multiple implementations

Commit 62b66de: Path resolution for simple paths with generic arguments

Uh oh!

zhassan-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Commit `690ba97`: Error for multiple implementations

Commit `62b66de`: Path resolution for simple paths with generic arguments