Add mir_cast_to_immut_ref
function
#1954
Labels
subsystem: crucible-mir
Issues related to Rust verification with crucible-mir and/or mir-json
type: feature request
Issues requesting a new feature or capability
The MIR backend has a couple of commands that produce a reference value with the same mutability as something else:
mir_static
function (seemir_static
andmir_static_initializer
#1941) produces a reference to astatic
value. If thestatic
value is immutable, then the reference will be immutable, and if thestatic
value is mutable, then the reference will be mutable.mir_slice_value
andmir_slice_range_value
functions (seemir_slice_value
andmir_slice_range_value
#1948) produces a slice reference from an array reference. Similarly, the slice reference will have the same mutability as the array reference.What is missing from these designs is a way to cast from a mutable reference to an immutable one, which is something that is allowed in Rust. We could envision variants of all the commands above that expect a mutable reference and return an immutable one, but this would result in an explosion of different variants of each command.
A somewhat nicer alternative would be to introduce a standalone
mir_cast_to_immut_ref : MIRValue -> MIRValue
function that performs this cast. That way, we can consolidate all of the logic needed to do the cast into a single command. In fact, this idea shares some similarities with the existingllvm_cast_pointer
command, so perhaps there is a way to design this such thatllvm_cast_pointer
andmir_cast_to_immut_ref
share the same underlying machinery.The text was updated successfully, but these errors were encountered: