Skip to content

MIR: Simplify the implementation of matchArg #2431

Open
@qsctr

Description

@qsctr

When I first implemented matchArg, I heavily drew inspiration from SAWCentral.Crucible.LLVM.Overrides.matchArg, which also matches on expectedTy (but where expectedTy is an LLVM MemType instead). Looking back on the MIR version of matchArg with fresh eyes, however, you are right: there really isn't much of a point in including expectedTy, since we could just as well use the Ty stored inside of the TypeShape. It might be nice to simplify the implementation of this function by removing expectedTy.

(To be honest, I also wonder if the LLVM matchArg really needs to match on expectedTy either, but that is a task best left for later.)

Originally posted by @RyanGlScott in #2427 (comment)

Metadata

Metadata

Assignees

No one assigned

    Labels

    easyIssues that are expected to be easy to resolve and might therefore be good for new contributorssubsystem: crucible-mirIssues related to Rust verification with crucible-mir and/or mir-jsontech debtIssues that document or involve technical debttype: enhancementIssues describing an improvement to an existing feature or capability

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions