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

mir_elem_{ref,value} and mir_field_{ref,value} #1983

Open
RyanGlScott opened this issue Nov 13, 2023 · 1 comment
Open

mir_elem_{ref,value} and mir_field_{ref,value} #1983

RyanGlScott opened this issue Nov 13, 2023 · 1 comment
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

Comments

@RyanGlScott
Copy link
Contributor

This issue exists to track implementing a family of MIR backend commands that are inspired by the existing llvm_elem and llvm_field commands in the LLVM backend. llvm_elem and llvm_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 underlying MirReferencePath.

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 and mir_field_ref for indexing into MIR references. These would behave much like today's llvm_elem and llvm_ref.
  • mir_elem_value and mir_field_value for indexing into raw MIR values (no references). We could conceivably introduce llvm_elem_value and llvm_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).
@RyanGlScott RyanGlScott added type: enhancement Issues describing an improvement to an existing feature or capability subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json labels Nov 13, 2023
@RyanGlScott
Copy link
Contributor Author

It would be nice to have a mir_ref_of command (#1999) to accompany these functions to avoid the issues described in #1999 (comment).

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: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Development

No branches or pull requests

1 participant