Skip to content

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

Open
@RyanGlScott

Description

@RyanGlScott

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).

Metadata

Metadata

Assignees

Labels

subsystem: crucible-mirIssues related to Rust verification with crucible-mir and/or mir-jsontype: enhancementIssues describing an improvement to an existing feature or capability

Type

No type

Projects

No projects

Relationships

None yet

Development

No branches or pull requests

Issue actions