GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
437 stars 63 forks source link

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

Open RyanGlScott opened 9 months ago

RyanGlScott commented 9 months ago

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

RyanGlScott commented 8 months ago

It would be nice to have a mir_ref_of command (#1999) to accompany these functions to avoid the issues described in https://github.com/GaloisInc/saw-script/issues/1999#issue-2048842038.