Skip to content

Conversation

@carolynzech
Copy link
Contributor

#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.

@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Apr 30, 2025
@carolynzech carolynzech changed the title fix checking the generic args path for equality Contracts/Stubs for multiple inherent impls: fix checking the generic args path for equality Apr 30, 2025
@carolynzech carolynzech marked this pull request as ready for review April 30, 2025 15:04
@carolynzech carolynzech requested a review from a team as a code owner April 30, 2025 15:04
@carolynzech carolynzech self-assigned this Apr 30, 2025
@carolynzech carolynzech added this pull request to the merge queue May 7, 2025
Merged via the queue into model-checking:main with commit 08d99d3 May 7, 2025
25 of 26 checks passed
@carolynzech carolynzech deleted the issue-3773-fix branch May 7, 2025 17:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants