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

Rearrange the handling of constant slices. #73

Merged
merged 7 commits into from
Aug 26, 2024
Merged

Conversation

sauclovian-g
Copy link
Contributor

@sauclovian-g sauclovian-g commented Aug 23, 2024

The idea is to split the slice into a reference and a separate static allocation for the body the reference points to. This then allows downstream code to treat the references as normal references to memory, which in turn avoids problems in SAW that arise when it goes to try to enforce disjointness.

Requires accompanying changes in Crucible so that crucible-mir can read and process the new output. (These changes are in crucible #1243.)

See saw-script #2064 for background.

String slices and ordinary array slices are still special cases, but
they're now handled like references: they contain a def_id that points
to an allocation, which for constants is a static allocation holding
the body. Previously they were handled like values and contained an
inline copy of the actual data.

This makes them come out in Crucible as global references rather than
(magic) constant references; the latter do not support operations that
are needed in practice. See saw-script #2064.

The special cases for bstr are removed; they're no longer needed.

It's probable that at least the body-data special cases for slices are
no longer needed either, but one thing at a time.
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
src/analyz/ty_json.rs Outdated Show resolved Hide resolved
Remove some entirely unused functions flagged by the compiler.
Use the "array" output kind. The code to generate slice bodies is
still different from the general array case, though.

None of this is true of _string_ slice bodies, whose elements fields
are just lists of character values. That should probably stay that way
to avoid bloating out large string constants.
(even though the logic is the same)

Add a note to this effect.
- expand some comments
- get a better name for make_static_ref
- adjust some other names for clarity
- assert if we hit a nonzero reference output
  (instead of silently emitting bad code)
(on the reference side, the bodies of strings are still special-cased)

Advice from those much more familiar with things is that the
representation of strings is not likely to diverge from [u8].
@sauclovian-g
Copy link
Contributor Author

I force-pushed to squash the second silence-warnings commit into the first one, and to squash the leftover comment change into the commit that it should have been in. No actual change.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants