GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
673 stars 44 forks source link

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

Open RyanGlScott opened 11 months ago

RyanGlScott commented 11 months ago

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)