Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add mir_cast_to_immut_ref function #1954

Open
RyanGlScott opened this issue Oct 11, 2023 · 0 comments
Open

Add mir_cast_to_immut_ref function #1954

RyanGlScott opened this issue Oct 11, 2023 · 0 comments
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

Comments

@RyanGlScott
Copy link
Contributor

The MIR backend has a couple of commands that produce a reference value with the same mutability as something else:

  • The mir_static function (see mir_static and mir_static_initializer #1941) produces a reference to a static value. If the static value is immutable, then the reference will be immutable, and if the static value is mutable, then the reference will be mutable.
  • The mir_slice_value and mir_slice_range_value functions (see mir_slice_value and mir_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 existing llvm_cast_pointer command, so perhaps there is a way to design this such that llvm_cast_pointer and mir_cast_to_immut_ref share the same underlying machinery.

@RyanGlScott RyanGlScott added type: feature request Issues requesting a new feature or capability subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json labels Oct 11, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
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
Projects
None yet
Development

No branches or pull requests

1 participant