Add mir_lifetime
combinator for looking up types with lifetime substitutions
#2005
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
If you write code that looks like this:
Then the resulting MIR for the
f
function will be:Note that the return type is
S<lifetime>
, but MIR currently lacks a combinator to pass tomir_find_adt
in order to instantiateS
withlifetime
. We should add amir_lifetime : MIRType
SAWScript combinator so that users can writemir_find_adt m "example::S" [mir_lifetime]
.Note that this should be considered a stopgap measure until GaloisInc/mir-json#58 is fixed. Once that issue is fixed, then
mir-json
will never emit types that require lifetime substitutions, at which pointmir_lifetime
will become moot (and should be removed). That being said, implementingmir_lifetime
will likely be much easier than fixing GaloisInc/mir-json#58, so it would be worth fixing this issue first so that specs involving lifetimes will work in the meantime.Here is a first attempt at a
mir_lifetime
implementation (without the accompanying SAW manual explanation, tests, etc.):The text was updated successfully, but these errors were encountered: