Conversation
These may change across Rust versions, so we just use all the libraries in rlibs, which should be kept up to date by mir-json-translate-libs
We never used it for anything, and it is now removed on the mir-json side
RyanGlScott
approved these changes
Dec 1, 2025
Comment on lines
+766
to
+779
| cell_swap_is_nonoverlapping :: (ExplodedDefId, CustomRHS) | ||
| cell_swap_is_nonoverlapping = | ||
| ( ["core", "cell", "{impl}", "swap", "crucible_cell_swap_is_nonoverlapping_hook"] | ||
| , \case | ||
| Substs [ty] -> Just $ CustomOp $ \_ ops -> case ops of | ||
| [MirExp MirReferenceRepr src, | ||
| MirExp MirReferenceRepr dest] -> do | ||
| size <- getLayoutFieldAsExpr "crucible_cell_swap_is_nonoverlapping_hook" laySize ty | ||
| MirExp C.BoolRepr <$> isNonOverlapping src dest size | ||
| _ -> mirFail $ | ||
| "bad arguments for Cell::swap::crucible_cell_swap_is_nonoverlapping_hook: " | ||
| ++ show ops | ||
| _ -> Nothing | ||
| ) |
Contributor
There was a problem hiding this comment.
Is there a crux-mir test case that uses Cell::swap in order to ensure that this override has test coverage?
Collaborator
Author
There was a problem hiding this comment.
Yeah, it's in test/conc_eval/cell/swap.rs. There are also a few crux-mir-comp tests that use it.
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.
mir-jsonsubmodule to bring in changes from Update Rust toolchain to 1.91 (nightly-2025-09-14) mir-json#200mir-jsonschema version to 6Cell::swap(mir-jsonside commit is GaloisInc/mir-json@7b67f3e)crucible-miraftermir-jsonchangescrux-mir, get the.rliband.mirpaths for the standard libraries by just listing everything in therlibsdirectory instead of keeping a hard-coded list, since the list of standard libraries changes across Rust versionscrux-mirtests for new standard library patches, and old patches that weren't previously covered by any testscrux-mirgolden test outputs and xfail test reasons