Skip to content

Use more rustc_public APIs for path resolution and attribute handling #4252

@carolynzech

Description

@carolynzech

Proposed change: Make https://github.com/model-checking/kani/blob/main/kani-compiler/src/kani_middle/resolve.rs and https://github.com/model-checking/kani/blob/main/kani-compiler/src/kani_middle/attributes.rs use rustc_public APIs whenever possible.

Motivation: Right now there's an odd mix of stable and unstable code there that makes the logic harder to follow and increases the risk of bugs and crashes.

For example, #4250 introduces a resolve_in_trait_def_stable function that does the same thing as resolve_in_trait_def, but for stable trait items. I tried to call the unstable version at first, but that ICEd inside rustc, so I introduced the stable version which logically does the same thing, but avoids the ICE. This is an example of how switching to StableMIR makes development easier and bugs less prevalent.

That's just an artifact of this code being older, when StableMIR was less developed. The stable APIs are mature enough now that we could write most of this code with rustc_public APIs and convert to unstable representations only when needed.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] InternalTracks some internal work. I.e.: Users should not be affected.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions