Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 3 commits into from
Jan 14, 2025

Conversation

carolynzech
Copy link
Contributor

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
@carolynzech carolynzech requested a review from a team as a code owner January 13, 2025 21:43
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Jan 13, 2025
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice, thanks!

@carolynzech carolynzech enabled auto-merge January 14, 2025 14:40
@carolynzech 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 carolynzech deleted the issue-3773 branch January 14, 2025 17:15
github-merge-queue bot pushed a commit that referenced this pull request Feb 6, 2025
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Can't verify contracts for a method defined inside more than one impl block
2 participants