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

crucible-mir: Add Mir.TransCustom overrides for {read,write}_volatile #1130

Open
RyanGlScott opened this issue Nov 13, 2023 · 0 comments
Open
Labels
crucible enhancement MIR Issues relating to Rust/MIR support

Comments

@RyanGlScott
Copy link
Contributor

The read_volatile and write_volatile Rust functions are useful when dealing with code that involves memory sanitization. Currently, crucible-mir lacks any Mir.TransCustom support for these functions, so we should add them. The most straightforward way to do so would be to treat them like ordinary reads and writes. That is:

volatile_load :: (ExplodedDefId, CustomRHS)
volatile_load = ( ["core", "intrinsics", "{extern}", "volatile_load"], \substs -> case substs of
    Substs [_] -> Just $ CustomOp $ \_ ops -> case ops of
        [MirExp (MirReferenceRepr tpr) ptr] ->
            MirExp tpr <$> readMirRef tpr ptr
        _ -> mirFail $ "bad arguments for ptr::read: " ++ show ops
    _ -> Nothing)

volatile_store :: (ExplodedDefId, CustomRHS)
volatile_store = ( ["core", "intrinsics", "{extern}", "volatile_store"], \substs -> case substs of
    Substs [_] -> Just $ CustomOp $ \_ ops -> case ops of
        [MirExp (MirReferenceRepr tpr) ptr, MirExp tpr' val]
          | Just Refl <- testEquality tpr tpr' -> do
            writeMirRef ptr val
            return $ MirExp C.UnitRepr $ R.App E.EmptyApp
        _ -> mirFail $ "bad arguments for ptr::write: " ++ show ops
    _ -> Nothing)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
crucible enhancement MIR Issues relating to Rust/MIR support
Projects
None yet
Development

No branches or pull requests

1 participant