MIR: Provide utility functions for looking up full identifiers #1980
Labels
subsystem: crucible-mir
Issues related to Rust verification with crucible-mir and/or mir-json
type: enhancement
Issues describing an improvement to an existing feature or capability
usability
An issue that impedes efficient understanding and use
Milestone
Finding the names of MIR identifiers in a MIR JSON file is challenging, and doubly so when the name is autogenerated. For instance, consider this file:
Let's suppose you want to look up the identifier corresponding to
f
when theA
type parameter is instantiated withu32
(as is the case wheng
invokes thef
function). Currently, there is no good way to do this—you'd have to dig into the MIR JSON file manually to discover that the autogenerated name is something liketest::f::_instc5e93708b8ca6e2a
. Users shouldn't have to do this!Instead, we should offer utility functions to make it possible to look up these sorts of names directly from SAW. For instance, we could imagine a command like this:
Where the
String
argument represents a polymorphic function being called (in this case,"test::f
) and the[MIRType]
list represents the list of types to instantiate the function with (in this case,[mir_u32]
). TheString
that it returns would then be the name of the fully instantiated function identifier (in this case,test::f::_instc5e93708b8ca6e2a
). This API closely resembles that of the existingmir_find_adt
function, which already performs a similar sort of type-based name lookup.Other useful commands worth adding would be something that granted users the ability to look up names using things that resemble fully qualified syntax (e.g.,
<Ty>::foo
). In order to support this, we may have to extendmir-json
to include more information linkingfoo
back toTy
, especially iffoo
is located in animpl Ty
block (currently, nothing in themir-json
file makes it obvious whichimpl<N>
block specifically corresponds to theimpl Ty
block).The text was updated successfully, but these errors were encountered: