runtimeverification / runtimeverification/mir-semantics
Incorrect handling of `drop` for `RefCell` (borrow flag modified during drop)
Nobody has claimed this yet.
- Dominant language
- Python
- Stars
- 52
- Forks
- 5
- PR merge metrics
- No merged PRs in 30d
Description
The current handling of drop appears to be incorrect.
In the case of RefCell, the drop operation modifies the internal borrow variable, which is not the intended behavior.
- See: https://github.com/runtimeverification/mir-semantics/pull/786 , which introduces a mock
dropforRefCell. However, the current implementation might be semantically unsound.
We plan to address this by introducing a spl-token specific cheatcode in a separate PR without touching the drop, along with fix: drop to handle drop generally not just for Refcell.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by reviewing PR #786 and the current handling of drop for RefCell. Determine how the borrow flag is modified and clarify the intended split between a spl-token-specific cheatcode and the general drop fix. Done means RefCell drop no longer has the reported semantic issue and general drop handling is addressed without relying on the mock introduced there.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- rust
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 35/100