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. #1243

Merged
merged 9 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 us 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 mir-json that produce the new output we read. (These are in mir-json #73.)

See saw-script #2064 for background.

Instead of sending them as blobs with values, mir-json now encodes
them as references to static definitions. The values appear as
separate bodies as static allocations.

The new input kinds "slicebody" and "strbody" are used to ship the
bodies in the JSON.

Change our internal representation of the input MIR to split the
ConstSlice and ConstStr cases accordingly. Kill off the ConstByteStr
case as it's no longer needed; byte strings come through as ordinary
references now.

Adjust the translation step to handle the bodies and references
separately. The critical part of this is that it produces globalMirRef
instead of constMirRef; this avoids using constMirRef for cases it
can't support that lead to "Cannot compare Const_RefRoots". See
saw-script #2064.

Note that the handling of slice and string slice bodies is probably
now the same as the handling for ordinary arrays and could be
simplified away. It is also possible that Const_RefRoots can be killed
off entirely. One thing at a time though.

Requires corresponding update to mir-json.
@sauclovian-g sauclovian-g added crucible MIR Issues relating to Rust/MIR support labels Aug 23, 2024
@sauclovian-g
Copy link
Contributor Author

Note that this shouldn't get merged without a commit that bumps the mir-json submodule reference, but that should wait until the mir-json changes are ready to merge.

@sauclovian-g
Copy link
Contributor Author

oh, of course none of the tests are going to work without the new mir-json...

crucible-mir/src/Mir/Generator.hs Outdated Show resolved Hide resolved
crucible-mir/src/Mir/PP.hs Outdated Show resolved Hide resolved
crucible-mir/src/Mir/PP.hs Outdated Show resolved Hide resolved
crucible-mir/src/Mir/Trans.hs Outdated Show resolved Hide resolved
crucible-mir/src/Mir/Trans.hs Outdated Show resolved Hide resolved
crucible-mir/src/Mir/Trans.hs Outdated Show resolved Hide resolved
crucible-mir/src/Mir/Trans.hs Outdated Show resolved Hide resolved
crucible-mir/src/Mir/Trans.hs Outdated Show resolved Hide resolved
@RyanGlScott
Copy link
Contributor

oh, of course none of the tests are going to work without the new mir-json...

Indeed, I think it would be worth bumping the mir-json submodule commit to the current state of GaloisInc/mir-json#73 so that we can verify that everything works. When GaloisInc/mir-json#73 lands, we can bump the submodule to the merge commit on mir-json's master branch.

Relatedly, I think it would be worth noting somewhere in the commit message that this depends on the changes from GaloisInc/mir-json#73.

- don't output rubbish when prettyprinting
- clarify some comments
- remove obsolete comments
- update some names
- remove separate binding of vec_tpr in the ConstStrBody case
  which no longer serves its original illustrative purpose
@sauclovian-g
Copy link
Contributor Author

I think it would be worth bumping the mir-json submodule commit to the current state of GaloisInc/mir-json#73 so that we can verify that everything works. When GaloisInc/mir-json#73 lands, we can bump the submodule to the merge commit on mir-json's master branch.

I have done this.

Relatedly, I think it would be worth noting somewhere in the commit message that this depends on the changes from GaloisInc/mir-json#73.

Now each of the descriptions references the other one.

@sauclovian-g
Copy link
Contributor Author

I force-pushed to squash the reference to the pre-merged version in mir-json. Perhaps not strictly necessary (since that version still exists) but it's untidy to leave it lying around.

@sauclovian-g sauclovian-g merged commit 465395b into master Aug 26, 2024
32 checks passed
@sauclovian-g sauclovian-g deleted the dholland-refroots branch August 26, 2024 22:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
crucible MIR Issues relating to Rust/MIR support
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants