mir_elem_{ref,value}
and mir_field_{ref,value}
#1983
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
This issue exists to track implementing a family of MIR backend commands that are inspired by the existing
llvm_elem
andllvm_field
commands in the LLVM backend.llvm_elem
andllvm_field
take an LLVM pointer and return a new pointer with an appropriate pointer offset applied that allows reading an underlying array/struct element or struct field (without actually performing the memory read itself). We will want something similar for MIR references, which can similarly be "offset" by extending the underlyingMirReferencePath
.One somewhat peculiar thing about Rust (when compared to C) is that it is more common for functions to pass arrays, structs, and other compount types by reference instead of by value. As a result, it would also be convenient to project out elements or fields from things passed by value, but this would require a different approach that what we use for things passed by reference. In particular, projecting elements/fields out of a raw SAWScript value may require indexing into a Cryptol value, which is not something that
llvm_elem
/llvm_field
has to deal with.To account for both use cases, we propose adding (names subject to change):
mir_elem_ref
andmir_field_ref
for indexing into MIR references. These would behave much like today'sllvm_elem
andllvm_ref
.mir_elem_value
andmir_field_value
for indexing into raw MIR values (no references). We could conceivably introducellvm_elem_value
andllvm_field_value
into the LLVM backend as well, although they'd be much less useful, since compound types are very rarely passed by value in C (and if they are, they usually look very different at the LLVM level due to ABI requirements).The text was updated successfully, but these errors were encountered: