volatile_{load,store} with statics. Heap allocations. And transmuting wrappers.#989
Open
volatile_{load,store} with statics. Heap allocations. And transmuting wrappers.#989
volatile_{load,store} with statics. Heap allocations. And transmuting wrappers.#989Conversation
Stevengre
approved these changes
Mar 17, 2026
Contributor
Stevengre
left a comment
Stevengre
left a comment
There was a problem hiding this comment.
LGTM! Want an issue just in case. If you don't have time, please let me know, I can introduce one when I have time.
| requires #transparentFieldTy(lookupTy(TY_TARGET)) ==K TY_SOURCE | ||
|
|
||
| // Down: Wrapper(T) -> T | ||
| rule <k> #cast(Aggregate(variantIdx(0), ListItem(VAL)), castKindTransmute, TY_SOURCE, TY_TARGET) |
Contributor
There was a problem hiding this comment.
LGTM! And I trust you that you've already saw the red and added these to make it green. I'd like to give you approval to let you continue.
Contributor
There was a problem hiding this comment.
But would you mind to draft an issue about refactoring these casting things? It looks quite the same but we have to deal with them one by one.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is a bit of everything in one go, but what I was trying to do was isolate the case seen in this Kompass test that was discussed in #987. The
volatile_loadis coming fromBox::newwhich we are not supporting right now as that does heap allocation.This PR:
Box::new#[repr(rust)]case and their wrapped type. Seen as athunkearlier in theBox::newproof and I thought I would solve it now. There are tests for this changed from failing passing in the commit history.So the
volatile_loadis expected to fail until we figure out some support for the things that these tests fail on. This is not blocking any work now so I think it is fine just to add the failing tests