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_fresh_expanded_value produces value of incorrect type for repr(transparent) structs #1973

Closed
RyanGlScott opened this issue Nov 10, 2023 · 0 comments · Fixed by #1974
Closed
Assignees
Labels
subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json type: bug Issues reporting bugs or unexpected/unwanted behavior

Comments

@RyanGlScott
Copy link
Contributor

Given this Rust code:

#[repr(transparent)]
pub struct S(u8);
pub fn f(_s: &S) {}

I would expect this specification for `` to verify:

enable_experimental;

m <- mir_load_module "test.linked-mir.json";

s_adt <- mir_find_adt m "test::S" [];

let f_spec = do {
  s_ref <- mir_alloc (mir_adt s_adt);
  s <- mir_fresh_expanded_value "s" (mir_adt s_adt);
  mir_points_to s_ref s;

  mir_execute_func [s_ref];
};

mir_verify m "test::f" [] false f_spec z3;

Surprisingly, it does not:

$ ./bin/saw test.saw



[17:18:57.230] Loading file "/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw"
[17:18:57.233] Stack trace:
"mir_verify" (/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:15:1-15:11)
Referent type incompatible with value in `mir_points_to` statement:
  Referent type: test/eeb62416::S[0]<>
  Value type:    u8

The use of repr(transparent) is key here, as the bug does not occur without it.

@RyanGlScott RyanGlScott added type: bug Issues reporting bugs or unexpected/unwanted behavior subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json labels Nov 10, 2023
@RyanGlScott RyanGlScott self-assigned this Nov 10, 2023
RyanGlScott added a commit that referenced this issue Nov 10, 2023
…ent)` structs

Previously, if `mir_fresh_expanded_value` was asked to generate a value whose
type was a struct marked `repr(transparent)`, then SAW would produce a value of
the underlying type, not the struct type. This fixes the issue by wrapping the
underlying value with `SetupStruct`.

Fixes #1973.
RyanGlScott added a commit that referenced this issue Nov 10, 2023
…ent)` structs

Previously, if `mir_fresh_expanded_value` was asked to generate a value whose
type was a struct marked `repr(transparent)`, then SAW would produce a value of
the underlying type, not the struct type. This fixes the issue by wrapping the
underlying value with `SetupStruct`.

Fixes #1973.
@mergify mergify bot closed this as completed in #1974 Nov 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: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant