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

Handle reference types in mir_fresh_expanded_value #1975

Open
RyanGlScott opened this issue Nov 13, 2023 · 0 comments
Open

Handle reference types in mir_fresh_expanded_value #1975

RyanGlScott opened this issue Nov 13, 2023 · 0 comments
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
Milestone

Comments

@RyanGlScott
Copy link
Contributor

Currently, the mir_fresh_expanded_value command will fail if you give it a type that contains a reference type somewhere in it. This is annoying in situations where you have a large compound type that incidentally contains a reference somewhere in it, e.g.,

struct S {
    x1: u32,
    x2: u32,
    ...
    x99: u32,
    x100: &u64,
}

It is conceivable that one would want to write a specification involving an S value that does not particularly care what x100 looks like. For these situations, it would be helpful to use mir_fresh_expanded_value to generate a reasonable default value for all of S's fields, including x100.

Here, a reasonable default would be to make x100 a fresh reference, i.e., a reference that is not required to point to allocated memory. This is close in spirit to the existing llvm_fresh_pointer command, and in fact, we may want to export this functionality as a standalone mir_fresh_ref command. Implementation-wise, we could likely create a fresh MIR reference by using MirReference_Integer:

  -- The result of an integer-to-pointer cast.  Guaranteed not to be
  -- dereferenceable.
  MirReference_Integer ::
    !(TypeRepr tp) ->
    !(RegValue sym UsizeType) ->
    MirReference sym tp

Namely, we could create a MirReference_Integer with a symbolic integer value. You wouldn't be able to do much with the resulting fresh reference (e.g., reading or writing to the reference would error), but for situations like the one above where you don't particularly care about the reference value, this would be fine.

@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
@sauclovian-g sauclovian-g added this to the Someday milestone Nov 8, 2024
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

2 participants